Merge pull request #5321 from danpoe/tests/pointer-primitives

Tests to check inconsistent assumptions involving __CPROVER_r_ok

Author: danpoe

regression/CMakeLists.txt

@@ -56,6 +56,7 @@ add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
 add_subdirectory(validate-trace-xml-schema)
+add_subdirectory(cbmc-primitives)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/Makefile

@@ -33,7 +33,8 @@ DIRS = cbmc \
        solver-hardness \
        goto-ld \
        validate-trace-xml-schema \
-			 # Empty last line
+       cbmc-primitives \
+       # Empty last line
 
 ifeq ($(OS),Windows_NT)
     detected_OS := Windows

regression/cbmc-primitives/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-primitives/Makefile

@@ -0,0 +1,18 @@
+default: tests.log
+
+test:
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cbmc-primitives/r_w_ok_bug/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p1;
+  __CPROVER_assume(__CPROVER_r_ok(p1 - 1, 1));
+  *p1;
+}

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Crashes during the flattening, issue #5328

regression/cbmc-primitives/r_w_ok_inconsistent_dead/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p;
+
+  {
+    char c;
+    p = &c;
+  }
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p;        // succeeds
+}

regression/cbmc-primitives/r_w_ok_inconsistent_dead/test-no-cp.desc

@@ -0,0 +1,13 @@
+FUTURE
+main.c
+--pointer-check --no-simplify --no-propagation
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0). We use
+--no-simplify and --no-propagation to ensure that the case is not solved by the
+constant propagation and thus tests the constraint encoding.

regression/cbmc-primitives/r_w_ok_inconsistent_dead/test.desc

@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--function test_global_pointer --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests that an inconsistent assumption involving a pointer to an out of scope
+variable and __CPROVER_r_ok() can be detected via assert(0).

regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *p = malloc(1);
+  free(p);
+
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+  assert(0); // fails
+  *p;        // succeeds
+}