Tweaks

robin-aws · Aug 15, 2023 · b2b266c · b2b266c
1 parent f249adb
commit b2b266c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
@@ -282,13 +282,13 @@ public void Resolve(ModuleResolver resolver) {
 
       // TODO: May not be the right place to do this, and may want something like InferredDecreases
       if (!Reads.Any()) {
+        // TODO: This is the right default for backwards-compatiblity,
+        // but we may want to infer a sensible default like decreases clauses instead.
         Reads.Add(new FrameExpression(tok, new WildcardExpr(tok), null));
       }
       foreach (FrameExpression fe in Reads) {
         resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this);
-        if (IsLemmaLike) {
-          resolver.reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have reads clauses", WhatKind);
-        } else if (IsGhost) {
+        if (IsGhost) {
           resolver.DisallowNonGhostFieldSpecifiers(fe);
         }
       }

diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
@@ -3865,6 +3865,7 @@ void GenerateIteratorImplPrelude(IteratorDecl iter, List<Variable> inParams, Lis
       var th = new ThisExpr(iter);
       iteratorFrame.Add(new FrameExpression(iter.tok, th, null));
       iteratorFrame.AddRange(iter.Modifies.Expressions);
+      DefineFrame(iter.tok, etran.ReadsFrame(iter.tok), iter.Reads.Expressions, builder, localVariables, null);
       DefineFrame(iter.tok, etran.ModifiesFrame(iter.tok), iteratorFrame, builder, localVariables, null);
       builder.AddCaptureState(iter.tok, false, "initial state");
     }