Well-formedness check for calc lines

1 files changed, 15 insertions, 9 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index b4f5a4dc..2af8d4b4 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -4000,14 +4000,13 @@ namespace Microsoft.Dafny {
         var s = (CalcStmt)stmt;

         Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver

         AddComment(builder, stmt, "calc statement");

-        // NadiaTodo: check well-formedness of lines

-        if (s.Steps.Count > 0) {

-          Contract.Assert(s.Result != null); // established by the resolver

+        if (s.Lines.Count > 0) {          

           Bpl.IfCmd ifCmd = null;

           Bpl.StmtList els = null;

-

+          Bpl.StmtListBuilder b;

+          // check steps:

           for (int i = s.Steps.Count; 0 <= --i; ) {

-            var b = new Bpl.StmtListBuilder();

+            b = new Bpl.StmtListBuilder();

             TrStmt(s.Hints[i], b, locals, etran);

             b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));

             b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

@@ -4019,12 +4018,19 @@ namespace Microsoft.Dafny {
               els = null;

             }

           }

-          if (ifCmd == null) {

-            // single step: generate an if without else parts

-            ifCmd = new Bpl.IfCmd(s.Tok, null, els, null, null);

+          // check well-formedness of lines:

+          b = new Bpl.StmtListBuilder();

+          foreach (var e in s.Lines) {            

+            TrStmt_CheckWellformed(e, b, locals, etran, false);

           }

+          b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

+          ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, els);

           builder.Add(ifCmd);

-          builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));

+          // assume result:

+          if (s.Steps.Count > 0) {

+            Contract.Assert(s.Result != null); // established by the resolver

+            builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));

+          }

         }

 

       } else if (stmt is MatchStmt) {