From cb4d41266301c26b9c863561df57ffd30ae0ec6f Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 18 Oct 2014 00:10:25 +0200 Subject: Made it produce more trace output for the verification result caching. --- Source/Core/CommandLineOptions.cs | 7 +- Source/ExecutionEngine/ExecutionEngine.cs | 36 +- Source/ExecutionEngine/VerificationResultCache.cs | 39 +- Source/VCGeneration/ConditionGeneration.cs | 84 +++- Test/snapshots/runtest.snapshot | 2 +- Test/snapshots/runtest.snapshot.expect | 547 ++++++++++++++++++++++ 6 files changed, 677 insertions(+), 38 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index c49b3b3c..eca410b2 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -389,7 +389,7 @@ namespace Microsoft.Boogie { public bool Trace = false; public bool TraceTimes = false; public bool TraceProofObligations = false; - public bool TraceCaching = false; + public int TraceCaching = 0; public bool NoResolve = false; public bool NoTypecheck = false; public bool OverlookBoogieTypeErrors = false; @@ -1324,6 +1324,10 @@ namespace Microsoft.Boogie { case "verifySnapshots": ps.GetNumericArgument(ref VerifySnapshots, 3); + return true; + + case "traceCaching": + ps.GetNumericArgument(ref TraceCaching, 4); return true; case "useSmtOutputFormat": { @@ -1393,7 +1397,6 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("wait", ref Wait) || ps.CheckBooleanFlag("trace", ref Trace) || ps.CheckBooleanFlag("traceTimes", ref TraceTimes) || - ps.CheckBooleanFlag("traceCaching", ref TraceCaching) || ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) || ps.CheckBooleanFlag("noResolve", ref NoResolve) || ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) || diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e0c3e006..76caa5d3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1017,11 +1017,8 @@ namespace Microsoft.Boogie programCache.Set(programId, program, policy); } - if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching) + if (0 <= CommandLineOptions.Clo.VerifySnapshots && 2 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - var end = DateTime.UtcNow; if (TimePerRequest.Count == 0) { @@ -1030,20 +1027,37 @@ namespace Microsoft.Boogie TimePerRequest[requestId] = end.Subtract(start); StatisticsPerRequest[requestId] = stats; - Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true)); + var printTimes = 3 <= CommandLineOptions.Clo.TraceCaching; + + Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes)); Console.Out.WriteLine("Statistics per request as CSV:"); - Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified"); + if (printTimes) + { + Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified"); + } + else + { + Console.Out.WriteLine("Request ID, Error, Inconclusive, Out of Memory, Timeout, Verified"); + } foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) { var s = StatisticsPerRequest[kv.Key]; - Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount); + if (printTimes) + { + Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount); + } + else + { + Console.Out.WriteLine("{0,-19}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount); + } } - Console.Out.WriteLine(""); - Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds); - - Console.Out.WriteLine(""); + if (printTimes) + { + Console.Out.WriteLine(""); + Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds); + } } #endregion diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index ba995cba..268ab9bd 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -39,7 +39,7 @@ namespace Microsoft.Boogie var wr = new StringWriter(); if (runs.Any()) { - wr.WriteLine("Cached verification result injector statistics as CSV:"); + wr.WriteLine("\nCached verification result injector statistics as CSV:"); if (printTime) { wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations"); @@ -269,7 +269,30 @@ namespace Microsoft.Boogie var assumed = new AssignCmd(Token.NoToken, new List { lhs }, new List { rhs }); after.Add(assumed); } + node.ExtendDesugaring(before, beforePrecondtionCheck, after); + if (1 <= CommandLineOptions.Clo.TraceCaching) + { + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + Console.Out.WriteLine("\nFor call to {0} in {1}:", node.Proc.Name, currentImplementation.Name); + foreach (var b in before) + { + Console.Out.Write("+ Added before: "); + b.Emit(tokTxtWr, 0); + } + foreach (var b in beforePrecondtionCheck) + { + Console.Out.Write("+ Added before precondition check: "); + b.Emit(tokTxtWr, 0); + } + foreach (var a in after) + { + Console.Out.Write("+ Added after: "); + a.Emit(tokTxtWr, 0); + } + } + } } return result; @@ -295,12 +318,9 @@ namespace Microsoft.Boogie } var end = DateTime.UtcNow; - if (CommandLineOptions.Clo.TraceCaching) + if (3 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - Console.Out.WriteLine(""); + Console.Out.WriteLine("\nCollected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); } } @@ -346,12 +366,9 @@ namespace Microsoft.Boogie dc.VisitProgram(program); var end = DateTime.UtcNow; - if (CommandLineOptions.Clo.TraceCaching) + if (3 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - Console.Out.WriteLine(""); + Console.Out.WriteLine("\nCollected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 7fb12589..6fa26967 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1336,12 +1336,24 @@ namespace VC { Dictionary r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo); var end = DateTime.UtcNow; - if (CommandLineOptions.Clo.TraceCaching) + if (3 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - Console.Out.WriteLine(""); + Console.Out.WriteLine("\nTurned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds); + + } + + if (2 <= CommandLineOptions.Clo.TraceCaching) + { + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + var pd = CommandLineOptions.Clo.PrintDesugarings; + var pu = CommandLineOptions.Clo.PrintUnstructured; + CommandLineOptions.Clo.PrintDesugarings = true; + CommandLineOptions.Clo.PrintUnstructured = 1; + impl.Emit(tokTxtWr, 0); + CommandLineOptions.Clo.PrintDesugarings = pd; + CommandLineOptions.Clo.PrintUnstructured = pu; + } } currentTemporaryVariableForAssertions = null; @@ -1458,6 +1470,27 @@ namespace VC { return Substituter.SubstitutionFromHashtable(oldFrameMap); } + void TraceCachingTransformation(Cmd from, string message, Cmd to = null) + { + if (1 <= CommandLineOptions.Clo.TraceCaching) + { + Console.WriteLine(""); + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + from.Emit(tokTxtWr, 0); + Console.Write(message); + if (to != null) + { + to.Emit(tokTxtWr, 0); + } + else + { + Console.WriteLine(""); + } + } + } + } + /// /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc /// Meanwhile, record any information needed to later reconstruct a model view. @@ -1504,9 +1537,13 @@ namespace VC { && currentImplementation.HasCachedSnapshot && !currentImplementation.AnyErrorsInCachedSnapshot && currentImplementation.InjectedAssumptionVariables.Count == 1) - { } + { + TraceCachingTransformation(pc, "==> did nothing\n"); + } else if (relevantDoomedAssumpVars.Any()) - { } + { + TraceCachingTransformation(pc, "==> did nothing\n"); + } else if (currentImplementation != null && currentImplementation.HasCachedSnapshot && checksum != null @@ -1524,15 +1561,19 @@ namespace VC { ac.IncarnationMap[incarnation] = identExpr; passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy))); copy = identExpr; - passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr))); + var a = new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)); + passiveCmds.Add(a); + TraceCachingTransformation(pc, "== marked as partially verified ==> ", a); } else if (isTrue) { if (alwaysUseSubsumption) { // Turn it into an assume statement. - pc = new AssumeCmd(ac.tok, copy); - pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List(), pc.Attributes); + var a = new AssumeCmd(ac.tok, copy); + a.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List(), a.Attributes); + TraceCachingTransformation(pc, "== marked as fully verified ==> ", a); + pc = a; } dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never; } @@ -1547,8 +1588,10 @@ namespace VC { if (alwaysUseSubsumption) { // Turn it into an assume statement. - pc = new AssumeCmd(ac.tok, copy); - pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), pc.Attributes); + var a = new AssumeCmd(ac.tok, copy); + a.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), a.Attributes); + TraceCachingTransformation(pc, "== recycled error ==> ", a); + pc = a; } dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never; if (dropCmd || alwaysUseSubsumption) @@ -1556,6 +1599,10 @@ namespace VC { currentImplementation.AddRecycledFailingAssertion(ac); } } + else + { + TraceCachingTransformation(pc, "==> did nothing\n"); + } } else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") @@ -1571,6 +1618,11 @@ namespace VC { if (!isTrue) { copy = LiteralExpr.Imp(assmVars, copy); + TraceCachingTransformation(pc, "==> marked as partially verified\n"); + } + else + { + TraceCachingTransformation(pc, "==> marked as full verified\n"); } } else @@ -1583,6 +1635,10 @@ namespace VC { { passiveCmds.Add(pc); } + else + { + TraceCachingTransformation(pc, "==> dropped\n"); + } } #endregion #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below] @@ -1664,7 +1720,9 @@ namespace VC { Expr incarnation; if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation)) { - passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation))); + var a = new AssumeCmd(c.tok, Expr.Not(incarnation)); + TraceCachingTransformation(assign, "== assumed negation of single assumption variable ==> ", a); + passiveCmds.Add(a); } } } diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index 04943c25..d5907196 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -errorTrace:0 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl > "%t" +// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 56e0aa7f..593ee2d8 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -1,162 +1,709 @@ + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold. + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold. + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 4 errors Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. + +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +==> did nothing + + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold. +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +==> did nothing + + Boogie program verifier finished with 2 verified, 2 errors Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +==> did nothing + + +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +==> did nothing + + Boogie program verifier finished with 2 verified, 1 error + +assert 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +==> did nothing + Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 1 verified, 1 error + +assert 2 != 2 /* checksum: 14-C1-28-03-D4-A3-E8-E9-0D-DF-F5-4A-B5-E9-BC-3F */ ; +==> did nothing + Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 1 verified, 1 error + +For call to P2 in P1: + +assert false /* checksum: D1-72-9A-D5-02-D4-C2-1C-72-57-E0-9B-63-83-FD-61 */ ; +==> did nothing + Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold. Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold. +assert 2 != 2 /* checksum: 80-D8-1C-F2-22-89-4E-46-9E-B6-B4-8E-71-D8-E1-7B */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors + +For call to P0 in P0: + +assert F0() /* checksum: D1-9A-AF-2B-D9-3C-97-D6-E1-5C-E1-33-99-55-01-42 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors + +For call to P0 in P0: ++ Added after: a##post##0 := a##post##0 && false; + +assert F0() /* checksum: 2D-F2-46-3A-8D-8E-C1-D6-F9-7D-25-C4-21-E9-A0-28 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors + +For call to P0 in P0: ++ Added before precondition check: assume {:precondition_previous_snapshot} F0(); + +assume {:precondition_previous_snapshot} F0(); +==> marked as full verified + + +assert F0() /* checksum: 2D-F2-46-3A-8D-8E-C1-D6-F9-7D-25-C4-21-E9-A0-28 */ ; +== marked as fully verified ==> assume {:verified_assertion} F0(); + +assert F0() /* checksum: 2D-F2-46-3A-8D-8E-C1-D6-F9-7D-25-C4-21-E9-A0-28 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors +assert G() /* checksum: 6F-4F-98-EE-0A-24-AE-77-E9-1F-47-90-5E-D1-AD-74 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +assert G() /* checksum: BF-E5-F1-9A-64-C1-5B-B7-45-00-F0-94-CA-6E-1E-AC */ ; +==> did nothing + Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path. Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold. Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 3 verified, 0 errors + +For call to P2 in P1: ++ Added after: a##post##0 := a##post##0 && false; + +assert false /* checksum: 15-08-03-72-EB-A5-47-46-57-90-24-B0-70-9D-3D-31 */ ; +==> did nothing + Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold. + +assert G() /* checksum: BF-E5-F1-9A-64-C1-5B-B7-45-00-F0-94-CA-6E-1E-AC */ ; +==> did nothing + Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path. Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold. Boogie program verifier finished with 2 verified, 2 errors +assert false /* checksum: 68-D1-81-97-87-FF-C5-55-21-B4-19-6E-9E-3B-A4-09 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +assert false /* checksum: 25-A1-AD-4D-EB-E0-89-92-B9-2C-F2-8C-50-9E-13-F8 */ ; +==> did nothing + Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert y == 0 /* checksum: 94-03-76-7A-91-FD-11-44-E2-49-32-50-5B-DB-56-A8 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added before: y##old##0 := y; ++ Added after: a##post##0 := a##post##0 && y##old##0 == y; + +a##post##0 := a##post##0 && y##old##0 == y; +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert y == 0 /* checksum: 94-03-76-7A-91-FD-11-44-E2-49-32-50-5B-DB-56-A8 */ ; +==> did nothing + Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert y < 0 /* checksum: 26-F9-F5-34-99-F6-84-ED-8A-39-A2-87-A0-91-55-98 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && y < z; + +a##post##0 := a##post##0 && y < z; +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert y < 0 /* checksum: 26-F9-F5-34-99-F6-84-ED-8A-39-A2-87-A0-91-55-98 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +assert 0 <= x /* checksum: 11-02-4B-47-F3-00-A3-7E-1B-2B-10-77-7F-BC-6F-98 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; ++ Added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; + +assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; +==> marked as full verified + + +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +a##post##0 := a##post##0 && 0 < call1formal#AT#r; +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert 0 <= x /* checksum: 11-02-4B-47-F3-00-A3-7E-1B-2B-10-77-7F-BC-6F-98 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +assert true /* checksum: 0B-95-06-ED-C6-73-4F-5C-E5-29-26-BB-18-39-FA-FC */ ; +==> did nothing + + +assert 0 <= x /* checksum: 11-02-4B-47-F3-00-A3-7E-1B-2B-10-77-7F-BC-6F-98 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true; ++ Added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r && true; + +assume {:precondition_previous_snapshot} 0 < call0formal#AT#n && true; +==> marked as full verified + + +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +a##post##0 := a##post##0 && 0 < call1formal#AT#r && true; +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert 0 <= x /* checksum: 11-02-4B-47-F3-00-A3-7E-1B-2B-10-77-7F-BC-6F-98 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +assert 0 <= x /* checksum: B1-53-93-E6-12-D0-01-C5-D6-F4-E8-65-49-9E-3F-E6 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; ++ Added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; + +assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; +==> marked as full verified + + +assert 0 < call0formal#AT#n /* checksum: 84-77-4F-21-82-94-59-A9-66-C3-77-B2-13-B8-C9-2A */ ; +==> did nothing + + +a##post##0 := a##post##0 && 0 < call1formal#AT#r; +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert 0 <= x /* checksum: B1-53-93-E6-12-D0-01-C5-D6-F4-E8-65-49-9E-3F-E6 */ ; +==> did nothing + Boogie program verifier finished with 1 verified, 0 errors + +assert 0 < call0formal#AT#n /* checksum: 80-3B-4F-44-75-E4-2D-86-E4-8B-F6-2F-5D-52-1F-25 */ ; +==> did nothing + + +assert 0 <= x /* checksum: 95-4E-4B-40-26-30-D7-F3-DD-63-7F-04-F1-12-F9-E9 */ ; +==> did nothing + Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold. Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold. Boogie program verifier finished with 0 verified, 1 error + +For call to N in M: ++ Added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n; ++ Added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r; + +assume {:precondition_previous_snapshot} 0 < n; +==> dropped + + +assert 0 < call0formal#AT#n /* checksum: 80-3B-4F-44-75-E4-2D-86-E4-8B-F6-2F-5D-52-1F-25 */ ; +== recycled error ==> assume {:recycled_failing_assertion} 0 < n; + +assert 0 <= x /* checksum: 95-4E-4B-40-26-30-D7-F3-DD-63-7F-04-F1-12-F9-E9 */ ; +== marked as partially verified ==> assume a##post##0#AT#0 ==> ##assertion#AT#0; Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold. Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold. Boogie program verifier finished with 0 verified, 1 error +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && false; + +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && false; + +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && F() && G(); + +a##post##0 := a##post##0 && F() && G(); +== assumed negation of single assumption variable ==> assume !a##post##0#AT#0; + +assert false /* checksum: 45-28-9E-B9-7D-00-88-8D-13-FA-31-27-A8-DA-FD-68 */ ; +==> did nothing + Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +==> did nothing + + +assert true /* checksum: 30-E0-21-77-66-D9-7F-0B-3C-12-29-6B-A8-3B-00-A5 */ ; +==> did nothing + + +assert false /* checksum: B5-48-47-B6-FB-21-97-C6-DF-18-E0-B4-E0-19-FD-35 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && false; + +For call to N in M: ++ Added after: a##post##1 := a##post##1 && false; + +assert true /* checksum: F7-FC-97-12-78-9F-88-2B-BF-B4-4F-35-55-71-AD-EA */ ; +== marked as fully verified ==> assume {:verified_assertion} true; + +assert true /* checksum: 30-E0-21-77-66-D9-7F-0B-3C-12-29-6B-A8-3B-00-A5 */ ; +== marked as partially verified ==> assume a##post##0#AT#0 ==> ##assertion#AT#0; + +assert false /* checksum: B5-48-47-B6-FB-21-97-C6-DF-18-E0-B4-E0-19-FD-35 */ ; +== marked as partially verified ==> assume a##post##0#AT#0 && a##post##1#AT#0 ==> ##assertion#AT#1; Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert F(0) == 1 /* checksum: 58-F6-BD-EA-70-FB-7A-78-A3-58-7A-11-49-BE-B1-D2 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +assert F(0) == 1 /* checksum: 32-BD-8D-95-77-41-39-3A-4C-8F-27-51-2F-F6-97-7A */ ; +==> did nothing + Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert true /* checksum: 17-6D-05-FB-27-8E-09-CB-76-67-1B-D1-AC-28-1E-BC */ ; +==> did nothing + + +assert false /* checksum: 3A-F2-06-60-5D-63-00-9C-7B-76-0A-81-C9-40-A4-8F */ ; +==> did nothing + + +assert true /* checksum: B6-DA-0F-69-58-5E-00-18-D7-B8-16-13-5A-2B-AA-EF */ ; +==> did nothing + + +assert x == 1 /* checksum: 8E-DA-C3-A4-92-2F-9B-29-8C-B4-61-B1-66-35-D7-99 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && false; + +For call to N in M: ++ Added after: a##post##1 := a##post##1 && false; + +For call to N in M: ++ Added after: a##post##2 := a##post##2 && false; + +assert true /* checksum: 17-6D-05-FB-27-8E-09-CB-76-67-1B-D1-AC-28-1E-BC */ ; +== marked as fully verified ==> assume {:verified_assertion} true; + +assert false /* checksum: 80-58-47-CB-BE-BA-FC-22-49-6B-79-1F-00-B0-76-C8 */ ; +==> did nothing + + +assert true /* checksum: 8C-AC-68-E0-D9-25-3C-E2-A1-47-07-CD-ED-9B-B8-8A */ ; +==> did nothing + + +assert x == 1 /* checksum: B4-68-64-D5-1B-10-5F-E3-FA-C7-B8-F7-D1-C5-45-2C */ ; +==> did nothing + Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold. Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 2 errors +assert 0 == 0 /* checksum: B1-21-7E-D6-6E-15-08-55-9F-FC-DD-C4-73-7C-FE-66 */ ; +==> did nothing + + +assert 1 != 1 /* checksum: 40-C2-E2-EC-B1-48-97-30-58-1B-D0-87-76-8D-5E-C9 */ ; +==> did nothing + + +assert 2 != 2 /* checksum: 18-79-6F-32-17-AC-69-D4-4D-E2-27-78-5D-13-E3-C6 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && false; + +For call to N in M: ++ Added after: a##post##1 := a##post##1 && false; + +assert 0 == 0 /* checksum: EB-9A-F3-AB-2C-6D-D5-85-C7-CA-03-01-F2-ED-12-D6 */ ; +==> did nothing + + +assert 1 != 1 /* checksum: DA-9B-89-CB-B7-20-E4-60-00-D9-C2-64-D5-7A-B2-39 */ ; +==> did nothing + + +assert 2 != 2 /* checksum: A8-A9-15-48-2F-DC-37-54-4D-12-CB-D8-39-07-DB-E6 */ ; +==> did nothing + Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold. Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 2 errors + +assert 2 == 2 /* checksum: E6-C5-48-63-99-F9-9F-0D-6D-A5-19-3D-76-A5-BE-6E */ ; +==> did nothing + + +assert 1 != 1 /* checksum: 7F-1D-5B-2B-B9-18-C2-12-DD-B9-E8-4E-C3-EC-5C-AC */ ; +==> did nothing + Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error + +For call to N in M: ++ Added before precondition check: assume {:precondition_previous_snapshot} 2 == 2; + +assume {:precondition_previous_snapshot} 2 == 2; +==> marked as full verified + + +assert 2 == 2 /* checksum: E6-C5-48-63-99-F9-9F-0D-6D-A5-19-3D-76-A5-BE-6E */ ; +== marked as fully verified ==> assume {:verified_assertion} 2 == 2; + +assert 1 != 1 /* checksum: 7F-1D-5B-2B-B9-18-C2-12-DD-B9-E8-4E-C3-EC-5C-AC */ ; +== recycled error ==> assume {:recycled_failing_assertion} 1 != 1; Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error + +assert 1 != 1 /* checksum: 7F-1D-5B-2B-B9-18-C2-12-DD-B9-E8-4E-C3-EC-5C-AC */ ; +==> did nothing + + +assert 2 != 2 /* checksum: 14-C1-28-03-D4-A3-E8-E9-0D-DF-F5-4A-B5-E9-BC-3F */ ; +==> did nothing + + +assert 3 != 3 /* checksum: 8E-F6-6B-B8-4C-24-97-50-0F-23-EA-73-D2-9E-3E-74 */ ; +==> did nothing + Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error + +For call to N in M: ++ Added after: a##post##0 := a##post##0 && 0 != 0; + +assert 1 != 1 /* checksum: 7F-1D-5B-2B-B9-18-C2-12-DD-B9-E8-4E-C3-EC-5C-AC */ ; +== marked as partially verified ==> assume a##post##0#AT#0 ==> ##assertion#AT#0; + +assert 2 != 2 /* checksum: 14-C1-28-03-D4-A3-E8-E9-0D-DF-F5-4A-B5-E9-BC-3F */ ; +== recycled error ==> assume {:recycled_failing_assertion} 2 != 2; + +assert 3 != 3 /* checksum: 8E-F6-6B-B8-4C-24-97-50-0F-23-EA-73-D2-9E-3E-74 */ ; +== marked as partially verified ==> assume a##post##0#AT#1 ==> ##assertion#AT#1; Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold. Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 2 errors + +assert 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +==> did nothing + + +assert 2 != 2 /* checksum: 14-C1-28-03-D4-A3-E8-E9-0D-DF-F5-4A-B5-E9-BC-3F */ ; +==> did nothing + + +assert 3 != 3 /* checksum: 5E-D6-64-57-02-21-AA-4B-43-C5-67-26-6A-B9-7E-4D */ ; +==> did nothing + Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold. Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 2 errors + +assert 1 == 1 /* checksum: 5E-6F-67-D1-06-87-65-19-00-DF-01-C8-02-E6-9E-C4 */ ; +==> did nothing + + +assert 2 != 2 /* checksum: 14-C1-28-03-D4-A3-E8-E9-0D-DF-F5-4A-B5-E9-BC-3F */ ; +== recycled error ==> assume {:recycled_failing_assertion} 2 != 2; + +assert 3 != 3 /* checksum: 8D-C4-E7-86-39-97-52-0B-CA-49-E3-35-73-44-30-5C */ ; +==> did nothing + Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold. Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 2 errors + +assert 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +==> did nothing + + +assert 2 == 2 /* checksum: B6-E5-D5-A8-0F-5C-50-C6-29-CF-0C-AA-AE-E2-7E-37 */ ; +==> did nothing + + +assert 3 == 3 /* checksum: 3E-01-56-38-C4-26-12-4C-34-A7-9F-21-B3-76-31-62 */ ; +==> did nothing + Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error +assert 1 == 1 /* checksum: 5E-6F-67-D1-06-87-65-19-00-DF-01-C8-02-E6-9E-C4 */ ; +==> did nothing + + +assert 2 == 2 /* checksum: B6-E5-D5-A8-0F-5C-50-C6-29-CF-0C-AA-AE-E2-7E-37 */ ; +== marked as fully verified ==> assume {:verified_assertion} 2 == 2; + +assert 3 == 3 /* checksum: E9-33-D7-E7-CD-5C-BA-0C-BD-2B-1B-32-B4-5D-73-53 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 0 errors + +assert 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +==> did nothing + + +assert 2 == 2 /* checksum: B6-E5-D5-A8-0F-5C-50-C6-29-CF-0C-AA-AE-E2-7E-37 */ ; +==> did nothing + + +assert 3 == 3 /* checksum: 3E-01-56-38-C4-26-12-4C-34-A7-9F-21-B3-76-31-62 */ ; +==> did nothing + Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 1 verified, 1 error Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold. +assert 4 == 4 /* checksum: F7-52-1B-27-96-FE-B0-15-1C-FB-93-71-A1-CC-06-A5 */ ; +==> did nothing + + Boogie program verifier finished with 1 verified, 1 error + +assert 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +== recycled error ==> assume {:recycled_failing_assertion} 1 != 1; + +assert 2 == 2 /* checksum: B6-E5-D5-A8-0F-5C-50-C6-29-CF-0C-AA-AE-E2-7E-37 */ ; +== marked as fully verified ==> assume {:verified_assertion} 2 == 2; Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 1 verified, 1 error + +assert {:subsumption 0} 1 != 1 /* checksum: 2F-3D-C6-E0-2F-BD-0D-D9-99-D3-FD-D9-1B-AB-9C-F5 */ ; +==> did nothing + + +assert {:subsumption 1} 5 != 5 /* checksum: F8-42-05-38-67-E2-63-71-35-11-CA-DC-EA-59-5C-3E */ ; +==> did nothing + + +assert {:subsumption 2} 6 != 6 /* checksum: 7B-ED-04-F8-9C-B4-D2-35-96-99-7D-18-C8-07-2D-73 */ ; +==> did nothing + + +assert {:subsumption 1} 2 == 2 /* checksum: B6-E5-D5-A8-0F-5C-50-C6-29-CF-0C-AA-AE-E2-7E-37 */ ; +==> did nothing + + +assert {:subsumption 2} 4 == 4 /* checksum: FD-E9-D0-7F-47-DA-00-EF-EB-EA-E7-E7-B3-92-44-0C */ ; +==> did nothing + + +assert 5 == 5 /* checksum: E6-65-AC-82-29-8D-B8-7B-B0-3F-CA-8B-23-C7-DD-6A */ ; +==> did nothing + + +assert {:subsumption 0} 3 == 3 /* checksum: FD-50-76-EE-43-01-17-4B-26-FD-3A-54-F4-0B-29-C6 */ ; +==> did nothing + Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold. Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold. Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 3 errors + +assert {:subsumption 0} 1 == 1 /* checksum: 5E-6F-67-D1-06-87-65-19-00-DF-01-C8-02-E6-9E-C4 */ ; +==> did nothing + + +assert {:subsumption 1} 5 == 5 /* checksum: 45-52-9C-E3-B0-EB-B8-8A-C5-69-33-72-8E-69-E1-1E */ ; +==> did nothing + + +assert {:subsumption 2} 6 != 6 /* checksum: 7B-ED-04-F8-9C-B4-D2-35-96-99-7D-18-C8-07-2D-73 */ ; +== recycled error ==> assume {:recycled_failing_assertion} 6 != 6; + +assert {:subsumption 2} 4 == 4 /* checksum: FD-E9-D0-7F-47-DA-00-EF-EB-EA-E7-E7-B3-92-44-0C */ ; +== marked as fully verified ==> assume {:verified_assertion} 4 == 4; + +assert 5 == 5 /* checksum: E6-65-AC-82-29-8D-B8-7B-B0-3F-CA-8B-23-C7-DD-6A */ ; +== marked as fully verified ==> assume {:verified_assertion} 5 == 5; + +assert {:subsumption 0} 3 == 3 /* checksum: F9-52-3E-D2-A3-8C-68-00-1F-D9-6D-3F-01-E6-80-17 */ ; +==> did nothing + Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold. Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3