diff options
| author |  leino <unknown> | 2014-11-19 00:49:51 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-11-19 00:49:51 -0800 |
| commit | 7b40f456229bb5c275450db60299db00e865696e (patch) | |
| tree | e6a24434f2eaaf10771057c2851e9a67f4ba2459 /Test/dafny0/Backticks.dfy.expect | |
| parent | f27cb29e16125a4132e67e826c13db46595a838e (diff) | |
Fixed bug where resolution was overly restrictive with ghost variables appearing in reads clauses.
Fixed bug in the checking of reads subset for field frame targets ("back ticks")
Diffstat (limited to 'Test/dafny0/Backticks.dfy.expect')
| -rw-r--r-- | Test/dafny0/Backticks.dfy.expect | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect new file mode 100644 index 00000000..82fc2933 --- /dev/null +++ b/Test/dafny0/Backticks.dfy.expect @@ -0,0 +1,11 @@ +Backticks.dfy(38,5): Error: insufficient reads clause to invoke function
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Backticks.dfy(77,7): Error: call may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
|