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;