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

Added a test in extractLoops directory.

1 files changed, 42 insertions, 0 deletions

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