From 22e353122e53fbf396f24977eee99cb5991f5455 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 27 Nov 2015 17:37:48 -0800
Subject: autocontracts: Don't add modifies clause to ghost methods

---
 Source/Dafny/Rewriter.cs | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 39c8f667..d9db03c7 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -81,10 +81,10 @@ namespace Microsoft.Dafny
   /// AutoContracts will then:
   ///
   /// Declare:
-  ///    ghost var Repr: set(object);
+  ///    ghost var Repr: set(object)
   ///
   /// For function/predicate Valid(), insert:
-  ///    reads this, Repr;
+  ///    reads this, Repr
   /// Into body of Valid(), insert (at the beginning of the body):
   ///    this in Repr && null !in Repr
   /// and also insert, for every array-valued field A declared in the class:
@@ -96,19 +96,23 @@ namespace Microsoft.Dafny
   ///
   /// For every constructor, add:
   ///    modifies this;
-  ///    ensures Valid() && fresh(Repr - {this});
+  ///    ensures Valid() && fresh(Repr - {this})
   /// At the end of the body of the constructor, add:
   ///    Repr := {this};
   ///    if (A != null) { Repr := Repr + {A}; }
   ///    if (F != null) { Repr := Repr + {F} + F.Repr; }
   ///
-  /// For every method, add:
-  ///    requires Valid();
-  ///    modifies Repr;
-  ///    ensures Valid() && fresh(Repr - old(Repr));
+  /// For every non-static non-ghost method that is not a "simple query method",
+  /// add:
+  ///    requires Valid()
+  ///    modifies Repr
+  ///    ensures Valid() && fresh(Repr - old(Repr))
   /// At the end of the body of the method, add:
   ///    if (A != null) { Repr := Repr + {A}; }
   ///    if (F != null) { Repr := Repr + {F} + F.Repr; }
+  /// For every non-static method that is either ghost or is a "simple query method",
+  /// add:
+  ///    requires Valid()
   /// </summary>
   public class AutoContractsRewriter : IRewriter
   {
@@ -293,7 +297,7 @@ namespace Microsoft.Dafny
             AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);
           }
 
-        } else if (member is Method && !member.IsStatic) {
+        } else if (member is Method && !member.IsStatic && !member.IsGhost) {
           var m = (Method)member;
           if (Valid != null && !IsSimpleQueryMethod(m)) {
             if (member.RefinementBase == null) {
-- 
cgit v1.2.3