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

6 files changed, 34 insertions, 8 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d0e0cb0e..b49c011f 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1367,7 +1367,7 @@ namespace Microsoft.Dafny {
         Type elType = cce.NonNull((MultiSetType)e.Type).Arg;

         wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));

         TrExprList(e.Elements);

-        

+

       } else if (expr is SeqDisplayExpr) {

         SeqDisplayExpr e = (SeqDisplayExpr)expr;

         Type elType = cce.NonNull((SeqType)e.Type).Arg;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 8272736c..99ebe8da 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -262,7 +262,7 @@ namespace Microsoft.Dafny {
       this.Arg = arg;

     }

   }

-  

+

   public class SetType : CollectionType {

     public SetType(Type arg) : base(arg) {

       Contract.Requires(arg != null);

@@ -2149,7 +2149,7 @@ namespace Microsoft.Dafny {
       get { return Elements; }

     }

   }

-  

+

   public class SetDisplayExpr : DisplayExpression {

     public SetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)

       : base(tok, elements) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1e41663..5f382eb6 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1499,7 +1499,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));

       req.Add(Requires(f.tok, true, context, null, null));

       Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

-        req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

+        req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq(), etran.TrAttributes(f.Attributes, null));

       sink.TopLevelDeclarations.Add(proc);

 

       VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 80e24356..6cc225d9 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -368,7 +368,7 @@ namespace Microsoft.Dafny
       }

     }

 

-        /// <summary>

+    /// <summary>

     /// Resolve, type check, infer invariants for, and verify the given Boogie program.

     /// The intention is that this Boogie program has been produced by translation from something

     /// else.  Hence, any resolution errors and type checking errors are due to errors in

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

+  }

+

 }