From 6ee99fcbb25fabab8f30314a317609651587fa53 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Mon, 8 Feb 2010 19:17:33 +0000
Subject: Fix a bug in checking for {:inline} procedure attribute. Resolves
 #6993.

---
 Source/Core/Inline.ssc | 42 +++++++-----------------------------------
 1 file changed, 7 insertions(+), 35 deletions(-)

(limited to 'Source')

diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc
index 4d633a24..13137927 100644
--- a/Source/Core/Inline.ssc
+++ b/Source/Core/Inline.ssc
@@ -138,44 +138,16 @@ namespace Microsoft.Boogie {
     // otherwise, the procedure is not inlined at the call site
     protected int GetInlineCount(Implementation! impl) {
       string! procName = impl.Name;
-      int c = -1;
+      int c;
       if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
         return c;
       }
-      
-      bool findattr = false;      
-      
-      QKeyValue kv = null;
-      // try proc attributes
-      if(impl.Proc != null) {
-        kv = impl.Proc.Attributes;
-        while(kv != null) {
-          if(kv.Key.Equals("inline")) {
-            findattr = true;
-            break;
-          }
-          kv = kv.Next;     
-        }
-      }     
-      // try impl attributes
-      if(!findattr) {
-        kv = impl.Attributes;
-        while(kv != null) {
-          if(kv.Key.Equals("inline")) {
-            findattr = true;  
-            break;
-          }
-          kv = kv.Next;     
-        }
-      }
-      
-      if (findattr) {
-        assert(kv != null && kv.Key.Equals("inline"));
-        if (kv.Params.Count == 1) {
-          LiteralExpr lit = kv.Params[0] as LiteralExpr;
-          if (lit != null && lit.isBigNum)
-            c = lit.asBigNum.ToIntSafe;
-        }
+
+      c = -1; // TryGetValue above always overwrites c
+      impl.CheckIntAttribute("inline", ref c);
+      // procedure attribute overrides implementation
+      if (impl.Proc != null) {
+        impl.Proc.CheckIntAttribute("inline", ref c);
       }
       
       recursiveProcUnrollMap[procName] = c;
-- 
cgit v1.2.3