From 597a558b2fde558b7f5c581481fd51258aa37c46 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 30 Sep 2015 21:53:31 +0200 Subject: Improve output for diagnosing timeouts. --- Source/ExecutionEngine/ExecutionEngine.cs | 37 +++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') 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 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; -- cgit v1.2.3