Boogie:

* Bug fix:  Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case)
* Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants.  Previously, the only option was to instrument at the beginning and end of every basic block.  The new option, which is now the default, is to instrument only at the beginning of loop heads.
* Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized
* Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1

Boogie refactoring:
* Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand
* Cleaned up some parsing of command-line options

12 files changed, 90 insertions, 20 deletions

diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index 15f36ab0..a4c12d8d 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -3,4 +3,4 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-%BGEXE% %* -infer:c -printInstrumented -noVerify constants.bpl

+%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl

diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat
index f2a4d3e5..3b2c382c 100644
--- a/Test/aitest1/runtest.bat
+++ b/Test/aitest1/runtest.bat
@@ -7,7 +7,7 @@ for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl
      Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl

      Linear7.bpl Linear8.bpl Linear9.bpl) do (

   echo -------------------- %%f --------------------

-  %BGEXE% %* -infer:p -printInstrumented -noVerify %%f

+  %BGEXE% %* -infer:p -instrumentInfer:e -printInstrumented -noVerify %%f

 )

 

 for %%f in (Bound.bpl) do (

diff --git a/Test/aitest9/answer b/Test/aitest9/answer
index d6bba688..27e18ca4 100644
--- a/Test/aitest9/answer
+++ b/Test/aitest9/answer
@@ -13,11 +13,8 @@ TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.
 Execution trace:

     TestIntervals.bpl(5,5): anon0

     TestIntervals.bpl(6,3): anon9_LoopHead

-    TestIntervals.bpl(6,3): anon9_LoopDone

     TestIntervals.bpl(12,14): anon10_Then

-    TestIntervals.bpl(13,3): anon4

     TestIntervals.bpl(13,14): anon11_Then

-    TestIntervals.bpl(14,3): anon6

     TestIntervals.bpl(14,14): anon12_Then

     TestIntervals.bpl(17,5): anon8

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 107cab0b..540bcb4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -87,17 +87,14 @@ Execution trace:
     (0,0): anon0

 SmallTests.dfy(61,36): Error: possible division by zero

 Execution trace:

-    (0,0): anon0

     (0,0): anon10_Then

 SmallTests.dfy(62,51): Error: possible division by zero

 Execution trace:

-    (0,0): anon0

     (0,0): anon10_Else

     (0,0): anon3

     (0,0): anon11_Else

 SmallTests.dfy(63,22): Error: target object may be null

 Execution trace:

-    (0,0): anon0

     (0,0): anon10_Then

     (0,0): anon3

     (0,0): anon11_Then

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 934b45ba..12cb5960 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1443,13 +1443,8 @@ Boogie program verifier finished with 5 verified, 0 errors
 test5.bpl(37,3): Error BP5001: This assertion might not hold.

 Execution trace:

     test5.bpl(34,10): anon0

-    test5.bpl(25,23): inline$P$0$Entry

     test5.bpl(28,10): inline$P$0$anon0

-    test5.bpl(25,23): inline$P$0$Return

-    test5.bpl(34,10): anon0$1

-    test5.bpl(25,23): inline$P$1$Entry

     test5.bpl(28,10): inline$P$1$anon0

-    test5.bpl(25,23): inline$P$1$Return

     test5.bpl(34,10): anon0$2

 

 Boogie program verifier finished with 4 verified, 1 error

@@ -1477,6 +1472,17 @@ Boogie program verifier finished with 1 verified, 1 error
 Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

 Execution trace:

     Elevator.bpl(15,3): anon0

+    Elevator.bpl(15,3): anon0$1

+    Elevator.bpl(16,3): anon10_LoopHead

+    Elevator.bpl(19,5): anon10_LoopBody

+    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0

+    Elevator.bpl(24,7): anon13_Then$1

+

+Boogie program verifier finished with 1 verified, 1 error

+-------------------- Elevator.bpl with empty blocks --------------------

+Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.

+Execution trace:

+    Elevator.bpl(15,3): anon0

     Elevator.bpl(68,23): inline$Initialize$0$Entry

     Elevator.bpl(71,13): inline$Initialize$0$anon0

     Elevator.bpl(68,23): inline$Initialize$0$Return

diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 335c857d..179509f8 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -18,6 +18,13 @@ for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
   %BGEXE% %* %%f

 )

 

+REM Peephole optimizations are so good that Elevator seems worthwhile

+REM to include twice among these inline tests

+for %%f in (Elevator.bpl) do (

+  echo -------------------- %%f with empty blocks --------------------

+  %BGEXE% /removeEmptyBlocks:0 %* %%f

+)

+

 echo -------------------- expansion2.bpl --------------------

 %BGEXE% %* /proverLog:expansion2.sx expansion2.bpl

 %SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx

diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index aaaee494..1a0327f6 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -51,6 +51,7 @@ Execution trace:
     bla1.bpl(1654,3): inline$storm_IoCompleteRequest$0$anon4_Else#1

     bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1

     bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1

