diff options
| author |  qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-07-15 02:26:38 -0700 |
| commit | 7395870356fb83f1b7cab70c95523d1c9f5738d4 (patch) | |
| tree | b8677cada625458aacba867081549e4a784c453d /Test/og/treiber-stack.bpl.expect | |
| parent | 85a60be8a0a7ef1438908364b7997dddc4524ed1 (diff) | |
simplified yield type chcking and added treiber stack (not fully done)
Diffstat (limited to 'Test/og/treiber-stack.bpl.expect')
| -rw-r--r-- | Test/og/treiber-stack.bpl.expect | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/og/treiber-stack.bpl.expect b/Test/og/treiber-stack.bpl.expect new file mode 100644 index 00000000..ed4a9b00 --- /dev/null +++ b/Test/og/treiber-stack.bpl.expect @@ -0,0 +1,8 @@ +(0,0): Error BP5003: A postcondition might not hold on this return path.
+(0,0): Related location: Commutativity check between Load and TransferToStack failed
+Execution trace:
+ (0,0): that_C
+ (0,0): this_A
+ (0,0): this_B
+
+Boogie program verifier finished with 3 verified, 1 error
|