summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-02-08 19:17:33 +0000
committerGravatar MichalMoskal <unknown>2010-02-08 19:17:33 +0000
commit6ee99fcbb25fabab8f30314a317609651587fa53 (patch)
treec8b46184b654d6d7a1b113014dfa79aea501dd85
parent83d8cdb90612d807c2a932ca601ab6ec9ff5de28 (diff)
Fix a bug in checking for {:inline} procedure attribute. Resolves #6993.
-rw-r--r--Source/Core/Inline.ssc42
1 files changed, 7 insertions, 35 deletions
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;