Add regression test for #640.

intTests/test_llvm_return_null/Makefile

@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c

intTests/test_llvm_return_null/test.c

@@ -0,0 +1,10 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+uint64_t *foo () {
+	return NULL;
+}
+
+int bar () {
+	return (foo() == NULL);
+}

intTests/test_llvm_return_null/test.saw

@@ -0,0 +1,26 @@
+// This test checks whether we can verify a spec that says a function
+// returns a fresh pointer, when in actuality the function returns
+// NULL. It is a regression test for saw-script issue #640.
+// https://github.com/GaloisInc/saw-script/issues/640
+
+bc <- llvm_load_module "test.bc";
+
+let i64 = llvm_int 64;
+
+fails (
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      crucible_execute_func [];
+      x <- crucible_alloc i64;
+      crucible_return x;
+    }
+    z3
+  );
+
+bar_ov1 <-
+  crucible_llvm_verify bc "bar" [] false
+    do {
+      crucible_execute_func [];
+      crucible_return (crucible_term {{ 1 : [32] }});
+    }
+    z3;

intTests/test_llvm_return_null/test.sh

@@ -0,0 +1 @@
+$SAW test.saw