diff options
Diffstat (limited to 'Test/extractloops/detLoopExtract.bpl')
-rw-r--r-- | Test/extractloops/detLoopExtract.bpl | 42 |
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 |