Range checks on empty ranges typically correspond to deactivated code
based on a given configuration (say, dead code inside a loop over the
empty range). In GNATprove mode, instead of issuing an error message
(which would stop analysis), enable the range check so that GNATprove
will issue a message if it cannot prove that the check is unreachable.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-11-20 Yannick Moy <m...@adacore.com>
* checks.adb (Apply_Scalar_Range_Check): In GNATprove mode,
put a range check when an empty range is used, instead of an
error message.
* sinfo.ads Update comment on GNATprove mode.
Index: sinfo.ads
===================================================================
--- sinfo.ads (revision 217828)
+++ sinfo.ads (working copy)
@@ -581,6 +581,12 @@
-- bounds are generated from an expression: Expand_Subtype_From_Expr
-- should be noop.
+ -- 5. Errors (instead of warnings) are issued on compile-time known
+ -- constraint errors, except in a few selected cases where it should
+ -- be allowed to let analysis proceed (e.g. range checks on empty
+ -- ranges, typically in deactivated code based on a given
+ -- configuration).
+
-----------------------
-- Check Flag Fields --
-----------------------
Index: checks.adb
===================================================================
--- checks.adb (revision 217828)
+++ checks.adb (working copy)
@@ -2926,7 +2926,21 @@
-- since all possible values will raise CE).
if Lov > Hiv then
- Bad_Value;
+
+ -- In GNATprove mode, do not issue a message in that case
+ -- (which would be an error stopping analysis), as this
+ -- likely corresponds to deactivated code based on a
+ -- given configuration (say, dead code inside a loop over
+ -- the empty range). Instead, we enable the range check
+ -- so that GNATprove will issue a message if it cannot be
+ -- proved.
+
+ if GNATprove_Mode then
+ Enable_Range_Check (Expr);
+ else
+ Bad_Value;
+ end if;
+
return;
end if;
