Adding an option for deterministicExtractLoops, that uses an alternate way to extract loops into procedures. Unsound for concurrency.

Added a test in extractLoops directory.

3 files changed, 50 insertions, 0 deletions

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index 954ea799..bf30d427 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -83,3 +83,8 @@ Execution trace:
 

 Boogie program verifier finished with 0 verified, 1 error

 -----

+----- Running regression test detLoopExtract.bpl with deterministicExtractLoops

+Stratified Inlining: Reached recursion bound of 4

+

+Boogie program verifier finished with 2 verified, 0 errors

+-----

diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl
new file mode 100644
index 00000000..8965f93e
--- /dev/null
+++ b/Test/extractloops/detLoopExtract.bpl
@@ -0,0 +1,42 @@
+var g:int;
+var h:int; //not modified
+var k:int; //modified in a procedure call
+
+procedure Foo(a:int)
+modifies g;
+modifies h;
+modifies k;
+ensures  g == old(g);
+{
+   var b: int;
+   b := 0;
+   g := a;
+   h := 5;  
+      
+LH:    assert (b + g == a);
+       if (g == 0) {
+          goto LE;
+       }
+       assume (b + g == a); // to help the loop extraction figure out the loop invariant
+       b := b + 1;
+       call Bar();
+       g := g - 1;
+       if (b > 100) {
+   	  goto L2;
+       }            
+       goto LH;
+
+LE: assert (b == a);
+
+    
+L2: g := old(g);
+    return;
+
+}
+
+procedure Bar() 
+modifies k;
+{
+ k := 0;
+ return; 
+}
\ No newline at end of file
diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index 4fbed727..05bfae55 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -16,4 +16,7 @@ echo -----
 echo ----- Running regression test t3.bpl with recursion bound 4

 %BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl

 echo -----

+echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops

+%BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl

+echo -----