From ba75a2d0b67ce5c330abd1903a6942a9b385d361 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 19 Feb 2012 00:18:00 -0800
Subject: Dafny: make sure assume->assert transformation gives rise to a check

---
 Dafny/DafnyAst.cs | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'Dafny/DafnyAst.cs')

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;
-- 
cgit v1.2.3