aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_res.adb
diff options
context:
space:
mode:
authorMarc Poulhiès <poulhies@adacore.com>2022-06-17 16:07:35 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2022-07-12 12:24:10 +0000
commit1ef1ac768ff108a6a2c08e18eec3309e182df142 (patch)
tree6320c0b697e8e6e537e34059d30f665686e3226d /gcc/ada/sem_res.adb
parent829b5a6075e63e84600b0eee5daebb3fab9aa491 (diff)
downloadgcc-1ef1ac768ff108a6a2c08e18eec3309e182df142.zip
gcc-1ef1ac768ff108a6a2c08e18eec3309e182df142.tar.gz
gcc-1ef1ac768ff108a6a2c08e18eec3309e182df142.tar.bz2
[Ada] Fix missing Overflow and Range checks
While doing Preanalysis (as is the case during ghost code handling), some range and/or overflow checks can be saved (see Saved_Checks in checks.adb) and later one omitted as they would be redundant (see Find_Check in checks.adb). In the case of ghost code, the node being Preanalyzed is a temporary copy that is discarded, so its corresponding check is not expanded later. The node that gets expanded later is not having any checks expanded as it is wrongly assumed it has already been done before. As is already the case in Preanalyze_And_Resolve, this change suppresses all checks during Preanalyze except for GNATprove mode. gcc/ada/ * sem.adb (Preanalyze): Suppress checks when not in GNATprove mode. * sem_res.adb (Preanalyze_And_Resolve): Add cross reference in comment to above procedure. * sinfo.ads: Typo fix in comment.
Diffstat (limited to 'gcc/ada/sem_res.adb')
-rw-r--r--gcc/ada/sem_res.adb8
1 files changed, 5 insertions, 3 deletions
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 3ff0afd..1053cec 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -2046,16 +2046,18 @@ package body Sem_Res is
Full_Analysis := False;
Expander_Mode_Save_And_Set (False);
+ -- See also Preanalyze_And_Resolve in sem.adb for similar handling
+
-- Normally, we suppress all checks for this preanalysis. There is no
-- point in processing them now, since they will be applied properly
-- and in the proper location when the default expressions reanalyzed
-- and reexpanded later on. We will also have more information at that
-- point for possible suppression of individual checks.
- -- However, in SPARK mode, most expansion is suppressed, and this
- -- later reanalysis and reexpansion may not occur. SPARK mode does
+ -- However, in GNATprove mode, most expansion is suppressed, and this
+ -- later reanalysis and reexpansion may not occur. GNATprove mode does
-- require the setting of checking flags for proof purposes, so we
- -- do the SPARK preanalysis without suppressing checks.
+ -- do the GNATprove preanalysis without suppressing checks.
-- This special handling for SPARK mode is required for example in the
-- case of Ada 2012 constructs such as quantified expressions, which are