diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl index 579eede1e33..60740d59b63 100644 --- a/Source/DafnyCore/DafnyPrelude.bpl +++ b/Source/DafnyCore/DafnyPrelude.bpl @@ -589,9 +589,9 @@ function {:inline} _System.real.Floor(x: real): int { Int(x) } // --------------------------------------------------------------- // -- The heap --------------------------------------------------- // --------------------------------------------------------------- -type Heap = [ref][Field alpha]alpha; -function {:inline} read(H:Heap, r:ref, f:Field alpha): alpha { H[r][f] } -function {:inline} update(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r := H[r][f := v]] } +type Heap = [ref][Field alpha]Box; +function {:inline} read(H: Heap, r: ref, f: Field alpha) : alpha { $Unbox(H[r][f]) } +function {:inline} update(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r := H[r][f := $Box(v)]] } function $IsGoodHeap(Heap): bool; function $IsHeapAnchor(Heap): bool; @@ -649,7 +649,7 @@ procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box); procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box)) returns (s: Set Box); ensures (forall bx: Box :: { s[bx] } s[bx] <==> - read(newHeap, this, NW)[bx] || + (read(newHeap, this, NW) : Set Box)[bx] || ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc))); // --------------------------------------------------------------- diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 991a1fe7a79..81f200b828b 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -323,7 +323,7 @@ private void AddInstanceFieldAllocationAxioms(Bpl.Declaration fieldDeclaration, } } else if (f.IsMutable) { // generate h[o,f] - oDotF = ReadHeap(c.tok, h, o, new Bpl.IdentifierExpr(c.tok, GetField(f))); + oDotF = ReadHeap(c.tok, h, o, new Bpl.IdentifierExpr(c.tok, GetField(f)), TrType(f.Type)); bvsTypeAxiom.Add(hVar); bvsTypeAxiom.Add(oVar); bvsAllocationAxiom.Add(hVar); diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index 4d3579cfcb4..bff021ebe47 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -439,8 +439,9 @@ public Boogie.Expr TrExpr(Expression expr) { return e.MemberSelectCase( field => { var useSurrogateLocal = translator.inBodyInitContext && Expression.AsThis(e.Obj) != null && !field.IsInstanceIndependentConstant; + var fType = translator.TrType(field.Type); if (useSurrogateLocal) { - return new Boogie.IdentifierExpr(GetToken(expr), translator.SurrogateName(field), translator.TrType(field.Type)); + return new Boogie.IdentifierExpr(GetToken(expr), translator.SurrogateName(field), fType); } else if (field is ConstantField) { var typeMap = e.TypeArgumentSubstitutionsWithParents(); var args = GetTypeParams(field.EnclosingClass).ConvertAll(tp => translator.TypeToTy(typeMap[tp])); @@ -458,7 +459,7 @@ public Boogie.Expr TrExpr(Expression expr) { Boogie.Expr obj = TrExpr(e.Obj); Boogie.Expr result; if (field.IsMutable) { - result = ReadHeap(GetToken(expr), HeapExpr, obj, new Boogie.IdentifierExpr(GetToken(expr), translator.GetField(field))); + result = ReadHeap(GetToken(expr), HeapExpr, obj, new Boogie.IdentifierExpr(GetToken(expr), translator.GetField(field)), fType); return translator.CondApplyUnbox(GetToken(expr), result, field.Type, expr.Type); } else { result = new Boogie.NAryExpr(GetToken(expr), new Boogie.FunctionCall(translator.GetReadonlyField(field)), @@ -1709,42 +1710,6 @@ public Boogie.Expr BoxIfNecessary(IToken tok, Boogie.Expr e, Type fromType) { return translator.BoxIfNecessary(tok, e, fromType); } - public static Boogie.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { - Contract.Requires(tok != null); - Contract.Requires(heap != null); - Contract.Requires(r != null); - Contract.Requires(f != null); - Contract.Ensures(Contract.Result() != null); - - List args = new List(); - args.Add(heap); - args.Add(r); - args.Add(f); - Boogie.Type t = (f.Type != null) ? f.Type : f.ShallowType; - return new Boogie.NAryExpr(tok, - new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])), - args); - } - - - public static Boogie.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v) { - Contract.Requires(tok != null); - Contract.Requires(heap != null); - Contract.Requires(r != null); - Contract.Requires(f != null); - Contract.Requires(v != null); - Contract.Ensures(Contract.Result() != null); - - List args = new List(); - args.Add(heap); - args.Add(r); - args.Add(f); - args.Add(v); - return new Boogie.NAryExpr(tok, - new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "update", heap.Type)), - args); - } - /// /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the /// translation, because such functions can mess up triggering. diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index 4777812e316..ad89f22fee4 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -87,7 +87,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List freeOfAlloc = ComprehensionExpr.BoundedPool.HasBounds(s.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); List xBvars = new List(); var xBody = etran.TrBoundVariables(s.BoundVars, xBvars, false, freeOfAlloc); @@ -1323,9 +1323,10 @@ private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List boundVar xAnte = BplAnd(xAnte, prevEtran.TrExpr(range)); var g = prevEtran.TrExpr(rhs); GetObjFieldDetails(lhs, prevEtran, out var obj, out var field); - var xHeapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, obj, field); + var xHeapOF = ReadHeap(tok, etran.HeapExpr, obj, field); Type lhsType = lhs is MemberSelectExpr ? ((MemberSelectExpr)lhs).Type : null; + g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType); Bpl.Trigger tr = null; @@ -2121,7 +2122,7 @@ void RecordNewObjectsIn_New(IToken tok, IteratorDecl iter, Bpl.Expr initHeap, Bp new List() { updatedSetIE }); builder.Add(cmd); // $Heap[this, _new] := $iter_newUpdate; - cmd = Bpl.Cmd.SimpleAssign(iter.tok, currentHeap, ExpressionTranslator.UpdateHeap(iter.tok, currentHeap, th, nwField, updatedSetIE)); + cmd = Bpl.Cmd.SimpleAssign(iter.tok, currentHeap, UpdateHeap(iter.tok, currentHeap, th, nwField, updatedSetIE)); builder.Add(cmd); // assume $IsGoodHeap($Heap) builder.Add(AssumeGoodHeap(tok, etran)); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 2973e139163..6ec91b9912d 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -1476,10 +1476,10 @@ public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr heapExpr, Bpl.Expr e) { Contract.Requires(e != null); Contract.Ensures(Contract.Result() != null); - return ReadHeap(tok, heapExpr, e, predef.Alloc(tok)); + return ReadHeap(tok, heapExpr, e, predef.Alloc(tok), Bpl.Type.Bool); } - public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { + public static Bpl.Expr ReadHeap(IToken tok, Expr heap, Expr r, Expr f, Bpl.Type ty = null) { Contract.Requires(tok != null); Contract.Requires(heap != null); Contract.Requires(r != null); @@ -1491,9 +1491,15 @@ public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { args.Add(r); args.Add(f); Bpl.Type t = (f.Type != null) ? f.Type : f.ShallowType; - return new Bpl.NAryExpr(tok, - new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])), - args); + Bpl.Expr readCall = + new Bpl.NAryExpr(tok, + new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", t.AsCtor.Arguments[0])), + args); + // Add a type coercion if supplied + if (ty is not null) { + Contract.Assert(ty.Equals(t.AsCtor.Arguments[0])); + } + return ty is null ? readCall : Bpl.Expr.CoerceType(tok, readCall, ty); } public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r) { @@ -1510,6 +1516,24 @@ public static Bpl.NAryExpr ReadHeap(IToken tok, Expr heap, Expr r) { args); } + public static Boogie.NAryExpr UpdateHeap(IToken tok, Expr heap, Expr r, Expr f, Expr v) { + Contract.Requires(tok != null); + Contract.Requires(heap != null); + Contract.Requires(r != null); + Contract.Requires(f != null); + Contract.Requires(v != null); + Contract.Ensures(Contract.Result() != null); + + List args = new List(); + args.Add(heap); + args.Add(r); + args.Add(f); + args.Add(v); + return new Boogie.NAryExpr(tok, + new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, "update", heap.Type)), + args); + } + public Bpl.Expr DType(Bpl.Expr e, Bpl.Expr type) { return Bpl.Expr.Eq(FunctionCall(e.tok, BuiltinFunction.DynamicType, null, e), type); } @@ -4019,7 +4043,7 @@ void AddFrameAxiom(Function f) { Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok, alpha), out field); Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); Bpl.Expr oNotNullAlloced = oNotNull; - Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field)); + Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field, alpha), ReadHeap(f.tok, h1, o, field, alpha)); Bpl.Expr h0IsHeapAnchor = FunctionCall(h0.tok, BuiltinFunction.IsHeapAnchor, null, h0); Bpl.Expr heapSucc = HeapSucc(h0, h1); @@ -6152,7 +6176,7 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 FunctionCall(tok, BuiltinFunction.Box, null, o) }) ), - Bpl.Expr.Eq(ReadHeap(tok, h0, o, fld), ReadHeap(tok, h1, o, fld)))); + Bpl.Expr.Eq(ReadHeap(tok, h0, o, fld, a), ReadHeap(tok, h1, o, fld, a)))); Func fn = h => FunctionCall(tok, fname, Bpl.Type.Bool, Concat(types, Cons(h, Cons(f, boxes)))); @@ -7095,8 +7119,8 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); f = new Bpl.IdentifierExpr(tok, fVar); quantifiedVars = new List { oVar, fVar }; - heapOF = ReadHeap(tok, etran.HeapExpr, o, f); - preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o, f); + heapOF = ReadHeap(tok, etran.HeapExpr, o, f, alpha); + preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o, f, alpha); } else { // object granularity typeVars = new List(); @@ -7136,8 +7160,8 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha))); Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar); - Bpl.Expr heapOF = ReadHeap(tok, etran.HeapExpr, o, f); - Bpl.Expr preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o, f); + Bpl.Expr heapOF = ReadHeap(tok, etran.HeapExpr, o, f, alpha); + Bpl.Expr preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o, f, alpha); Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o)); Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF); @@ -8771,7 +8795,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Contract.Assert(fseField != null); Check_NewRestrictions(tok, obj, fseField, rhs, bldr, et); var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fseField)), rhs)); + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, new Bpl.IdentifierExpr(tok, GetField(fseField)), rhs)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8799,7 +8823,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs)); + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, et)); @@ -8822,7 +8846,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi lhsBuilders.Add(delegate (Bpl.Expr rhs, bool origRhsIsHavoc, BoogieStmtListBuilder bldr, ExpressionTranslator et) { if (rhs != null) { var h = (Bpl.IdentifierExpr)et.HeapExpr; // TODO: is this cast always justified? - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, obj, fieldName, rhs)); + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, UpdateHeap(tok, h, obj, fieldName, rhs)); bldr.Add(cmd); // assume $IsGoodHeap($Heap); bldr.Add(AssumeGoodHeap(tok, etran)); @@ -8994,7 +9018,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New)); var thisDotNew = ReadHeap(tok, etran.HeapExpr, th, nwField); var unionOne = FunctionCall(tok, BuiltinFunction.SetUnionOne, predef.BoxType, thisDotNew, FunctionCall(tok, BuiltinFunction.Box, null, nw)); - var heapRhs = ExpressionTranslator.UpdateHeap(tok, etran.HeapExpr, th, nwField, unionOne); + var heapRhs = UpdateHeap(tok, etran.HeapExpr, th, nwField, unionOne); heapAllocationRecorder = Bpl.Cmd.SimpleAssign(tok, etran.HeapCastToIdentifierExpr, heapRhs); } CommitAllocatedObject(tok, nw, heapAllocationRecorder, builder, etran); @@ -9133,7 +9157,7 @@ private void CommitAllocatedObject(IToken tok, Bpl.IdentifierExpr nw, Bpl.Cmd ex // $Heap[$nw, alloc] := true; Bpl.Expr alloc = predef.Alloc(tok); Bpl.IdentifierExpr heap = etran.HeapCastToIdentifierExpr; - Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, heap, ExpressionTranslator.UpdateHeap(tok, heap, nw, alloc, Bpl.Expr.True)); + Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, heap, UpdateHeap(tok, heap, nw, alloc, Bpl.Expr.True)); builder.Add(cmd); if (extraCmd != null) { builder.Add(extraCmd); @@ -9227,7 +9251,7 @@ void Check_NewRestrictions(IToken tok, Bpl.Expr obj, Field f, Bpl.Expr rhs, Boog // Assignments to an iterator _new field is only allowed to shrink the set, so: // assert Set#Subset(rhs, obj._new); var fId = new Bpl.IdentifierExpr(tok, GetField(f)); - var subset = FunctionCall(tok, BuiltinFunction.SetSubset, null, rhs, ReadHeap(tok, etran.HeapExpr, obj, fId)); + var subset = FunctionCall(tok, BuiltinFunction.SetSubset, null, rhs, ReadHeap(tok, etran.HeapExpr, obj, fId, TrType(f.Type))); builder.Add(Assert(tok, subset, new PODesc.AssignmentShrinks(f.Name))); } } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index 559647b0b0a..228914a64b9 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -464,29 +464,16 @@ await AssertHoverMatches(documentItem, (6, 11), [Fact(Timeout = 5 * MaxTestExecutionTimeMs)] public async Task IndicateClickableWarningSignsOnMethodHoverWhenResourceLimitReached10MThreshold() { var documentItem = await GetDocumentItem(@" -lemma {:rlimit 12000} SquareRoot2NotRational(p: nat, q: nat) - requires p > 0 && q > 0 - ensures (p * p) != 2 * (q * q) -{ - if (p * p) == 2 * (q * q) { - calc == { - (2 * q - p) * (2 * q - p); - 4 * q * q + p * p - 4 * p * q; - {assert {:split_here} 2 * q * q == p * p;} - 2 * q * q + 2 * p * p - 4 * p * q; - 2 * (p - q) * (p - q); - } - } - assert {:split_here} true; +ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)} + +lemma{:rlimit 10000} L() +{ + assert f(10, 5) == 0; } ", "testfileSlow.dfy", true); - await AssertHoverMatches(documentItem, (0, 22), - @"**Verification performance metrics for method `SquareRoot2NotRational`**: - -- Total resource usage: ??? RU [⚠](???) -- Most costly [assertion batches](???): - - #2/3 with 2 assertions at line 3, ??? RU [⚠](???) - - #???/3 with 2 assertions at line ???, ??? RU - - #???/3 with 2 assertions at line ???9, ??? RU" + await AssertHoverMatches(documentItem, (2, 22), + @"**Verification performance metrics for method `L`**: + +- Total resource usage: ??? RU [⚠](???)" ); } diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs index 0736d4a90c8..fea167d23d1 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs @@ -28,7 +28,7 @@ public class DafnyModel { fNull, fSetUnion, fSetIntersection, fSetDifference, fSetUnionOne, fSetEmpty, fSeqEmpty, fSeqBuild, fSeqAppend, fSeqDrop, fSeqTake, fSeqUpdate, fSeqCreate, fU2Real, fU2Bool, fU2Int, - fMapDomain, fMapElements, fMapBuild, fIs, fIsBox; + fMapDomain, fMapElements, fMapBuild, fIs, fIsBox, fUnbox; private readonly Dictionary datatypeValues = new(); // maps a numeric type (int, real, bv4, etc.) to the set of integer @@ -85,6 +85,7 @@ public DafnyModel(Model model, DafnyOptions options) { fU2Int = new ModelFuncWrapper(this, "U_2_int", 1, 0); fTag = new ModelFuncWrapper(this, "Tag", 1, 0); fBv = new ModelFuncWrapper(this, "TBitvector", 1, 0); + fUnbox = new ModelFuncWrapper(this, "$Unbox", 2, 0); InitDataTypes(); RegisterReservedChars(); RegisterReservedInts(); @@ -840,7 +841,11 @@ private Model.Element Unbox(Model.Element elt) { return null; } var unboxed = fBox.AppWithResult(elt); - return unboxed != null ? unboxed.Args[0] : elt; + if (unboxed != null) { + return Unbox(unboxed.Args[0]); + } + unboxed = fUnbox.AppWithArg(1, elt); + return unboxed != null ? Unbox(unboxed.Result) : elt; } } } diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy index 9dc7de9991f..a70667f5843 100644 --- a/Test/concurrency/11-MutexGuard2.dfy +++ b/Test/concurrency/11-MutexGuard2.dfy @@ -1,3 +1,4 @@ +// UNSUPPORTED: windows,posix // RUN: %dafny /compile:0 /proverOpt:O:smt.qi.eager_threshold=30 /typeEncoding:p "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect index de0de4449ca..27f7a49c9b7 100755 --- a/Test/dafny0/Fuel.dfy.expect +++ b/Test/dafny0/Fuel.dfy.expect @@ -46,13 +46,13 @@ Fuel.dfy(329,21): Related location Fuel.dfy(313,41): Related location Fuel.dfy(336,45): Error: function precondition could not be proved Fuel.dfy(329,21): Related location -Fuel.dfy(314,72): Related location +Fuel.dfy(312,43): Related location Fuel.dfy(336,45): Error: function precondition could not be proved Fuel.dfy(329,21): Related location -Fuel.dfy(314,93): Related location +Fuel.dfy(314,72): Related location Fuel.dfy(336,45): Error: function precondition could not be proved Fuel.dfy(329,21): Related location -Fuel.dfy(312,43): Related location +Fuel.dfy(314,93): Related location Fuel.dfy(336,45): Error: function precondition could not be proved Fuel.dfy(329,21): Related location Fuel.dfy(312,58): Related location diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect index 84a60a4b747..69ea8b73caa 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -3,7 +3,7 @@ Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); Dafny program verifier finished with 1 verified, 0 errors Processing call to procedure bar (call) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): - >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap))) + >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && read(call0old#AT#$Heap, $o, alloc): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap))) >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); >>> AssumeNegationOfAssumptionVariable diff --git a/Test/git-issues/git-issue-1207.dfy b/Test/git-issues/git-issue-1207.dfy index 6605a4a9e20..a06d0cc747b 100644 --- a/Test/git-issues/git-issue-1207.dfy +++ b/Test/git-issues/git-issue-1207.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /compile:0 /errorLimit:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The point of all of these tests is to make sure no boolean operators slip into diff --git a/Test/git-issues/git-issue-1207.dfy.expect b/Test/git-issues/git-issue-1207.dfy.expect index 349ea6d225f..40d9f8c1486 100644 --- a/Test/git-issues/git-issue-1207.dfy.expect +++ b/Test/git-issues/git-issue-1207.dfy.expect @@ -8,20 +8,30 @@ git-issue-1207.dfy(11,9): Error: assertion might not hold git-issue-1207.dfy(14,9): Error: assertion might not hold git-issue-1207.dfy(15,9): Error: assertion might not hold git-issue-1207.dfy(16,9): Error: assertion might not hold +git-issue-1207.dfy(17,9): Error: assertion might not hold +git-issue-1207.dfy(18,9): Error: assertion might not hold git-issue-1207.dfy(22,9): Error: assertion might not hold git-issue-1207.dfy(23,9): Error: assertion might not hold git-issue-1207.dfy(24,9): Error: assertion might not hold git-issue-1207.dfy(26,9): Error: assertion might not hold git-issue-1207.dfy(27,9): Error: assertion might not hold +git-issue-1207.dfy(28,9): Error: assertion might not hold +git-issue-1207.dfy(29,9): Error: assertion might not hold +git-issue-1207.dfy(30,9): Error: assertion might not hold git-issue-1207.dfy(34,9): Error: assertion might not hold git-issue-1207.dfy(35,9): Error: assertion might not hold git-issue-1207.dfy(38,9): Error: assertion might not hold git-issue-1207.dfy(39,9): Error: assertion might not hold git-issue-1207.dfy(40,9): Error: assertion might not hold +git-issue-1207.dfy(41,9): Error: assertion might not hold +git-issue-1207.dfy(42,9): Error: assertion might not hold +git-issue-1207.dfy(43,9): Error: assertion might not hold git-issue-1207.dfy(47,9): Error: assertion might not hold git-issue-1207.dfy(48,9): Error: assertion might not hold git-issue-1207.dfy(49,9): Error: assertion might not hold +git-issue-1207.dfy(50,9): Error: assertion might not hold git-issue-1207.dfy(50,49): Error: index out of range git-issue-1207.dfy(50,57): Error: index out of range +git-issue-1207.dfy(51,9): Error: assertion might not hold -Dafny program verifier finished with 0 verified, 20 errors +Dafny program verifier finished with 0 verified, 30 errors diff --git a/Test/git-issues/git-issue-2026.dfy.expect b/Test/git-issues/git-issue-2026.dfy.expect index a887933fac5..d9a38be0bce 100644 --- a/Test/git-issues/git-issue-2026.dfy.expect +++ b/Test/git-issues/git-issue-2026.dfy.expect @@ -8,29 +8,25 @@ git-issue-2026.dfy(12,0): initial state: ret : _System.array> = () git-issue-2026.dfy(13,24): n : int = 2 - ret : _System.array?> = (Length := 2, [(- 1)] := @0, [0] := @1) - @0 : ? = ? - @1 : seq = ['o', 'd', 'd'] + ret : _System.array?> = (Length := 2, [(- 39)] := @0, [0] := @0) + @0 : seq = ['o', 'd', 'd'] git-issue-2026.dfy(15,14): n : int = 2 - ret : _System.array?> = (Length := 2, [(- 1)] := @0, [0] := @1) + ret : _System.array?> = (Length := 2, [(- 39)] := @0, [0] := @0) i : int = 0 - @0 : ? = ? - @1 : seq = ['o', 'd', 'd'] + @0 : seq = ['o', 'd', 'd'] git-issue-2026.dfy(16,4): after some loop iterations: n : int = 2 - ret : _System.array?> = (Length := 2, [(- 1)] := @0) + ret : _System.array?> = (Length := 2, [(- 39)] := @0) i : int = 0 - @0 : ? = ? + @0 : seq = ['o', 'd', 'd'] git-issue-2026.dfy(22,27): n : int = 2 - ret : _System.array?> = (Length := 2, [(- 1)] := @0, [0] := @1) + ret : _System.array?> = (Length := 2, [(- 39)] := @0, [0] := @0) i : int = 0 - @0 : ? = ? - @1 : seq = ['o', 'd', 'd'] + @0 : seq = ['o', 'd', 'd'] git-issue-2026.dfy(26,18): n : int = 2 - ret : _System.array?> = (Length := 2, [(- 1)] := @0, [0] := @1) + ret : _System.array?> = (Length := 2, [(- 39)] := @0, [0] := @0) i : int = 1 - @0 : ? = ? - @1 : seq = ['o', 'd', 'd'] + @0 : seq = ['o', 'd', 'd'] diff --git a/Test/git-issues/git-issue-2299.dfy.expect b/Test/git-issues/git-issue-2299.dfy.expect index 2c938effc18..319e0e2fb07 100644 --- a/Test/git-issues/git-issue-2299.dfy.expect +++ b/Test/git-issues/git-issue-2299.dfy.expect @@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location git-issue-2299.dfy(67,13): Error: assertion might not hold git-issue-2299.dfy(21,4): Related location git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,4): Related location -git-issue-2299.dfy(10,11): Related location +git-issue-2299.dfy(27,18): Related location +git-issue-2299.dfy(16,4): Related location git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,32): Related location git-issue-2299.dfy(21,4): Related location git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,18): Related location -git-issue-2299.dfy(16,4): Related location +git-issue-2299.dfy(27,4): Related location +git-issue-2299.dfy(10,11): Related location Dafny program verifier finished with 7 verified, 7 errors diff --git a/Test/git-issues/git-issue-2605.dfy b/Test/git-issues/git-issue-2605.dfy index 1a9d45934a4..a72dca5ad8f 100644 --- a/Test/git-issues/git-issue-2605.dfy +++ b/Test/git-issues/git-issue-2605.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /compile:0 /errorLimit:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" method M(a: array, j: int) { diff --git a/Test/git-issues/git-issue-2605.dfy.expect b/Test/git-issues/git-issue-2605.dfy.expect index 2c8cc2e51ad..4d8b7f382a0 100644 --- a/Test/git-issues/git-issue-2605.dfy.expect +++ b/Test/git-issues/git-issue-2605.dfy.expect @@ -3,5 +3,6 @@ git-issue-2605.dfy(6,23): Error: possible division by zero git-issue-2605.dfy(7,13): Error: index out of range git-issue-2605.dfy(7,21): Error: index out of range git-issue-2605.dfy(9,11): Error: assertion might not hold +git-issue-2605.dfy(11,9): Error: assertion might not hold -Dafny program verifier finished with 0 verified, 5 errors +Dafny program verifier finished with 0 verified, 6 errors diff --git a/Test/git-issues/git-issue-3855.dfy b/Test/git-issues/git-issue-3855.dfy index d0250a36af4..5839defe290 100644 --- a/Test/git-issues/git-issue-3855.dfy +++ b/Test/git-issues/git-issue-3855.dfy @@ -637,7 +637,7 @@ function partitionOfJustHeapRegions(os : set) : (partition : map // property; converting the resulting tree back into a // sequence yields exactly that portion of the input // sequence that has been consumed. -function build_rec(d: int, s: seq): Result +function {:vcs_split_on_every_assert} build_rec(d: int, s: seq): Result ensures build_rec(d, s).Res? ==> |build_rec(d, s).sOut| < |s| && build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..]