From 9be82a702255a26e458440e8fdee9be061c8e39e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 22 Nov 2011 14:00:52 -0800
Subject: Boogie: don't resolve ignored types (that is, "extern" types that
 have been thrown out)

---
 Source/Core/Absy.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/Core/Absy.cs')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 32b27ae6..4ec6eef8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -308,7 +308,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(rc != null);
       // first resolve type constructors
       foreach (Declaration d in TopLevelDeclarations) {
-        if (d is TypeCtorDecl)
+        if (d is TypeCtorDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
           d.Resolve(rc);
       }
 
@@ -316,7 +316,7 @@ namespace Microsoft.Boogie {
       List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
       foreach (Declaration d in TopLevelDeclarations) {
         Contract.Assert(d != null);
-        if (d is TypeSynonymDecl)
+        if (d is TypeSynonymDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
           synonymDecls.Add((TypeSynonymDecl)d);
       }
 
-- 
cgit v1.2.3