From 736eb8d7b2d80e7672fcdffba8d731c7bb9bb9d7 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Wed, 9 Jul 2014 19:17:43 +0200 Subject: Worked on the more advanced verification result caching. --- Source/ExecutionEngine/ExecutionEngine.cs | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'Source/ExecutionEngine/ExecutionEngine.cs') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 04726cff..ea69b29e 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -216,12 +216,12 @@ namespace Microsoft.Boogie public class ErrorInformationFactory { - public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null) + public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null) { Contract.Requires(1 <= tok.line && 1 <= tok.col); Contract.Requires(msg != null); - return ErrorInformation.CreateErrorInformation(tok, msg, requestId, category); + return ErrorInformation.CreateErrorInformation(tok, msg, requestId, originalRequestId, category); } } @@ -233,6 +233,7 @@ namespace Microsoft.Boogie public string Category { get; set; } public string BoogieErrorCode { get; set; } public readonly List Aux = new List(); + public string OriginalRequestId { get; set; } public string RequestId { get; set; } public ErrorKind Kind { get; set; } public string ImplementationName { get; set; } @@ -284,10 +285,11 @@ namespace Microsoft.Boogie Msg = CleanUp(msg); } - internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null) + internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null) { var result = new ErrorInformation(tok, msg); result.RequestId = requestId; + result.OriginalRequestId = originalRequestId; result.Category = category; return result; } @@ -1564,39 +1566,39 @@ namespace Microsoft.Boogie var assertError = error as AssertCounterexample; if (callError != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, callError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5002"; errorInfo.Kind = ErrorKind.Precondition; errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "This is the precondition that might not hold.", "Related location"); if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, callError.OriginalRequestId, cause); } } else if (returnError != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, returnError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5003"; errorInfo.Kind = ErrorKind.Postcondition; errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "This is the postcondition that might not hold.", "Related location"); if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null) { - errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, returnError.OriginalRequestId, cause); } } else // error is AssertCounterexample { if (assertError.FailingAssert is LoopInitAssertCmd) { - errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5004"; errorInfo.Kind = ErrorKind.InvariantEntry; } else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd) { - errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5005"; errorInfo.Kind = ErrorKind.InvariantMaintainance; } @@ -1620,7 +1622,7 @@ namespace Microsoft.Boogie bec = "BP5001"; } - errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = bec; errorInfo.Kind = ErrorKind.Assertion; } -- cgit v1.2.3