Update regression test for #641 to indicate expected failure.

GaloisInc · Aug 27, 2020 · 58c89d2 · 58c89d2
1 parent ccf73dc
commit 58c89d2
Showing 1 changed file with 14 additions and 3 deletions.
diff --git a/intTests/test_llvm_non_fresh/test.saw b/intTests/test_llvm_non_fresh/test.saw
@@ -9,23 +9,34 @@ bc <- llvm_load_module "test.bc";
 let i64 = llvm_int 64;
 
 foo_ov <-
+  crucible_llvm_verify bc "foo" [] false
+    do {
+      x <- crucible_alloc i64;
+      crucible_execute_func [x];
+      crucible_return x;
+    }
+    z3;
+
+fails (
   crucible_llvm_verify bc "foo" [] false
     do {
       x <- crucible_alloc i64;
       crucible_execute_func [x];
       y <- crucible_alloc i64;
       crucible_return y;
     }
-    z3;
+    z3
+  );
 
-bar_ov0 <-
+fails (
   crucible_llvm_verify bc "bar" [foo_ov] false
     do {
       x <- crucible_alloc i64;
       crucible_execute_func [x];
       crucible_return (crucible_term {{ 0 : [32] }});
     }
-    z3;
+    z3
+  );
 
 bar_ov1 <-
   crucible_llvm_verify bc "bar" [] false