Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Read clauses on methods #4440

Merged
merged 59 commits into from
Aug 30, 2023
Merged

feat: Read clauses on methods #4440

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
59 commits
Select commit Hold shift + click to select a range
1bf4616
First step, adding to parser and Method model
robin-aws Sep 16, 2021
6cf7685
Split TheFrame into ReadsFrame and ModifiesFrame
robin-aws Sep 17, 2021
e29db85
Just enough to support the first test case
robin-aws Sep 17, 2021
6fa7f62
Set default of "reads *" for methods
robin-aws Sep 17, 2021
c538c2b
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 4, 2023
12c9933
Partial fixes to bad merge
robin-aws Aug 4, 2023
41ee604
Remove zombie files from merge
robin-aws Aug 4, 2023
57d9919
More fixes
robin-aws Aug 4, 2023
dbb4ce0
Another batch of error fixes
robin-aws Aug 4, 2023
9ce3f2a
Finally builds
robin-aws Aug 4, 2023
905f103
Fix test
robin-aws Aug 4, 2023
bbeefdb
Address missing resolution etc.
robin-aws Aug 4, 2023
7f77f7c
Clean up WFOptions
robin-aws Aug 4, 2023
11d4a0d
Partially get test working
robin-aws Aug 4, 2023
20118e6
Missing cloning case
robin-aws Aug 14, 2023
f249adb
Default to reads *
robin-aws Aug 15, 2023
b2b266c
Tweaks
robin-aws Aug 15, 2023
e53422e
Fix iterators (different kind of reads frame)
robin-aws Aug 17, 2023
f1b1657
Avoid reads checks when reads clause is * (not working yet?)
robin-aws Aug 17, 2023
b2b3189
Test todos
robin-aws Aug 17, 2023
46f9367
Fixing check for wildcard, adding etran.WithReads/ModifiesClause()
robin-aws Aug 17, 2023
e94bc0f
Fix null readsFrame bug
robin-aws Aug 17, 2023
e0afd4a
Do reads checks on function by method bodies too
robin-aws Aug 17, 2023
f6dad35
Clean up test file
robin-aws Aug 17, 2023
267acae
Updates to documentation
robin-aws Aug 18, 2023
7518121
Whitespace
robin-aws Aug 18, 2023
4f4ace4
Apply reads clause to other clauses, {:concurrent} checks for empty f…
robin-aws Aug 19, 2023
22d8d4d
Typo fixes, more testing
robin-aws Aug 19, 2023
998b100
Add WithDelayedReadsChecks
robin-aws Aug 19, 2023
37fa445
Fix default values
robin-aws Aug 20, 2023
0a82760
Add ReadsCheckDelayer and apply it to other cases as well
robin-aws Aug 21, 2023
f7be5ed
Several missing calls to Method.Reads, beef up test cases
robin-aws Aug 21, 2023
1a0d6be
Whoops, dropping delayed reads checks statements
robin-aws Aug 21, 2023
38cdbf5
Subclassing and method call checks
robin-aws Aug 21, 2023
a00fc44
Enable reads checks on statements outside of method contexts
robin-aws Aug 22, 2023
0a54826
Trying out defaulting to `reads {}` on ghost methods
robin-aws Aug 22, 2023
22a4867
Lemmas instead of ghost methods
robin-aws Aug 23, 2023
347563e
No reads or checking on lemmas, more LHS fixes, more tests
robin-aws Aug 25, 2023
af497ec
update TODOs
robin-aws Aug 25, 2023
275e56d
Add option to enable, most testing (and reorganize old file tests)
robin-aws Aug 25, 2023
1386c43
More tests
robin-aws Aug 25, 2023
1cb1175
Cloning another test file
robin-aws Aug 25, 2023
0254121
Remaining tests
robin-aws Aug 25, 2023
82a160e
Whitespace and todos
robin-aws Aug 25, 2023
d376bf8
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 25, 2023
ee39edc
Fix function-by-method handling, update test
robin-aws Aug 26, 2023
85f9db2
PR feedback (more to come)
robin-aws Aug 29, 2023
71b0a2f
Merge duplicated code into AddMethodOverrideFrameSubsetChk
robin-aws Aug 29, 2023
5993220
More feedback (especially fixing {:concurrent} w.r.t. default reads!)
robin-aws Aug 29, 2023
96dde55
Address TODO about method specs referring to the set of allocated obj…
robin-aws Aug 29, 2023
b484dae
Mark test inconsistent with function version as expected for now
robin-aws Aug 29, 2023
1f8b12c
Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSu…
robin-aws Aug 30, 2023
79d541a
Update expect files
robin-aws Aug 30, 2023
f16064a
Add “Do” to “WithDelayedReadsChecks”
robin-aws Aug 30, 2023
e27efe4
Reorder {:concurrent} checks
robin-aws Aug 30, 2023
3cdf36e
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 30, 2023
0acef7f
Whitespace
robin-aws Aug 30, 2023
5fcf4a3
Fix reference manual (options and attribute section numbering)
robin-aws Aug 30, 2023
33ac004
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 30, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Source/DafnyCore.Test/ClonerTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public void ClonerKeepsBodyStartTok() {
var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
new List<Formal>(), new List<AttributedExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);

