Turn deref caching off by default in tests

Author: TGWDB

jbmc/regression/jbmc/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-cache-dereferences"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace"
 )
 
 if(DEFINED BDD_GUARDS)

regression/cbmc/CMakeLists.txt

@@ -6,32 +6,21 @@ else()
   set(gcc_only_string "")
 endif()
 
-# We run cbmc tests with dereference cache on by default. There are a handful
-# of tests (mostly tests that check SSA output) which that'd interefere with,
-# so we just exclude those here and run those few tests without dereference
-# caching.
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --symex-cache-dereferences" -X smt-backend -X no-dereference-cache ${gcc_only}
-)
-
-add_test_pl_profile(
-    "cbmc-no-dereference-cache"
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
-    "-C;-X;smt-backend;-I;no-dereference-cache;${gcc_only_string}"
-    "CORE"
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
 )
 
 add_test_pl_profile(
     "cbmc-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo --symex-cache-dereferences"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;-X;no-dereference-cache"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2 --symex-cache-dereferences"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2;-X;no-dereference-cache"
+    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
 )
 

regression/cbmc/Makefile

@@ -10,42 +10,17 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --symex-cache-dereferences" \
-	   -X smt-backend \
-	   -X no-dereference-cache \
-	   $(GCC_ONLY)
-
-test-no-dereference-cache:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" \
-	  -X smt-backend \
-	  -I no-dereference-cache \
-	  $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2 --symex-cache-dereferences" \
-	  -X broken-smt-backend \
-	  -X thorough-smt-backend \
-	  -X no-dereference-cache \
-	  $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend -X thorough-smt-backend $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo --symex-cache-dereferences" \
-	  -X thorough-paths \
-	  -X smt-backend \
-	  -X paths-lifo-expected-failure \
-	  -X no-dereference-cache \
-	  $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
 
 tests.log: ../test.pl test
 
-show:
-	@for dir in *; do \
-		if [ -d "$$dir" ]; then \
-			vim -o "$$dir/*.c" "$$dir/*.out"; \
-		fi; \
-	done;
-
 clean:
-	find -name '*.out' -execdir $(RM) '{}' \;
-	find -name '*.smt2' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log tests-paths-lifo.log tests-cprover-smt2.log

regression/cbmc/dereference-cache-flag/test-no-cache.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 test.c
 --show-vcc
 \(main::1::p!0@1#2 = address_of

regression/cbmc/dereference-cache-flag/test-with-cache.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---show-vcc
+--show-vcc --symex-cache-dereferences
 symex::dereference_cache!0#1 = 0
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 double_deref.c
 --show-vcc
 \{1\} \(main::1::pptr!0@1#2 = address_of\(main::1::ptr[12]!0@1\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]\)

regression/cbmc/double_deref/double_deref_with_cast.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 double_deref_with_cast.c
 --show-vcc
 \{1\} \(cast\(main::1::pptr!0@1#2, signedbv\[32\]\*\*\) = address_of\(main::1::ptr2!0@1\) \? main::argc!0@1#1 = 2 \: main::argc!0@1#1 = 1\)

regression/cbmc/double_deref/double_deref_with_member.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 double_deref_with_member.c
 --show-vcc
 ^\{1\} \(main::1::cptr!0@1#2 = address_of\(main::1::container2!0@1\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,4 +1,4 @@
-CORE no-dereference-cache
+CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
 \{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)