diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 21 | ||||
| -rw-r--r-- | Test/dafny0/Reads.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/Reads.dfy.expect | 6 | ||||
| -rw-r--r-- | Test/hofs/Classes.dfy | 9 | ||||
| -rw-r--r-- | Test/hofs/Classes.dfy.expect | 9 |
5 files changed, 34 insertions, 27 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8bb628a8..90d0b11c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4027,20 +4027,23 @@ namespace Microsoft.Dafny { DefineFrame(f.tok, f.Reads, builder, locals, null);
- // check well-formedness of the preconditions (including termination, and reads checks), and then
- // assume each one of them
-
- // check well-formedness of the reads clause
- var wfo = new WFOptions(null, true, true /* do delayed reads checks over requires */);
- CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran);
- wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder);
-
- wfo = new WFOptions(null, true, true /* do delayed reads checks */);
+ // Check well-formedness of the preconditions (including termination), and then
+ // assume each one of them. After all that (in particular, after assuming all
+ // of them), do the postponed reads checks.
+ var wfo = new WFOptions(null, true, true /* do delayed reads checks */);
foreach (Expression p in f.Req) {
CheckWellformedAndAssume(p, wfo, locals, builder, etran);
}
wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder);
+ // Check well-formedness of the reads clause. Note that this is done after assuming
+ // the preconditions. In other words, the well-formedness of the reads clause is
+ // allowed to assume the precondition (yet, the requires clause is checked to
+ // read only those things indicated in the reads clause).
+ wfo = new WFOptions(null, true, true /* do delayed reads checks */);
+ CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran);
+ wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder);
+
// check well-formedness of the decreases clauses (including termination, but no reads checks)
foreach (Expression p in f.Decreases.Expressions)
{
diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 7e0ca1c4..6dedbada 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -58,7 +58,7 @@ function ok5(r : R):() // Reads checking where there are circularities among the expressions class CircularChecking { - var Repr: set<object> + ghost var Repr: set<object> function F(): int reads this, Repr @@ -76,8 +76,8 @@ class CircularChecking { requires Repr == {} function H0(cell: Cell): int - reads Repr // error: reads is not self-framing (unless "this in Repr") - requires this in Repr // lo and behold! So, reads clause is fine, if we can assume the precondition + reads Repr // by itself, this reads is not self-framing + requires this in Repr // lo and behold! So, reads clause is fine after all function H1(cell: Cell): int reads this, Repr @@ -126,3 +126,13 @@ function FunctionInQuantifier2(): int var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // fine :) :) f(10) } + +class DynamicFramesIdiom { + ghost var Repr: set<object> + predicate IllFormed_Valid() + reads Repr // error: reads is not self framing (notice the absence of "this") + { + this in Repr // this says that the predicate returns true if "this in Repr", but the + // predicate can also be invoked in a state where its body will evaluate to false + } +} diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 0b599f3f..1199797f 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -1,4 +1,4 @@ -Reads.dfy(79,11): Error: insufficient reads clause to read field
+Reads.dfy(133,11): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
Reads.dfy(9,30): Error: insufficient reads clause to read field
@@ -7,8 +7,6 @@ Execution trace: Reads.dfy(18,30): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
- (0,0): anon10_Then
- (0,0): anon4
Reads.dfy(28,50): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
@@ -32,4 +30,4 @@ Reads.dfy(120,38): Error: insufficient reads clause to invoke function Execution trace:
(0,0): anon0
-Dafny program verifier finished with 16 verified, 9 errors
+Dafny program verifier finished with 17 verified, 9 errors
diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy index 2b892b35..0ceb46f1 100644 --- a/Test/hofs/Classes.dfy +++ b/Test/hofs/Classes.dfy @@ -30,15 +30,14 @@ function B(t : T) : int -> int } function J(t : T) : int - requires t != null; - requires t.h.reads(0) == {}; - reads t; - reads if t != null then t.h.reads(0) else {}; + requires t != null + reads t + reads t.h.reads(0) { if t.h.requires(0) then B(t)(0) else - B(t)(0) // fail + B(t)(0) // error: precondition violation } method U(t : T) diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 21188d62..e490dbe0 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,10 +1,7 @@ -Classes.dfy(41,6): Error: possible violation of function precondition
+Classes.dfy(40,6): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- (0,0): anon13_Then
- (0,0): anon4
- (0,0): anon14_Then
- (0,0): anon15_Else
- (0,0): anon16_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Else
Dafny program verifier finished with 6 verified, 1 error
|