diff options
| author |  wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
| commit | a1fa34eaba18abe4d6c7e610d939806332930ead (patch) | |
| tree | a1035659063ea335ad786f074f76482f55ec75f1 /Test/dafny0/SmallTests.dfy | |
| parent | 8e692b4f59635eae79c83aa13fbf510416ec13b4 (diff) | |
Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable wellformedness checks).
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index d4a0ad9a..2074e484 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -359,6 +359,16 @@ method {:verify false} test1() assert false;
}
+function test2() : bool
+{
+ !test2() // error
+}
+
+function {:verify false} test3() : bool
+{
+ !test3()
+}
+
class Test {
method test0()
@@ -381,4 +391,14 @@ class Test { assert false;
}
+ function test2() : bool
+ {
+ !test2() // error
+ }
+
+ function {:verify false} test3() : bool
+ {
+ !test3()
+ }
+
}
|