diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-04-18 12:33:46 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-04-18 12:33:46 +0000 |
| commit | a0a15971b87c33e1482ba7bccccf2662149805df (patch) | |
| tree | 783e6520a642cfa7cdf10a2ad41167a9372dc11b /gcc/ada/sem_util.adb | |
| parent | dfcae73695a789358650091aeef1b8caafafede2 (diff) | |
| download | gcc-a0a15971b87c33e1482ba7bccccf2662149805df.tar.gz | |
2016-04-18 Arnaud Charlet <charlet@adacore.com>
* osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New.
* gnat1drv.adb (Gnat1drv): Delete old C files before regenerating them.
* debug.adb: Reserve -gnatd.4 to force generation of C files.
2016-04-18 Yannick Moy <moy@adacore.com>
* sem_eval.adb (Eval_Arithmetic_Op): Do not issue error on static
division by zero, instead possibly issue a warning.
* sem_res.adb (Resolve_Arithmetic_Op): Do not issue error on
static division by zero, instead add check flag on original
expression.
* sem_util.adb, sem_util.ads (Compile_Time_Constraint_Error):
Only issue error when both SPARK_Mode is On and Warn is False.
2016-04-18 Yannick Moy <moy@adacore.com>
* checks.adb (Apply_Scalar_Range_Check): Force
warning instead of error when SPARK_Mode is On, on index out of
bounds, and set check flag for GNATprove.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@235138 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/sem_util.adb')
| -rw-r--r-- | gcc/ada/sem_util.adb | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1146b9dfb1e..348da03b26f 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -4574,9 +4574,16 @@ package body Sem_Util is begin -- If this is a warning, convert it into an error if we are in code - -- subject to SPARK_Mode being set ON. + -- subject to SPARK_Mode being set On, unless Warn is True to force a + -- warning. The rationale is that a compile-time constraint error should + -- lead to an error instead of a warning when SPARK_Mode is On, but in + -- a few cases we prefer to issue a warning and generate both a suitable + -- run-time error in GNAT and a suitable check message in GNATprove. + -- Those cases are those that likely correspond to deactivated SPARK + -- code, so that this kind of code can be compiled and analyzed instead + -- of being rejected. - Error_Msg_Warn := SPARK_Mode /= On; + Error_Msg_Warn := Warn or SPARK_Mode /= On; -- A static constraint error in an instance body is not a fatal error. -- we choose to inhibit the message altogether, because there is no @@ -4648,8 +4655,6 @@ package body Sem_Util is -- evaluated. if not Is_Statically_Unevaluated (N) then - Error_Msg_Warn := SPARK_Mode /= On; - if Present (Ent) then Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc); else |