Dafny: some bug fixes

4 files changed, 31 insertions, 13 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index ca779bf1..c2cb9353 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1190,14 +1190,11 @@ namespace Microsoft.Dafny {
       SpillLetVariableDecls(targetExpr, indent);

       var tRhs = rhs as TypeRhs;

       if (tRhs != null && tRhs.InitCall != null) {

-        foreach (Expression dim in tRhs.ArrayDimensions) {

-          SpillLetVariableDecls(dim, indent);

-        }

         string nw = "_nw" + tmpVarCount;

         tmpVarCount++;

         Indent(indent);

         wr.Write("var {0} = ", nw);

-        TrAssignmentRhs(rhs);

+        TrAssignmentRhs(rhs);  // in this case, this call will not require us to spill any let variables first

         wr.WriteLine(";");

         TrCallStmt(tRhs.InitCall, nw, indent);

         Indent(indent);

@@ -1207,9 +1204,15 @@ namespace Microsoft.Dafny {
           TrExpr(targetExpr);

         }

         wr.WriteLine(" = {0};", nw);

-      } else if (!(rhs is HavocRhs)) {

+      } else if (rhs is HavocRhs) {

+        // do nothing

+      } else {

         if (rhs is ExprRhs) {

           SpillLetVariableDecls(((ExprRhs)rhs).Expr, indent);

+        } else if (tRhs != null) {

+          foreach (Expression dim in tRhs.ArrayDimensions) {

+            SpillLetVariableDecls(dim, indent);

+          }

         }

         Indent(indent);

         if (target != null) {

@@ -1217,7 +1220,7 @@ namespace Microsoft.Dafny {
         } else {

           TrExpr(targetExpr);

         }

-        wr.Write(" = ", target);

+        wr.Write(" = ");

         TrAssignmentRhs(rhs);

         wr.WriteLine(";");

       }

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 9686de5a..3085fc3b 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -181,8 +181,19 @@ namespace Microsoft.Dafny {
       } else {

         var m = (Method)member;

         var tps = m.TypeArgs.ConvertAll(CloneTypeParam);

-        return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, m.Ins.ConvertAll(CloneFormal), m.Outs.ConvertAll(CloneFormal),

-          m.Req.ConvertAll(CloneMayBeFreeExpr), CloneSpecFrameExpr(m.Mod), m.Ens.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(m.Decreases), CloneBlockStmt(m.Body), null);

+        var ins = m.Ins.ConvertAll(CloneFormal);

+        var req = m.Req.ConvertAll(CloneMayBeFreeExpr);

+        var mod = CloneSpecFrameExpr(m.Mod);

+        var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);

+        var decreases = CloneSpecExpr(m.Decreases);

+        var body = CloneBlockStmt(m.Body);

+        if (member is Constructor) {

+          return new Constructor(Tok(m.tok), m.Name, tps, ins,

+            req, mod, ens, decreases, body, null);

+        } else {

+          return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

+            req, mod, ens, decreases, body, null);

+        }

       }

     }

 

@@ -282,6 +293,10 @@ namespace Microsoft.Dafny {
           return new SeqDisplayExpr(Tok(e.tok), e.Elements.ConvertAll(CloneExpr));

         }

 

+      } else if (expr is ExprDotName) {

+        var e = (ExprDotName)expr;

+        return new ExprDotName(Tok(e.tok), CloneExpr(e.Obj), e.SuffixName);

+

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

         return new FieldSelectExpr(Tok(e.tok), CloneExpr(e.Obj), e.FieldName);

@@ -372,7 +387,7 @@ namespace Microsoft.Dafny {
       } else if (expr is IdentifierSequence) {

         var e = (IdentifierSequence)expr;

         var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);

-        return new IdentifierSequence(e.Tokens.ConvertAll(tk => Tok(tk)), Tok(e.OpenParen), aa);

+        return new IdentifierSequence(e.Tokens.ConvertAll(tk => Tok(tk)), e.OpenParen == null ? null : Tok(e.OpenParen), aa);

 

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1505885b..088ca9d9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1870,10 +1870,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(method != null);

       bool isInitCall = receiverType != null;

 

-      // resolve receiver, unless told otherwise

+      // resolve receiver

+      ResolveReceiver(s.Receiver, true);

+      Contract.Assert(s.Receiver.Type != null);  // follows from postcondition of ResolveExpression

       if (receiverType == null) {

-        ResolveReceiver(s.Receiver, true);

-        Contract.Assert(s.Receiver.Type != null);  // follows from postcondition of ResolveExpression

         receiverType = s.Receiver.Type;

       }

       // resolve the method name

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index cb0d1b7e..27880f9d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4048,7 +4048,7 @@ namespace Microsoft.Dafny {
       Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

 

       Contract.Requires(tok != null);

-      Contract.Requires((dafnyReceiver != null) || (bReceiver != null));

+      Contract.Requires(dafnyReceiver != null || bReceiver != null);

       Contract.Requires(method != null);

       Contract.Requires(cce.NonNullElements(Args));

       Contract.Requires(cce.NonNullElements(Lhss));