Fix: Error wording closer to semantics (#676)

* Fix: Error wording closer to semantics This PR is the companion of dafny-lang/dafny#3324 We established numerous times this year that the wording "might not hold" still incorrectly provides the feeling that the postcondition is incorrect. Rather than focusing on whether assertions hold or not, this PR fixes the status by focusing on the fact that the verifier was not able to prove the assertion. * Fixed tests * proven => proved. Fixed tests * Fixed one more en->ed * Fixed a test * Fixed all the boogie files with messages inline * Fixed 3 more tests * Fixed last 2 CI errors * Support for the last two CI tests * Wording for invariants as well
boogie-org · Jan 14, 2023 · 4166fbb · 4166fbb
1 parent 1d0614b
commit 4166fbb
Show file tree

Hide file tree

Showing 190 changed files with 586 additions and 586 deletions.
diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -516,7 +516,7 @@ private void InjectGate(Action action, CallCmd callCmd, bool assume = false)
         else
         {
           newCmdSeq.Add(CmdHelper.AssertCmd(assertCmd.tok, expr,
-            $"This gate of {action.proc.Name} might not hold."));
+            $"this gate of {action.proc.Name} could not be proved"));
         }
       }
 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
@@ -2556,7 +2556,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       // assert that unpacked value has the correct constructor
       var assertCmd = new AssertCmd(tok,
         new NAryExpr(tok, new IsConstructor(tok, Constructor.datatypeTypeCtorDecl, Constructor.index),
-          new List<Expr> { rhs })) { Description = new FailureOnlyDescription("The precondition for unpack might not hold") };
+          new List<Expr> { rhs })) { Description = new FailureOnlyDescription("the precondition for unpack could not be proved") };
       cmds.Add(assertCmd);
       // read fields into lhs variables from localRhs
       var assignLhss = lhs.Args.Select(arg => new SimpleAssignLhs(tok, (IdentifierExpr)arg)).ToList<AssignLhs>();

diff --git a/Source/Core/ProofObligationDescription.cs b/Source/Core/ProofObligationDescription.cs
@@ -11,7 +11,7 @@ namespace Microsoft.Boogie;
 public abstract class ProofObligationDescription {
   /// <summary>
   /// A description of what this proof obligation means when it has been
-  /// successfully proven.
+  /// successfully proved.
   /// </summary>
   public abstract string SuccessDescription { get; }
 
@@ -32,75 +32,75 @@ public abstract class ProofObligationDescription {
 
 public class AssertionDescription : ProofObligationDescription
 {
-  public override string SuccessDescription => "This assertion holds.";
+  public override string SuccessDescription => "this assertion holds";
 
-  public override string FailureDescription => "This assertion might not hold.";
+  public override string FailureDescription => "this assertion could not be proved";
 
   public override string ShortDescription => "assert";
 }
 
 public class PreconditionDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "All preconditions hold for this call.";
+    "all preconditions hold for this call";
 
   public override string FailureDescription =>
-    "A precondition for this call might not hold.";
+    "a precondition for this call could not be proved";
 
   public override string ShortDescription => "precondition";
 }
 
 public class RequiresDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "This precondition holds.";
+    "this precondition holds";
 
   public override string FailureDescription =>
-    "This is the precondition that might not hold.";
+    "this is the precondition that could not be proved";
 
   public override string ShortDescription => "requires";
 }
 
 public class PostconditionDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "All postconditions hold for this return path.";
+    "all postconditions hold for this return path";
 
   public override string FailureDescription =>
