diff options
author | Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
commit | cc0a7cae53c068993e3b3004049629dd396cb649 (patch) | |
tree | bb1ae056cded89fdcddcd84294d6accc4c9d03ac | |
parent | 58d639bff25a2d4dadf6febb81b1438e957c43cd (diff) |
Changed logical order of requires and reads clauses on functions. Reads clauses
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
-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
|