Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable wellformedness checks).

2 files changed, 29 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..0128f2ae 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -213,12 +213,15 @@ Execution trace:
     (0,0): anon0

     SmallTests.dfy(266,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(366,12): Error: assertion violation

+SmallTests.dfy(376,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(376,12): Error: assertion violation

+SmallTests.dfy(386,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

+SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon3_Else

 SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -237,8 +240,11 @@ Execution trace:
 SmallTests.dfy(354,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

+SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon3_Else

 

-Dafny program verifier finished with 47 verified, 18 errors

+Dafny program verifier finished with 47 verified, 20 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

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()

+  }

+

 }