Merge pull request #2196 from GaloisInc/220-inexact-postcond-test

Add the (modernized) test case from #220

intTests/test0220/Makefile

@@ -0,0 +1,18 @@
+# The current checked-in test.bc was generated by:
+#    Apple clang version 15.0.0 (clang-1500.1.0.2.5)
+#    Target: arm64-apple-darwin22.6.0
+#    Thread model: posix
+#    InstalledDir: /Library/Developer/CommandLineTools/usr/bin
+# but neither the target nor the clang/llvm version is expected to be
+# significant.
+CC = clang
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test0220/test.c

@@ -0,0 +1,5 @@
+unsigned char y;
+
+void f(void) {
+   y = 6;
+}

intTests/test0220/test.saw

@@ -0,0 +1,15 @@
+// Test an inexact postcondition.
+
+mod <- llvm_load_module "test.bc";
+
+let spec = do {
+   llvm_alloc_global "y";
+   y <- llvm_fresh_var "y" (llvm_int 8); 
+   llvm_points_to (llvm_global "y") (llvm_term y); 
+   llvm_execute_func [];
+   y_new <- llvm_fresh_var "y_new" (llvm_int 8);
+   llvm_points_to (llvm_global "y") (llvm_term y_new);
+   llvm_postcond {{ y_new > 0 }};
+};
+
+llvm_verify mod "f" [] false spec abc;

intTests/test0220/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw