diff options
author | Unknown <Shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-05-25 11:22:51 -0700 |
---|---|---|
committer | Unknown <Shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-05-25 11:22:51 -0700 |
commit | e23a208872d904ae9f8e5e7fd57727e422b123a2 (patch) | |
tree | 1f1ebb2871214f447b7aa96e90a971b475e75da7 | |
parent | 8bd9e0a7727b2c6977a59ac4af4f82357b7ba39c (diff) |
Fixed the regression for deterministicExtractLoops.
-rw-r--r-- | Test/extractloops/Answer | 5 | ||||
-rw-r--r-- | Test/extractloops/detLoopExtract.bpl | 14 |
2 files changed, 13 insertions, 6 deletions
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index 08b1fffc..b9083fae 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 1 verified, 0 errors
+-----
diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl index 8965f93e..976d58d6 100644 --- a/Test/extractloops/detLoopExtract.bpl +++ b/Test/extractloops/detLoopExtract.bpl @@ -2,22 +2,22 @@ var g:int; var h:int; //not modified var k:int; //modified in a procedure call -procedure Foo(a:int) +procedure {:entrypoint} Foo(a:int) modifies g; modifies h; modifies k; -ensures g == old(g); +//ensures g == old(g); { var b: int; b := 0; g := a; h := 5; -LH: assert (b + g == a); +LH: //assert (b + g == a); if (g == 0) { goto LE; } - assume (b + g == a); // to help the loop extraction figure out the loop invariant + //assume (b + g == a); // to help the loop extraction figure out the loop invariant b := b + 1; call Bar(); g := g - 1; @@ -26,10 +26,12 @@ LH: assert (b + g == a); } goto LH; -LE: assert (b == a); +LE: -L2: g := old(g); +L2: //g := old(g); + //assert (b == a); + assume (b != a); return; } |