diff options
| author |  qadeer <unknown> | 2010-02-16 05:07:46 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-02-16 05:07:46 +0000 |
| commit | 717eaee0063074b804098d3cfd44a7a3f822b064 (patch) | |
| tree | 5ca65ed1265ed238195ad25476c9ab506d5a8360 | |
| parent | f1d626d71fef69995f34daae4341473d597f5d27 (diff) | |
Implemented block coalescing invoked right after type checking.
Controlled by the option /coalesceBlocks (default is to perform the optimization).
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 5 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 24 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.ssc | 78 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 2 | ||||
| -rw-r--r-- | Test/aitest1/Answer | 90 | ||||
| -rw-r--r-- | Test/aitest1/Linear4.bpl | 4 | ||||
| -rw-r--r-- | Test/aitest1/Linear5.bpl | 8 | ||||
| -rw-r--r-- | Test/aitest9/answer | 2 | ||||
| -rw-r--r-- | Test/inline/Answer | 41 | ||||
| -rw-r--r-- | Test/livevars/Answer | 178 | ||||
| -rw-r--r-- | Test/test2/Answer | 8 |
11 files changed, 151 insertions, 289 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 035879ec..7b22d6fe 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -420,6 +420,11 @@ namespace Microsoft.Boogie // Eliminate dead variables
Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ // Coalesce blocks
+ if (CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
// Inline
List<Declaration!>! TopLevelDeclarations = program.TopLevelDeclarations;
if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index bd54d624..2dd85a65 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -162,7 +162,8 @@ namespace Microsoft.Boogie public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set
public bool RemoveEmptyBlocks = true;
-
+ public bool CoalesceBlocks = true;
+
[Rep] public ProverFactory TheProverFactory;
public string ProverName;
[Peer] public List<string!>! ProverOptions = new List<string!>();
@@ -842,6 +843,25 @@ namespace Microsoft.Boogie }
break;
+ case "-coalesceBlocks":
+ case "/coalesceBlocks":
+ if (ps.ConfirmArgumentCount(1))
+ {
+ switch (args[ps.i])
+ {
+ case "0":
+ CoalesceBlocks = false;
+ break;
+ case "1":
+ CoalesceBlocks = true;
+ break;
+ default:
+ ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
+ break;
+ }
+ }
+ break;
+
case "/DoomDebug":
vcVariety = VCVariety.Doomed;
useDoomDebug = true;
@@ -1846,6 +1866,8 @@ namespace Microsoft.Boogie 1 = perform live variable analysis (default)
/noVerify : skip VC generation and invocation of the theorem prover
/noRemoveEmptyBlocks : do not remove empty blocks during VC generation
+ /coalesceBlocks:<c> : 0 = do not coalesce blocks
+ 1 = coalesce blocks (default)
/vc:<variety> : n = nested block (default for non-/prover:z3),
m = nested block reach,
b = flat block, r = flat block reach,
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index c7b0c7d8..e60a59c3 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -45,8 +45,84 @@ namespace Microsoft.Boogie }
}
+ public class BlockCoalescer : StandardVisitor {
+ public static void CoalesceBlocks(Program! program) {
+ BlockCoalescer blockCoalescer = new BlockCoalescer();
+ blockCoalescer.Visit(program);
+ }
+
+ private static Set<Block!>! ComputeMultiPredecessorBlocks(Implementation !impl) {
+ Set<Block!> visitedBlocks = new Set<Block!>();
+ Set<Block!> multiPredBlocks = new Set<Block!>();
+ Stack<Block!> dfsStack = new Stack<Block!>();
+ dfsStack.Push(impl.Blocks[0]);
+ while (dfsStack.Count > 0) {
+ Block! b = dfsStack.Pop();
+ if (visitedBlocks.Contains(b)) {
+ multiPredBlocks.Add(b);
+ continue;
+ }
+ visitedBlocks.Add(b);
+ if (b.TransferCmd == null) continue;
+ if (b.TransferCmd is ReturnCmd) continue;
+ assert b.TransferCmd is GotoCmd;
+ GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+ if (gotoCmd.labelTargets == null) continue;
+ foreach (Block! succ in gotoCmd.labelTargets) {
+ dfsStack.Push(succ);
+ }
+ }
+ return multiPredBlocks;
+ }
+
+ public override Implementation! VisitImplementation(Implementation! impl) {
+ Set<Block!> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
+ Set<Block!> visitedBlocks = new Set<Block!>();
+ Set<Block!> removedBlocks = new Set<Block!>();
+ Stack<Block!> dfsStack = new Stack<Block!>();
+ dfsStack.Push(impl.Blocks[0]);
+ while (dfsStack.Count > 0) {
+ Block! b = dfsStack.Pop();
+ if (visitedBlocks.Contains(b)) continue;
+ visitedBlocks.Add(b);
+ if (b.TransferCmd == null) continue;
+ if (b.TransferCmd is ReturnCmd) continue;
+ assert b.TransferCmd is GotoCmd;
+ GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+ if (gotoCmd.labelTargets == null) continue;
+ if (gotoCmd.labelTargets.Length == 1) {
+ Block! succ = (!)gotoCmd.labelTargets[0];
+ if (!multiPredBlocks.Contains(succ)) {
+ foreach (Cmd! cmd in succ.Cmds) {
+ b.Cmds.Add(cmd);
+ }
+ b.TransferCmd = succ.TransferCmd;
+ if (!b.tok.IsValid && succ.tok.IsValid)
+ b.tok = succ.tok;
+ removedBlocks.Add(succ);
+ dfsStack.Push(b);
+ visitedBlocks.Remove(b);
+ continue;
+ }
+ }
+ foreach (Block! succ in gotoCmd.labelTargets) {
+ dfsStack.Push(succ);
+ }
+ }
+
+ List<Block!> newBlocks = new List<Block!>();
+ foreach (Block! b in impl.Blocks) {
+ if (!removedBlocks.Contains(b)) {
+ newBlocks.Add(b);
+ }
+ }
+ impl.Blocks = newBlocks;
+ return impl;
+ }
+ }
+
public class LiveVariableAnalysis {
- public static void ComputeLiveVariables(Program! program, Implementation! impl) {
+ public static void ComputeLiveVariables(Implementation! impl) {
Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis");
Graphing.Graph<Block> dag = new Graph<Block>();
dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index 24104fb4..a9b47222 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1754,7 +1754,7 @@ namespace VC #endregion
if (CommandLineOptions.Clo.LiveVariableAnalysis) {
- Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(program, impl);
+ Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
}
Convert2PassiveCmd(impl);
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index 4e5c8f27..ca9ff22a 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -121,29 +121,9 @@ implementation FooTooStepByStep() L0:
assume true;
i := 5;
- assume i == 5;
- goto L1;
-
- L1:
- assume i == 5;
i := 3 * i + 1;
- assume i == 16;
- goto L2;
-
- L2:
- assume i == 16;
i := 3 * (i + 1);
- assume 1 / 3 * i == 17;
- goto L3;
-
- L3:
- assume 1 / 3 * i == 17;
i := 1 + 3 * i;
- assume i == 154;
- goto L4;
-
- L4:
- assume i == 154;
i := (i + 1) * 3;
assume 1 / 3 * i == 155;
return;
@@ -256,13 +236,18 @@ implementation p() assume true;
assume x < y;
assume x + 1 <= y;
- goto B;
+ goto B, C;
B:
assume x + 1 <= y;
x := x * x;
assume true;
return;
+
+ C:
+ assume x + 1 <= y;
+ assume x + 1 <= y;
+ return;
}
@@ -285,25 +270,30 @@ implementation p() assume true;
assume 0 - 1 <= x;
assume -1 <= x;
- goto B;
+ goto B, E;
B:
assume -1 <= x;
assume x < y;
assume x + 1 <= y && -1 <= x;
- goto C;
+ goto C, E;
C:
assume x + 1 <= y && -1 <= x;
x := x * x;
assume 0 <= y;
- goto D;
+ goto D, E;
D:
assume 0 <= y;
x := y;
assume x == y && 0 <= y;
return;
+
+ E:
+ assume true;
+ assume true;
+ return;
}
@@ -405,54 +395,14 @@ implementation foo() A:
assume true;
n := 0;
- assume n == 0;
- goto B;
-
- B:
- assume n == 0;
j := 0;
- assume j == 0 && n == 0;
- goto C;
-
- C:
- assume j == 0 && n == 0;
i := j + 1;
- assume i == j + 1 && j == 0 && n == 0;
- goto D;
-
- D:
- assume i == j + 1 && j == 0 && n == 0;
i := i + 1;
- assume i == j + 2 && j == 0 && n == 0;
- goto E;
-
- E:
- assume i == j + 2 && j == 0 && n == 0;
i := i + 1;
- assume i == j + 3 && j == 0 && n == 0;
- goto F;
-
- F:
- assume i == j + 3 && j == 0 && n == 0;
i := i + 1;
- assume i == j + 4 && j == 0 && n == 0;
- goto G;
-
- G:
- assume i == j + 4 && j == 0 && n == 0;
i := i + 1;
- assume i == j + 5 && j == 0 && n == 0;
- goto H;
-
- H:
- assume i == j + 5 && j == 0 && n == 0;
j := j + 1;
assume i == j + 4 && j == 1 && n == 0;
- goto I;
-
- I:
- assume i == j + 4 && j == 1 && n == 0;
- assume i == j + 4 && j == 1 && n == 0;
return;
}
@@ -481,19 +431,9 @@ implementation foo() loop0: // cut point
assume 4 <= n && 0 <= i && j == i + 1;
assume j <= n;
- assume j <= n && 4 <= n && 0 <= i && j == i + 1;
- goto loop1;
-
- loop1:
- assume j <= n && 4 <= n && 0 <= i && j == i + 1;
i := i + 1;
- assume 1 <= i && j == i && j <= n && 4 <= n;
- goto loop2;
-
- loop2:
- assume j <= n && 4 <= n && 1 <= i && j == i;
j := j + 1;
- assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;
+ assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
goto loop0, exit;
exit:
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl index c8c4605c..2207debe 100644 --- a/Test/aitest1/Linear4.bpl +++ b/Test/aitest1/Linear4.bpl @@ -8,8 +8,10 @@ procedure p() {
A:
assume x < y;
- goto B;
+ goto B, C;
B:
x := x*x;
return;
+ C:
+ return;
}
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl index 4f04999c..199cb6f2 100644 --- a/Test/aitest1/Linear5.bpl +++ b/Test/aitest1/Linear5.bpl @@ -8,14 +8,16 @@ procedure p() {
A:
assume -1 <= x;
- goto B;
+ goto B, E;
B:
assume x < y;
- goto C;
+ goto C, E;
C:
x := x*x;
- goto D;
+ goto D, E;
D:
x := y;
return;
+ E:
+ return;
}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer index dd10a8b3..d6bba688 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -14,13 +14,11 @@ Execution trace: TestIntervals.bpl(5,5): anon0
TestIntervals.bpl(6,3): anon9_LoopHead
TestIntervals.bpl(6,3): anon9_LoopDone
- TestIntervals.bpl(11,5): anon2
TestIntervals.bpl(12,14): anon10_Then
TestIntervals.bpl(13,3): anon4
TestIntervals.bpl(13,14): anon11_Then
TestIntervals.bpl(14,3): anon6
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
- TestIntervals.bpl(21,3): Next
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/inline/Answer b/Test/inline/Answer index d5a12321..934b45ba 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -356,9 +356,6 @@ implementation recursivetest() inline$recursive$0$anon3_Else:
assume inline$recursive$0$x != 0;
- goto inline$recursive$0$anon2;
-
- inline$recursive$0$anon2:
goto inline$recursive$1$Entry;
inline$recursive$1$Entry:
@@ -375,9 +372,6 @@ implementation recursivetest() inline$recursive$1$anon3_Else:
assume inline$recursive$1$x != 0;
- goto inline$recursive$1$anon2;
-
- inline$recursive$1$anon2:
goto inline$recursive$2$Entry;
inline$recursive$2$Entry:
@@ -394,26 +388,23 @@ implementation recursivetest() inline$recursive$2$anon3_Else:
assume inline$recursive$2$x != 0;
- goto inline$recursive$2$anon2;
-
- inline$recursive$2$anon2:
call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
goto inline$recursive$2$Return;
inline$recursive$2$Return:
inline$recursive$1$k := inline$recursive$2$y;
- goto inline$recursive$1$anon2$1;
+ goto inline$recursive$1$anon3_Else$1;
- inline$recursive$1$anon2$1:
+ inline$recursive$1$anon3_Else$1:
inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
goto inline$recursive$1$Return;
inline$recursive$1$Return:
inline$recursive$0$k := inline$recursive$1$y;
- goto inline$recursive$0$anon2$1;
+ goto inline$recursive$0$anon3_Else$1;
- inline$recursive$0$anon2$1:
+ inline$recursive$0$anon3_Else$1:
inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
goto inline$recursive$0$Return;
@@ -453,9 +444,6 @@ implementation recursive(x: int) returns (y: int) anon3_Else:
assume x != 0;
- goto anon2;
-
- anon2:
goto inline$recursive$0$Entry;
inline$recursive$0$Entry:
@@ -472,9 +460,6 @@ implementation recursive(x: int) returns (y: int) inline$recursive$0$anon3_Else:
assume inline$recursive$0$x != 0;
- goto inline$recursive$0$anon2;
-
- inline$recursive$0$anon2:
goto inline$recursive$1$Entry;
inline$recursive$1$Entry:
@@ -491,9 +476,6 @@ implementation recursive(x: int) returns (y: int) inline$recursive$1$anon3_Else:
assume inline$recursive$1$x != 0;
- goto inline$recursive$1$anon2;
-
- inline$recursive$1$anon2:
goto inline$recursive$2$Entry;
inline$recursive$2$Entry:
@@ -510,34 +492,31 @@ implementation recursive(x: int) returns (y: int) inline$recursive$2$anon3_Else:
assume inline$recursive$2$x != 0;
- goto inline$recursive$2$anon2;
-
- inline$recursive$2$anon2:
call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
goto inline$recursive$2$Return;
inline$recursive$2$Return:
inline$recursive$1$k := inline$recursive$2$y;
- goto inline$recursive$1$anon2$1;
+ goto inline$recursive$1$anon3_Else$1;
- inline$recursive$1$anon2$1:
+ inline$recursive$1$anon3_Else$1:
inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
goto inline$recursive$1$Return;
inline$recursive$1$Return:
inline$recursive$0$k := inline$recursive$1$y;
- goto inline$recursive$0$anon2$1;
+ goto inline$recursive$0$anon3_Else$1;
- inline$recursive$0$anon2$1:
+ inline$recursive$0$anon3_Else$1:
inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
goto inline$recursive$0$Return;
inline$recursive$0$Return:
k := inline$recursive$0$y;
- goto anon2$1;
+ goto anon3_Else$1;
- anon2$1:
+ anon3_Else$1:
y := y + k;
return;
}
diff --git a/Test/livevars/Answer b/Test/livevars/Answer index d958205f..aaaee494 100644 --- a/Test/livevars/Answer +++ b/Test/livevars/Answer @@ -4,16 +4,12 @@ Execution trace: bla1.bpl(789,3): anon10_Then#1
bla1.bpl(794,3): anon2#1
bla1.bpl(822,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
- bla1.bpl(830,3): inline$storm_IoAllocateIrp$0$label_13#1
bla1.bpl(854,3): inline$storm_IoAllocateIrp$0$anon14_Then#1
bla1.bpl(859,3): inline$storm_IoAllocateIrp$0$anon2#1
bla1.bpl(879,3): inline$storm_IoAllocateIrp$0$anon16_Then#1
bla1.bpl(884,3): inline$storm_IoAllocateIrp$0$anon5#1
bla1.bpl(904,3): inline$storm_IoAllocateIrp$0$anon18_Then#1
bla1.bpl(909,3): inline$storm_IoAllocateIrp$0$anon8#1
- bla1.bpl(913,3): inline$storm_IoAllocateIrp$0$label_20#1
- bla1.bpl(917,3): inline$storm_IoAllocateIrp$0$label_21#1
- bla1.bpl(921,3): inline$storm_IoAllocateIrp$0$label_22#1
bla1.bpl(945,3): inline$storm_IoAllocateIrp$0$anon20_Then#1
bla1.bpl(950,3): inline$storm_IoAllocateIrp$0$anon11#1
bla1.bpl(981,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1
@@ -21,12 +17,6 @@ Execution trace: bla1.bpl(1018,3): inline$storm_IoAllocateIrp$0$anon22_Then#1
bla1.bpl(1023,3): inline$storm_IoAllocateIrp$0$anon13#1
bla1.bpl(1035,3): inline$storm_IoAllocateIrp$0$label_36#1
- bla1.bpl(1039,3): inline$storm_IoAllocateIrp$0$label_1#1
- bla1.bpl(1042,3): inline$storm_IoAllocateIrp$0$Return#1
- bla1.bpl(1046,3): label_6$1#1
- bla1.bpl(1049,3): label_9#1
- bla1.bpl(1053,3): label_10#1
- bla1.bpl(1068,3): inline$IoSetNextIrpStackLocation$0$label_3#1
bla1.bpl(1089,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1
bla1.bpl(1094,3): inline$IoSetNextIrpStackLocation$0$anon2#1
bla1.bpl(1112,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1
@@ -35,7 +25,6 @@ Execution trace: bla1.bpl(1162,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1
bla1.bpl(1197,3): anon12_Then#1
bla1.bpl(1202,3): anon5#1
- bla1.bpl(1209,3): label_20#1
bla1.bpl(1255,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1
bla1.bpl(1259,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1
bla1.bpl(1308,3): inline$I8xDeviceControl$0$anon3_Then#1
@@ -43,7 +32,6 @@ Execution trace: bla1.bpl(1348,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1
bla1.bpl(1376,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1
bla1.bpl(1408,3): inline$storm_IoSetCancelRoutine$0$label_8#1
- bla1.bpl(1412,3): inline$storm_IoSetCancelRoutine$0$label_16#1
bla1.bpl(1415,3): inline$storm_IoSetCancelRoutine$0$anon9_Else#1
bla1.bpl(1423,3): inline$storm_IoSetCancelRoutine$0$anon10_Then#1
bla1.bpl(1431,3): inline$storm_IoSetCancelRoutine$0$anon3#1
@@ -56,7 +44,6 @@ Execution trace: bla1.bpl(1532,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1
bla1.bpl(1542,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1
bla1.bpl(1566,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1
- bla1.bpl(1570,3): inline$I8xKeyboardGetSysButtonEvent$0$label_27#1
bla1.bpl(1579,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13#1
bla1.bpl(1586,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1
bla1.bpl(1619,3): inline$storm_IoCompleteRequest$0$label_6_false#1
@@ -65,7 +52,7 @@ Execution trace: bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1
bla1.bpl(1734,3): anon14_Then#1
- bla1.bpl(1747,3): label_24#1
+ bla1.bpl(1739,3): anon7#1
bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1
bla1.bpl(1801,3): inline$storm_IoCancelIrp$0$anon2#1
bla1.bpl(1812,3): inline$storm_IoCancelIrp$0$anon14_Else#1
@@ -76,9 +63,7 @@ Execution trace: bla1.bpl(1856,3): inline$storm_IoCancelIrp$0$anon8#1
bla1.bpl(1867,3): inline$storm_IoCancelIrp$0$anon18_Then#1
bla1.bpl(1872,3): inline$storm_IoCancelIrp$0$anon10#1
- bla1.bpl(1876,3): inline$storm_IoCancelIrp$0$label_13#1
bla1.bpl(1932,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1
- bla1.bpl(1938,3): inline$storm_IoAcquireCancelSpinLock$0$label_15#1
bla1.bpl(1947,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1
bla1.bpl(1955,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_Then#1
bla1.bpl(1965,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1
@@ -86,16 +71,10 @@ Execution trace: bla1.bpl(1981,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1
bla1.bpl(2005,3): inline$storm_IoCancelIrp$0$label_16_true#1
bla1.bpl(2023,3): inline$storm_IoCancelIrp$0$label_22_true#1
- bla1.bpl(2027,3): inline$storm_IoCancelIrp$0$label_24#1
bla1.bpl(2036,3): inline$storm_IoCancelIrp$0$label_25_false#1
bla1.bpl(2054,3): inline$storm_IoCancelIrp$0$label_1#1
- bla1.bpl(2057,3): inline$storm_IoCancelIrp$0$Return#1
- bla1.bpl(2060,3): inline$cancel$0$label_3$1#1
- bla1.bpl(2063,3): inline$cancel$0$label_1#1
- bla1.bpl(2066,3): inline$cancel$0$Return#1
- bla1.bpl(2069,3): label_24$1#1
bla1.bpl(2076,3): anon15_Then#1
- bla1.bpl(2086,3): label_1#1
+ bla1.bpl(2081,3): anon9#1
Boogie program verifier finished with 0 verified, 1 error
@@ -106,7 +85,6 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(846,3): anon22_Then#2
daytona_bug2_ioctl_example_2.bpl(851,3): anon2#2
daytona_bug2_ioctl_example_2.bpl(879,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2
- daytona_bug2_ioctl_example_2.bpl(887,3): inline$storm_IoAllocateIrp$0$label_13#2
daytona_bug2_ioctl_example_2.bpl(911,3): inline$storm_IoAllocateIrp$0$anon18_Then#2
daytona_bug2_ioctl_example_2.bpl(916,3): inline$storm_IoAllocateIrp$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(936,3): inline$storm_IoAllocateIrp$0$anon20_Then#2
@@ -114,9 +92,6 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(961,3): inline$storm_IoAllocateIrp$0$anon22_Then#2
daytona_bug2_ioctl_example_2.bpl(966,3): inline$storm_IoAllocateIrp$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(974,3): inline$storm_IoAllocateIrp$0$anon24_Else#2
- daytona_bug2_ioctl_example_2.bpl(978,3): inline$storm_IoAllocateIrp$0$anon10#2
- daytona_bug2_ioctl_example_2.bpl(982,3): inline$storm_IoAllocateIrp$0$label_21#2
- daytona_bug2_ioctl_example_2.bpl(986,3): inline$storm_IoAllocateIrp$0$label_22#2
daytona_bug2_ioctl_example_2.bpl(1010,3): inline$storm_IoAllocateIrp$0$anon25_Then#2
daytona_bug2_ioctl_example_2.bpl(1015,3): inline$storm_IoAllocateIrp$0$anon13#2
daytona_bug2_ioctl_example_2.bpl(1046,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2
@@ -125,11 +100,8 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(1090,3): inline$storm_IoAllocateIrp$0$anon28_Then#2
daytona_bug2_ioctl_example_2.bpl(1095,3): inline$storm_IoAllocateIrp$0$anon17#2
daytona_bug2_ioctl_example_2.bpl(1115,3): inline$storm_IoAllocateIrp$0$label_36#2
- daytona_bug2_ioctl_example_2.bpl(1119,3): inline$storm_IoAllocateIrp$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(1129,3): anon24_Else#2
daytona_bug2_ioctl_example_2.bpl(1144,3): anon25_Else#2
- daytona_bug2_ioctl_example_2.bpl(1148,3): anon6#2
- daytona_bug2_ioctl_example_2.bpl(1163,3): inline$IoSetNextIrpStackLocation$0$label_3#2
daytona_bug2_ioctl_example_2.bpl(1184,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2
daytona_bug2_ioctl_example_2.bpl(1189,3): inline$IoSetNextIrpStackLocation$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1207,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2
@@ -142,15 +114,11 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(1311,3): anon13#2
daytona_bug2_ioctl_example_2.bpl(1343,3): inline$myInitDriver$0$anon5_Then#2
daytona_bug2_ioctl_example_2.bpl(1348,3): inline$myInitDriver$0$anon2#2
- daytona_bug2_ioctl_example_2.bpl(1353,3): inline$myInitDriver$0$label_5#2
- daytona_bug2_ioctl_example_2.bpl(1359,3): inline$storm_KeInitializeSpinLock$0$Entry#2
daytona_bug2_ioctl_example_2.bpl(1383,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1388,3): inline$storm_KeInitializeSpinLock$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(1401,3): inline$myInitDriver$0$anon7_Else#2
daytona_bug2_ioctl_example_2.bpl(1416,3): inline$myInitDriver$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(1419,3): label_19$1#2
daytona_bug2_ioctl_example_2.bpl(1422,3): anon30_Else#2
- daytona_bug2_ioctl_example_2.bpl(1432,3): label_23#2
daytona_bug2_ioctl_example_2.bpl(1478,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1482,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2
daytona_bug2_ioctl_example_2.bpl(1495,3): inline$dispatch$0$anon4_Else#2
@@ -164,30 +132,23 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(1629,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2
daytona_bug2_ioctl_example_2.bpl(1642,3): inline$I8xDeviceControl$0$anon16_Else#2
daytona_bug2_ioctl_example_2.bpl(1655,3): inline$I8xDeviceControl$0$label_19_case_2#2
- daytona_bug2_ioctl_example_2.bpl(1668,3): inline$I8xKeyboardGetSysButtonEvent$0$start#2
daytona_bug2_ioctl_example_2.bpl(1719,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2
daytona_bug2_ioctl_example_2.bpl(1723,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2
daytona_bug2_ioctl_example_2.bpl(1736,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2
daytona_bug2_ioctl_example_2.bpl(1749,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2
daytona_bug2_ioctl_example_2.bpl(1757,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2
- daytona_bug2_ioctl_example_2.bpl(1762,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23#2
- daytona_bug2_ioctl_example_2.bpl(1768,3): inline$storm_KeAcquireSpinLock$0$Entry#2
daytona_bug2_ioctl_example_2.bpl(1811,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2
- daytona_bug2_ioctl_example_2.bpl(1815,3): inline$storm_KeAcquireSpinLock$0$anon1#2
daytona_bug2_ioctl_example_2.bpl(1835,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2
daytona_bug2_ioctl_example_2.bpl(1843,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2
- daytona_bug2_ioctl_example_2.bpl(1847,3): inline$storm_KeAcquireSpinLock$0$anon4#2
daytona_bug2_ioctl_example_2.bpl(1867,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2
daytona_bug2_ioctl_example_2.bpl(1872,3): inline$storm_KeAcquireSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(1883,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1888,3): inline$storm_KeAcquireSpinLock$0$anon9#2
daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(1906,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23$1#2
daytona_bug2_ioctl_example_2.bpl(1909,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
daytona_bug2_ioctl_example_2.bpl(1920,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
daytona_bug2_ioctl_example_2.bpl(1951,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2
daytona_bug2_ioctl_example_2.bpl(1991,3): inline$storm_IoSetCancelRoutine$0$label_8#2
- daytona_bug2_ioctl_example_2.bpl(1995,3): inline$storm_IoSetCancelRoutine$0$label_16#2
daytona_bug2_ioctl_example_2.bpl(2010,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2
daytona_bug2_ioctl_example_2.bpl(2014,3): inline$storm_IoSetCancelRoutine$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(2034,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2
@@ -195,14 +156,12 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(2050,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2055,3): inline$storm_IoSetCancelRoutine$0$anon10#2
daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(2072,3): inline$I8xKeyboardGetSysButtonEvent$0$label_62$1#2
daytona_bug2_ioctl_example_2.bpl(2075,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
daytona_bug2_ioctl_example_2.bpl(2200,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
daytona_bug2_ioctl_example_2.bpl(2208,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2
daytona_bug2_ioctl_example_2.bpl(2218,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2
daytona_bug2_ioctl_example_2.bpl(2246,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2
daytona_bug2_ioctl_example_2.bpl(2286,3): inline$storm_IoSetCancelRoutine$1$label_8#2
- daytona_bug2_ioctl_example_2.bpl(2290,3): inline$storm_IoSetCancelRoutine$1$label_16#2
daytona_bug2_ioctl_example_2.bpl(2293,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2
daytona_bug2_ioctl_example_2.bpl(2301,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2
daytona_bug2_ioctl_example_2.bpl(2311,3): inline$storm_IoSetCancelRoutine$1$anon5#2
@@ -212,18 +171,14 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(2348,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2353,3): inline$storm_IoSetCancelRoutine$1$anon10#2
daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2
- daytona_bug2_ioctl_example_2.bpl(2372,3): inline$I8xKeyboardGetSysButtonEvent$0$label_69$1#2
daytona_bug2_ioctl_example_2.bpl(2375,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
daytona_bug2_ioctl_example_2.bpl(2385,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
daytona_bug2_ioctl_example_2.bpl(2407,3): inline$storm_IoMarkIrpPending$2$label_6_false#2
daytona_bug2_ioctl_example_2.bpl(2447,3): inline$storm_IoMarkIrpPending$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2454,3): inline$storm_IoMarkIrpPending$2$Return#2
- daytona_bug2_ioctl_example_2.bpl(2457,3): inline$I8xKeyboardGetSysButtonEvent$0$label_73$1#2
daytona_bug2_ioctl_example_2.bpl(2460,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2
daytona_bug2_ioctl_example_2.bpl(2507,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2
- daytona_bug2_ioctl_example_2.bpl(2514,3): inline$storm_KeReleaseSpinLock$0$Entry#2
daytona_bug2_ioctl_example_2.bpl(2533,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2
- daytona_bug2_ioctl_example_2.bpl(2537,3): inline$storm_KeReleaseSpinLock$0$anon1#2
daytona_bug2_ioctl_example_2.bpl(2574,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(2581,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2
daytona_bug2_ioctl_example_2.bpl(2589,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2
@@ -231,7 +186,6 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(2610,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(2615,3): inline$storm_KeReleaseSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(2629,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59$1#2
daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
daytona_bug2_ioctl_example_2.bpl(2858,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51#2
daytona_bug2_ioctl_example_2.bpl(2865,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2
@@ -241,23 +195,18 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(2959,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
daytona_bug2_ioctl_example_2.bpl(2969,3): inline$storm_IoCompleteRequest$2$anon2#2
daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#2
- daytona_bug2_ioctl_example_2.bpl(2983,3): inline$I8xCompleteSysButtonIrp$0$label_6$1#2
daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
daytona_bug2_ioctl_example_2.bpl(3000,3): inline$I8xCompleteSysButtonIrp$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(3003,3): inline$I8xKeyboardGetSysButtonEvent$0$label_53$1#2
daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3169,3): inline$I8xKeyboardGetSysButtonEvent$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(3172,3): inline$I8xDeviceControl$0$label_24$1#2
daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2
daytona_bug2_ioctl_example_2.bpl(3644,3): inline$I8xDeviceControl$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3655,3): inline$I8xDeviceControl$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(3658,3): inline$dispatch$0$label_8$1#2
daytona_bug2_ioctl_example_2.bpl(3661,3): inline$dispatch$0$anon5_Else#2
daytona_bug2_ioctl_example_2.bpl(3682,3): inline$dispatch$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(3685,3): label_23$1#2
daytona_bug2_ioctl_example_2.bpl(3692,3): anon31_Then#2
- daytona_bug2_ioctl_example_2.bpl(3705,3): label_27#2
+ daytona_bug2_ioctl_example_2.bpl(3697,3): anon17#2
daytona_bug2_ioctl_example_2.bpl(3754,3): inline$storm_IoCancelIrp$0$anon23_Then#2
daytona_bug2_ioctl_example_2.bpl(3759,3): inline$storm_IoCancelIrp$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(3783,3): inline$storm_IoCancelIrp$0$anon25_Then#2
@@ -266,137 +215,85 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(3814,3): inline$storm_IoCancelIrp$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(3825,3): inline$storm_IoCancelIrp$0$anon29_Then#2
daytona_bug2_ioctl_example_2.bpl(3830,3): inline$storm_IoCancelIrp$0$anon10#2
- daytona_bug2_ioctl_example_2.bpl(3834,3): inline$storm_IoCancelIrp$0$label_13#2
daytona_bug2_ioctl_example_2.bpl(3890,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(3900,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
- daytona_bug2_ioctl_example_2.bpl(3904,3): inline$storm_IoAcquireCancelSpinLock$0$anon2#2
daytona_bug2_ioctl_example_2.bpl(3913,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
daytona_bug2_ioctl_example_2.bpl(3921,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
daytona_bug2_ioctl_example_2.bpl(3931,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3942,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(3947,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(3961,3): inline$storm_IoCancelIrp$0$label_13$1#2
daytona_bug2_ioctl_example_2.bpl(3964,3): inline$storm_IoCancelIrp$0$anon30_Else#2
daytona_bug2_ioctl_example_2.bpl(3982,3): inline$storm_IoCancelIrp$0$label_16_true#2
daytona_bug2_ioctl_example_2.bpl(4000,3): inline$storm_IoCancelIrp$0$label_22_true#2
daytona_bug2_ioctl_example_2.bpl(4008,3): inline$storm_IoCancelIrp$0$anon32_Else#2
- daytona_bug2_ioctl_example_2.bpl(4012,3): inline$storm_IoCancelIrp$0$anon16#2
daytona_bug2_ioctl_example_2.bpl(4021,3): inline$storm_IoCancelIrp$0$label_27_false#2
daytona_bug2_ioctl_example_2.bpl(4722,3): inline$storm_IoCancelIrp$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(4741,3): inline$storm_IoCancelIrp$0$Return#2
- daytona_bug2_ioctl_example_2.bpl(4744,3): inline$cancel$0$label_3$1#2
daytona_bug2_ioctl_example_2.bpl(4757,3): inline$cancel$0$anon2_Then#2
daytona_bug2_ioctl_example_2.bpl(4771,3): anon32_Then#2
- daytona_bug2_ioctl_example_2.bpl(4784,3): label_31#2
+ daytona_bug2_ioctl_example_2.bpl(4776,3): anon19#2
daytona_bug2_ioctl_example_2.bpl(4814,3): anon33_Then#2
- daytona_bug2_ioctl_example_2.bpl(4824,3): label_1#2
+ daytona_bug2_ioctl_example_2.bpl(4819,3): anon21#2
Boogie program verifier finished with 0 verified, 1 error
stack_overflow.bpl(97942,5): Error BP5001: This assertion might not hold.
Execution trace:
stack_overflow.bpl(1141,3): start#1
- stack_overflow.bpl(1163,3): label_8#1
- stack_overflow.bpl(1168,3): label_9#1
stack_overflow.bpl(1197,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
- stack_overflow.bpl(1205,3): inline$storm_IoAllocateIrp$0$label_13#1
- stack_overflow.bpl(1216,3): inline$storm_IoAllocateIrp$0$label_18#1
- stack_overflow.bpl(1221,3): inline$storm_IoAllocateIrp$0$label_19#1
stack_overflow.bpl(1230,3): inline$storm_IoAllocateIrp$0$anon6_Else#1
- stack_overflow.bpl(1234,3): inline$storm_IoAllocateIrp$0$anon1#1
- stack_overflow.bpl(1238,3): inline$storm_IoAllocateIrp$0$label_21#1
- stack_overflow.bpl(1242,3): inline$storm_IoAllocateIrp$0$label_22#1
stack_overflow.bpl(1283,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1
stack_overflow.bpl(1302,3): inline$storm_IoAllocateIrp$0$anon7_Else#1
stack_overflow.bpl(1321,3): inline$storm_IoAllocateIrp$0$anon8_Else#1
stack_overflow.bpl(1330,3): inline$storm_IoAllocateIrp$0$anon5#1
stack_overflow.bpl(1350,3): inline$storm_IoAllocateIrp$0$label_36#1
- stack_overflow.bpl(1354,3): inline$storm_IoAllocateIrp$0$label_1#1
stack_overflow.bpl(1364,3): anon10_Else#1
stack_overflow.bpl(1379,3): anon11_Else#1
- stack_overflow.bpl(1383,3): anon3#1
stack_overflow.bpl(1418,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1
stack_overflow.bpl(1424,3): inline$IoSetNextIrpStackLocation$0$label_5#1
- stack_overflow.bpl(1432,3): inline$IoSetNextIrpStackLocation$0$label_6#1
stack_overflow.bpl(1446,3): anon12_Else#1
stack_overflow.bpl(1486,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1
stack_overflow.bpl(1507,3): anon13_Else#1
- stack_overflow.bpl(1532,3): inline$myInitDriver$0$label_4#1
- stack_overflow.bpl(1541,3): inline$myInitDriver$0$label_6#1
- stack_overflow.bpl(1547,3): inline$storm_KeInitializeSpinLock$0$Entry#1
- stack_overflow.bpl(1555,3): inline$storm_KeInitializeSpinLock$0$label_3#1
stack_overflow.bpl(1569,3): inline$myInitDriver$0$anon8_Else#1
- stack_overflow.bpl(1577,3): inline$myInitDriver$0$label_9#1
- stack_overflow.bpl(1583,3): inline$storm_KeInitializeSpinLock$1$Entry#1
- stack_overflow.bpl(1591,3): inline$storm_KeInitializeSpinLock$1$label_3#1
stack_overflow.bpl(1605,3): inline$myInitDriver$0$anon9_Else#1
- stack_overflow.bpl(1613,3): inline$myInitDriver$0$label_12#1
- stack_overflow.bpl(1619,3): inline$storm_KeInitializeSpinLock$2$Entry#1
- stack_overflow.bpl(1627,3): inline$storm_KeInitializeSpinLock$2$label_3#1
stack_overflow.bpl(1641,3): inline$myInitDriver$0$anon10_Else#1
- stack_overflow.bpl(1649,3): inline$myInitDriver$0$label_15#1
- stack_overflow.bpl(1655,3): inline$storm_KeInitializeSpinLock$3$Entry#1
- stack_overflow.bpl(1663,3): inline$storm_KeInitializeSpinLock$3$label_3#1
stack_overflow.bpl(1677,3): inline$myInitDriver$0$anon11_Else#1
stack_overflow.bpl(1704,3): inline$myInitDriver$0$Return#1
- stack_overflow.bpl(1707,3): label_23$1#1
stack_overflow.bpl(1710,3): anon14_Else#1
- stack_overflow.bpl(1729,3): inline$storm_thread_dispatch$0$start#1
stack_overflow.bpl(1773,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1
stack_overflow.bpl(1794,3): inline$storm_thread_dispatch$0$anon4_Else#1
- stack_overflow.bpl(1827,3): inline$BDLPnP$0$label_6#1
stack_overflow.bpl(1877,3): inline$BDLPnP$0$anon54_Else#1
stack_overflow.bpl(1891,3): inline$BDLPnP$0$label_16_true#1
- stack_overflow.bpl(1895,3): inline$BDLPnP$0$label_20#1
- stack_overflow.bpl(1899,3): inline$BDLPnP$0$label_21#1
- stack_overflow.bpl(1903,3): inline$BDLPnP$0$label_22#1
stack_overflow.bpl(1935,3): inline$BDLPnP$0$anon55_Else#1
stack_overflow.bpl(1949,3): inline$BDLPnP$0$label_26_true#1
- stack_overflow.bpl(1953,3): inline$BDLPnP$0$label_30#1
- stack_overflow.bpl(1957,3): inline$BDLPnP$0$label_31#1
- stack_overflow.bpl(1961,3): inline$BDLPnP$0$label_32#1
stack_overflow.bpl(1993,3): inline$BDLPnP$0$anon56_Else#1
stack_overflow.bpl(2007,3): inline$BDLPnP$0$label_36_true#1
stack_overflow.bpl(2052,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(2073,3): inline$BDLPnP$0$anon57_Else#1
- stack_overflow.bpl(2083,3): inline$BDLPnP$0$label_43#1
stack_overflow.bpl(2100,3): inline$BDLPnP$0$label_44_true#1
stack_overflow.bpl(2109,3): inline$BDLPnP$0$label_47#1
stack_overflow.bpl(2113,3): inline$BDLPnP$0$anon58_Else#1
stack_overflow.bpl(2127,3): inline$BDLPnP$0$label_51_false#1
stack_overflow.bpl(77682,3): inline$BDLPnP$0$label_52_case_1#1
- stack_overflow.bpl(77695,3): inline$BDLPnPStart$0$start#1
stack_overflow.bpl(77742,3): inline$BDLPnPStart$0$anon36_Else#1
stack_overflow.bpl(77756,3): inline$BDLPnPStart$0$label_11_true#1
- stack_overflow.bpl(77760,3): inline$BDLPnPStart$0$label_15#1
- stack_overflow.bpl(77764,3): inline$BDLPnPStart$0$label_16#1
- stack_overflow.bpl(77768,3): inline$BDLPnPStart$0$label_17#1
stack_overflow.bpl(77800,3): inline$BDLPnPStart$0$anon37_Else#1
stack_overflow.bpl(77814,3): inline$BDLPnPStart$0$label_21_true#1
- stack_overflow.bpl(77818,3): inline$BDLPnPStart$0$label_25#1
- stack_overflow.bpl(77822,3): inline$BDLPnPStart$0$label_26#1
- stack_overflow.bpl(77826,3): inline$BDLPnPStart$0$label_27#1
stack_overflow.bpl(77858,3): inline$BDLPnPStart$0$anon38_Else#1
stack_overflow.bpl(77872,3): inline$BDLPnPStart$0$label_31_true#1
- stack_overflow.bpl(77886,3): inline$BDLCallLowerLevelDriverAndWait$0$start#1
+ stack_overflow.bpl(77879,3): inline$BDLPnPStart$0$label_32#1
stack_overflow.bpl(77951,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1
stack_overflow.bpl(77972,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1
stack_overflow.bpl(78013,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1
stack_overflow.bpl(78032,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1
stack_overflow.bpl(78060,3): inline$IoCopyCurrentIrpStackLocationToNext$0$Return#1
- stack_overflow.bpl(78063,3): inline$BDLCallLowerLevelDriverAndWait$0$label_6$1#1
stack_overflow.bpl(78066,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1
- stack_overflow.bpl(78086,3): inline$storm_KeInitializeEvent$0$label_3#1
stack_overflow.bpl(78100,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1
stack_overflow.bpl(78128,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1
stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1
- stack_overflow.bpl(78170,3): inline$IoGetNextIrpStackLocation$2$Entry#1
- stack_overflow.bpl(78174,3): inline$IoGetNextIrpStackLocation$2$start#1
- stack_overflow.bpl(78178,3): inline$IoGetNextIrpStackLocation$2$label_3#1
stack_overflow.bpl(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1
- stack_overflow.bpl(78247,3): inline$BDLCallLowerLevelDriverAndWait$0$label_12$1#1
stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
stack_overflow.bpl(78311,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1
@@ -404,37 +301,24 @@ Execution trace: stack_overflow.bpl(83288,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1
stack_overflow.bpl(83333,3): inline$storm_IoCallDriver$1$label_9_false#1
stack_overflow.bpl(83372,3): inline$storm_IoCallDriver$1$label_10#1
- stack_overflow.bpl(83375,3): inline$IoSetNextIrpStackLocation$2$Entry#1
- stack_overflow.bpl(83379,3): inline$IoSetNextIrpStackLocation$2$start#1
- stack_overflow.bpl(83383,3): inline$IoSetNextIrpStackLocation$2$label_3#1
stack_overflow.bpl(83403,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(83409,3): inline$IoSetNextIrpStackLocation$2$label_5#1
- stack_overflow.bpl(83417,3): inline$IoSetNextIrpStackLocation$2$label_6#1
stack_overflow.bpl(83431,3): inline$storm_IoCallDriver$1$anon11_Else#1
stack_overflow.bpl(83471,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1
stack_overflow.bpl(83492,3): inline$storm_IoCallDriver$1$anon13_Else#1
- stack_overflow.bpl(83505,3): inline$storm_IoCallDriver$1$label_23#1
stack_overflow.bpl(85859,3): inline$storm_IoCallDriver$1$label_27_case_1#1
stack_overflow.bpl(85929,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1
stack_overflow.bpl(85950,3): inline$CallCompletionRoutine$3$anon10_Else#1
stack_overflow.bpl(86007,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1
stack_overflow.bpl(86028,3): inline$CallCompletionRoutine$3$anon11_Else#1
stack_overflow.bpl(86045,3): inline$CallCompletionRoutine$3$label_18_true#1
- stack_overflow.bpl(86049,3): inline$CallCompletionRoutine$3$label_19#1
stack_overflow.bpl(87162,3): inline$CallCompletionRoutine$3$label_20_icall_2#1
- stack_overflow.bpl(87173,3): inline$BDLDevicePowerIoCompletion$3$start#1
stack_overflow.bpl(87239,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1
stack_overflow.bpl(87262,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1
stack_overflow.bpl(87307,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1
stack_overflow.bpl(87321,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1
- stack_overflow.bpl(87325,3): inline$BDLDevicePowerIoCompletion$3$label_24#1
- stack_overflow.bpl(87329,3): inline$BDLDevicePowerIoCompletion$3$label_25#1
- stack_overflow.bpl(87333,3): inline$BDLDevicePowerIoCompletion$3$label_26#1
stack_overflow.bpl(87365,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1
stack_overflow.bpl(87379,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1
- stack_overflow.bpl(87383,3): inline$BDLDevicePowerIoCompletion$3$label_34#1
- stack_overflow.bpl(87387,3): inline$BDLDevicePowerIoCompletion$3$label_35#1
- stack_overflow.bpl(87391,3): inline$BDLDevicePowerIoCompletion$3$label_36#1
stack_overflow.bpl(87423,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1
stack_overflow.bpl(87437,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1
stack_overflow.bpl(87452,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1
@@ -442,14 +326,8 @@ Execution trace: stack_overflow.bpl(87527,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1
stack_overflow.bpl(87555,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1
stack_overflow.bpl(87569,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1
- stack_overflow.bpl(87573,3): inline$BDLDevicePowerIoCompletion$3$label_66#1
- stack_overflow.bpl(87577,3): inline$BDLDevicePowerIoCompletion$3$label_67#1
- stack_overflow.bpl(87581,3): inline$BDLDevicePowerIoCompletion$3$label_68#1
stack_overflow.bpl(87613,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1
stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
- stack_overflow.bpl(87631,3): inline$BDLDevicePowerIoCompletion$3$label_76#1
- stack_overflow.bpl(87635,3): inline$BDLDevicePowerIoCompletion$3$label_77#1
- stack_overflow.bpl(87639,3): inline$BDLDevicePowerIoCompletion$3$label_78#1
stack_overflow.bpl(87671,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
stack_overflow.bpl(87685,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
@@ -458,103 +336,63 @@ Execution trace: stack_overflow.bpl(87738,3): inline$storm_IoCompleteRequest$7$label_6_false#1
stack_overflow.bpl(87777,3): inline$storm_IoCompleteRequest$7$label_7#1
stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#1
- stack_overflow.bpl(87792,3): inline$BDLDevicePowerIoCompletion$3$label_92$1#1
stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
stack_overflow.bpl(87837,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1
stack_overflow.bpl(87851,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1
- stack_overflow.bpl(87855,3): inline$BDLDevicePowerIoCompletion$3$label_105#1
- stack_overflow.bpl(87859,3): inline$BDLDevicePowerIoCompletion$3$label_106#1
- stack_overflow.bpl(87863,3): inline$BDLDevicePowerIoCompletion$3$label_107#1
stack_overflow.bpl(87895,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1
stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
- stack_overflow.bpl(87913,3): inline$BDLDevicePowerIoCompletion$3$label_115#1
- stack_overflow.bpl(87917,3): inline$BDLDevicePowerIoCompletion$3$label_116#1
- stack_overflow.bpl(87921,3): inline$BDLDevicePowerIoCompletion$3$label_117#1
stack_overflow.bpl(87953,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
stack_overflow.bpl(87967,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1
- stack_overflow.bpl(88043,3): inline$CallCompletionRoutine$3$label_20_icall_2$1#1
stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1
stack_overflow.bpl(88146,3): inline$CallCompletionRoutine$3$label_20_icall_return#1
- stack_overflow.bpl(88149,3): inline$CallCompletionRoutine$3$label_23#1
- stack_overflow.bpl(88153,3): inline$CallCompletionRoutine$3$label_24#1
stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1
- stack_overflow.bpl(88164,3): inline$CallCompletionRoutine$3$label_25#1
stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1
- stack_overflow.bpl(88187,3): inline$storm_IoCallDriver$1$label_39$1#1
stack_overflow.bpl(88190,3): inline$storm_IoCallDriver$1$anon15_Else#1
stack_overflow.bpl(88218,3): inline$storm_IoCallDriver$1$label_36#1
stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#1
- stack_overflow.bpl(88241,3): inline$storm_PoCallDriver$0$label_3$1#1
stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1
stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1
- stack_overflow.bpl(88266,3): inline$BDLCallLowerLevelDriverAndWait$0$label_25$1#1
stack_overflow.bpl(88269,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1
stack_overflow.bpl(88283,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1
stack_overflow.bpl(88441,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1
- stack_overflow.bpl(88445,3): inline$BDLCallLowerLevelDriverAndWait$0$label_1#1
stack_overflow.bpl(88477,3): inline$BDLCallLowerLevelDriverAndWait$0$Return#1
- stack_overflow.bpl(88481,3): inline$BDLPnPStart$0$label_32$1#1
stack_overflow.bpl(88484,3): inline$BDLPnPStart$0$anon39_Else#1
stack_overflow.bpl(88675,3): inline$BDLPnPStart$0$label_37_true#1
stack_overflow.bpl(88987,3): inline$BDLPnPStart$0$label_51_true#1
stack_overflow.bpl(89015,3): inline$BDLPnPStart$0$anon41_Else#1
stack_overflow.bpl(89029,3): inline$BDLPnPStart$0$label_56_true#1
- stack_overflow.bpl(89033,3): inline$BDLPnPStart$0$label_60#1
- stack_overflow.bpl(89037,3): inline$BDLPnPStart$0$label_61#1
- stack_overflow.bpl(89041,3): inline$BDLPnPStart$0$label_62#1
stack_overflow.bpl(89073,3): inline$BDLPnPStart$0$anon42_Else#1
stack_overflow.bpl(89087,3): inline$BDLPnPStart$0$label_66_true#1
- stack_overflow.bpl(89091,3): inline$BDLPnPStart$0$label_70#1
- stack_overflow.bpl(89095,3): inline$BDLPnPStart$0$label_71#1
- stack_overflow.bpl(89099,3): inline$BDLPnPStart$0$label_72#1
stack_overflow.bpl(89131,3): inline$BDLPnPStart$0$anon43_Else#1
stack_overflow.bpl(89145,3): inline$BDLPnPStart$0$label_76_true#1
stack_overflow.bpl(89176,3): inline$BDLPnPStart$0$anon44_Else#1
stack_overflow.bpl(89190,3): inline$BDLPnPStart$0$label_81_true#1
- stack_overflow.bpl(89194,3): inline$BDLPnPStart$0$label_85#1
- stack_overflow.bpl(89198,3): inline$BDLPnPStart$0$label_86#1
- stack_overflow.bpl(89202,3): inline$BDLPnPStart$0$label_87#1
stack_overflow.bpl(89234,3): inline$BDLPnPStart$0$anon45_Else#1
stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1
- stack_overflow.bpl(89252,3): inline$BDLPnPStart$0$label_95#1
- stack_overflow.bpl(89256,3): inline$BDLPnPStart$0$label_96#1
- stack_overflow.bpl(89260,3): inline$BDLPnPStart$0$label_97#1
stack_overflow.bpl(89292,3): inline$BDLPnPStart$0$anon46_Else#1
stack_overflow.bpl(89306,3): inline$BDLPnPStart$0$label_101_true#1
stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#1
- stack_overflow.bpl(89365,3): inline$BDLPnP$0$label_113$1#1
stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1
stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1
stack_overflow.bpl(94593,3): inline$BDLPnP$0$label_139_true#1
stack_overflow.bpl(94622,3): inline$storm_IoCompleteRequest$57$label_6_true#1
stack_overflow.bpl(94630,3): inline$storm_IoCompleteRequest$57$anon3_Else#1
- stack_overflow.bpl(94634,3): inline$storm_IoCompleteRequest$57$anon1#1
stack_overflow.bpl(94642,3): inline$storm_IoCompleteRequest$57$label_9_false#1
stack_overflow.bpl(94662,3): inline$storm_IoCompleteRequest$57$label_1#1
stack_overflow.bpl(94669,3): inline$storm_IoCompleteRequest$57$Return#1
- stack_overflow.bpl(94672,3): inline$BDLPnP$0$label_142$1#1
stack_overflow.bpl(94710,3): inline$BDLPnP$0$anon75_Then#1
stack_overflow.bpl(95206,3): inline$BDLPnP$0$Return#1
- stack_overflow.bpl(95209,3): inline$storm_thread_dispatch$0$label_8$1#1
stack_overflow.bpl(95226,3): inline$storm_thread_dispatch$0$anon5_Then#1
stack_overflow.bpl(95234,3): inline$storm_thread_dispatch$0$Return#1
- stack_overflow.bpl(95237,3): label_29$1#1
- stack_overflow.bpl(95240,3): label_32#1
- stack_overflow.bpl(95243,3): inline$storm_thread_cancel$0$Entry#1
- stack_overflow.bpl(95247,3): inline$storm_thread_cancel$0$start#1
- stack_overflow.bpl(95276,3): inline$storm_IoCancelIrp$0$label_8#1
- stack_overflow.bpl(95282,3): inline$storm_IoCancelIrp$0$label_9#1
stack_overflow.bpl(95294,3): inline$storm_IoCancelIrp$0$anon9_Then#1
stack_overflow.bpl(95299,3): inline$storm_IoCancelIrp$0$anon1#1
- stack_overflow.bpl(95303,3): inline$storm_IoCancelIrp$0$label_13#1
stack_overflow.bpl(95356,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1
stack_overflow.bpl(95518,3): inline$storm_IoCancelIrp$0$anon10_Then#1
stack_overflow.bpl(95539,3): inline$storm_thread_cancel$0$anon2_Then#1
- stack_overflow.bpl(95555,3): inline$storm_thread_dpc$0$start#1
- stack_overflow.bpl(95578,3): inline$storm_thread_completion$0$start#1
+ stack_overflow.bpl(95543,3): inline$storm_thread_cancel$0$Return#1
stack_overflow.bpl(97931,3): inline$storm_thread_completion$0$anon4_Then#1
- stack_overflow.bpl(97941,3): label_1#1
+ stack_overflow.bpl(97935,3): inline$storm_thread_completion$0$Return#1
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test2/Answer b/Test/test2/Answer index dd1d944d..1e5a0d5f 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -250,22 +250,22 @@ Where.bpl(111,3): Error BP5001: This assertion might not hold. Execution trace:
Where.bpl(102,5): anon0
Where.bpl(104,3): anon3_LoopHead
- Where.bpl(110,3): anon2
+ Where.bpl(104,3): anon3_LoopDone
Where.bpl(128,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(121,5): anon0
Where.bpl(122,3): anon3_LoopHead
- Where.bpl(125,3): anon2
+ Where.bpl(122,3): anon3_LoopDone
Where.bpl(145,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(138,5): anon0
Where.bpl(139,3): anon3_LoopHead
- Where.bpl(142,3): anon2
+ Where.bpl(139,3): anon3_LoopDone
Where.bpl(162,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(155,5): anon0
Where.bpl(156,3): anon3_LoopHead
- Where.bpl(159,3): anon2
+ Where.bpl(156,3): anon3_LoopDone
Boogie program verifier finished with 2 verified, 9 errors
|