From 7fbe519af9271420e5b513021dd1f846a4337e7e Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 5 Jul 2013 14:37:11 -0700
Subject: Added support in the abstract interpreter for an attribute
 {:identity}, which says that a function is an identity function.

---
 Source/AbsInt/IntervalDomain.cs | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'Source/AbsInt')

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index be62eb58..c024a62a 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -857,6 +857,14 @@ namespace Microsoft.Boogie.AbstractInterpretation
             Lo = Node.Min(lo0, lo1, false);
             Hi = Node.Max(hi0, hi1, false);
           }
+        } else if (node.Fun is FunctionCall) {
+          var call = (FunctionCall)node.Fun;
+          // See if this is an identity function, which we do by checking: that the function has
+          // exactly one argument and the function has been marked by the user with the attribute {:identity}
+          bool claimsToBeIdentity = false;
+          if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) {
+            VisitExpr(node.Args[0]);
+          }
         }
         return node;
       }
-- 
cgit v1.2.3