From ae44269a34b002797b2583b93a0041059b57cbda Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Oct 2011 14:22:08 -0700 Subject: Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. --- Test/bitvectors/Answer | 8 +------- Test/bitvectors/runtest.bat | 9 +++------ 2 files changed, 4 insertions(+), 13 deletions(-) (limited to 'Test/bitvectors') 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 -- cgit v1.2.3