diff options
author | Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2011-07-14 19:04:48 -0700 |
commit | bd0939ffe92812966dfe2aac15d28cc1e3c37b42 (patch) | |
tree | ea5861dcf473be51b024b7fe178e820e8be18c9d /Test/dafny0/Definedness.dfy | |
parent | 5e9cfe9da36b5efda394c1bde3f5536f1a5308a0 (diff) |
Fixed failing regression tests.
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
-rw-r--r-- | Test/dafny0/Definedness.dfy | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 2063eec4..44b54f3d 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -48,27 +48,35 @@ class SoWellformed { requires next != null;
modifies this;
ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
+ {
+ }
method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null;
modifies s;
ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
-
+ {
+
+ }
method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null && this !in s;
modifies s;
ensures next.xyz < 100; // fine
+ {
+
+ }
}
// ---------------------- welldefinedness checks for statements -------------------
class StatementTwoShoes {
var x: int;
-
+ var s: StatementTwoShoes;
function method F(b: int): StatementTwoShoes
requires 0 <= b;
+ reads this;
{
- this
+ s
}
method M(p: StatementTwoShoes, a: int)
@@ -175,7 +183,7 @@ class StatementTwoShoes { }
function G(w: int): int { 5 }
- function method H(x: int): int
+ function method H(x: int): int { -x }
method V(s: set<StatementTwoShoes>, a: int, b: int)
modifies s;
|