diff options
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 8 |
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;
}
|