+    bla1.bpl(1676,3): inline$storm_IoCompleteRequest$0$label_1#1

     bla1.bpl(1734,3): anon14_Then#1

     bla1.bpl(1739,3): anon7#1

     bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1

@@ -144,6 +145,7 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1872,3): inline$storm_KeAcquireSpinLock$0$anon7#2

     daytona_bug2_ioctl_example_2.bpl(1883,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2

     daytona_bug2_ioctl_example_2.bpl(1888,3): inline$storm_KeAcquireSpinLock$0$anon9#2

+    daytona_bug2_ioctl_example_2.bpl(1892,3): inline$storm_KeAcquireSpinLock$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(1909,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2

     daytona_bug2_ioctl_example_2.bpl(1920,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2

@@ -155,6 +157,7 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2039,3): inline$storm_IoSetCancelRoutine$0$anon8#2

     daytona_bug2_ioctl_example_2.bpl(2050,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2

     daytona_bug2_ioctl_example_2.bpl(2055,3): inline$storm_IoSetCancelRoutine$0$anon10#2

+    daytona_bug2_ioctl_example_2.bpl(2062,3): inline$storm_IoSetCancelRoutine$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(2075,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2

     daytona_bug2_ioctl_example_2.bpl(2200,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2

@@ -170,6 +173,7 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2337,3): inline$storm_IoSetCancelRoutine$1$anon8#2

     daytona_bug2_ioctl_example_2.bpl(2348,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2

     daytona_bug2_ioctl_example_2.bpl(2353,3): inline$storm_IoSetCancelRoutine$1$anon10#2

+    daytona_bug2_ioctl_example_2.bpl(2361,3): inline$storm_IoSetCancelRoutine$1$label_1#2

     daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2

     daytona_bug2_ioctl_example_2.bpl(2375,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2

     daytona_bug2_ioctl_example_2.bpl(2385,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2

@@ -185,6 +189,7 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2599,3): inline$storm_KeReleaseSpinLock$0$anon5#2

     daytona_bug2_ioctl_example_2.bpl(2610,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2

     daytona_bug2_ioctl_example_2.bpl(2615,3): inline$storm_KeReleaseSpinLock$0$anon7#2

+    daytona_bug2_ioctl_example_2.bpl(2619,3): inline$storm_KeReleaseSpinLock$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2

     daytona_bug2_ioctl_example_2.bpl(2858,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51#2

@@ -194,10 +199,12 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2951,3): inline$storm_IoCompleteRequest$2$anon6_Else#2

     daytona_bug2_ioctl_example_2.bpl(2959,3): inline$storm_IoCompleteRequest$2$anon7_Then#2

     daytona_bug2_ioctl_example_2.bpl(2969,3): inline$storm_IoCompleteRequest$2$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(2973,3): inline$storm_IoCompleteRequest$2$label_1#2

     daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#2

     daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2

     daytona_bug2_ioctl_example_2.bpl(3000,3): inline$I8xCompleteSysButtonIrp$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3013,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2

     daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(3169,3): inline$I8xKeyboardGetSysButtonEvent$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2

@@ -222,6 +229,7 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(3931,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2

     daytona_bug2_ioctl_example_2.bpl(3942,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2

     daytona_bug2_ioctl_example_2.bpl(3947,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2

+    daytona_bug2_ioctl_example_2.bpl(3951,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2

     daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2

     daytona_bug2_ioctl_example_2.bpl(3964,3): inline$storm_IoCancelIrp$0$anon30_Else#2

     daytona_bug2_ioctl_example_2.bpl(3982,3): inline$storm_IoCancelIrp$0$label_16_true#2

@@ -293,6 +301,7 @@ Execution trace:
     stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1

     stack_overflow.bpl(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1

     stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1

+    stack_overflow.bpl(78233,3): inline$storm_IoSetCompletionRoutine$0$label_1#1

     stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1

     stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1

     stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1

@@ -330,11 +339,13 @@ Execution trace:
     stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1

     stack_overflow.bpl(87671,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1

     stack_overflow.bpl(87685,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1

+    stack_overflow.bpl(87692,3): inline$BDLDevicePowerIoCompletion$3$label_83#1

     stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1

     stack_overflow.bpl(87702,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1

     stack_overflow.bpl(87713,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1

     stack_overflow.bpl(87738,3): inline$storm_IoCompleteRequest$7$label_6_false#1

     stack_overflow.bpl(87777,3): inline$storm_IoCompleteRequest$7$label_7#1

+    stack_overflow.bpl(87782,3): inline$storm_IoCompleteRequest$7$label_1#1

     stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#1

     stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1

     stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1

@@ -344,13 +355,16 @@ Execution trace:
     stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1

     stack_overflow.bpl(87953,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1

     stack_overflow.bpl(87967,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1

+    stack_overflow.bpl(87974,3): inline$BDLDevicePowerIoCompletion$3$label_122#1

     stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1

     stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1

     stack_overflow.bpl(88146,3): inline$CallCompletionRoutine$3$label_20_icall_return#1

     stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1

+    stack_overflow.bpl(88169,3): inline$CallCompletionRoutine$3$label_1#1

     stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1

     stack_overflow.bpl(88190,3): inline$storm_IoCallDriver$1$anon15_Else#1

     stack_overflow.bpl(88218,3): inline$storm_IoCallDriver$1$label_36#1

+    stack_overflow.bpl(88222,3): inline$storm_IoCallDriver$1$label_1#1

     stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#1

     stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1

     stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1

@@ -373,6 +387,7 @@ Execution trace:
     stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1

     stack_overflow.bpl(89292,3): inline$BDLPnPStart$0$anon46_Else#1

     stack_overflow.bpl(89306,3): inline$BDLPnPStart$0$label_101_true#1

+    stack_overflow.bpl(89313,3): inline$BDLPnPStart$0$label_102#1

     stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#1

     stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1

     stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1

diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index 5fb6fe62..de255422 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -6,15 +6,11 @@ implementation b(x: int)
 

 

   anon0:

-    assume true;

-    assume true;

     goto anon3_Then;

 

   anon3_Then:

-    assume true;

     assume x < 0;

     y := 1;

-    assume 1 <= y && y <= 1;

     assert false;

     return;

 }

diff --git a/Test/test2/Answer b/Test/test2/Answer
index ef808373..8abc36c9 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -34,6 +34,7 @@ Execution trace:
 Passification.bpl(165,3): Error BP5001: This assertion might not hold.

 Execution trace:

     Passification.bpl(158,1): L0

+    Passification.bpl(161,1): L1

     Passification.bpl(164,1): L2

 

 Boogie program verifier finished with 7 verified, 4 errors

@@ -213,14 +214,16 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar
 Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement.

 Structured.bpl(243,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    Structured.bpl(245,3): anon0

+    Structured.bpl(244,5): anon0

     Structured.bpl(246,5): anon6_LoopBody

     Structured.bpl(247,7): anon7_LoopBody

+    Structured.bpl(248,11): anon8_Then

     Structured.bpl(252,5): anon4

     Structured.bpl(252,14): anon9_Then

 Structured.bpl(303,3): Error BP5001: This assertion might not hold.

 Execution trace:

     Structured.bpl(299,5): anon0

+    Structured.bpl(300,3): anon3_Else

     Structured.bpl(303,3): anon2

 Structured.bpl(311,7): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -378,3 +381,18 @@ Execution trace:
     CallForall.bpl(124,3): anon0

 

 Boogie program verifier finished with 10 verified, 8 errors

+

+-------------------- ContractEvaluationOrder.bpl --------------------

+ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.

+ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.

+Execution trace:

+    ContractEvaluationOrder.bpl(7,5): anon0

+ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    ContractEvaluationOrder.bpl(12,5): anon0

+ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.

+ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    ContractEvaluationOrder.bpl(23,5): anon0

+

+Boogie program verifier finished with 1 verified, 3 errors

diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
new file mode 100644
index 00000000..3eab4bda
--- /dev/null
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -0,0 +1,34 @@
+procedure P() returns (x, y: int)

+  ensures x == y;  // ensured by the body

+  ensures x == 0;  // error: not ensured by the body

+  ensures y == 0;  // follows from the previous two ensures clauses (provided they are

+                   // indeed evaluated in this order, which they are supposed to be)

+{

+  x := y;

+}

+

+procedure Q() returns (x, y: int)

+{

+  x := y;

+

+  assert x == y;  // ensured by the body

+  assert x == 0;  // error: not ensured by the body

+  assert y == 0;  // follows from the previous two asserts (provided they are

+                  // indeed evaluated in this order, which they are supposed to be)

+}

+

+procedure R()

+{

+  var a, b: int;

+  a := b;

+  call S(a, b);

+}

+

+procedure S(x, y: int)

+                    // In the call from R:

+  requires x == y;  // ensured by the body of R

+  requires x == 0;  // error: not ensured by the body of R

+  requires y == 0;  // follows from the previous two requires clauses (provided they are

+                    // indeed evaluated in this order, which they are supposed to be)

+{

+}

diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index ce97b145..69ea2576 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -241,7 +241,7 @@ procedure RunOffEnd2() returns (x: int)
 

 procedure RunOffEnd3() returns (x: int)

   ensures x == 9;

-{

+{ x := 9;

   while (true) {

     while (true) {

       if (*) {

diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f472741c..dbe5b726 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
 echo -------------------- sk_hack.bpl --------------------

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

 

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

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

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* %%f