Fix setting of token and text for error messages (#282)

Co-authored-by: Bernhard Kragl <[email protected]>
boogie-org · Sep 7, 2020 · 15582d4 · 15582d4
1 parent bae82d3
commit 15582d4
Show file tree

Hide file tree

Showing 15 changed files with 69 additions and 66 deletions.
diff --git 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 <string>}
+       Prints <string> 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
@@ -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<Block> trace)
     {
       var msg = "assertion violation";

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,12 +1,12 @@
-(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
     pending-async-1.bpl(50,3): anon0$1
     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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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