Add some integration tests for issue GaloisInc#30

intTests/test_llvm_unsound_alloc/test.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if ! $SAW unsound_alloc.saw ; then
+    exit 0
+else
+    exit 1
+fi

intTests/test_llvm_unsound_alloc/unsound_alloc.c

@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+uint32_t foo(uint32_t *x) {
+	uint32_t tmp = *x + 1;
+	*x += 42;
+	return tmp;
+};
+
+uint32_t bar() {
+	uint32_t val = 1;
+	return foo(&val) + val;
+};

intTests/test_llvm_unsound_alloc/unsound_alloc.saw

@@ -0,0 +1,23 @@
+MODULE <- llvm_load_module "unsound_alloc.bc";
+
+let foo_setup = do {
+  x <- crucible_alloc (llvm_int 32);
+  x_star <- crucible_fresh_var "x" (llvm_int 32);
+  crucible_points_to x (crucible_term x_star);
+  crucible_execute_func [x];
+  crucible_return (crucible_term {{ x_star + 1 : [32] }});
+};
+foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3;
+
+let bar_setup = do {
+  crucible_execute_func [];
+  crucible_return (crucible_term {{ 3 : [32] }});
+};
+
+// the below line (without override) correctly fails
+// crucible_llvm_verify MODULE "bar" [] false bar_setup z3;
+
+// works, but shouldn't
+crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3;
+
+print "Should not have succeeded - unsound!";

intTests/test_llvm_unsound_global/test.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if ! $SAW unsound_global.saw ; then
+    exit 0
+else
+    exit 1
+fi

intTests/test_llvm_unsound_global/unsound_global.c

@@ -0,0 +1,22 @@
+// unsound_global.c
+
+#include <stdint.h>
+#include <stdio.h>
+
+uint32_t TEST;
+
+uint32_t GLOBAL[2];
+
+uint32_t foo(uint32_t x) {
+	GLOBAL[1] = x;
+	return x + 1;
+};
+
+uint32_t bar() {
+	TEST = 42;
+	GLOBAL[1] = 0;
+	uint32_t val = foo(1);
+	printf("%u\n", TEST);
+	// GLOBAL[1] = 0;
+	return val + GLOBAL[1];
+};

intTests/test_llvm_unsound_global/unsound_global.saw

@@ -0,0 +1,25 @@
+MODULE <- llvm_load_module "unsound_global.bc";
+
+let foo_setup = do {
+  crucible_alloc_global "GLOBAL";
+  x <- crucible_fresh_var "x" (llvm_int 32);
+  crucible_execute_func [crucible_term x];
+  crucible_return (crucible_term {{ x + 1 : [32] }});
+  // crucible_points_to (crucible_elem (crucible_global "GLOBAL") 1) (crucible_term x);
+};
+foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3;
+
+let bar_setup = do {
+  crucible_alloc_global "GLOBAL";
+  crucible_alloc_global "TEST";
+  crucible_execute_func [];
+  crucible_return (crucible_term {{ 2 : [32] }});
+};
+
+// the below line (without override) correctly fails
+// crucible_llvm_verify MODULE "bar" [] false bar_setup z3;
+
+// works, but shouldn't
+crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3;
+
+print "Should not have succeeded - unsound!";