diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-27 20:22:44 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-27 20:22:44 -0700 |
| commit | 8522c867c262c0972873e6ee69f2ae8c914cb2e5 (patch) | |
| tree | 3ad05878bf37a473f8db2e2b001018b0c08e2827 /Test/dafny0/NonGhostQuantifiers.dfy | |
| parent | bcb6fdad0da726bbee87f1a62c921a8190a4931a (diff) | |
| parent | b541877f2a5cbc59c5d923cd84e59dbe6e12c02d (diff) | |
Merge
Diffstat (limited to 'Test/dafny0/NonGhostQuantifiers.dfy')
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index 58e64827..dc938496 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -138,3 +138,54 @@ class MyClass<T> { }
}
}
+
+// The following functions test what was once a soundness problem
+module DependencyOnAllAllocatedObjects {
+ function AllObjects0(): bool
+ {
+ forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
+ }
+ function AllObjects1(): bool
+ {
+ forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
+ }
+ function AllObjects10(): bool
+ reads *;
+ {
+ forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
+ }
+ function AllObjects11(): bool
+ reads *;
+ {
+ forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
+ }
+ function method AllObjects20(): bool
+ {
+ forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
+ }
+ function method AllObjects21(): bool
+ {
+ forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
+ }
+ function method AllObjects30(): bool
+ reads *;
+ {
+ forall c: SomeClass :: c != null ==> c.f == 0 // error: not allowed to dependend on which objects are allocated
+ }
+ function method AllObjects31(): bool
+ reads *;
+ {
+ forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
+ }
+
+ method M()
+ {
+ var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
+ ghost var g := forall c: SomeClass :: c != null ==> c.f == 0; // cool (this is in a ghost context
+ // outside a function)
+ }
+
+ class SomeClass {
+ var f: int;
+ }
+}
|