summaryrefslogtreecommitdiff
path: root/Source/AbsInt/IntervalDomain.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-07-05 14:37:11 -0700
committerGravatar Rustan Leino <unknown>2013-07-05 14:37:11 -0700
commit7fbe519af9271420e5b513021dd1f846a4337e7e (patch)
treee5f6f182941bef103b49a461518a30ab343b43d4 /Source/AbsInt/IntervalDomain.cs
parentfc33b0b2938ad4e81e34c87f054c2880bb56cd17 (diff)
Added support in the abstract interpreter for an attribute {:identity}, which says that a function is an identity function.
Diffstat (limited to 'Source/AbsInt/IntervalDomain.cs')
-rw-r--r--Source/AbsInt/IntervalDomain.cs8
1 files changed, 8 insertions, 0 deletions
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;
}