Remove unrealted tests

qinheping · Oct 24, 2023 · 081df88 · 081df88
1 parent 153be82
commit 081df88
Show file tree

Hide file tree

Showing 74 changed files with 1 addition and 851 deletions.
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -23,79 +23,5 @@ endmacro(add_test_pl_tests)
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-add_subdirectory(cbmc)
-add_subdirectory(cbmc-library)
-add_subdirectory(cprover)
-if(NOT WIN32)
-  add_subdirectory(crangler)
-endif()
-add_subdirectory(goto-analyzer)
-add_subdirectory(ansi-c)
-add_subdirectory(goto-instrument)
-add_subdirectory(cpp)
-add_subdirectory(cbmc-concurrency)
-add_subdirectory(cbmc-cover)
-add_subdirectory(cbmc-incr-oneloop)
-add_subdirectory(cbmc-incr-smt2)
-add_subdirectory(cbmc-incr)
-add_subdirectory(cbmc-shadow-memory)
-add_subdirectory(cbmc-output-file)
-add_subdirectory(cbmc-with-incr)
-add_subdirectory(array-refinement-with-incr)
-add_subdirectory(goto-instrument-chc)
-add_subdirectory(goto-instrument-json)
-add_subdirectory(goto-instrument-wmm-core)
-add_subdirectory(goto-instrument-typedef)
-add_subdirectory(goto-inspect)
-add_subdirectory(smt2_solver)
-add_subdirectory(smt2_strings)
-add_subdirectory(strings)
-add_subdirectory(invariants)
-add_subdirectory(goto-diff)
-add_subdirectory(test-script)
-add_subdirectory(goto-analyzer-taint)
-add_subdirectory(goto-bmc/goto-bmc-symex-ready-goto)
-add_subdirectory(goto-bmc/goto-bmc-non-symex-ready-goto)
-add_subdirectory(goto-bmc)
-if(NOT WIN32)
-  add_subdirectory(goto-gcc)
-else()
-  add_subdirectory(goto-cl)
-endif()
-add_subdirectory(goto-cc-cbmc)
-add_subdirectory(goto-cc-cbmc-shared-options)
-add_subdirectory(cbmc-cpp)
-add_subdirectory(goto-cc-goto-analyzer)
-add_subdirectory(goto-analyzer-simplify)
-add_subdirectory(statement-list)
-add_subdirectory(systemc)
-add_subdirectory(contracts)
-add_subdirectory(contracts-dfcc)
 add_subdirectory(goto-synthesizer)
-add_subdirectory(acceleration)
-add_subdirectory(k-induction)
-add_subdirectory(goto-harness)
-add_subdirectory(goto-harness-multi-file-project)
-add_subdirectory(goto-cc-file-local)
-add_subdirectory(goto-cc-regression-gh-issue-5380)
-add_subdirectory(linking-goto-binaries)
-add_subdirectory(symtab2gb)
-add_subdirectory(symtab2gb-cbmc)
-add_subdirectory(solver-hardness)
-if(NOT WIN32)
-  add_subdirectory(goto-ld)
-endif()
-add_subdirectory(validate-trace-xml-schema)
-add_subdirectory(cbmc-primitives)
-add_subdirectory(goto-interpreter)
-add_subdirectory(cbmc-sequentialization)
-add_subdirectory(cpp-linter)
-add_subdirectory(catch-framework)
-add_subdirectory(libcprover-cpp)
-add_subdirectory(book-examples)
 
