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

Report assertion errors at the assertion keyword #6012

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Report assertion errors at the assertion keyword #6012

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
84ab199
When asserting a condition, do not use just condition's origin as an …
keyboardDrummer Dec 31, 2024
dd54f09
Improve calc handling
keyboardDrummer Dec 31, 2024
503d2a2
Merge remote-tracking branch 'origin/master' into conditionOrigins
keyboardDrummer Jan 2, 2025
c9e601b
Update code and some expect files
keyboardDrummer Jan 2, 2025
35e1252
Merge remote-tracking branch 'origin/master' into conditionOrigins
keyboardDrummer Jan 7, 2025
782a7a6
Change origin of AttributedExpression
keyboardDrummer Jan 7, 2025
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
6 changes: 3 additions & 3 deletions Source/DafnyCore/AST/Cloner.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -353,7 +353,7 @@ public Attributes CloneAttributes(Attributes attrs) {
}

public AttributedExpression CloneAttributedExpr(AttributedExpression expr) {
var mfe = new AttributedExpression(CloneExpr(expr.E),
var mfe = new AttributedExpression(Origin(expr.Origin), CloneExpr(expr.E),
expr.Label == null ? null : new AssertLabel(Origin(expr.Label.Tok), expr.Label.Name),
CloneAttributes(expr.Attributes));
mfe.Attributes = CloneAttributes(expr.Attributes);
Expand Down Expand Up @@ -486,9 +486,9 @@ public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) {
if (op == null) {
return null;
} else if (op is CalcStmt.BinaryCalcOp) {
return new CalcStmt.BinaryCalcOp(((CalcStmt.BinaryCalcOp)op).Op);
return new CalcStmt.BinaryCalcOp(op.Token, ((CalcStmt.BinaryCalcOp)op).Op);
} else if (op is CalcStmt.TernaryCalcOp) {
return new CalcStmt.TernaryCalcOp(CloneExpr(((CalcStmt.TernaryCalcOp)op).Index));
return new CalcStmt.TernaryCalcOp(op.Token, CloneExpr(((CalcStmt.TernaryCalcOp)op).Index));
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
Expand Down
18 changes: 5 additions & 13 deletions Source/DafnyCore/AST/Expressions/AttributedExpression.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,7 @@ void ObjectInvariant() {
Contract.Invariant(E != null);
}

private Attributes attributes;
public Attributes Attributes {
get {
return attributes;
}
set {
attributes = value;
}
}
public Attributes Attributes { get; set; }

string IAttributeBearingDeclaration.WhatKind => "expression";

Expand All @@ -31,15 +23,15 @@ public bool HasAttributes() {
return Attributes != null;
}

public AttributedExpression(Expression e)
: this(e, null) {
public AttributedExpression(IOrigin origin, Expression e)
: this(origin, e, null) {
Contract.Requires(e != null);
}

public AttributedExpression(Expression e, Attributes attrs) : this(e, null, attrs) {
public AttributedExpression(IOrigin origin, Expression e, Attributes attrs) : this(origin, e, null, attrs) {
}

public AttributedExpression(Expression e, AssertLabel/*?*/ label, Attributes attrs) : base(e.Origin) {
public AttributedExpression(IOrigin origin, Expression e, AssertLabel/*?*/ label, Attributes attrs) : base(e.Origin) {
Contract.Requires(e != null);
E = e;
Label = label;
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Members/Function.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -585,7 +585,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies rewriter, Dafn
Body = bodyExpr;

if (Req.Any() || Ens.Any()) {
Req.Insert(0, new AttributedExpression(reqExpr));
Req.Insert(0, new AttributedExpression(Token.NoToken, reqExpr));
}
}

Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Members/Method.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -498,7 +498,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
}

if (Req.Any() || Ens.Any()) {
Req.Insert(0, new AttributedExpression(reqExpr));
Req.Insert(0, new AttributedExpression(Token.NoToken, reqExpr));
}
}

Expand Down
40 changes: 28 additions & 12 deletions Source/DafnyCore/AST/Statements/CalcStmt.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,12 @@ namespace Microsoft.Dafny;

public class CalcStmt : Statement, ICloneable<CalcStmt>, ICanFormat {
public abstract class CalcOp {
public Token Token { get; }

protected CalcOp(Token token) {
this.Token = token;
}

/// <summary>
/// Resulting operator "x op z" if "x this y" and "y other z".
/// Returns null if this and other are incompatible.
Expand Down Expand Up @@ -50,7 +56,7 @@ public static bool LogicOp(BinaryExpr.Opcode op) {
return op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp || op == BinaryExpr.Opcode.Exp;
}

public BinaryCalcOp(BinaryExpr.Opcode op) {
public BinaryCalcOp(Token token, BinaryExpr.Opcode op) : base(token) {
Contract.Requires(ValidOp(op));
Op = op;
}
Expand Down Expand Up @@ -100,11 +106,16 @@ public override CalcOp ResultOp(CalcOp other) {
}

public override Expression StepExpr(Expression line0, Expression line1) {
var token = Token;
if (token == Token.NoToken && line0.EndToken != Token.NoToken) {
token = line0.EndToken.Next;
}
var origin = new SourceOrigin(line0.StartToken, line1.EndToken, token);
if (Op == BinaryExpr.Opcode.Exp) {
// The order of operands is reversed so that it can be turned into implication during resolution
return new BinaryExpr(new AutoGeneratedOrigin(line0.Origin), Op, line1, line0);
return new BinaryExpr(origin, Op, line1, line0);
} else {
return new BinaryExpr(new AutoGeneratedOrigin(line0.Origin), Op, line0, line1);
return new BinaryExpr(origin, Op, line0, line1);
}
}

Expand All @@ -122,7 +133,7 @@ void ObjectInvariant() {
Contract.Invariant(Index != null);
}

public TernaryCalcOp(Expression idx) {
public TernaryCalcOp(Token token, Expression idx) : base(token) {
Contract.Requires(idx != null);
Index = idx;
}
Expand All @@ -137,15 +148,20 @@ public override CalcOp ResultOp(CalcOp other) {
var a = Index;
var b = ((TernaryCalcOp)other).Index;
var minIndex = new ITEExpr(a.Origin, false, new BinaryExpr(a.Origin, BinaryExpr.Opcode.Le, a, b), a, b);
return new TernaryCalcOp(minIndex); // ToDo: if we could compare expressions for syntactic equality, we could use this here to optimize
return new TernaryCalcOp(Token.NoToken, minIndex); // ToDo: if we could compare expressions for syntactic equality, we could use this here to optimize
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
}
}

public override Expression StepExpr(Expression line0, Expression line1) {
return new TernaryExpr(new AutoGeneratedOrigin(line0.Origin), TernaryExpr.Opcode.PrefixEqOp, Index, line0, line1);
var token = Token;
if (token == Token.NoToken && line0.EndToken != Token.NoToken) {
token = line0.EndToken.Next;
}
var origin = new SourceOrigin(line0.StartToken, line1.EndToken, token);
return new TernaryExpr(origin, TernaryExpr.Opcode.PrefixEqOp, Index, line0, line1);
}

public override string ToString() {
Expand Down Expand Up @@ -173,13 +189,13 @@ public CalcOp GetInferredDefaultOp() {
}

if (Expression.IsBoolLiteral(Lines.First(), out var firstOperatorIsBoolLiteral)) {
alternativeOp = new BinaryCalcOp(firstOperatorIsBoolLiteral ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.Exp);
alternativeOp = new BinaryCalcOp(Token.NoToken, firstOperatorIsBoolLiteral ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.Exp);
} else if (Expression.IsBoolLiteral(Lines.Last(), out var lastOperatorIsBoolLiteral)) {
alternativeOp = new BinaryCalcOp(lastOperatorIsBoolLiteral ? BinaryExpr.Opcode.Exp : BinaryExpr.Opcode.Imp);
alternativeOp = new BinaryCalcOp(Token.NoToken, lastOperatorIsBoolLiteral ? BinaryExpr.Opcode.Exp : BinaryExpr.Opcode.Imp);
} else if (Expression.IsEmptySetOrMultiset(Lines.First())) {
alternativeOp = new BinaryCalcOp(BinaryExpr.Opcode.Ge);
alternativeOp = new BinaryCalcOp(Token.NoToken, BinaryExpr.Opcode.Ge);
} else if (Expression.IsEmptySetOrMultiset(Lines.Last())) {
alternativeOp = new BinaryCalcOp(BinaryExpr.Opcode.Le);
alternativeOp = new BinaryCalcOp(Token.NoToken, BinaryExpr.Opcode.Le);
} else {
return null;
}
Expand All @@ -202,10 +218,10 @@ public CalcOp GetInferredDefaultOp() {
public readonly List<CalcOp/*?*/> StepOps; // StepOps[i] comes after line i
[FilledInDuringResolution]
public CalcOp Op; // main operator of the calculation (either UserSuppliedOp or (after resolution) an inferred CalcOp)
[FilledInDuringResolution] public readonly List<Expression> Steps; // expressions li op l<i + 1> (last step is dummy)
[FilledInDuringResolution] public readonly List<Expression> Steps; // expressions l<i> op l<i + 1> (last step is dummy)
[FilledInDuringResolution] public Expression Result; // expression l0 ResultOp ln

public static readonly CalcOp DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq);
public static readonly CalcOp DefaultOp = new BinaryCalcOp(Token.NoToken, BinaryExpr.Opcode.Eq);

public override IEnumerable<INode> Children => Steps.Concat(Result != null ? new Node[] { Result } : new Node[] { }).Concat(Hints);
public override IEnumerable<INode> PreResolveChildren => Lines.Take(Lines.Count > 0 ? Lines.Count - 1 : 0).Concat<Node>(Hints.Where(hintBatch => hintBatch.Body.Count() != 0));
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/AST/Substituter.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -941,7 +941,7 @@ protected GuardedAlternative SubstGuardedAlternative(GuardedAlternative alt) {

protected AttributedExpression SubstMayBeFreeExpr(AttributedExpression expr) {
Contract.Requires(expr != null);
var mfe = new AttributedExpression(Substitute(expr.E));
var mfe = new AttributedExpression(expr.Origin, Substitute(expr.E));
mfe.Attributes = SubstAttributes(expr.Attributes);
return mfe;
}
Expand Down Expand Up @@ -994,9 +994,9 @@ protected CalcStmt.CalcOp SubstCalcOp(CalcStmt.CalcOp op) {
if (op == null) {
return null;
} else if (op is CalcStmt.BinaryCalcOp) {
return new CalcStmt.BinaryCalcOp(((CalcStmt.BinaryCalcOp)op).Op);
return new CalcStmt.BinaryCalcOp(op.Token, ((CalcStmt.BinaryCalcOp)op).Op);
} else if (op is CalcStmt.TernaryCalcOp) {
return new CalcStmt.TernaryCalcOp(Substitute(((CalcStmt.TernaryCalcOp)op).Index));
return new CalcStmt.TernaryCalcOp(op.Token, Substitute(((CalcStmt.TernaryCalcOp)op).Index));
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
Expand Down
28 changes: 14 additions & 14 deletions Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -201,27 +201,27 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) {
var ens = Member_Init.Ens;
foreach (var p in Ins) {
// ensures this.x == x;
ens.Add(new AttributedExpression(new BinaryExpr(p.Origin, BinaryExpr.Opcode.Eq,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(p.Origin, BinaryExpr.Opcode.Eq,
new ExprDotName(p.Origin, new ThisExpr(p.Origin), p.NameNode, null), new IdentifierExpr(p.Origin, p.Name))));
}
foreach (var p in OutsHistoryFields) {
// ensures this.ys == [];
ens.Add(new AttributedExpression(new BinaryExpr(p.Origin, BinaryExpr.Opcode.Eq,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(p.Origin, BinaryExpr.Opcode.Eq,
new ExprDotName(p.Origin, new ThisExpr(p.Origin), p.NameNode, null), new SeqDisplayExpr(p.Origin, new List<Expression>()))));
}
// ensures this.Valid();
var valid_call = AutoContractsRewriter.CreateUnresolvedValidCall(tok);
ens.Add(new AttributedExpression(valid_call));
ens.Add(new AttributedExpression(Token.NoToken, valid_call));
AddConstructorFramePostconditions(tok, ens, resolver);
// ensures this._new == {};
ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null),
new SetDisplayExpr(tok, true, new List<Expression>()))));
// ensures this._decreases0 == old(DecreasesClause[0]) && ...;
Contract.Assert(Decreases.Expressions.Count == DecreasesFields.Count);
for (int i = 0; i < Decreases.Expressions.Count; i++) {
var p = Decreases.Expressions[i];
ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
new ExprDotName(tok, new ThisExpr(tok), DecreasesFields[i].NameNode, null),
new OldExpr(tok, p))));
}
Expand All @@ -236,7 +236,7 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) {
// requires this.Valid();
var req = Member_MoveNext.Req;
valid_call = AutoContractsRewriter.CreateUnresolvedValidCall(tok);
req.Add(new AttributedExpression(valid_call));
req.Add(new AttributedExpression(Token.NoToken, valid_call));
// requires YieldRequires;
req.AddRange(YieldRequires);
// modifies this, this._modifies, this._new;
Expand All @@ -246,17 +246,17 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) {
mod.Add(new FrameExpression(tok, new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null), null));
// ensures fresh(_new - old(_new));
ens = Member_MoveNext.Ens;
ens.Add(new AttributedExpression(new FreshExpr(tok,
ens.Add(new AttributedExpression(Token.NoToken, new FreshExpr(tok,
new BinaryExpr(tok, BinaryExpr.Opcode.Sub,
new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null),
new OldExpr(tok, new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null))))));
// ensures null !in _new
ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.NotIn,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.NotIn,
new LiteralExpr(tok),
new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null))));
// ensures more ==> this.Valid();
valid_call = AutoContractsRewriter.CreateUnresolvedValidCall(tok);
ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Imp,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Imp,
new IdentifierExpr(tok, "more"),
valid_call)));
// ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys);
Expand All @@ -270,17 +270,17 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) {
new SeqDisplayExpr(tok, new List<Expression>() { new ExprDotName(tok, new ThisExpr(tok), y.NameNode, null) })),
new OldExpr(tok, new ExprDotName(tok, new ThisExpr(tok), ys.NameNode, null)));
var eq = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new ExprDotName(tok, new ThisExpr(tok), ys.NameNode, null), ite);
ens.Add(new AttributedExpression(eq));
ens.Add(new AttributedExpression(Token.NoToken, eq));
}
// ensures more ==> YieldEnsures;
foreach (var ye in YieldEnsures) {
ens.Add(new AttributedExpression(
ens.Add(new AttributedExpression(Token.NoToken,
new BinaryExpr(tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(tok, "more"), ye.E)
));
}
// ensures !more ==> Ensures;
foreach (var e in Ensures) {
ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Imp,
ens.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Imp,
new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Not, new IdentifierExpr(tok, "more")),
e.E)
));
Expand Down Expand Up @@ -314,7 +314,7 @@ private void AddConstructorFramePostconditions(AutoGeneratedOrigin tok, List<Att
frameSet = new BinaryExpr(fr.Origin, BinaryExpr.Opcode.Add, frameSet, fr.E);
}
}
iteratorCtorEnsures.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
iteratorCtorEnsures.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
new ExprDotName(tok, new ThisExpr(tok), new Name("_reads"), null),
new OldExpr(tok, frameSet))));

