diff options
author | leino <unknown> | 2015-09-28 13:16:15 -0700 |
---|---|---|
committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Test/dafny0/NonGhostQuantifiers.dfy | |
parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) |
Changed computation of ghosts until pass 2 of resolution.
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
Diffstat (limited to 'Test/dafny0/NonGhostQuantifiers.dfy')
-rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index bff1d65b..e522d0fc 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects { forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
+ class SomeClass {
+ var f: int;
+ }
+}
+
+module DependencyOnAllAllocatedObjects_More {
method M()
{
var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects { var f: int;
}
}
+
|