Default to reads *

robin-aws · Aug 15, 2023 · f249adb · f249adb
1 parent 20118e6
commit f249adb
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
@@ -21,6 +21,7 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext,
   public readonly List<Formal> Ins;
   public readonly List<Formal> Outs;
   public readonly List<AttributedExpression> Req;
+  // TODO: make a Specification<FrameExpression> as well? Function.Reads isn't...
   public readonly List<FrameExpression> Reads;
   public readonly Specification<FrameExpression> Mod;
   public readonly List<AttributedExpression> Ens;
@@ -279,6 +280,10 @@ public void Resolve(ModuleResolver resolver) {
         resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})");
       }
 
+      // TODO: May not be the right place to do this, and may want something like InferredDecreases
+      if (!Reads.Any()) {
+        Reads.Add(new FrameExpression(tok, new WildcardExpr(tok), null));
+      }
       foreach (FrameExpression fe in Reads) {
         resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this);
         if (IsLemmaLike) {