-if(WITH_MEMORY_ANALYZER)
-  add_subdirectory(snapshot-harness)
-  add_subdirectory(memory-analyzer)
-  add_subdirectory(extract_type_header)
-endif()
diff --git a/regression/Makefile b/regression/Makefile
@@ -1,69 +1,7 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = cbmc-shadow-memory \
-       cbmc \
-       cbmc-library \
-       cprover \
-       crangler \
-       goto-analyzer \
-       ansi-c \
-       goto-instrument \
-       cpp \
-       cbmc-concurrency \
-       cbmc-cover \
-       cbmc-incr-oneloop \
-       cbmc-incr-smt2 \
-       cbmc-incr \
-       cbmc-output-file \
-       cbmc-with-incr \
-       array-refinement-with-incr \
-       goto-instrument-chc \
-       goto-instrument-json \
-       goto-instrument-wmm-core \
-       goto-instrument-typedef \
-       goto-inspect \
-       smt2_solver \
-       smt2_strings \
-       strings \
-       invariants \
-       goto-diff \
-       test-script \
-       goto-analyzer-taint \
-       goto-bmc/goto-bmc-symex-ready-goto \
-       goto-bmc/goto-bmc-non-symex-ready-goto \
-       goto-bmc \
-       goto-gcc \
-       goto-cl \
-       goto-cc-cbmc \
-       goto-cc-cbmc-shared-options \
-       cbmc-cpp \
-       goto-cc-goto-analyzer \
-       goto-analyzer-simplify \
-       statement-list \
-       systemc \
-       contracts \
-       contracts-dfcc \
-       goto-synthesizer \
-       acceleration \
-       k-induction \
-       goto-harness \
-       goto-harness-multi-file-project \
-       goto-cc-file-local \
-       goto-cc-regression-gh-issue-5380 \
-       linking-goto-binaries \
-       symtab2gb \
-       symtab2gb-cbmc \
-       solver-hardness \
-       goto-ld \
-       validate-trace-xml-schema \
-       cbmc-primitives \
-       goto-interpreter \
-       cbmc-sequentialization \
-       cpp-linter \
-       catch-framework \
-       libcprover-cpp \
-       book-examples \
+DIRS = goto-synthesizer \
        # Empty last line
 
 ifndef WITH_MEMORY_ANALYZER
@@ -80,11 +18,6 @@ ifndef WITH_MEMORY_ANALYZER
   endif
 endif
 
-ifeq ($(WITH_MEMORY_ANALYZER),1)
-  DIRS += snapshot-harness \
-          memory-analyzer \
-          extract_type_header
-endif
 
 # Run all test directories in sequence
 .PHONY: test

diff --git a/regression/acceleration/array_safe1/main.c b/regression/acceleration/array_safe1/main.c
diff --git a/regression/acceleration/array_safe1/test.desc b/regression/acceleration/array_safe1/test.desc
diff --git a/regression/acceleration/array_safe2/main.c b/regression/acceleration/array_safe2/main.c
diff --git a/regression/acceleration/array_safe2/test.desc b/regression/acceleration/array_safe2/test.desc
diff --git a/regression/acceleration/array_safe3/main.c b/regression/acceleration/array_safe3/main.c
diff --git a/regression/acceleration/array_safe3/test.desc b/regression/acceleration/array_safe3/test.desc
diff --git a/regression/acceleration/array_safe4/main.c b/regression/acceleration/array_safe4/main.c
diff --git a/regression/acceleration/array_safe4/test.desc b/regression/acceleration/array_safe4/test.desc
diff --git a/regression/acceleration/array_unsafe1/main.c b/regression/acceleration/array_unsafe1/main.c
diff --git a/regression/acceleration/array_unsafe1/test.desc b/regression/acceleration/array_unsafe1/test.desc
diff --git a/regression/acceleration/array_unsafe2/main.c b/regression/acceleration/array_unsafe2/main.c
diff --git a/regression/acceleration/array_unsafe2/test.desc b/regression/acceleration/array_unsafe2/test.desc
diff --git a/regression/acceleration/array_unsafe3/main.c b/regression/acceleration/array_unsafe3/main.c
diff --git a/regression/acceleration/array_unsafe3/test.desc b/regression/acceleration/array_unsafe3/test.desc
diff --git a/regression/acceleration/array_unsafe4/main.c b/regression/acceleration/array_unsafe4/main.c
diff --git a/regression/acceleration/array_unsafe4/test.desc b/regression/acceleration/array_unsafe4/test.desc
diff --git a/regression/acceleration/const_safe1/main.c b/regression/acceleration/const_safe1/main.c
diff --git a/regression/acceleration/const_safe1/test.desc b/regression/acceleration/const_safe1/test.desc
diff --git a/regression/acceleration/const_unsafe1/main.c b/regression/acceleration/const_unsafe1/main.c
diff --git a/regression/acceleration/const_unsafe1/test.desc b/regression/acceleration/const_unsafe1/test.desc
diff --git a/regression/acceleration/diamond_safe1/main.c b/regression/acceleration/diamond_safe1/main.c
diff --git a/regression/acceleration/diamond_safe1/test.desc b/regression/acceleration/diamond_safe1/test.desc