diff options
| author |  qadeer <unknown> | 2014-01-14 12:57:36 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-01-14 12:57:36 -0800 |
| commit | 9d531ea4e1d862132c2bbf50017b184612176990 (patch) | |
| tree | 34fc75f50873e9c19276b9fae20a82689813b957 /Test/og/Answer | |
| parent | dca5ebaacf57702e3270df74a2965e08d9a7d1cb (diff) | |
added more information to assert messages
Diffstat (limited to 'Test/og/Answer')
| -rw-r--r-- | Test/og/Answer | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index 73ec8537..067a6534 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -1,6 +1,6 @@ -------------------- foo.bpl --------------------
-foo.bpl(14,3): Error BP5001: This assertion might not hold.
+foo.bpl(14,3): Error: Non-interference check failed
Execution trace:
foo.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -8,11 +8,11 @@ Execution trace: Boogie program verifier finished with 4 verified, 1 error
-------------------- bar.bpl --------------------
-bar.bpl(13,3): Error BP5001: This assertion might not hold.
+bar.bpl(13,3): Error: Non-interference check failed
Execution trace:
bar.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
-bar.bpl(13,3): Error BP5001: This assertion might not hold.
+bar.bpl(13,3): Error: Non-interference check failed
Execution trace:
bar.bpl(23,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -24,11 +24,11 @@ Boogie program verifier finished with 3 verified, 2 errors Boogie program verifier finished with 2 verified, 0 errors
-------------------- parallel1.bpl --------------------
-parallel1.bpl(10,1): Error BP5001: This assertion might not hold.
+parallel1.bpl(10,1): Error: Non-interference check failed
Execution trace:
parallel1.bpl(6,5): anon0
(0,0): inline$Proc_YieldChecker_PC_2147483647$0$L0
-parallel1.bpl(14,3): Error BP5001: This assertion might not hold.
+parallel1.bpl(14,3): Error: Non-interference check failed
Execution trace:
parallel1.bpl(6,5): anon0
(0,0): inline$Impl_YieldChecker_PC_2147483647$0$L0
@@ -72,7 +72,7 @@ Boogie program verifier finished with 4 verified, 0 errors Boogie program verifier finished with 3 verified, 0 errors
-------------------- t1.bpl --------------------
-t1.bpl(35,5): Error BP5001: This assertion might not hold.
+t1.bpl(35,5): Error: Non-interference check failed
Execution trace:
(0,0): og_init
(0,0): inline$Impl_YieldChecker_A_2147483647$0$L1
@@ -88,7 +88,7 @@ Boogie program verifier finished with 2 verified, 0 errors Boogie program verifier finished with 2 verified, 0 errors
-------------------- async.bpl --------------------
-async.bpl(14,1): Error BP5001: This assertion might not hold.
+async.bpl(14,1): Error: Non-interference check failed
Execution trace:
async.bpl(7,3): anon0
async.bpl(7,3): anon0$1
|