-    "A postcondition might not hold on this return path.";
+    "a postcondition could not be proved on this return path";
 
   public override string ShortDescription => "postcondition";
 }
 
 public class EnsuresDescription : ProofObligationDescription
 {
   public override string SuccessDescription =>
-    "This postcondition holds.";
+    "this postcondition holds";
 
   public override string FailureDescription =>
-    "This is the postcondition that might not hold.";
+    "this is the postcondition that could not be proved";
 
   public override string ShortDescription => "ensures";
 }
 
 public class InvariantEstablishedDescription : AssertionDescription
 {
   public override string SuccessDescription =>
-    "This loop invariant holds on entry.";
+    "this loop invariant holds on entry";
 
   public override string FailureDescription =>
-    "This loop invariant might not hold on entry.";
+    "this loop invariant could not be proved on entry";
 
   public override string ShortDescription => "invariant established";
 }
 
 public class InvariantMaintainedDescription : AssertionDescription
 {
   public override string SuccessDescription =>
-    "This loop invariant is maintained by the loop.";
+    "this loop invariant is maintained by the loop";
 
   public override string FailureDescription =>
-    "This loop invariant might not be maintained by the loop.";
+    "this invariant could not be proved to be maintained by the loop";
 
   public override string ShortDescription => "invariant maintained";
 }

diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -76,10 +76,10 @@ procedure Bad2(y: int)
     options.VcsCores = 4;
     var engine = ExecutionEngine.CreateWithoutSharedCache(options);
 
-    var expected = @"fakeFilename1(3,3): Error: This assertion might not hold.
+    var expected = @"fakeFilename1(3,3): Error: this assertion could not be proved
 Execution trace:
     fakeFilename1(3,3): anon0
-fakeFilename1(8,3): Error: This assertion might not hold.
+fakeFilename1(8,3): Error: this assertion could not be proved
 Execution trace:
     fakeFilename1(8,3): anon0
 
@@ -125,12 +125,12 @@ procedure Good(y: int)
     await task1Writer.DisposeAsync();
     await task2Writer.DisposeAsync();
     var output = writer.ToString();
-    var expected = @"fakeFilename1(3,3): Error: This assertion might not hold.
+    var expected = @"fakeFilename1(3,3): Error: this assertion could not be proved
 Execution trace:
     fakeFilename1(3,3): anon0
 
 Boogie program verifier finished with 1 verified, 1 error
-fakeFilename2(3,3): Error: This assertion might not hold.
+fakeFilename2(3,3): Error: this assertion could not be proved
 Execution trace:
     fakeFilename2(3,3): anon0
 
@@ -175,7 +175,7 @@ public async Task LoopInvariantDescriptions()
     await engine.ProcessProgram(writer, program1, "fakeFilename");
     await writer.DisposeAsync();
     var output = writer.ToString();
-    var expected = @"fakeFilename(10,5): Error: This loop invariant might not be maintained by the loop.
+    var expected = @"fakeFilename(10,5): Error: this invariant could not be proved to be maintained by the loop
 fakeFilename(10,5): Related message: fake failure
 Execution trace:
     fakeFilename(5,3): entry

diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
@@ -1,13 +1,13 @@
-Intervals.bpl(64,3): Error: This assertion might not hold.
-Intervals.bpl(75,3): Error: This assertion might not hold.
-Intervals.bpl(94,3): Error: This assertion might not hold.
-Intervals.bpl(140,3): Error: This assertion might not hold.
-Intervals.bpl(151,3): Error: This assertion might not hold.
-Intervals.bpl(202,3): Error: This assertion might not hold.
-Intervals.bpl(240,3): Error: This assertion might not hold.
-Intervals.bpl(252,3): Error: This assertion might not hold.
-Intervals.bpl(263,3): Error: This assertion might not hold.
-Intervals.bpl(285,3): Error: This assertion might not hold.
-Intervals.bpl(307,3): Error: This assertion might not hold.
+Intervals.bpl(64,3): Error: this assertion could not be proved
+Intervals.bpl(75,3): Error: this assertion could not be proved
+Intervals.bpl(94,3): Error: this assertion could not be proved
+Intervals.bpl(140,3): Error: this assertion could not be proved
+Intervals.bpl(151,3): Error: this assertion could not be proved
+Intervals.bpl(202,3): Error: this assertion could not be proved
+Intervals.bpl(240,3): Error: this assertion could not be proved
+Intervals.bpl(252,3): Error: this assertion could not be proved
+Intervals.bpl(263,3): Error: this assertion could not be proved
+Intervals.bpl(285,3): Error: this assertion could not be proved
+Intervals.bpl(307,3): Error: this assertion could not be proved
 
 Boogie program verifier finished with 17 verified, 11 errors
diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect
@@ -1,5 +1,5 @@
-Issue25.bpl(12,1): Error: A postcondition might not hold on this return path.
-Issue25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Issue25.bpl(12,1): Error: a postcondition could not be proved on this return path
+Issue25.bpl(8,1): Related location: this is the postcondition that could not be proved
 Execution trace:
     Issue25.bpl(11,3): anon0
     Issue25.bpl(12,1): anon2_LoopHead

diff --git a/Test/aitest1/Bound.bpl.expect b/Test/aitest1/Bound.bpl.expect
@@ -1,4 +1,4 @@
-Bound.bpl(26,3): Error: This assertion might not hold.
+Bound.bpl(26,3): Error: this assertion could not be proved
 Execution trace:
     Bound.bpl(10,1): start
     Bound.bpl(16,1): LoopHead

diff --git a/Test/aitest9/TestIntervals.bpl.expect b/Test/aitest9/TestIntervals.bpl.expect
@@ -1,5 +1,5 @@
-TestIntervals.bpl(26,3): Error: This assertion might not hold.
-TestIntervals.bpl(71,3): Error: This assertion might not hold.
-TestIntervals.bpl(72,3): Error: This assertion might not hold.
+TestIntervals.bpl(26,3): Error: this assertion could not be proved
+TestIntervals.bpl(71,3): Error: this assertion could not be proved
+TestIntervals.bpl(72,3): Error: this assertion could not be proved
 
 Boogie program verifier finished with 2 verified, 3 errors
diff --git a/Test/aitest9/VarMapFixpoint.bpl.expect b/Test/aitest9/VarMapFixpoint.bpl.expect
@@ -1,4 +1,4 @@
-VarMapFixpoint.bpl(13,5): Error: This loop invariant might not be maintained by the loop.
+VarMapFixpoint.bpl(13,5): Error: this invariant could not be proved to be maintained by the loop
 Execution trace:
     VarMapFixpoint.bpl(7,3): start
     VarMapFixpoint.bpl(12,3): LoopHead

diff --git a/Test/bitvectors/bv5.bpl.expect b/Test/bitvectors/bv5.bpl.expect
@@ -1,4 +1,4 @@
-bv5.bpl(12,3): Error: This assertion might not hold.
+bv5.bpl(12,3): Error: this assertion could not be proved
 Execution trace:
     bv5.bpl(7,12): anon0
 

diff --git a/Test/bitvectors/bv6.bpl.expect b/Test/bitvectors/bv6.bpl.expect
@@ -1,4 +1,4 @@
-bv6.bpl(10,3): Error: This assertion might not hold.
+bv6.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     bv6.bpl(7,5): anon0
 

diff --git a/Test/civl/Program4-fail.bpl.expect b/Test/civl/Program4-fail.bpl.expect
@@ -1,5 +1,5 @@
-Program4-fail.bpl(27,1): Error: A postcondition might not hold on this return path.
-Program4-fail.bpl(6,1): Related location: This is the postcondition that might not hold.
+Program4-fail.bpl(27,1): Error: a postcondition could not be proved on this return path
+Program4-fail.bpl(6,1): Related location: this is the postcondition that could not be proved
 Execution trace:
     Program4-fail.bpl(24,3): anon0
     Program4-fail.bpl(37,5): inline$AtomicIncr$0$anon0

diff --git a/Test/civl/assert-not-first-4.bpl.expect b/Test/civl/assert-not-first-4.bpl.expect
@@ -1,4 +1,4 @@
-assert-not-first-4.bpl(15,5): Error: This gate of FOO might not hold.
+assert-not-first-4.bpl(15,5): Error: this gate of FOO could not be proved
 Execution trace:
     assert-not-first-4.bpl(8,5): anon0
 

