summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Absy.cs21
-rw-r--r--Test/extractloops/detLoopExtract2.bpl27
-rw-r--r--Test/extractloops/detLoopExtract2.bpl.expect2
-rw-r--r--Test/snapshots/Snapshots41.v0.bpl70
-rw-r--r--Test/snapshots/Snapshots41.v1.bpl78
5 files changed, 120 insertions, 78 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..8c04007b 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -750,15 +750,28 @@ namespace Microsoft.Boogie {
Contract.Assert(block != null);
var auxCmd = block.TransferCmd as GotoCmd;
if (auxCmd == null) continue;
- foreach(var bl in auxCmd.labelTargets)
+ foreach (var bl in auxCmd.labelTargets)
{
if (loopBlocks.Contains(bl)) continue;
- immSuccBlks.Add(bl);
+ immSuccBlks.Add(bl);
}
}
return immSuccBlks;
}
+ private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+ {
+ Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+ var allBlocksInNaturalLoops = new HashSet<Block>();
+ foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+ {
+ Contract.Assert(source != null);
+ g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+ }
+ return allBlocksInNaturalLoops;
+ }
+
+
void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
List<Implementation/*!*/>/*!*/ loopImpls,
Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -975,8 +988,8 @@ namespace Microsoft.Boogie {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
- var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
- var loopNodes = g.NaturalLoops(header, source);
+ //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+ var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source);
foreach(var bl in auxGotoCmd.labelTargets) {
if (!loopNodes.Contains(bl)) {
Block auxNewBlock = new Block();
diff --git a/Test/extractloops/detLoopExtract2.bpl b/Test/extractloops/detLoopExtract2.bpl
new file mode 100644
index 00000000..f2befc53
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -nologo -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:6 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/4
+procedure {:entrypoint} Main() returns(r:int)
+{
+ var i, j : int;
+ var Flag : bool;
+ var b : bool;
+ i := 0;
+ j := 0;
+ Flag := false;
+ while(i<3)
+ {
+ havoc b;
+ if (b || Flag) {
+ i := i + 1;
+ j := j + 1;
+ }
+ else {
+ Flag := true;
+ j := j + 1;
+ }
+ }
+ assume !(i == j || i == j - 1);
+ return;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl.expect b/Test/extractloops/detLoopExtract2.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
index 631fe544..dbfe3e2d 100644
--- a/Test/snapshots/Snapshots41.v0.bpl
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -1,35 +1,35 @@
-procedure {:checksum "0"} M(x: int);
-implementation {:id "M"} {:checksum "1"} M(x: int)
-{ assert x < 20 || 10 <= x; // always true
- assert x < 10; // error
- call Other(x); // error: precondition violation
-}
-
-procedure {:checksum "10"} Other(y: int);
- requires 0 <= y;
-implementation {:id "Other"} {:checksum "11"} Other(y: int)
-{
-}
-
-procedure {:checksum "20"} Posty() returns (z: int);
- ensures 2 <= z; // error: postcondition violation
-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
-{
- var t: int;
- t := 20;
- if (t < z) {
- } else { // the postcondition violation occurs on this 'else' branch
- }
-}
-
-procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
-implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
-{
- assert u != 53; // error
-}
-
-procedure {:checksum "40"} NoChangeAndCorrect();
-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
-{
- assert true;
-}
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{ assert x < 20 || 10 <= x; // always true
+ assert x < 10; // error
+ call Other(x); // error: precondition violation
+}
+
+procedure {:checksum "10"} Other(y: int);
+ requires 0 <= y;
+implementation {:id "Other"} {:checksum "11"} Other(y: int)
+{
+}
+
+procedure {:checksum "20"} Posty() returns (z: int);
+ ensures 2 <= z; // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+ var t: int;
+ t := 20;
+ if (t < z) {
+ } else { // the postcondition violation occurs on this 'else' branch
+ }
+}
+
+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+{
+ assert u != 53; // error
+}
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
+{
+ assert true;
+}
diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
index 0cd9fbf9..9864e0e4 100644
--- a/Test/snapshots/Snapshots41.v1.bpl
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -1,39 +1,39 @@
-procedure {:checksum "0"} M(x: int);
-implementation {:id "M"} {:checksum "1"} M(x: int)
-{
-assert x < 20 || 10 <= x; // always true
-
- assert x < 10; // error
- call Other(x); // error: precondition violation
- assert x == 7; // error: this is a new error in v1
-}
-
-
- procedure {:checksum "10"} Other(y: int);
- requires 0 <= y;
- implementation {:id "Other"} {:checksum "11"} Other(y: int)
- {
- }
-
-
-
-procedure {:checksum "20"} Posty() returns (z: int);
- ensures 2 <= z; // error: postcondition violation
-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
-{
- var t: int;
- t := 20;
- if (t < z) {
- assert true; // this is a new assert
- } else { // the postcondition violation occurs on this 'else' branch
- }
-}
-
- procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
- implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
- {
- assert u != 53; // error
- }
-
-procedure {:checksum "40"} NoChangeAndCorrect();
-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{
+assert x < 20 || 10 <= x; // always true
+
+ assert x < 10; // error
+ call Other(x); // error: precondition violation
+ assert x == 7; // error: this is a new error in v1
+}
+
+
+ procedure {:checksum "10"} Other(y: int);
+ requires 0 <= y;
+ implementation {:id "Other"} {:checksum "11"} Other(y: int)
+ {
+ }
+
+
+
+procedure {:checksum "20"} Posty() returns (z: int);
+ ensures 2 <= z; // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+ var t: int;
+ t := 20;
+ if (t < z) {
+ assert true; // this is a new assert
+ } else { // the postcondition violation occurs on this 'else' branch
+ }
+}
+
+ procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+ implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+ {
+ assert u != 53; // error
+ }
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 16:11:40 +0000