Skip to content

Commit 3f973be

Browse files
committed
Regression tests: synchronise Make/CMake test sequence
This is in the spirit of item 3 from #5986: we have again diverged in the set of tests run by Makefile and CMake, respectively. This commit aligns the ordering of tests to make for an easier visual comparison, and adds the missing cbmc-output-file test to Make.
1 parent 53e448b commit 3f973be

File tree

2 files changed

+6
-7
lines changed

2 files changed

+6
-7
lines changed

regression/CMakeLists.txt

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,11 @@ endmacro(add_test_pl_tests)
2525
# listed with decreasing runtimes (i.e. longest running at the top)
2626
add_subdirectory(cbmc)
2727
add_subdirectory(cbmc-library)
28-
add_subdirectory(goto-analyzer)
2928
add_subdirectory(cprover)
29+
if(NOT WIN32)
30+
add_subdirectory(crangler)
31+
endif()
32+
add_subdirectory(goto-analyzer)
3033
add_subdirectory(ansi-c)
3134
add_subdirectory(goto-instrument)
3235
add_subdirectory(cpp)
@@ -80,15 +83,10 @@ add_subdirectory(cbmc-primitives)
8083
add_subdirectory(goto-interpreter)
8184
add_subdirectory(cbmc-sequentialization)
8285
add_subdirectory(cpp-linter)
86+
add_subdirectory(catch-framework)
8387

8488
if(WITH_MEMORY_ANALYZER)
8589
add_subdirectory(snapshot-harness)
8690
add_subdirectory(memory-analyzer)
8791
add_subdirectory(extract_type_header)
8892
endif()
89-
90-
if(NOT WIN32)
91-
add_subdirectory(crangler)
92-
endif()
93-
94-
add_subdirectory(catch-framework)

regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ DIRS = cbmc \
1414
cbmc-incr-oneloop \
1515
cbmc-incr-smt2 \
1616
cbmc-incr \
17+
cbmc-output-file \
1718
cbmc-with-incr \
1819
array-refinement-with-incr \
1920
goto-instrument-chc \

0 commit comments

Comments
 (0)