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 | |
| 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')
| -rw-r--r-- | Test/dafny0/Backticks.dfy | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/Test/dafny0/Backticks.dfy b/Test/dafny0/Backticks.dfy new file mode 100644 index 00000000..08606b55 --- /dev/null +++ b/Test/dafny0/Backticks.dfy @@ -0,0 +1,80 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C {
+ var x: int
+ var y: int
+ ghost var z: int
+
+ function F(): int
+ reads `x
+ {
+ x
+ }
+
+ function G(): int
+ reads `x
+ {
+ F()
+ }
+
+ function H(): int
+ reads this
+ {
+ F()
+ }
+
+ function I(n: nat): int
+ reads this
+ {
+ x + y + z + J(n)
+ }
+
+ function J(n: nat): int
+ reads `x, this`z
+ decreases {this}, n, 0
+ {
+ if n == 0 then 5 else
+ I(n-1) // error: insufficient reads clause
+ }
+
+ function K(n: nat): int
+ reads `x
+ decreases {this}, n+1
+ {
+ L(n)
+ }
+
+ function L(n: nat): int
+ reads `x
+ {
+ if n < 2 then 5 else K(n-2)
+ }
+
+ method M()
+ modifies `x
+ {
+ N();
+ }
+
+ method N()
+ modifies `x
+ {
+ x := x + 1;
+ }
+
+ method O(n: nat)
+ modifies this
+ {
+ P(n);
+ }
+ method P(n: nat)
+ modifies `x
+ decreases n, 0
+ {
+ x := x + 1;
+ if n != 0 {
+ O(n-1); // error: insufficient modifies clause to make call
+ }
+ }
+}
|