From 39f0fa29d043e4b05c2eb43b2b811303e60dba4f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 20 Nov 2014 12:24:51 +0100 Subject: [multiple changes] 2014-11-20 Thomas Quinot * sem_util.adb: Minor reformatting. 2014-11-20 Robert Dewar * sem_prag.adb (Analyze_Pragma, case Linker_Section): Detect duplicate Linker_Section. 2014-11-20 Ed Schonberg * exp_ch4.adb: Add guard for build-in-place boolean op. 2014-11-20 Yannick Moy * 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. 2014-11-20 Arnaud Charlet * a-stream.ads, s-osinte-linux.ads, a-reatim.ads, a-calend.ads, s-crtl.ads, interfac.ads, s-taskin.ads: Replace uses of 2 ** 63 and 2 ** 64 by references to Long_Long_Integer instead, to allow these units to be analyzed by codepeer or spark when using a target configuration file with long_long_size set to 32. From-SVN: r217840 --- gcc/ada/checks.adb | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'gcc/ada/checks.adb') diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 046c517..e822db3 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2926,7 +2926,21 @@ package body Checks is -- 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; -- cgit v1.1