diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:22:08 -0700 |
| commit | ae44269a34b002797b2583b93a0041059b57cbda (patch) | |
| tree | 3ec4a7a8ca3477298f93feb1267d854062a26417 /Test/bitvectors | |
| parent | 6be1fd5fa2617602d0a86e95d656018b172ef8d2 (diff) | |
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
Diffstat (limited to 'Test/bitvectors')
| -rw-r--r-- | Test/bitvectors/Answer | 8 | ||||
| -rw-r--r-- | Test/bitvectors/runtest.bat | 9 |
2 files changed, 4 insertions, 13 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index f0f65b04..e20474d9 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -28,12 +28,6 @@ Boogie program verifier finished with 1 verified, 0 errors 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
-bv4.bpl(3,13): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-bv4.bpl(5,6): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-bv4.bpl(5,14): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-4 type checking errors detected in bv4.bpl
-------------------- bv5.bpl --------------------
bv5.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -52,6 +46,6 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- bv10.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
+-------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat index a0480645..2a140368 100644 --- a/Test/bitvectors/runtest.bat +++ b/Test/bitvectors/runtest.bat @@ -5,16 +5,13 @@ set BGEXE=..\..\Binaries\Boogie.exe for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% /proverWarnings:1 /bv:z %* /logPrefix:-0 %%f
+ %BGEXE% /proverWarnings:1 %* %%f
)
-echo -------------------- bv4.bpl - /bv:n --------------------
-%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl
-
for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
-echo -------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
-%BGEXE% /bv:z /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl
+echo -------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true --------------------
+%BGEXE% /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl
|