diff --git a/Source/DafnyCore/Compilers/Compiler-js.cs b/Source/DafnyCore/Compilers/Compiler-js.cs
index 1620a0e8ba8..335692e9041 100644
--- a/Source/DafnyCore/Compilers/Compiler-js.cs
+++ b/Source/DafnyCore/Compilers/Compiler-js.cs
@@ -2535,9 +2535,9 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str
var psi = new ProcessStartInfo("node", "") {
RedirectStandardInput = true,
- StandardInputEncoding = Encoding.UTF8,
RedirectStandardOutput = true,
RedirectStandardError = true,
+ StandardInputEncoding = Encoding.UTF8,
};
try {
diff --git a/Source/DafnyCore/Compilers/Compiler-python.cs b/Source/DafnyCore/Compilers/Compiler-python.cs
index 8003b3db6ad..ff46268dd83 100644
--- a/Source/DafnyCore/Compilers/Compiler-python.cs
+++ b/Source/DafnyCore/Compilers/Compiler-python.cs
@@ -1768,10 +1768,7 @@ private static string FindModuleName(string externFilename) {
}
}
rd.Close();
- if (externFilename.EndsWith(".py")) {
- return externFilename.Substring(0, externFilename.Length - 3);
- }
- return null;
+ return externFilename.EndsWith(".py") ? externFilename[..^3] : null;
}
static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {
diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
index be765714d9b..db582f56305 100644
--- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
+++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs
@@ -3,26 +3,26 @@
namespace Microsoft.Dafny {
public class FunctionCallSubstituter : Substituter {
public readonly Function A, B;
- public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Function a, Function b)
- : base(receiverReplacement, substMap, new Dictionary()) {
+ public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary typeMap, Function a, Function b)
+ : base(receiverReplacement, substMap, typeMap) {
A = a;
B = b;
}
public override Expression Substitute(Expression expr) {
- if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
- Expression receiver = Substitute(e.Receiver);
- List newArgs = SubstituteExprList(e.Args);
- FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
- if (e.Function == A) {
+ if (expr is FunctionCallExpr e) {
+ var receiver = Substitute(e.Receiver);
+ var newArgs = SubstituteExprList(e.Args);
+ var newFce = new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel);
+ if (e.Function == A && e.Receiver is ThisExpr && receiver is ThisExpr) {
newFce.Function = B;
newFce.Type = e.Type; // TODO: this may not work with type parameters.
+ receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass);
} else {
newFce.Function = e.Function;
newFce.Type = e.Type;
}
- newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here
- newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here
+ newFce.TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass); // resolve here
+ newFce.TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction); // resolve here
newFce.IsByMethodCall = e.IsByMethodCall;
return newFce;
}
diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
index 10c96e1a5c3..6ccb0204787 100644
--- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
+++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
@@ -213,7 +213,8 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To
AddWellformednessCheck(cf);
if (InVerificationScope(cf)) {
var etran = new ExpressionTranslator(this, predef, f.tok);
- heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight());
+ var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf);
+ heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
}
}
@@ -877,8 +878,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
}
// the procedure itself
var req = new List();
- // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
- req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null));
+ // free requires fh == FunctionContextHeight;
+ req.Add(Requires(f.tok, true, etran.HeightContext(f, true), null, null));
if (f is TwoStateFunction) {
// free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
@@ -920,18 +921,16 @@ private void AddFunctionOverrideCheckImpl(Function f) {
}
var substMap = new Dictionary();
- for (int i = 0; i < f.Formals.Count; i++) {
- //get corresponsing formal in the class
- var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f.IdGenerator));
- ie.Var = f.Formals[i]; ie.Type = ie.Var.Type;
- substMap.Add(f.OverriddenFunction.Formals[i], ie);
+ foreach (var (formal, overriddenFormal) in f.Formals.Zip(f.OverriddenFunction.Formals, Tuple.Create)) {
+ // get corresponding formal in the class
+ var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type };
+ substMap.Add(overriddenFormal, ie);
}
if (f.OverriddenFunction.Result != null) {
Contract.Assert(pOut != null);
- //get corresponsing formal in the class
- var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator));
- ie.Var = pOut; ie.Type = ie.Var.Type;
+ // get corresponding formal in the class
+ var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type };
substMap.Add(f.OverriddenFunction.Result, ie);
}
@@ -946,8 +945,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
//adding assert W <= Frame’
AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);
- //adding assume Q; assert Post’;
- //adding assume J.F(ins) == C.F(ins);
+ //adding assume Q;
+ //assert Post’;
AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]);
var stmts = builder.Collect(f.tok);
@@ -1134,7 +1133,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti
// The axiom
Boogie.Expr ax = BplForall(f.tok, new List(), forallFormals, null, tr,
Boogie.Expr.Imp(Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype), synonyms));
- var activate = AxiomActivation(f, etran);
+ var activate = AxiomActivation(overridingFunction, etran, true);
string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName;
return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment);
}
diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
index d4e5a6ededf..35c1b85f727 100644
--- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
+++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs
@@ -258,12 +258,11 @@ public Boogie.IdentifierExpr FunctionContextHeight() {
return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int);
}
- public Boogie.Expr HeightContext(ICallable m) {
+ public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) {
Contract.Requires(m != null);
// free requires fh == FunctionContextHeight;
- var module = m.EnclosingModule;
- Boogie.Expr context =
- Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight());
+ var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m);
+ Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight());
return context;
}
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 426863fff9d..4adeb7b2324 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -2054,7 +2054,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
// (mh == ModuleContextHeight && fh <= FunctionContextHeight)
//
// USE_VIA_CONTEXT
- // (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
+ // fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2157,10 +2157,9 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
foreach (AttributedExpression req in f.Req) {
pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap)));
}
- // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
- var mod = f.EnclosingClass.EnclosingModuleDefinition;
- Bpl.Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True :
- (Bpl.Expr)Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
+ // useViaContext: fh < FunctionContextHeight
+ var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f.OverriddenFunction ?? f);
+ Expr useViaContext = Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
// useViaCanCall: f#canCall(args)
Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
@@ -2255,15 +2254,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
return (olderParameterCount, olderCondition);
}
- Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) {
+ Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) {
Contract.Requires(f != null);
Contract.Requires(etran != null);
Contract.Requires(VisibleInScope(f));
- var module = f.EnclosingClass.EnclosingModuleDefinition;
if (InVerificationScope(f)) {
- return
- Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
+ var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
+ return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight());
} else {
return Bpl.Expr.True;
}
@@ -2303,7 +2301,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) {
// for visibility==ForeignModuleOnly, means:
// GOOD_PARAMETERS
// for visibility==IntraModuleOnly, means:
- // fh != FunctionContextHeight &&
+ // fh < FunctionContextHeight &&
// GOOD_PARAMETERS
// where GOOD_PARAMETERS means:
// $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2508,12 +2506,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) {
return null;
}
- // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
- ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
+ // useViaContext: fh < FunctionContextHeight
+ var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
Bpl.Expr useViaContext = !InVerificationScope(f)
- ? (Bpl.Expr)Bpl.Expr.True
- : Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)),
- etran.FunctionContextHeight());
+ ? Bpl.Expr.True
+ : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
// ante := (useViaContext && typeAnte && pre)
ante = BplAnd(useViaContext, BplAnd(ante, pre));
@@ -3483,65 +3480,42 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E)));
}
- //generating assume J.F(ins) == C.F(ins)
- Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
- Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
- List argsC = new List();
- List argsT = new List();
- // add type arguments
- argsT.AddRange(GetTypeArguments(f.OverriddenFunction, f).ConvertAll(TypeToTy));
- argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
- // add fuel arguments
- if (f.IsFuelAware()) {
- argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
- }
- if (f.OverriddenFunction.IsFuelAware()) {
- argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));
- }
- // add heap arguments
- if (f is TwoStateFunction) {
- argsC.Add(etran.Old.HeapExpr);
- argsT.Add(etran.Old.HeapExpr);
- }
- if (AlwaysUseHeap || f.ReadsHeap) {
- argsC.Add(etran.HeapExpr);
- }
- if (AlwaysUseHeap || f.OverriddenFunction.ReadsHeap) {
- argsT.Add(etran.HeapExpr);
- }
- // add "ordinary" parameters (including "this", if any)
- var prefixCount = implInParams.Count - f.Formals.Count;
- for (var i = 0; i < implInParams.Count; i++) {
- Bpl.Expr cParam = new Bpl.IdentifierExpr(f.tok, implInParams[i]);
- Bpl.Expr tParam = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, implInParams[i]);
- if (prefixCount <= i && ModeledAsBoxType(f.OverriddenFunction.Formals[i - prefixCount].Type)) {
- tParam = BoxIfNecessary(f.tok, tParam, f.Formals[i - prefixCount].Type);
- }
- argsC.Add(cParam);
- argsT.Add(tParam);
- }
- Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
- Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
- var funcExpCPossiblyBoxed = funcExpC;
- if (ModeledAsBoxType(f.OverriddenFunction.ResultType)) {
- funcExpCPossiblyBoxed = BoxIfUnboxed(funcExpCPossiblyBoxed, f.ResultType);
- }
- builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpCPossiblyBoxed, funcExpT)));
-
//generating assume C.F(ins) == out, if a result variable was given
if (resultVariable != null) {
+ var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
+ var argsC = new List();
+
+ // add type arguments
+ argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
+
+ // add fuel arguments
+ if (f.IsFuelAware()) {
+ argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));
+ }
+
+ // add heap arguments
+ if (f is TwoStateFunction) {
+ argsC.Add(etran.Old.HeapExpr);
+ }
+ if (AlwaysUseHeap || f.ReadsHeap) {
+ argsC.Add(etran.HeapExpr);
+ }
+
+ argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var)));
+
+ var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable);
builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar)));
}
//generating trait post-conditions with class variables
foreach (var en in f.OverriddenFunction.Ens) {
- Expression postcond = Substitute(en.E, null, substMap, typeMap);
- bool splitHappened; // we don't actually care
- foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) {
- if (s.IsChecked) {
- builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
- }
+ // We replace all occurrences of the trait version of the function with the class version. This is only allowed
+ // if the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
+ // expressions that evaluate to one.
+ var sub = new FunctionCallSubstituter(null, substMap, typeMap, f.OverriddenFunction, f);
+ foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
+ builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
}
}
}
@@ -4765,7 +4739,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) {
Contract.Requires(predef != null);
Contract.Ensures(Contract.Result() != null);
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {
+ if (expr is LiteralExpr or ThisExpr or IdentifierExpr or WildcardExpr or BoogieWrapper) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -10752,6 +10726,14 @@ List MkTyParamFormals(List args, bool includeWhereClaus
return null;
}
+ // We use the $FunctionContextHeight to restrict the applicability of certain axioms. The entity at the end of a
+ // dependency chain has the highest number. To get more granular control over the visibility, we extend every
+ // visibility level by a precursory intermediate level. This additional level is helpful for proofs that would be
+ // disturbed by axioms that are visible the the final level.
+ static Bpl.Expr MkFunctionHeight(int visibilityLevel, bool intermediateScope = false) {
+ return Expr.Literal(visibilityLevel * 2 + (intermediateScope ? 0 : 1));
+ }
+
public static void MapM(IEnumerable xs, Action K) {
Contract.Requires(xs != null);
Contract.Requires(K != null);
diff --git a/Test/concurrency/10-SequenceInvariant.dfy b/Test/concurrency/10-SequenceInvariant.dfy
index 09f540e7947..4bd942e9e2c 100644
--- a/Test/concurrency/10-SequenceInvariant.dfy
+++ b/Test/concurrency/10-SequenceInvariant.dfy
@@ -256,7 +256,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
@@ -322,7 +322,7 @@ trait OwnedObject extends Object {
assert owner in universe.content;
}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& localUserInv()
}
diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy
index 07d8ed4a8bc..c1927624ef4 100644
--- a/Test/concurrency/11-MutexGuard2.dfy
+++ b/Test/concurrency/11-MutexGuard2.dfy
@@ -261,7 +261,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
@@ -332,7 +332,7 @@ trait OwnedObject extends Object {
&& unchangedNonvolatileUserFields()
}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& localUserInv()
}
diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy
index cb1b97ccbf6..18fba5266c5 100644
--- a/Test/concurrency/12-MutexLifetime-short.dfy
+++ b/Test/concurrency/12-MutexLifetime-short.dfy
@@ -365,7 +365,7 @@ class Thread extends Object {
}
twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
}
predicate inv() reads * ensures inv() ==> localInv() {
@@ -439,7 +439,7 @@ trait OwnedObject extends Object {
&& unchangedNonvolatileUserFields()
}
- predicate localInv() reads * {
+ predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() {
&& objectGlobalBaseInv()
&& this in lifetime.elements
&& (lifetime.alive() ==> owner != null)
diff --git a/Test/dafny4/git-issue245.dfy b/Test/dafny4/git-issue245.dfy
index 187cef8bc42..a5458a2cd7c 100644
--- a/Test/dafny4/git-issue245.dfy
+++ b/Test/dafny4/git-issue245.dfy
@@ -37,23 +37,23 @@ class C extends T {
{ 5 + y }
}
-// class D is like C, but in each case, the spec is NOT weaker than that in T
+// class D is like C, but in each case, the spec is NOT stronger than that in T
class D extends T {
// d does not name the result in either trait or class
function method d(y: nat): nat
- ensures d(y) < 20 + y // error: specification is not weaker
+ ensures d(y) < 20 + y // error: specification is not stronger
{ 11 + y }
// f names the result in both trait and class
function method f(y: nat): (result: nat)
- ensures result < 20 + y // error: specification is not weaker
+ ensures result < 20 + y // error: specification is not stronger
{ 11 + y }
// g names the result in just the class
function method g(y: nat): (result: nat)
- ensures result < 20 + y // error: specification is not weaker
+ ensures result < 20 + y // error: specification is not stronger
{ 11 + y }
// h names the result in just the trait
function method h(y: nat): nat
- ensures h(y) < 20 + y // error: specification is not weaker
+ ensures h(y) < 20 + y // error: specification is not stronger
{ 11 + y }
}
@@ -62,19 +62,19 @@ class D extends T {
class E extends T {
// d does not name the result in either trait or class
function method d(y: nat): nat
- ensures d(y) < 20 + y
+ ensures d(y) < 20 + y // error: specification is not stronger
{ 5 + y }
// f names the result in both trait and class
function method f(y: nat): (result: nat)
- ensures result < 20 + y
+ ensures result < 20 + y // error: specification is not stronger
{ 5 + y }
// g names the result in just the class
function method g(y: nat): (result: nat)
- ensures result < 20 + y
+ ensures result < 20 + y // error: specification is not stronger
{ 5 + y }
// h names the result in just the trait
function method h(y: nat): nat
- ensures h(y) < 20 + y
+ ensures h(y) < 20 + y // error: specification is not stronger
{ 5 + y }
}
diff --git a/Test/dafny4/git-issue245.dfy.expect b/Test/dafny4/git-issue245.dfy.expect
index f154a354f05..52dc0dd66b2 100644
--- a/Test/dafny4/git-issue245.dfy.expect
+++ b/Test/dafny4/git-issue245.dfy.expect
@@ -2,6 +2,10 @@ git-issue245.dfy(43,18): Error: the function must provide an equal or more detai
git-issue245.dfy(47,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
git-issue245.dfy(51,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
git-issue245.dfy(55,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(64,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(68,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(72,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue245.dfy(76,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait
git-issue245.dfy(84,18): Error: A postcondition might not hold on this return path.
git-issue245.dfy(85,17): Related location: This is the postcondition that might not hold.
git-issue245.dfy(88,18): Error: A postcondition might not hold on this return path.
@@ -11,4 +15,4 @@ git-issue245.dfy(93,19): Related location: This is the postcondition that might
git-issue245.dfy(96,18): Error: A postcondition might not hold on this return path.
git-issue245.dfy(97,17): Related location: This is the postcondition that might not hold.
-Dafny program verifier finished with 28 verified, 8 errors
+Dafny program verifier finished with 24 verified, 12 errors
diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy
new file mode 100644
index 00000000000..0066c9df862
--- /dev/null
+++ b/Test/git-issues/git-issue-2500.dfy
@@ -0,0 +1,29 @@
+// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M {
+ trait {:termination false} Tr {
+ function True(): (ret: bool) ensures ret
+ function True'(): (ret: bool) ensures True'()
+ function ActuallyTrue(): (ret: bool) ensures var alsoThis := this; alsoThis.ActuallyTrue()
+ function Other(x:nat, free: Tr): bool
+ ensures x != 0 && free.Other(x-1, free) ==> Other(x-1, free)
+ }
+}
+
+class Class extends M.Tr {
+ function True(): (ret: bool)
+ // Missing: ensures ret
+ { false }
+ function True'(): (ret: bool)
+ // Missing: ensures True'()
+ { false }
+ function ActuallyTrue(): (ret: bool)
+ // This is logically correct, but the disguised receiver in the Tr spec prevents the override check from passing.
+ ensures ActuallyTrue()
+ { true }
+ function Other(x: nat, free: M.Tr): bool
+ // Different receiver
+ ensures x != 0 && Other(x-1, free) ==> Other(x-1, free)
+ { false }
+}
diff --git a/Test/git-issues/git-issue-2500.dfy.expect b/Test/git-issues/git-issue-2500.dfy.expect
new file mode 100644
index 00000000000..6b05539973a
--- /dev/null
+++ b/Test/git-issues/git-issue-2500.dfy.expect
@@ -0,0 +1,6 @@
+git-issue-2500.dfy(15,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(18,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(21,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+git-issue-2500.dfy(25,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+
+Dafny program verifier finished with 6 verified, 4 errors
diff --git a/docs/dev/news/3223.fix b/docs/dev/news/3223.fix
new file mode 100644
index 00000000000..96e3176bae2
--- /dev/null
+++ b/docs/dev/news/3223.fix
@@ -0,0 +1 @@
+To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now.