diff options
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 37 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 13 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 1 |
3 files changed, 48 insertions, 3 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 15fdc081..4ab0a9c5 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1459,11 +1459,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); - ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit); + ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors); } - private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit) + private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors) { ErrorInformation errorInfo = null; @@ -1476,6 +1476,35 @@ namespace Microsoft.Boogie if (implName != null && implTok != null) { errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId); + + // Report timed out assertions as auxiliary info. + if (errors != null) + { + var cmpr = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList(); + timedOutAssertions.Sort(cmpr); + int idx = 1; + foreach (Counterexample error in timedOutAssertions) + { + var callError = error as CallCounterexample; + var returnError = error as ReturnCounterexample; + var assertError = error as AssertCounterexample; + IToken tok = null; + if (callError != null) + { + tok = callError.FailingCall.tok; + } + else if (returnError != null) + { + tok = returnError.FailingReturn.tok; + } + else + { + tok = assertError.FailingAssert.tok; + } + errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count)); + } + } } break; case VCGen.Outcome.OutOfMemory: @@ -1592,6 +1621,10 @@ namespace Microsoft.Boogie errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { + if (error.IsAuxiliaryCexForDiagnosingTimeouts) + { + continue; + } var errorInfo = CreateErrorInformation(error, outcome); errorInfo.ImplementationName = implName; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 1f010757..ae0a1147 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -85,6 +85,7 @@ namespace Microsoft.Boogie { public string RequestId; public abstract byte[] Checksum { get; } public byte[] SugaredCmdChecksum; + public bool IsAuxiliaryCexForDiagnosingTimeouts; public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples; @@ -313,7 +314,7 @@ namespace Microsoft.Boogie { public abstract int GetLocation(); } - public class CounterexampleComparer : IComparer<Counterexample> { + public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> { private int Compare(List<Block> bs1, List<Block> bs2) { @@ -375,6 +376,16 @@ namespace Microsoft.Boogie { } return -1; } + + public bool Equals(Counterexample x, Counterexample y) + { + return Compare(x, y) == 0; + } + + public int GetHashCode(Counterexample obj) + { + return 0; + } } public class AssertCounterexample : Counterexample { diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 94584027..33e2f928 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2113,6 +2113,7 @@ namespace VC { foreach (var cmd in assertCmds) { Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context); + cex.IsAuxiliaryCexForDiagnosingTimeouts = true; callback.OnCounterexample(cex, msg); } } |