Expand All @@ -331,7 +331,7 @@ private void AddConstructorFramePostconditions(AutoGeneratedOrigin tok, List<Att
frameSet = new BinaryExpr(fr.Origin, BinaryExpr.Opcode.Add, frameSet, fr.E);
}
}
iteratorCtorEnsures.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
iteratorCtorEnsures.Add(new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Eq,
new ExprDotName(tok, new ThisExpr(tok), new Name("_modifies"), null),
new OldExpr(tok, frameSet))));
}
Expand Down
12 changes: 7 additions & 5 deletions Source/DafnyCore/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1299,17 +1299,18 @@ RequiresClause<.List<AttributedExpression> req, bool allowLabel.>
LabelName<out lbl> ":"
]
Expression<out e, false, false>
OldSemi (. req.Add(new AttributedExpression(e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); .)
OldSemi (. req.Add(new AttributedExpression(new SourceOrigin(t, e.EndToken), e, lbl == null ? null : new AssertLabel(lbl, lbl.val), attrs)); .)
.

/*------------------------------------------------------------------------*/
EnsuresClause<.List<AttributedExpression> ens, bool allowLambda.>
= "ensures" (. Expression e;
Token start = t;
Attributes attrs = null;
.)
{ Attribute<ref attrs> }
Expression<out e, false, allowLambda>
OldSemi (. ens.Add(new AttributedExpression(e, attrs)); .)
OldSemi (. ens.Add(new AttributedExpression(new SourceOrigin(start, e.EndToken), e, attrs)); .)
.

/*------------------------------------------------------------------------*/
Expand Down Expand Up @@ -1354,9 +1355,10 @@ ReadsClause<.List<FrameExpression/*!*/>/*!*/ reads, ref Attributes attrs,
InvariantClause<. List<AttributedExpression> invariants.> =
"invariant" (. Attributes attrs = null;
Expression e;
Token start = t;
.)
{ Attribute<ref attrs> }
Expression<out e, false, true> (. invariants.Add(new AttributedExpression(e, attrs)); .)
Expression<out e, false, true> (. invariants.Add(new AttributedExpression(new SourceOrigin(t, e.EndToken), e, attrs)); .)
OldSemi
.

Expand Down Expand Up @@ -3254,9 +3256,9 @@ CalcOp<out Token x, out CalcStmt.CalcOp/*!*/ op>
)
(.
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(x, binOp);
} else {
op = new Microsoft.Dafny.CalcStmt.TernaryCalcOp(k);
op = new Microsoft.Dafny.CalcStmt.TernaryCalcOp(x, k);
}
.)
.
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/Resolver/ModuleResolver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -784,7 +784,7 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) {
new ExprDotName(tok, receiver, f.NameNode, f.TypeArgs.ConvertAll(typeParameter => (Type)new UserDefinedType(f.Origin, typeParameter))),
new ActualBindings(f.Ins.ConvertAll(Expression.CreateIdentExpr)).ArgumentBindings,
Token.NoToken);
var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn));
var post = new AttributedExpression(Token.NoToken, new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn));
Specification<FrameExpression> reads;
if (Options.Get(Method.ReadsClausesOnMethods)) {
// If f.Reads is empty, replace it with an explicit `reads {}` so that we don't replace that
Expand Down Expand Up @@ -1695,7 +1695,7 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
var subst = new ExtremeLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.Origin, k.Name),
this.reporter, true);
var post = subst.CloneExpr(p.E);
prefixLemma.Ens.Add(new AttributedExpression(post));
prefixLemma.Ens.Add(new AttributedExpression(Token.NoToken, post));
foreach (var e in coConclusions) {
if (e is FunctionCallExpr fce) {
GreatestPredicate predicate = (GreatestPredicate)fce.Function;
Expand All @@ -1722,7 +1722,7 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
var subst = new ExtremeLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.Origin, k.Name),
this.reporter, false);
var pre = subst.CloneExpr(p.E);
prefixLemma.Req.Add(new AttributedExpression(pre, p.Label, null));
prefixLemma.Req.Add(new AttributedExpression(Token.NoToken, pre, p.Label, null));
foreach (var e in antecedents) {
var fce = (FunctionCallExpr)e; // we expect "antecedents" to contain only FunctionCallExpr's
LeastPredicate predicate = (LeastPredicate)fce.Function;
Expand Down
Loading
Loading