diff mbox

[Ada] Fix evaluation of comparisons for GNATprove

Message ID 20170427105525.GA3946@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 27, 2017, 10:55 a.m. UTC 
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  <moy@adacore.com>

	* sem_res.adb (Resolve_Comparison_Op): Always
	evaluate comparisons between values of universal types.
diff mbox

Patch

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;