add DefiniteAssignment proof obligation expression

Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs

@@ -163,7 +163,8 @@ public partial class BoogieGenerator {
 
  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 @@ public partial class BoogieGenerator {
  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 @@ public partial class BoogieGenerator {
 
  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));
  }
  }

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -1394,20 +1394,26 @@ public class ElementInDomain : ProofObligationDescription {
 
 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 {

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<G>
+{
+ 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<G>(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<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ return x, y;
+ }
+ return a, b;
+}
+
+method M2<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x := a;
+ return x, y;
+ }
+ return a, b;
+}
+
+method M3<G>(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<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x := a;
+ return;
+ }
+ return a, b;
+}
+
+method M5<G>(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<G>(i: int, a: G, b: G) returns (x: G, y: G)
+{
+ if i < 0 {
+ x, y := y, x;
+ return;
+ }
+ return a, 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