diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index ad5a0852b..9987dc614 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1966,6 +1966,10 @@ Verifies code leading to this point and code leading from this point to the next split_here as separate pieces. May help with timeouts. May also occasionally double-report errors. + {:msg } + Prints rather than the standard message for assertion failure. + Also applicable to requires and ensures declarations. + ---- The end --------------------------------------------------------------- "); } diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index dfa3fee28..29ab71973 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -9,6 +9,7 @@ using VC; using BoogiePL = Microsoft.Boogie; using System.Runtime.Caching; +using System.Diagnostics; namespace Microsoft.Boogie { @@ -1858,50 +1859,55 @@ private static ErrorInformation CreateErrorInformation(Counterexample error, VC. cause = "Out of resource on"; } - var callError = error as CallCounterexample; - var returnError = error as ReturnCounterexample; - var assertError = error as AssertCounterexample; - if (callError != null) + if (error is CallCounterexample callError) { - 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) + if (callError.FailingRequires.ErrorMessage == null || CommandLineOptions.Clo.ForceBplErrors) + { + 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"); + } + else { - errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, + errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, + callError.FailingRequires.ErrorMessage, callError.RequestId, callError.OriginalRequestId, cause); } } - else if (returnError != null) + else if (error is ReturnCounterexample returnError) { - 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) + if (returnError.FailingEnsures.ErrorMessage == null || CommandLineOptions.Clo.ForceBplErrors) { - errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, + 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"); + } + else + { + errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, + returnError.FailingEnsures.ErrorMessage, returnError.RequestId, returnError.OriginalRequestId, cause); } } else // error is AssertCounterexample { + Debug.Assert(error is AssertCounterexample); + var assertError = (AssertCounterexample)error; if (assertError.FailingAssert is LoopInitAssertCmd) { errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, - "This loop invariant might not hold on entry.", assertError.RequestId, assertError.OriginalRequestId, - cause); + "This loop invariant might not hold on entry.", + assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5004"; errorInfo.Kind = ErrorKind.InvariantEntry; if ((assertError.FailingAssert.ErrorData as string) != null) @@ -1913,8 +1919,8 @@ private static ErrorInformation CreateErrorInformation(Counterexample error, VC. else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd) { errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, - "This loop invariant might not be maintained by the loop.", assertError.RequestId, - assertError.OriginalRequestId, cause); + "This loop invariant might not be maintained by the loop.", + assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = "BP5005"; errorInfo.Kind = ErrorKind.InvariantMaintainance; if ((assertError.FailingAssert.ErrorData as string) != null) @@ -1925,27 +1931,21 @@ private static ErrorInformation CreateErrorInformation(Counterexample error, VC. } else { - var msg = assertError.FailingAssert.ErrorData as string; - var tok = assertError.FailingAssert.tok; - if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null) - { - msg = assertError.FailingAssert.ErrorMessage; - tok = null; - if (cause == "Error") - { - cause = null; - } - } - + string msg = null; string bec = null; - if (msg == null) + + if (assertError.FailingAssert.ErrorMessage == null || CommandLineOptions.Clo.ForceBplErrors) { - msg = "This assertion might not hold."; + msg = assertError.FailingAssert.ErrorData as string ?? "This assertion might not hold."; bec = "BP5001"; } + else + { + msg = assertError.FailingAssert.ErrorMessage; + } - errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, - assertError.OriginalRequestId, cause); + errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, msg, + assertError.RequestId, assertError.OriginalRequestId, cause); errorInfo.BoogieErrorCode = bec; errorInfo.Kind = ErrorKind.Assertion; } @@ -1954,7 +1954,6 @@ private static ErrorInformation CreateErrorInformation(Counterexample error, VC. return errorInfo; } - private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, List trace) { var msg = "assertion violation"; diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index 952797e37..d683bf686 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -1,9 +1,9 @@ -bar.bpl(23,1): Error: Non-interference check failed +bar.bpl(23,1): Error BP5001: Non-interference check failed Execution trace: bar.bpl(7,3): anon0 bar.bpl(12,5): inline$AtomicIncr$0$anon0 (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0 -bar.bpl(23,1): Error: Non-interference check failed +bar.bpl(23,1): Error BP5001: Non-interference check failed Execution trace: bar.bpl(32,3): anon0 (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0 diff --git a/Test/civl/chris5.bpl.expect b/Test/civl/chris5.bpl.expect index ca2ed3abe..b1ca600ec 100644 --- a/Test/civl/chris5.bpl.expect +++ b/Test/civl/chris5.bpl.expect @@ -1,4 +1,4 @@ -chris5.bpl(7,3): Error: This gate of P might not hold. +chris5.bpl(7,3): Error BP5001: This gate of P might not hold. Execution trace: chris5.bpl(12,3): anon0 diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index 6fb8c8765..e8565e352 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -1,4 +1,4 @@ -foo.bpl(23,1): Error: Non-interference check failed +foo.bpl(23,1): Error BP5001: Non-interference check failed Execution trace: foo.bpl(7,3): anon0 foo.bpl(12,5): inline$AtomicIncr$0$anon0 diff --git a/Test/civl/intro-nonblocking.bpl.expect b/Test/civl/intro-nonblocking.bpl.expect index e0ae9ed82..cb36d9b59 100644 --- a/Test/civl/intro-nonblocking.bpl.expect +++ b/Test/civl/intro-nonblocking.bpl.expect @@ -1,4 +1,4 @@ -intro-nonblocking.bpl(4,30): Error: Non-blocking check for intro failed +intro-nonblocking.bpl(4,30): Error BP5001: Non-blocking check for intro failed Execution trace: intro-nonblocking.bpl(4,30): L diff --git a/Test/civl/left-mover.bpl.expect b/Test/civl/left-mover.bpl.expect index 7642611d7..2a846143f 100644 --- a/Test/civl/left-mover.bpl.expect +++ b/Test/civl/left-mover.bpl.expect @@ -10,7 +10,7 @@ Execution trace: left-mover.bpl(19,32): inline$init$0$Entry left-mover.bpl(8,5): inline$inc$0$anon0 left-mover.bpl(6,30): inline$inc$0$Return -left-mover.bpl(26,30): Error: Non-blocking check for block failed +left-mover.bpl(26,30): Error BP5001: Non-blocking check for block failed Execution trace: left-mover.bpl(26,30): L diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index ab31dd64d..b38eeb23b 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -1,4 +1,4 @@ -parallel1.bpl(23,1): Error: Non-interference check failed +parallel1.bpl(23,1): Error BP5001: Non-interference check failed Execution trace: parallel1.bpl(7,3): anon0 parallel1.bpl(12,5): inline$AtomicIncr$0$anon0 diff --git a/Test/civl/parallel6.bpl.expect b/Test/civl/parallel6.bpl.expect index f7da260a0..cadd6fa88 100644 --- a/Test/civl/parallel6.bpl.expect +++ b/Test/civl/parallel6.bpl.expect @@ -1,4 +1,4 @@ -(0,0): Error: Transition invariant violated in final state +(0,0): Error BP5001: Transition invariant violated in final state Execution trace: parallel6.bpl(10,5): anon0 parallel6.bpl(28,7): inline$atomic_incr$0$anon0 diff --git a/Test/civl/pending-async-1.bpl.expect b/Test/civl/pending-async-1.bpl.expect index 664c13fe1..feea0d367 100644 --- a/Test/civl/pending-async-1.bpl.expect +++ b/Test/civl/pending-async-1.bpl.expect @@ -1,4 +1,4 @@ -(0,0): Error: Failed to execute atomic action before procedure return +(0,0): Error BP5001: Failed to execute atomic action before procedure return Execution trace: pending-async-1.bpl(50,3): anon0 pending-async-1.bpl(16,7): inline$B$0$anon0 @@ -6,7 +6,7 @@ Execution trace: pending-async-1.bpl(16,7): inline$B$1$anon0 pending-async-1.bpl(50,3): anon0$2 (0,0): Civl_ReturnChecker -pending-async-1.bpl(64,3): Error: Pending asyncs created by this call are not summarized +pending-async-1.bpl(64,3): Error BP5001: Pending asyncs created by this call are not summarized Execution trace: pending-async-1.bpl(64,3): anon0 pending-async-1.bpl(21,7): inline$C$0$anon0 diff --git a/Test/civl/pending-async-noninterference-fail.bpl.expect b/Test/civl/pending-async-noninterference-fail.bpl.expect index b834c7b04..2154f63bd 100644 --- a/Test/civl/pending-async-noninterference-fail.bpl.expect +++ b/Test/civl/pending-async-noninterference-fail.bpl.expect @@ -1,4 +1,4 @@ -pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed +pending-async-noninterference-fail.bpl(7,1): Error BP5001: Non-interference check failed Execution trace: pending-async-noninterference-fail.bpl(15,31): inline$A$0$Entry pending-async-noninterference-fail.bpl(18,5): inline$A$0$anon0 diff --git a/Test/civl/r2.bpl.expect b/Test/civl/r2.bpl.expect index 27e75b598..ae3fd670b 100644 --- a/Test/civl/r2.bpl.expect +++ b/Test/civl/r2.bpl.expect @@ -1,10 +1,10 @@ -(0,0): Error: Failed to execute atomic action before procedure return +(0,0): Error BP5001: Failed to execute atomic action before procedure return Execution trace: r2.bpl(11,5): anon0 (0,0): Civl_call_refinement_4 r2.bpl(21,34): inline$atomic_nop$0$Return (0,0): Civl_ReturnChecker -(0,0): Error: Globals must not be modified +(0,0): Error BP5001: Globals must not be modified Execution trace: r2.bpl(11,5): anon0 (0,0): Civl_call_refinement_3 diff --git a/Test/civl/refinement.bpl.expect b/Test/civl/refinement.bpl.expect index 471f31c5e..8c01955f1 100644 --- a/Test/civl/refinement.bpl.expect +++ b/Test/civl/refinement.bpl.expect @@ -1,16 +1,16 @@ -(0,0): Error: Transition invariant violated in final state +(0,0): Error BP5001: Transition invariant violated in final state Execution trace: refinement.bpl(8,3): anon0 refinement.bpl(37,5): inline$INCR$0$anon0 refinement.bpl(8,3): anon0_0 refinement.bpl(37,5): inline$INCR$1$anon0 (0,0): Civl_ReturnChecker -(0,0): Error: Transition invariant violated in initial state +(0,0): Error BP5001: Transition invariant violated in initial state Execution trace: refinement.bpl(16,3): anon0 refinement.bpl(44,5): inline$DECR$0$anon0 (0,0): Civl_RefinementChecker -(0,0): Error: Transition invariant violated in final state +(0,0): Error BP5001: Transition invariant violated in final state Execution trace: refinement.bpl(16,3): anon0 refinement.bpl(44,5): inline$DECR$0$anon0 diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index 76e6af135..3a1eb58d0 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -1,4 +1,4 @@ -t1.bpl(75,5): Error: Non-interference check failed +t1.bpl(75,5): Error BP5001: Non-interference check failed Execution trace: t1.bpl(94,13): anon0 t1.bpl(94,13): anon0_1 diff --git a/Test/civl/yield-invariant-fails.bpl.expect b/Test/civl/yield-invariant-fails.bpl.expect index 918e1895e..95960f154 100644 --- a/Test/civl/yield-invariant-fails.bpl.expect +++ b/Test/civl/yield-invariant-fails.bpl.expect @@ -1,4 +1,4 @@ -yield-invariant-fails.bpl(7,1): Error: Non-interference check failed +yield-invariant-fails.bpl(7,1): Error BP5001: Non-interference check failed Execution trace: yield-invariant-fails.bpl(11,5): anon0 yield-invariant-fails.bpl(18,7): inline$atomic_A$0$anon0