intTests: Adapt test_stack_traces to new llvm_execute_func requirement.

An llvm_execute_func declaration is now required in all LLVMSetup
blocks.

Author: brianhuffman

intTests/test_stack_traces/trace004.log.good

@@ -4,28 +4,40 @@
  just llvm_stack
 Stack trace:
    (builtin) in llvm_stack
-   trace004.saw:15:32-15:42 in (callback)
+   trace004.saw:15:39-15:49 in (callback)
    (builtin) in llvm_verify
-   trace004.saw:15:1-15:45 (at top level)
+   trace004.saw:15:8-15:52 in (callback)
+   (builtin) in fails
+   trace004.saw:15:1-15:52 (at top level)
+
+== Anticipated failure message ==
+Stack trace:
+   (builtin) in llvm_verify
+   trace004.saw:15:8-15:52 in (callback)
+   (builtin) in fails
+   trace004.saw:15:1-15:52 (at top level)
+Missing llvm_execute_func specification when verifying foo
 
- Verifying foo...
- Simulating foo...
- Checking proof obligations foo...
- Proof succeeded! foo
 
  ------------------------------------------------------------
  llvm_stack via let
 Stack trace:
    (builtin) in llvm_stack
    trace004.saw:22:13-22:23 in spec0
-   trace004.saw:23:32-23:37 in (callback)
+   trace004.saw:23:39-23:44 in (callback)
    (builtin) in llvm_verify
-   trace004.saw:23:1-23:40 (at top level)
+   trace004.saw:23:8-23:47 in (callback)
+   (builtin) in fails
+   trace004.saw:23:1-23:47 (at top level)
+
+== Anticipated failure message ==
+Stack trace:
+   (builtin) in llvm_verify
+   trace004.saw:23:8-23:47 in (callback)
+   (builtin) in fails
+   trace004.saw:23:1-23:47 (at top level)
+Missing llvm_execute_func specification when verifying foo
 
- Verifying foo...
- Simulating foo...
- Checking proof obligations foo...
- Proof succeeded! foo
 
  ------------------------------------------------------------
  do-block

intTests/test_stack_traces/trace004.saw

@@ -9,18 +9,18 @@ print "";
 
 
 // Test just llvm_stack by itself.
-// This probably should not actually verify, but it does...
+// This should not actually verify.
 print "------------------------------------------------------------";
 print "just llvm_stack";
-llvm_verify mod "foo" [] false llvm_stack z3;
+fails (llvm_verify mod "foo" [] false llvm_stack z3);
 print "";
 
 // Test just llvm_stack via a let-binding.
-// This probably should not actually verify, but it does...
+// This should not actually verify.
 print "------------------------------------------------------------";
 print "llvm_stack via let";
 let spec0 = llvm_stack;
-llvm_verify mod "foo" [] false spec0 z3;
+fails (llvm_verify mod "foo" [] false spec0 z3);
 print "";
 
 // Test with an inline do-block.