Dafny: make sure assume->assert transformation gives rise to a check

1 files changed, 12 insertions, 1 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 27fbb05c..c9c0ec08 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -101,7 +101,18 @@ namespace Microsoft.Dafny {
       Prev = prev;

     }

 

-    public class Argument {

+    public static bool Contains(Attributes attrs, string nm) {

+      Contract.Requires(nm != null);

+      for (; attrs != null; attrs = attrs.Prev) {

+        if (attrs.Name == nm) {

+          return true;

+        }

+      }

+      return false;

+    }

+

+    public class Argument

+    {

       public readonly IToken Tok;

       public readonly string S;

       public readonly Expression E;