From 5f5c19de9731c551a91307e97d31e4f181edf216 Mon Sep 17 00:00:00 2001
From: Unknown <Shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com>
Date: Fri, 25 May 2012 11:13:38 -0700
Subject: Adding an option for deterministicExtractLoops, that uses an
 alternate way to extract loops into procedures. Unsound for concurrency.

Added a test in extractLoops directory.
---
 Test/extractloops/Answer             |  5 +++++
 Test/extractloops/detLoopExtract.bpl | 42 ++++++++++++++++++++++++++++++++++++
 Test/extractloops/runtest.bat        |  3 +++
 3 files changed, 50 insertions(+)
 create mode 100644 Test/extractloops/detLoopExtract.bpl

(limited to 'Test/extractloops')

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 -----
 
-- 
cgit v1.2.3