diff options
| author |  rustanleino <unknown> | 2010-10-26 01:28:32 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-26 01:28:32 +0000 |
| commit | 14fd1ed33b759735c9bd8255c37885c066f7040f (patch) | |
| tree | 10a21e3c8dbd045e85462234c5240fc6303f84ed /Test/bitvectors | |
| parent | 0557e6509f413fe48ee21f538b69bf72e52fc36e (diff) | |
Updated parser.cs files to pick up the new .frame improvements from boogiepartners
Diffstat (limited to 'Test/bitvectors')
| -rw-r--r-- | Test/bitvectors/Answer | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index d861d253..6f4068c6 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -25,8 +25,8 @@ bv3.bpl(2,5): Error: type name: bv16 is registered for bitvectors Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv7.bpl --------------------
-bv7.bpl(4,14): Error: arguments of extract need to be integer literals
-bv7.bpl(5,15): Error: parentheses around bitvector bounds are not allowed
+bv7.bpl(4,14): error: arguments of extract need to be integer literals
+bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed
2 parse errors detected in bv7.bpl
-------------------- bv4.bpl - /bv:n --------------------
bv4.bpl(3,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
@@ -37,13 +37,13 @@ bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z -------------------- bv5.bpl --------------------
bv5.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
- bv5.bpl(5,12): anon0
+ bv5.bpl(5,12): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv6.bpl --------------------
bv6.bpl(8,3): Error BP5001: This assertion might not hold.
Execution trace:
- bv6.bpl(5,5): anon0
+ bv6.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- bv8.bpl --------------------
|