diff --git a/Test/civl/chris4.bpl.expect b/Test/civl/chris4.bpl.expect
@@ -1,4 +1,4 @@
-chris4.bpl(13,3): Error: This assertion might not hold.
+chris4.bpl(13,3): Error: this assertion could not be proved
 Execution trace:
     chris4.bpl(12,3): anon0
     chris4.bpl(12,3): anon0_0

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: this gate of P could not be proved
 Execution trace:
     chris5.bpl(12,3): anon0
 

diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect
@@ -1,4 +1,4 @@
-chris6.bpl(11,3): Error: This assertion might not hold.
+chris6.bpl(11,3): Error: this assertion could not be proved
 Execution trace:
     chris6.bpl(11,3): anon0
 

diff --git a/Test/civl/linear/allocator.bpl.expect b/Test/civl/linear/allocator.bpl.expect
@@ -1,4 +1,4 @@
-allocator.bpl(16,3): Error: This assertion might not hold.
+allocator.bpl(16,3): Error: this assertion could not be proved
 Execution trace:
     allocator.bpl(14,5): anon0
 

diff --git a/Test/civl/linear/bug.bpl.expect b/Test/civl/linear/bug.bpl.expect
@@ -1,4 +1,4 @@
-bug.bpl(15,3): Error: This assertion might not hold.
+bug.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     bug.bpl(14,3): anon0
 

diff --git a/Test/civl/linear/f1.bpl.expect b/Test/civl/linear/f1.bpl.expect
@@ -1,4 +1,4 @@
-f1.bpl(35,4): Error: This assertion might not hold.
+f1.bpl(35,4): Error: this assertion could not be proved
 Execution trace:
     f1.bpl(29,6): anon0
 

diff --git a/Test/civl/linear/f2.bpl.expect b/Test/civl/linear/f2.bpl.expect
@@ -1,4 +1,4 @@
-f2.bpl(26,4): Error: This assertion might not hold.
+f2.bpl(26,4): Error: this assertion could not be proved
 Execution trace:
     f2.bpl(22,4): anon0
 

diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect
@@ -1,4 +1,4 @@
-parallel4.bpl(26,3): Error: This assertion might not hold.
+parallel4.bpl(26,3): Error: this assertion could not be proved
 Execution trace:
     parallel4.bpl(24,5): anon0
     parallel4.bpl(24,5): anon0_0

