Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.

6 files changed, 174 insertions, 201 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

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index 9a6c95a3..954ea799 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -64,6 +64,10 @@ Boogie program verifier finished with 1 verified, 0 errors
 t3.bpl(38,5): Error BP5001: This assertion might not hold.

 Execution trace:

     t3.bpl(19,3): anon0

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

     t3.bpl(27,3): anon3_LoopBody

     t3.bpl(23,3): anon3_LoopHead

     Inlined call to procedure foo begins

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 290059d6..aee2722e 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -2,31 +2,31 @@
 bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.

 bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar1.bpl(24,3): anon0

-        Inlined call to procedure foo begins

-            bar1.bpl(13,5): anon0

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar1.bpl(24,3): anon0

+    Inlined call to procedure foo begins

+        bar1.bpl(13,5): anon0

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar2.bpl

 bar2.bpl(21,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        bar2.bpl(19,3): anon0

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(6,7): anon3_Then

-        Inlined call to procedure foo ends

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(9,7): anon3_Else

-        Inlined call to procedure foo ends

+    bar2.bpl(19,3): anon0

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(9,7): anon3_Else

+    Inlined call to procedure foo ends

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(6,7): anon3_Then

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error
 bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.

 bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar3.bpl(38,3): anon0

-        Inlined call to procedure foo begins

-            bar3.bpl(18,3): anon0

-            bar3.bpl(19,7): anon3_Then

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar3.bpl(38,3): anon0

+    Inlined call to procedure foo begins

+        bar3.bpl(18,3): anon0

+        bar3.bpl(19,7): anon3_Then

+        Inlined call to procedure bar begins

+            bar3.bpl(7,3): anon0

+            bar3.bpl(8,7): anon3_Then

+        Inlined call to procedure bar ends

         Inlined call to procedure bar begins

             bar3.bpl(7,3): anon0

-            bar3.bpl(10,7): anon3_Else

+            bar3.bpl(8,7): anon3_Then

         Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

+    Inlined call to procedure bar begins

+        bar3.bpl(7,3): anon0

+        bar3.bpl(10,7): anon3_Else

+    Inlined call to procedure bar ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 11f0e658..4e3886aa 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -2,56 +2,49 @@
 -------------------- NullInModel --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 3:int

-*3 {@false} -> 4:int

+*0 {%lbl%+24 %lbl%+37} -> true

+*1 {%lbl%@47} -> false

+*2 {s null} 

+*3 {refType} 

 *4 {intType} 

 *5 {boolType} 

-*6 {refType} 

-*7 {s null} 

-*8 -> 0:int

-*9 -> 1:int

-*10 -> 2:int

-*11 

+*6 -> 0:int

+*7 -> 1:int

+*8 -> 2:int

+*9 

 function interpretations:

-$pow2 -> {

-  *8 -> *9

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

-Ctor -> {

-  *4 -> *8

-  *5 -> *9

-  *6 -> *10

+type -> {

+  *2 -> *3

   else -> #unspecified

 }

-type -> {

-  *7 -> *6

+Ctor -> {

+  *4 -> *6

+  *5 -> *7

+  *3 -> *8

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

+%lbl%+24 : *0

+%lbl%+37 : *0

+%lbl%@47 : *1

+s : *2

+null : *2

+refType : *3

 intType : *4

 boolType : *5

-refType : *6

-s : *7

-null : *7

 valueToPartition:

 True : *0

 False : *1

-3 : *2

-4 : *3

-0 : *8

-1 : *9

-2 : *10

+0 : *6

+1 : *7

+2 : *8

 End of model.

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -62,45 +55,38 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- IntInModel --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 2:int

-*3 {@false} -> 3:int

-*4 {intType} 

-*5 {boolType} 

-*6 {i} -> 0:int

-*7 -> 1:int

-*8 

+*0 {%lbl%+29 %lbl%+23} -> true

+*1 {%lbl%@39} -> false

+*2 {intType} 

+*3 {boolType} 

+*4 {i} -> 0:int

+*5 -> 1:int

+*6 

 function interpretations:

-$pow2 -> {

-  *6 -> *7

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

 Ctor -> {

-  *4 -> *6

-  *5 -> *7

+  *2 -> *4

+  *3 -> *5

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

-i : *6

+%lbl%+29 : *0

+%lbl%+23 : *0

+%lbl%@39 : *1

+intType : *2

+boolType : *3

+i : *4

 valueToPartition:

 True : *0

 False : *1

-2 : *2

-3 : *3

-0 : *6

-1 : *7

+0 : *4

+1 : *5

 End of model.

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -111,66 +97,59 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- ModelTest --------------------

 Z3 error model: 

 partitions:

-*0 -> true

-*1 -> false

-*2 {@true} -> 5:int

-*3 {@false} -> 6:int

-*4 {intType} 

-*5 {boolType} 

+*0 {%lbl%+64 %lbl%+119} -> true

+*1 {%lbl%@182} -> false

+*2 {s} 

+*3 {j@2} -> 4:int

+*4 {boolType} 

+*5 {intType} 

 *6 {refType} 

-*7 {s} 

-*8 {r} 

-*9 {i@0} -> 1:int

-*10 {j@0} -> 2:int

-*11 {j@1} -> 3:int

-*12 {j@2} -> 4:int

-*13 -> 0:int

-*14 

+*7 {i@0} -> 1:int

+*8 {j@0} -> 2:int

+*9 {j@1} -> 3:int

+*10 {r} 

+*11 -> 0:int

+*12 

 function interpretations:

-$pow2 -> {

-  *13 -> *9

-  else -> #unspecified

-}

 tickleBool -> {

-  *1 -> *0

   *0 -> *0

+  *1 -> *0

   else -> #unspecified

 }

-Ctor -> {

-  *4 -> *13

-  *5 -> *9

-  *6 -> *10

+type -> {

+  *2 -> *6

+  *10 -> *6

   else -> #unspecified

 }

-type -> {

-  *7 -> *6

-  *8 -> *6

+Ctor -> {

+  *5 -> *11

+  *4 -> *7

+  *6 -> *8

   else -> #unspecified

 }

 END_OF_MODEL

 .

 identifierToPartition:

-@true : *2

-@false : *3

-intType : *4

-boolType : *5

+%lbl%+64 : *0

+%lbl%+119 : *0

+%lbl%@182 : *1

+s : *2

+j@2 : *3

+boolType : *4

+intType : *5

 refType : *6

-s : *7

-r : *8

-i@0 : *9

-j@0 : *10

-j@1 : *11

-j@2 : *12

+i@0 : *7

+j@0 : *8

+j@1 : *9

+r : *10

 valueToPartition:

 True : *0

 False : *1

-5 : *2

-6 : *3

-1 : *9

-2 : *10

-3 : *11

-4 : *12

-0 : *13

+4 : *3

+1 : *7

+2 : *8

+3 : *9

+0 : *11

 End of model.

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -199,86 +178,85 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

-@true -> 6

-@false -> 7

+%lbl%+112 -> true

+%lbl%+116 -> true

+%lbl%+110 -> true

+%lbl%+189 -> true

+%lbl%@334 -> false

+m@3 -> -1

+m@2 -> -1

+this -> *3

 intType -> *4

-boolType -> *5

-RefType -> *6

-FieldNameType -> *7

-Heap -> *8

-this -> *9

-F -> *10

-@MV_state_const -> 8

+Heap -> *5

+FieldNameType -> *6

 m@0 -> -2

 r@0 -> -2

+boolType -> *8

+RefType -> *9

+F -> *10

+@MV_state_const -> 6

 x@@4 -> 797

-m@2 -> -1

-m@3 -> -1

 y@@1 -> **y@@1

 r -> **r

 m -> **m

-$pow2 -> {

-  0 -> 1

-  else -> *23

-}

 tickleBool -> {

-  false -> true

   true -> true

-  else -> *23

-}

-Ctor -> {

-  *4 -> 0

-  *5 -> 1

-  *6 -> 3

-  *7 -> 4

-  *19 -> 2

-  else -> *23

+  false -> true

+  else -> true

 }

 type -> {

-  *8 -> *19

-  *9 -> *6

-  *10 -> *7

+  *5 -> *13

+  *3 -> *9

+  *10 -> *6

   -2 -> *4

-  else -> *23

+  else -> *13

 }

-MapType0Type -> {

-  *6 *7 *4 -> *19

-  else -> *23

-}

-MapType0TypeInv2 -> {

-  *19 -> *4

-  else -> *23

-}

-MapType0TypeInv1 -> {

-  *19 -> *7

-  else -> *23

-}

-MapType0TypeInv0 -> {

-  *19 -> *6

-  else -> *23

+Ctor -> {

+  *4 -> 0

+  *8 -> 1

+  *9 -> 3

+  *6 -> 4

+  *13 -> 2

+  else -> 0

 }

 @MV_state -> {

-  8 0 -> true

-  8 3 -> true

-  8 4 -> true

-  8 5 -> true

-  else -> *23

+  6 0 -> true

+  6 3 -> true

+  6 4 -> true

+  6 5 -> true

+  else -> true

 }

 [3] -> {

-  *8 *9 *10 -> -2

-  else -> *23

+  *5 *3 *10 -> -2

+  else -> -2

 }

 U_2_int -> {

   -2 -> -2

-  else -> *23

+  else -> -2

+}

+MapType0TypeInv1 -> {

+  *13 -> *6

+  else -> *6

+}

+MapType0Type -> {

+  *9 *6 *4 -> *13

+  else -> *13

+}

+MapType0TypeInv2 -> {

+  *13 -> *4

+  else -> *4

+}

+MapType0TypeInv0 -> {

+  *13 -> *9

+  else -> *9

 }

 int_2_U -> {

   -2 -> -2

-  else -> *23

+  else -> -2

 }

 *** STATE <initial>

-  Heap -> *8

-  this -> *9

+  Heap -> *5

+  this -> *3

   x -> 797

   y -> **y@@1

   r -> **r

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 3dc7d0c3..8ce2f66e 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
 )

 

 echo -------------------- sk_hack.bpl --------------------

-%BGEXE% %* /noinfer /bv:z sk_hack.bpl

+%BGEXE% %* /noinfer sk_hack.bpl

 

 for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (

   echo.