Expand Down
2 changes: 2 additions & 0 deletions Source/DafnyCore/AST/AstVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,8 @@ public virtual void VisitMethod(Method method) {

method.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));

method.Reads.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));

VisitAttributes(method.Mod, method.EnclosingClass.EnclosingModuleDefinition);
method.Mod.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));

Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/AST/BottomUpVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ public void Visit(NewtypeDecl ntd) {
}
public void Visit(Method method) {
Visit(method.Req);
Visit(method.Reads);
Visit(method.Mod.Expressions);
Visit(method.Ens);
Visit(method.Decreases.Expressions);
Expand Down
6 changes: 4 additions & 2 deletions Source/DafnyCore/AST/Members/Constructor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,14 @@ public Constructor(RangeToken rangeToken, Name name,
bool isGhost,
List<TypeParameter> typeArgs,
List<Formal> ins,
List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
List<AttributedExpression> req,
List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
List<AttributedExpression> ens,
Specification<Expression> decreases,
DividedBlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, false, isGhost, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, false, isGhost, typeArgs, ins, new List<Formal>(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand Down
18 changes: 12 additions & 6 deletions Source/DafnyCore/AST/Members/ExtremeLemma.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,14 @@ public ExtremeLemma(RangeToken rangeToken, Name name,
bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
List<TypeParameter> typeArgs,
List<Formal> ins, [Captured] List<Formal> outs,
List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
List<AttributedExpression> req,
List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
List<AttributedExpression> ens,
Specification<Expression> decreases,
BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand All @@ -50,12 +52,14 @@ public LeastLemma(RangeToken rangeToken, Name name,
bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
List<TypeParameter> typeArgs,
List<Formal> ins, [Captured] List<Formal> outs,
List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
List<AttributedExpression> req,
List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
List<AttributedExpression> ens,
Specification<Expression> decreases,
BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand All @@ -78,12 +82,14 @@ public GreatestLemma(RangeToken rangeToken, Name name,
bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
List<TypeParameter> typeArgs,
List<Formal> ins, [Captured] List<Formal> outs,
List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
List<AttributedExpression> req,
List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
List<AttributedExpression> ens,
Specification<Expression> decreases,
BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand Down
4 changes: 0 additions & 4 deletions Source/DafnyCore/AST/Members/Function.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,10 +52,6 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
}

if (Body is not null && HasConcurrentAttribute) {
yield return new Assumption(this, tok, AssumptionDescription.HasConcurrentAttribute);
}

if (HasExternAttribute) {
yield return new Assumption(this, tok, AssumptionDescription.ExternFunction);
if (HasPostcondition && !HasAxiomAttribute) {
Expand Down
9 changes: 6 additions & 3 deletions Source/DafnyCore/AST/Members/Lemma.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,14 @@ public Lemma(RangeToken rangeToken, Name name,
bool hasStaticKeyword,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins, [Captured] List<Formal> outs,
[Captured] List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
[Captured] List<AttributedExpression> req,
[Captured] List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
[Captured] List<AttributedExpression> ens,
[Captured] Specification<Expression> decreases,
[Captured] BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
}

public Lemma(Cloner cloner, Lemma lemma) : base(cloner, lemma) {
Expand All @@ -33,12 +35,13 @@ public TwoStateLemma(RangeToken rangeToken, Name name,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins, [Captured] List<Formal> outs,
[Captured] List<AttributedExpression> req,
[Captured] List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
[Captured] List<AttributedExpression> ens,
[Captured] Specification<Expression> decreases,
[Captured] BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(rangeToken != null);
Contract.Requires(name != null);
Contract.Requires(typeArgs != null);
Expand Down
46 changes: 38 additions & 8 deletions Source/DafnyCore/AST/Members/Method.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,10 @@

namespace Microsoft.Dafny;

public class Method : MemberDecl, TypeParameter.ParentType,
IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanVerify {
public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanVerify {
public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).
Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
Concat(Req).Concat(Ens).Concat(Mod.Expressions);
Concat(Req).Concat(Ens).Concat(Reads).Concat(Mod.Expressions);
public override IEnumerable<INode> PreResolveChildren => Children;

public override string WhatKind => "method";
Expand All @@ -22,6 +21,7 @@ public class Method : MemberDecl, TypeParameter.ParentType,
public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
public readonly List<AttributedExpression> Req;
public readonly List<FrameExpression> Reads;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems to be some duplication between Function and Method that this PR increases, that we could reduce some time.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, but I couldn't see an easy way without a fair bit of refactoring.

public readonly Specification<FrameExpression> Mod;
public readonly List<AttributedExpression> Ens;
public readonly Specification<Expression> Decreases;
Expand All @@ -48,10 +48,6 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
}

if (Body is not null && HasConcurrentAttribute) {
yield return new Assumption(this, tok, AssumptionDescription.HasConcurrentAttribute);
}

if (HasExternAttribute && HasPostcondition && !HasAxiomAttribute) {
yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition);
}
Expand Down Expand Up @@ -79,6 +75,9 @@ public override IEnumerable<Expression> SubExpressions {
foreach (var e in Req) {
yield return e.E;
}
foreach (var e in Reads) {
yield return e.E;
}
foreach (var e in Mod.Expressions) {
yield return e.E;
}
Expand All @@ -97,6 +96,7 @@ void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Ins));
Contract.Invariant(cce.NonNullElements(Outs));
Contract.Invariant(cce.NonNullElements(Req));
Contract.Invariant(cce.NonNullElements(Reads));
Contract.Invariant(Mod != null);
Contract.Invariant(cce.NonNullElements(Ens));
Contract.Invariant(Decreases != null);
Expand All @@ -110,6 +110,7 @@ public Method(Cloner cloner, Method original) : base(cloner, original) {
}

this.Req = original.Req.ConvertAll(cloner.CloneAttributedExpr);
this.Reads = original.Reads.ConvertAll(cloner.CloneFrameExpr);
this.Mod = cloner.CloneSpecFrameExpr(original.Mod);
this.Decreases = cloner.CloneSpecExpr(original.Decreases);
this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr);
Expand All @@ -122,7 +123,9 @@ public Method(RangeToken rangeToken, Name name,
bool hasStaticKeyword, bool isGhost,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins, [Captured] List<Formal> outs,
[Captured] List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
[Captured] List<AttributedExpression> req,
[Captured] List<FrameExpression> reads,
[Captured] Specification<FrameExpression> mod,
[Captured] List<AttributedExpression> ens,
[Captured] Specification<Expression> decreases,
[Captured] BlockStmt body,
Expand All @@ -134,12 +137,14 @@ public Method(RangeToken rangeToken, Name name,
Contract.Requires(cce.NonNullElements(ins));
Contract.Requires(cce.NonNullElements(outs));
Contract.Requires(cce.NonNullElements(req));
Contract.Requires(reads != null);
Contract.Requires(mod != null);
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
this.TypeArgs = typeArgs;
this.Ins = ins;
this.Outs = outs;
this.Reads = reads;
this.Req = req;
this.Mod = mod;
this.Ens = ens;
Expand Down Expand Up @@ -213,6 +218,10 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
formatter.SetAttributedExpressionIndentation(req, indentBefore + formatter.SpaceTab);
}

foreach (var read in Reads) {
formatter.SetFrameExpressionIndentation(read, indentBefore + formatter.SpaceTab);
MikaelMayer marked this conversation as resolved.
Show resolved Hide resolved
}

foreach (var mod in Mod.Expressions) {
formatter.SetFrameExpressionIndentation(mod, indentBefore + formatter.SpaceTab);
}
Expand Down Expand Up @@ -270,6 +279,27 @@ public void Resolve(ModuleResolver resolver) {
resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})");
}

var readsClausesOnMethodsEnabled = resolver.Options.Get(CommonOptionBag.ReadsClausesOnMethods);
// Set the default of `reads *` if reads clauses on methods is enabled and this isn't a lemma.
// Doing it before resolution is a bit easier than adding resolved frame expressions afterwards.
// Note that `reads *` is the right default for backwards-compatibility,
// but we may want to infer a sensible default like decreases clauses instead in the future.
if (readsClausesOnMethodsEnabled && !IsLemmaLike && !Reads.Any()) {
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 (they are allowed to read all memory locations)",
WhatKind);
} else if (!readsClausesOnMethodsEnabled) {
resolver.reporter.Error(MessageSource.Resolver, fe.tok,
"reads clauses on methods are forbidden without the command-line flag `--reads-clauses-on-methods`");
} else if (IsGhost) {
resolver.DisallowNonGhostFieldSpecifiers(fe);
}
}

resolver.ResolveAttributes(Mod, new ResolutionContext(this, false));
foreach (FrameExpression fe in Mod.Expressions) {
resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Modifies, this);
Expand Down
5 changes: 3 additions & 2 deletions Source/DafnyCore/AST/Members/PrefixLemma.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,10 @@ public class PrefixLemma : Method {
public readonly ExtremeLemma ExtremeLemma;
public PrefixLemma(RangeToken rangeToken, Name name, bool hasStaticKeyword,
List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,
List<AttributedExpression> req, Specification<FrameExpression> mod, List<AttributedExpression> ens, Specification<Expression> decreases,
List<AttributedExpression> req, [Captured] List<FrameExpression> reads,
Specification<FrameExpression> mod, List<AttributedExpression> ens, Specification<Expression> decreases,
BlockStmt body, Attributes attributes, ExtremeLemma extremeLemma)
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {
: base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, null) {
Contract.Requires(k != null);
Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k);
Contract.Requires(extremeLemma != null);
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/AST/TopDownVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ public void Visit(ICallable decl, State st) {
public virtual void Visit(Method method, State st) {
Visit(method.Ens, st);
Visit(method.Req, st);
Visit(method.Reads, st);
Visit(method.Mod.Expressions, st);
Visit(method.Decreases.Expressions, st);
if (method.Body != null) { Visit(method.Body, st); }
Expand Down
2 changes: 2 additions & 0 deletions Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -421,6 +421,7 @@ public void Resolve(ModuleResolver resolver) {
var init = new Constructor(rangeToken, new Name(NameNode.RangeToken, "_ctor"), false,
new List<TypeParameter>(), Ins,
new List<AttributedExpression>(),
new List<FrameExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<AttributedExpression>(),
new Specification<Expression>(new List<Expression>(), null),
Expand All @@ -440,6 +441,7 @@ public void Resolve(ModuleResolver resolver) {
new List<TypeParameter>(),
new List<Formal>(), new List<Formal>() { new Formal(tok, "more", Type.Bool, false, false, null) },
new List<AttributedExpression>(),
new List<FrameExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null),
new List<AttributedExpression>(),
new Specification<Expression>(new List<Expression>(), null),
Expand Down
5 changes: 3 additions & 2 deletions Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,8 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary<string, MemberDe
: extremeLemma.Ens.ConvertAll(cloner.CloneAttributedExpr);
extremeLemma.PrefixLemma = new PrefixLemma(extremeLemma.RangeToken, extraName, extremeLemma.HasStaticKeyword,
extremeLemma.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, extremeLemma.Outs.ConvertAll(f => cloner.CloneFormal(f, false)),
req, cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
req, extremeLemma.Reads.ConvertAll(cloner.CloneFrameExpr),
cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
new Specification<Expression>(decr, null),
null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known
cloner.CloneAttributes(extremeLemma.Attributes), extremeLemma);
Expand All @@ -255,7 +256,7 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary<string, MemberDe
extraMember.InheritVisibility(m, false);
members.Add(extraName.Value, extraMember);
} else if (m is Function f && f.ByMethodBody != null) {
ModuleResolver.RegisterByMethod(f, this);
resolver.RegisterByMethod(f, this);
}
} else if (m is Constructor && !((Constructor)m).HasName) {
resolver.reporter.Error(MessageSource.Resolver, m, "More than one anonymous constructor");
Expand Down
Loading