diff --git a/Test/codeexpr/CodeExpr0.bpl.expect b/Test/codeexpr/CodeExpr0.bpl.expect
@@ -1,10 +1,10 @@
-CodeExpr0.bpl(17,3): Error: This assertion might not hold.
+CodeExpr0.bpl(17,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(17,3): anon0
-CodeExpr0.bpl(22,3): Error: This assertion might not hold.
+CodeExpr0.bpl(22,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(22,3): anon0
-CodeExpr0.bpl(54,3): Error: This assertion might not hold.
+CodeExpr0.bpl(54,3): Error: this assertion could not be proved
 Execution trace:
     CodeExpr0.bpl(54,3): anon0
 

diff --git a/Test/codeexpr/CodeExpr1.bpl.expect b/Test/codeexpr/CodeExpr1.bpl.expect
@@ -1,11 +1,11 @@
-CodeExpr1.bpl(46,5): Error: A postcondition might not hold on this return path.
-CodeExpr1.bpl(42,3): Related location: This is the postcondition that might not hold.
+CodeExpr1.bpl(46,5): Error: a postcondition could not be proved on this return path
+CodeExpr1.bpl(42,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     CodeExpr1.bpl(44,3): start
-CodeExpr1.bpl(54,5): Error: This assertion might not hold.
+CodeExpr1.bpl(54,5): Error: this assertion could not be proved
 Execution trace:
     CodeExpr1.bpl(51,3): start
-CodeExpr1.bpl(68,5): Error: This assertion might not hold.
+CodeExpr1.bpl(68,5): Error: this assertion could not be proved
 Execution trace:
     CodeExpr1.bpl(59,3): start
 

diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
@@ -16,7 +16,7 @@
 // CHECK:      checking split 10/12, .*
 // CHECK:      checking split 11/12, .*
 // CHECK:      checking split 12/12, .*
-// CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: This assertion might not hold.
+// CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)
   ensures y >= 0;

diff --git a/Test/commandline/noProc.bpl.1.expect b/Test/commandline/noProc.bpl.1.expect
@@ -1,7 +1,7 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
-noProc.bpl(15,3): Error: This assertion might not hold.
+noProc.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(15,3): anon0
 

diff --git a/Test/commandline/noProc.bpl.2.expect b/Test/commandline/noProc.bpl.2.expect
@@ -1,4 +1,4 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
 

diff --git a/Test/commandline/noProc.bpl.3.expect b/Test/commandline/noProc.bpl.3.expect
@@ -1,7 +1,7 @@
-noProc.bpl(10,3): Error: This assertion might not hold.
+noProc.bpl(10,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(10,3): anon0
-noProc.bpl(15,3): Error: This assertion might not hold.
+noProc.bpl(15,3): Error: this assertion could not be proved
 Execution trace:
     noProc.bpl(15,3): anon0
 

diff --git a/Test/datatypes/field_access_verification_error.bpl.expect b/Test/datatypes/field_access_verification_error.bpl.expect
@@ -1,22 +1,22 @@
-field_access_verification_error.bpl(13,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(9,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(13,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(9,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(11,5): anon0
-field_access_verification_error.bpl(21,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(17,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(21,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(17,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(19,8): anon0
-field_access_verification_error.bpl(34,1): Error: A postcondition might not hold on this return path.
-field_access_verification_error.bpl(28,3): Related location: This is the postcondition that might not hold.
+field_access_verification_error.bpl(34,1): Error: a postcondition could not be proved on this return path
+field_access_verification_error.bpl(28,3): Related location: this is the postcondition that could not be proved
 Execution trace:
     field_access_verification_error.bpl(31,5): anon0
-field_access_verification_error.bpl(43,3): Error: This assertion might not hold.
+field_access_verification_error.bpl(43,3): Error: this assertion could not be proved
 Execution trace:
     field_access_verification_error.bpl(42,11): anon0
-field_access_verification_error.bpl(50,11): Error: The precondition for unpack might not hold
+field_access_verification_error.bpl(50,11): Error: the precondition for unpack could not be proved
 Execution trace:
     field_access_verification_error.bpl(50,11): anon0
-field_access_verification_error.bpl(60,3): Error: This assertion might not hold.
+field_access_verification_error.bpl(60,3): Error: this assertion could not be proved
 Execution trace:
     field_access_verification_error.bpl(59,5): anon0
 

diff --git a/Test/datatypes/t1.bpl.expect b/Test/datatypes/t1.bpl.expect
@@ -1,4 +1,4 @@
-t1.bpl(25,3): Error: This assertion might not hold.
+t1.bpl(25,3): Error: this assertion could not be proved
 Execution trace:
     t1.bpl(18,3): anon0
 

diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect
@@ -1,4 +1,4 @@
-(0,0): Error: This assertion might not hold.
+(0,0): Error: this assertion could not be proved
 Execution trace:
     detLoopExtractNested.bpl(12,12): anon0
     detLoopExtractNested.bpl(14,8): anon5_LoopBody

diff --git a/Test/extractloops/t1.bpl.expect b/Test/extractloops/t1.bpl.expect
@@ -1,4 +1,4 @@
-(0,0): Error: This assertion might not hold.
+(0,0): Error: this assertion could not be proved
 Execution trace:
     t1.bpl(19,3): anon0
     t1.bpl(24,3): anon3_LoopHead
-Original file line number
+Diff line change
@@ Expand Up @@
             else
             {
               newCmdSeq.Add(CmdHelper.AssertCmd(assertCmd.tok, expr,
-                $"This gate of {action.proc.Name} might not hold."));
+                $"this gate of {action.proc.Name} could not be proved"));
             }
           }
@@ Expand Down @@