Static analysis tools benefit from some evaluations being done in
frontend, in particular comparisons between values of universal types
which are supposed to be evaluated at compile time and which static
analysis tools like GNATprove may not support. Restore such evaluation
during semantic analysis for arguments of universal types, which was
disabled previously inside assertions to provide static analysis tools
with more information (but still disable when arguments are not of
universal type).
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-04-27 Yannick Moy <m...@adacore.com>
* sem_res.adb (Resolve_Comparison_Op): Always
evaluate comparisons between values of universal types.
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 247312)
+++ sem_res.adb (working copy)
@@ -6927,8 +6927,15 @@
-- this Eval call may change N to True/False. Skip this evaluation
-- inside assertions, in order to keep assertions as written by users
-- for tools that rely on these, e.g. GNATprove for loop invariants.
+ -- Except evaluation is still performed even inside assertions for
+ -- comparisons between values of universal type, which are useless
+ -- for static analysis tools, and not supported even by GNATprove.
- if In_Assertion_Expr = 0 then
+ if In_Assertion_Expr = 0
+ or else (Is_Universal_Numeric_Type (Etype (L))
+ and then
+ Is_Universal_Numeric_Type (Etype (R)))
+ then
Eval_Relational_Op (N);
end if;
end Resolve_Comparison_Op;
