Restore testing of jbmc

Author: smowton

CMakeLists.txt

@@ -34,14 +34,15 @@ set(sat_impl "minisat2" CACHE STRING
     "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
 )
 
-add_subdirectory(src)
-add_subdirectory(jbmc)
-
 if(${enable_cbmc_tests})
     enable_testing()
 endif()
-add_subdirectory(unit)
+
+add_subdirectory(src)
 add_subdirectory(regression)
+add_subdirectory(unit)
+
+add_subdirectory(jbmc)
 
 set_target_properties(
     analyses

jbmc/regression/CMakeLists.txt

@@ -1,24 +1,4 @@
-set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
-
-macro(add_test_pl_profile name cmdline flag profile)
-    add_test(
-        NAME "${name}-${profile}"
-        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
-        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-    )
-    set_tests_properties("${name}-${profile}" PROPERTIES
-        LABELS "${profile};CBMC"
-    )
-endmacro(add_test_pl_profile)
-
-macro(add_test_pl_tests cmdline)
-    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
-    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
-    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
-endmacro(add_test_pl_tests)
+set(test_pl_path "${CMAKE_SOURCE_DIR}/regression/test.pl")
 
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are

jbmc/regression/janalyzer-taint/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-analyzer>"
+    "$<TARGET_FILE:janalyzer>"
 )

jbmc/regression/jbmc/CMakeLists.txt

@@ -3,7 +3,7 @@ add_test_pl_tests(
 )
 
 add_test_pl_profile(
-    "cbmc-java-symex-driven-lazy-loading"
+    "jbmc-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
     "-C;-X;symex-driven-lazy-loading-expected-failure"
     "CORE"

jbmc/regression/jdiff/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-diff>"
+    "$<TARGET_FILE:jdiff>"
 )