From ac05f473787e14648fc9c82f767bd150fd3d03fe Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Tue, 28 May 2024 12:22:41 -0700 Subject: [PATCH 1/5] implement assigned(e) expression --- .../AST/Expressions/Operators/UnaryOpExpr.cs | 5 ++- .../AST/Grammar/Printer/Printer.Expression.cs | 4 ++ Source/DafnyCore/Dafny.atg | 2 + .../CheckDividedConstructorInit_Visitor.cs | 2 + Source/DafnyCore/Resolver/ExpressionTester.cs | 2 +- .../NameResolutionAndTypeInference.cs | 4 ++ .../PreType/PreTypeResolve.Expressions.cs | 4 ++ .../BoogieGenerator.ExpressionTranslator.cs | 20 +++++++++ .../BoogieGenerator.ExpressionWellformed.cs | 7 +++- .../LitTests/LitTest/dafny0/Assigned.dfy | 42 +++++++++++++++++++ .../LitTest/dafny0/Assigned.dfy.expect | 2 + 11 files changed, 91 insertions(+), 3 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect diff --git a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs index 44c3ed134ec..bf1f6d82a85 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs @@ -9,6 +9,7 @@ public enum Opcode { Fresh, // fresh also has a(n optional) second argument, namely the @-label Allocated, Lit, // there is no syntax for this operator, but it is sometimes introduced during translation + Assigned, } public readonly Opcode Op; @@ -22,7 +23,8 @@ public enum ResolvedOpcode { MapCard, Fresh, Allocated, - Lit + Lit, + Assigned, } private ResolvedOpcode _ResolvedOp = ResolvedOpcode.YetUndetermined; @@ -42,6 +44,7 @@ public ResolvedOpcode ResolveOp() { (Opcode.Fresh, _) => ResolvedOpcode.Fresh, (Opcode.Allocated, _) => ResolvedOpcode.Allocated, (Opcode.Lit, _) => ResolvedOpcode.Lit, + (Opcode.Assigned, _) => ResolvedOpcode.Assigned, _ => ResolvedOpcode.YetUndetermined // Unreachable }; Contract.Assert(_ResolvedOp != ResolvedOpcode.YetUndetermined); diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs index 5c8ac801b14..b58f1ffc183 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs @@ -767,6 +767,10 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, wr.Write("Lit("); PrintExpression(e.E, false); wr.Write(")"); + } else if (e.Op == UnaryOpExpr.Opcode.Assigned) { + wr.Write("assigned("); + PrintExpression(e.E, false); + wr.Write(")"); } else { Contract.Assert(e.Op != UnaryOpExpr.Opcode.Fresh); // this is handled is "is FreshExpr" case above // Prefix operator. diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index fc45713db39..d01760aefea 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -3640,6 +3640,8 @@ ConstAtomExpression | "|" (. x = t; .) Expression (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Cardinality, e); .) "|" + | "assigned" (. x = t; .) + "(" NameSegment ")" (. e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Assigned, e); .) | ParensExpression ) (. if(x!= null) { e.RangeToken = new RangeToken(x, t); } .) . diff --git a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs b/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs index 3c88cafc9bb..d667c83a80b 100644 --- a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs @@ -63,6 +63,8 @@ protected override bool VisitOneExpr(Expression expr, ref int unused) { if (e.Member.IsInstanceIndependentConstant && Expression.AsThis(e.Obj) != null) { return false; // don't continue the recursion } + } else if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) { + return false; // don't continue the recursion } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) { reporter.Error(MessageSource.Resolver, expr.tok, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields"); } diff --git a/Source/DafnyCore/Resolver/ExpressionTester.cs b/Source/DafnyCore/Resolver/ExpressionTester.cs index 3edd99015d3..f18328117cf 100644 --- a/Source/DafnyCore/Resolver/ExpressionTester.cs +++ b/Source/DafnyCore/Resolver/ExpressionTester.cs @@ -557,7 +557,7 @@ public static bool UsesSpecFeatures(Expression expr) { return true; } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; - if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Fresh or UnaryOpExpr.Opcode.Allocated }) { + if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Fresh or UnaryOpExpr.Opcode.Allocated or UnaryOpExpr.Opcode.Assigned }) { return true; } if (expr is TypeTestExpr tte && !IsTypeTestCompilable(tte)) { diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 566fb5c6f7a..d84c3e934bf 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -758,6 +758,10 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont reporter.Error(MessageSource.Resolver, expr, "a {0} definition is not allowed to depend on the set of allocated references", declKind); } break; + case UnaryOpExpr.Opcode.Assigned: + // the argument is allowed to have any type + expr.Type = Type.Bool; + break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index fc798f3490e..36d92647157 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -419,6 +419,10 @@ resolutionContext.CodeContext is ConstantField || ReportError(expr, "a {0} definition is not allowed to depend on the set of allocated references", declKind); } break; + case UnaryOpExpr.Opcode.Assigned: + // the argument is allowed to have any type at all + expr.PreType = ConstrainResultToBoolFamily(expr.tok, "assigned", "boolean literal used as if it had type {0}"); + break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 8d325004e69..778a59f356d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -832,6 +832,26 @@ public Boogie.Expr TrExpr(Expression expr) { // both the $IsAllocBox and $IsAlloc forms, because the axioms that connects these two is triggered // by $IsAllocBox. return BoogieGenerator.MkIsAllocBox(BoxIfNecessary(e.E.tok, TrExpr(e.E), e.E.Type), e.E.Type, HeapExpr); + case UnaryOpExpr.ResolvedOpcode.Assigned: + var ns = e.E as NameSegment; + Contract.Assert(ns != null); + string name = null; + switch (ns.Resolved) { + case IdentifierExpr ie: + name = ie.Var.UniqueName; + break; + case MemberSelectExpr mse: + if (BoogieGenerator.inBodyInitContext && Expression.AsThis(mse.Obj) != null) { + name = BoogieGenerator.SurrogateName(mse.Member as Field); + } + break; + } + + if (name == null) { + return Expr.True; + } + BoogieGenerator.definiteAssignmentTrackers.TryGetValue(name, out var defass); + return defass; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 90502c2f60d..2705545a9a0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -919,7 +919,12 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re } case UnaryExpr unaryExpr: { UnaryExpr e = unaryExpr; - CheckWellformed(e.E, wfOptions, locals, builder, etran); + if (e is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) { + CheckWellformed(e.E.Resolved, wfOptions.WithLValueContext(true), locals, builder, etran); + } else { + CheckWellformed(e.E, wfOptions, locals, builder, etran); + } + if (e is ConversionExpr ee) { CheckResultToBeInType(unaryExpr.tok, ee.E, ee.ToType, locals, builder, etran, ee.messagePrefix); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy new file mode 100644 index 00000000000..7d0d575bdf8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy @@ -0,0 +1,42 @@ +// RUN: %verify --relax-definite-assignment "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class C +{ + var x: G + const y: G + + constructor Con0(i: int, a: G, b: G) + { + x := a; + y := b; + assert assigned(x); + assert assigned(y); + new; + if i > 0 { + x := y; + } + } + + constructor Con1(i: int, a: G, b: G) + { + x := a; + assert assigned(x); + assume {:axiom} assigned(y); + new; + if i > 0 { + x := y; + } + } +} + +method M0(x: int, a: G, b: G) returns (y: G) +{ + if x < 10 { + y := a; + } else if x < 20 { + return b; + } else { + assume {:axiom} assigned(y); + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect new file mode 100644 index 00000000000..cf4d1a14e57 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Assigned.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors From 0ad72ae256c61167cdb4acfb8c711fbc87c3aee6 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Tue, 28 May 2024 20:53:13 -0700 Subject: [PATCH 2/5] add DefiniteAssignment proof obligation expression --- .../BoogieGenerator.DefiniteAssignment.cs | 9 +- .../Verifier/ProofObligationDescription.cs | 16 ++-- .../definite-assignment.dfy | 89 +++++++++++++++++++ .../definite-assignment.dfy.expect | 32 +++++++ 4 files changed, 137 insertions(+), 9 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs index cdb1eb62d12..b4d8990da0f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs @@ -163,7 +163,8 @@ void CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) Bpl.IdentifierExpr ie; if (definiteAssignmentTrackers.TryGetValue(expr.Var.UniqueName, out ie)) { - builder.Add(Assert(GetToken(expr), ie, new PODesc.DefiniteAssignment($"variable '{expr.Var.Name}'", "here"))); + builder.Add(Assert(GetToken(expr), ie, + new PODesc.DefiniteAssignment("variable", expr.Var.Name, "here"))); } } @@ -187,8 +188,8 @@ void CheckDefiniteAssignmentSurrogate(IToken tok, Field field, bool atNew, Boogi var nm = SurrogateName(field); Bpl.IdentifierExpr ie; if (definiteAssignmentTrackers.TryGetValue(nm, out ie)) { - var desc = new PODesc.DefiniteAssignment($"field '{field.Name}'", - atNew ? "at this point in the constructor body" : "here"); + var desc = new PODesc.DefiniteAssignment( + "field", field.Name, atNew ? "at this point in the constructor body" : "here"); builder.Add(Assert(tok, ie, desc)); } } @@ -230,7 +231,7 @@ void CheckDefiniteAssignmentReturn(IToken tok, Formal p, BoogieStmtListBuilder b Bpl.IdentifierExpr ie; if (definiteAssignmentTrackers.TryGetValue(p.UniqueName, out ie)) { - var desc = new PODesc.DefiniteAssignment($"out-parameter '{p.Name}'", "at this return point"); + var desc = new PODesc.DefiniteAssignment("out-parameter", p.Name, "at this return point"); builder.Add(Assert(tok, ie, desc)); } } diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 83c02f09334..8508507a3a2 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -1394,20 +1394,26 @@ public override Expression GetAssertedExpr(DafnyOptions options) { public class DefiniteAssignment : ProofObligationDescription { public override string SuccessDescription => - $"{what}, which is subject to definite-assignment rules, is always initialized {where}"; + $"{kind} '{name}', which is subject to definite-assignment rules, is always initialized {where}"; public override string FailureDescription => - $"{what}, which is subject to definite-assignment rules, might be uninitialized {where}"; + $"{kind} '{name}', which is subject to definite-assignment rules, might be uninitialized {where}"; public override string ShortDescription => "definite assignment"; - private readonly string what; + private readonly string kind; + private readonly string name; private readonly string where; - public DefiniteAssignment(string what, string where) { - this.what = what; + public DefiniteAssignment(string kind, string name, string where) { + this.kind = kind; + this.name = name; this.where = where; } + + public override Expression GetAssertedExpr(DafnyOptions options) { + return new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Assigned, new IdentifierExpr(Token.NoToken, name)); + } } public class InRange : ProofObligationDescription { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy new file mode 100644 index 00000000000..d0483aa3ee5 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy @@ -0,0 +1,89 @@ +// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class C +{ + var x: G + const y: G + + constructor Con0(i: int, a: G, b: G) + { + if i > 0 { + x := a; + } else { + y := b; + } + new; + if i > 10 { + x := y; + } + } +} + +method M0(i: int, a: G, b: G) returns (x: G, y: G) +{ + if i < 0 { + x := a; + } else if i < 10 { + y := b; + } else if i < 20 { + x := a; + y := x; + } else if i < 30 { + x := y; + y := b; + } +} + +method M1(i: int, a: G, b: G) returns (x: G, y: G) +{ + if i < 0 { + return x, y; + } + return a, b; +} + +method M2(i: int, a: G, b: G) returns (x: G, y: G) +{ + if i < 0 { + x := a; + return x, y; + } + return a, b; +} + +method M3(i: int, a: G, b: G, c: G) returns (x: G, y: G, z: G) +{ + if i < 0 { + x := y; + return x, y, z; + } + return a, b, c; +} + +method M4(i: int, a: G, b: G) returns (x: G, y: G) +{ + if i < 0 { + x := a; + return; + } + return a, b; +} + +method M5(i: int, a: G, b: G, c: G) returns (x: G, y: G, z: G) +{ + if i < 0 { + x := y; + return; + } + return a, b, c; +} + +method M6(i: int, a: G, b: G) returns (x: G, y: G) +{ + if i < 0 { + x, y := y, x; + return; + } + return a, b; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect new file mode 100644 index 00000000000..d47adc8f7af --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/definite-assignment.dfy.expect @@ -0,0 +1,32 @@ +definite-assignment.dfy(16,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body + Asserted expression: assigned(x) +definite-assignment.dfy(16,4): Error: field 'y', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body + Asserted expression: assigned(y) +definite-assignment.dfy(33,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(36,0): Error: out-parameter 'x', which is subject to definite-assignment rules, might be uninitialized at this return point + Asserted expression: assigned(x) +definite-assignment.dfy(36,0): Error: out-parameter 'y', which is subject to definite-assignment rules, might be uninitialized at this return point + Asserted expression: assigned(y) +definite-assignment.dfy(41,11): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(x) +definite-assignment.dfy(41,14): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(50,14): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(58,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(59,17): Error: variable 'z', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(z) +definite-assignment.dfy(68,4): Error: out-parameter 'y', which is subject to definite-assignment rules, might be uninitialized at this return point + Asserted expression: assigned(y) +definite-assignment.dfy(76,9): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(77,4): Error: out-parameter 'z', which is subject to definite-assignment rules, might be uninitialized at this return point + Asserted expression: assigned(z) +definite-assignment.dfy(85,12): Error: variable 'y', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(y) +definite-assignment.dfy(85,15): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here + Asserted expression: assigned(x) + +Dafny program verifier finished with 0 verified, 15 errors From cc62103a05fce14ad9dbcc1654d1ea8dc69bb7c7 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Tue, 28 May 2024 21:14:13 -0700 Subject: [PATCH 3/5] update documentation --- docs/DafnyRef/Expressions.md | 21 +++++++++++++++++++-- docs/DafnyRef/Types.md | 2 +- docs/dev/news/5501.feat | 1 + 3 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 docs/dev/news/5501.feat diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index b3f1f92b245..13349e8264b 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -632,6 +632,7 @@ old(x) allocated(x) unchanged(x) fresh(e) +assigned(x) ``` These expressions are never l-values. They include @@ -644,6 +645,7 @@ These expressions are never l-values. They include - [unchanged expressions](#sec-unchanged-expression) - [old expressions](#sec-old-expression) - [cardinality expressions](#sec-cardinality-expression) +- [assigned expressions](#sec-assigned-expression) ## 9.20. Literal Expressions ([grammar](#g-literal-expression)} {#sec-literal-expression} @@ -1851,7 +1853,21 @@ value for each optional parameter, and must never name non-existent formals. Any optional parameter that is not given a value takes on the default value declared in the callee for that optional parameter. -## 9.37. Compile-Time Constants {#sec-compile-time-constants} +## 9.37. Assigned Expressions {#sec-assigned-expression} + +Examples: + +```dafny +assigned(x) +``` + +For any variable, constant, out-parameter, or object field `x`, +the expression `assigned(x)` evaluates to `true` in a state +if `x` is definitely assigned in that state. + +See [Section 12.6](#sec-definite-assignment) for more details on definite assignment. + +## 9.38. Compile-Time Constants {#sec-compile-time-constants} In certain situations in Dafny it is helpful to know what the value of a constant is during program analysis, before verification or execution takes @@ -1892,7 +1908,7 @@ In Dafny, the following expressions are compile-time constants[^CTC], recursivel [^CTC]: This set of operations that are constant-folded may be enlarged in future versions of `dafny`. -## 9.38. List of specification expressions {#sec-list-of-specification-expressions} +## 9.39. List of specification expressions {#sec-list-of-specification-expressions} The following is a list of expressions that can only appear in specification contexts or in ghost blocks. @@ -1900,5 +1916,6 @@ The following is a list of expressions that can only appear in specification con * [Allocated expressions](#sec-allocated-expression) * [Unchanged expressions](#sec-unchanged-expression) * [Old expressions](#sec-old-expression) +- [Assigned expressions](#sec-assigned-expression) * [Assert and calc expressions](#sec-statement-in-an-expression) * [Hash Calls](#sec-hash-call) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 008f5b2637b..ff04336cb8a 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -1937,7 +1937,7 @@ Furthermore, for the compiler to be able to make an appropriate choice of representation, the constants in the defining expression as shown above must be known constants at compile-time. They need not be numeric literals; combinations of basic operations and symbolic constants are also allowed as described -in [Section 9.37](#sec-compile-time-constants). +in [Section 9.38](#sec-compile-time-constants). ### 5.7.1. Conversion operations {#sec-conversion} diff --git a/docs/dev/news/5501.feat b/docs/dev/news/5501.feat new file mode 100644 index 00000000000..1cc889990a5 --- /dev/null +++ b/docs/dev/news/5501.feat @@ -0,0 +1 @@ +The new `assigned` expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. \ No newline at end of file From 300c480b74ade88f6c91cdbf20eed6e39882826c Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Tue, 28 May 2024 21:15:42 -0700 Subject: [PATCH 4/5] fix whitespace --- Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs | 2 +- .../DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs index b4d8990da0f..eff44d2a7ab 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs @@ -163,7 +163,7 @@ void CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder) Bpl.IdentifierExpr ie; if (definiteAssignmentTrackers.TryGetValue(expr.Var.UniqueName, out ie)) { - builder.Add(Assert(GetToken(expr), ie, + builder.Add(Assert(GetToken(expr), ie, new PODesc.DefiniteAssignment("variable", expr.Var.Name, "here"))); } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 2705545a9a0..7d26542e32b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -924,7 +924,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re } else { CheckWellformed(e.E, wfOptions, locals, builder, etran); } - + if (e is ConversionExpr ee) { CheckResultToBeInType(unaryExpr.tok, ee.E, ee.ToType, locals, builder, etran, ee.messagePrefix); } From 61bf4199666ad0c703211eb7af3a41b38c511c7b Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Wed, 29 May 2024 19:14:47 -0700 Subject: [PATCH 5/5] update section number --- docs/DafnyRef/Types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index ff04336cb8a..dbd087ab486 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -1937,7 +1937,7 @@ Furthermore, for the compiler to be able to make an appropriate choice of representation, the constants in the defining expression as shown above must be known constants at compile-time. They need not be numeric literals; combinations of basic operations and symbolic constants are also allowed as described -in [Section 9.38](#sec-compile-time-constants). +in [Section 9.39](#sec-compile-time-constants). ### 5.7.1. Conversion operations {#sec-conversion}