Fix ProofDependencyLogging test

dafny-lang · Aug 13, 2024 · 288d151 · 288d151
1 parent b6a9d8a
commit 288d151
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
@@ -1209,7 +1209,7 @@ void CheckOperand(Expression operand) {
 
                   void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
                     if (rangeType != null) {
-                      CheckSubsetType(etran, result, resultIe, rangeType, returnBuilder);
+                      CheckSubsetType(etran, result, resultIe, rangeType, returnBuilder, "lambda expression");
                     }
                   }
 
@@ -1343,13 +1343,13 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
     }
 
     public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Expr selfCall, Type resultType,
-      BoogieStmtListBuilder builder) {
+      BoogieStmtListBuilder builder, string comment) {
 
       Contract.Assert(resultType != null);
       var bResult = etran.TrExpr(expr);
       CheckSubrange(expr.tok, bResult, expr.Type, resultType, expr, builder);
       builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr,
-        e => Bpl.Expr.Eq(selfCall, AdaptBoxing(expr.tok, e, expr.Type, resultType))));
+        e => Bpl.Expr.Eq(selfCall, AdaptBoxing(expr.tok, e, expr.Type, resultType)), comment));
       builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr)));
       builder.Add(new CommentCmd("CheckWellformedWithResult: any expression"));
       builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType)));
@@ -1518,7 +1518,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, List<Varia
           var rIe = new Bpl.IdentifierExpr(rhs.tok, r);
 
           void CheckPostconditionForRhs(BoogieStmtListBuilder innerBuilder, Expression body) {
-            CheckSubsetType(etran, body, rIe, pat.Expr.Type, innerBuilder);
+            CheckSubsetType(etran, body, rIe, pat.Expr.Type, innerBuilder, "let expression binding RHS well-formed");
           }
 
           CheckWellformedWithResult(e.RHSs[i], wfOptions, locals, builder, etran, CheckPostconditionForRhs);

diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs
@@ -205,7 +205,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat
         var wfo = new WFOptions(null, doReadsChecks, doReadsChecks, false);
 
         void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody) {
-          generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder);
+          generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder, "function call result");
           if (f.Result != null) {
             var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result)));
             generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f));

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy
@@ -56,7 +56,7 @@
 // CHECK:       ProofDependencies.dfy\(250,11\)-\(250,17\): ensures clause
 // CHECK:       ProofDependencies.dfy\(252,7\)-\(252,7\): let expression binding
 // CHECK:       ProofDependencies.dfy\(252,12\)-\(252,16\): let expression binding RHS well-formed
-// CHECK:       ProofDependencies.dfy\(254,3\)-\(254,3\): let expression result
+// CHECK:       ProofDependencies.dfy\(254,3\)-\(254,3\): function call result
 //
 // CHECK: Results for M.ObviouslyUnconstrainedCodeMethod \(correctness\)
 // CHECK:     Proof dependencies:
@@ -139,7 +139,7 @@
 // CHECK:       ProofDependencies.dfy\(373,1\)-\(380,1\): function definition for ObviouslyUnreachableIfExpressionBranchFunc
 // CHECK:       ProofDependencies.dfy\(374,12\)-\(374,16\): requires clause
 // CHECK:       ProofDependencies.dfy\(375,11\)-\(375,15\): ensures clause
-// CHECK:       ProofDependencies.dfy\(379,8\)-\(379,12\): if expression else branch
+// CHECK:       ProofDependencies.dfy\(379,8\)-\(379,12\): function call result
 //
 // CHECK: Results for M.ObviouslyUnreachableIfStatementBranchMethod \(correctness\)
 // CHECK:     Proof dependencies:
@@ -153,7 +153,7 @@
 // CHECK:       ProofDependencies.dfy\(395,1\)-\(403,1\): function definition for ObviouslyUnreachableMatchExpressionCaseFunction
 // CHECK:       ProofDependencies.dfy\(396,12\)-\(396,17\): requires clause
 // CHECK:       ProofDependencies.dfy\(397,11\)-\(397,15\): ensures clause
-// CHECK:       ProofDependencies.dfy\(401,15\)-\(401,15\): match expression branch result
+// CHECK:       ProofDependencies.dfy\(401,15\)-\(401,15\): function call result
 //
 // CHECK: Results for M.ObviouslyUnreachableMatchStatementCaseMethod \(correctness\)
 // CHECK:     Proof dependencies: