From bf3c95c9b96553159b0d121881179feff7853e5d Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 20 Feb 2010 09:43:34 +0000
Subject: 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
---
 Test/inline/Answer      | 16 +++++++++++-----
 Test/inline/runtest.bat |  7 +++++++
 2 files changed, 18 insertions(+), 5 deletions(-)

(limited to 'Test/inline')

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
@@ -1475,6 +1470,17 @@ Execution trace:
 Boogie program verifier finished with 1 verified, 1 error
 -------------------- Elevator.bpl --------------------
 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
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
-- 
cgit v1.2.3