diff options
| author |  qunyanm <unknown> | 2015-11-04 16:27:42 -0800 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-11-04 16:27:42 -0800 |
| commit | d3c778854c2dc792a2dfbd9c5b05d667d18fb4c4 (patch) | |
| tree | 7c5c0554b13c19256b8bb8863188797f9ca047dc | |
| parent | 2b7d31bb3e0276028a8bc50c4933ea60fed5fb60 (diff) | |
Fix issue 104. Use ResolvedExpression to compute subexpressions for
DatatypeUpdateExpr if ResovedExpression is not null.
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 12 | ||||
| -rw-r--r-- | Test/dafny4/Bug104.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny4/Bug104.dfy.expect | 3 |
3 files changed, 24 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 16b29c2b..fdbd484e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7800,9 +7800,15 @@ namespace Microsoft.Dafny { public override IEnumerable<Expression> SubExpressions {
get {
- yield return Root;
- foreach (var update in Updates) {
- yield return update.Item3;
+ if (ResolvedExpression == null) {
+ yield return Root;
+ foreach (var update in Updates) {
+ yield return update.Item3;
+ }
+ } else {
+ foreach (var e in ResolvedExpression.SubExpressions) {
+ yield return e;
+ }
}
}
}
diff --git a/Test/dafny4/Bug104.dfy b/Test/dafny4/Bug104.dfy new file mode 100644 index 00000000..ffabbb92 --- /dev/null +++ b/Test/dafny4/Bug104.dfy @@ -0,0 +1,12 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype PartRealPartGhost = PartRealPartGhost(x:int, ghost y:int)
+
+method UpdateField()
+{
+ var v := PartRealPartGhost(3, 4);
+ ghost var g := 5;
+ v := v[y := g];
+ v := v.(y := g);
+}
\ No newline at end of file diff --git a/Test/dafny4/Bug104.dfy.expect b/Test/dafny4/Bug104.dfy.expect new file mode 100644 index 00000000..1cc43cbf --- /dev/null +++ b/Test/dafny4/Bug104.dfy.expect @@ -0,0 +1,3 @@ +Bug104.dfy(10,7): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)
+
+Dafny program verifier finished with 2 verified, 0 errors
|