public inbox for gcc-cvs@sourceware.org help / color / mirror / Atom feed
From: Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-1618] [Ada] Fix missing Overflow and Range checks Date: Tue, 12 Jul 2022 12:25:00 +0000 (GMT) [thread overview] Message-ID: <20220712122500.BF5073857806@sourceware.org> (raw) https://gcc.gnu.org/g:1ef1ac768ff108a6a2c08e18eec3309e182df142 commit r13-1618-g1ef1ac768ff108a6a2c08e18eec3309e182df142 Author: Marc Poulhiès <poulhies@adacore.com> Date: Fri Jun 17 16:07:35 2022 +0200 [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. Diff: --- gcc/ada/sem.adb | 10 +++++++++- gcc/ada/sem_res.adb | 8 +++++--- gcc/ada/sinfo.ads | 6 +++--- 3 files changed, 17 insertions(+), 7 deletions(-) diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 796fffb3065..6c1e9d7eb01 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -1338,7 +1338,15 @@ package body Sem is Full_Analysis := False; Expander_Mode_Save_And_Set (False); - Analyze (N); + -- See comment in sem_res.adb for Preanalyze_And_Resolve + + if GNATprove_Mode + or else Nkind (Parent (N)) = N_Simple_Return_Statement + then + Analyze (N); + else + Analyze (N, Suppress => All_Checks); + end if; Expander_Mode_Restore; Full_Analysis := Save_Full_Analysis; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 3ff0afd1712..1053cec6dd2 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 diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index a9099e3a0d9..ddac1c92834 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -554,9 +554,9 @@ package Sinfo is -- The tree after this light expansion should be fully analyzed -- semantically, which sometimes requires the insertion of semantic -- preanalysis, for example for subprogram contracts and pragma - -- check/assert. In particular, all expression must have their proper type, - -- and semantic links should be set between tree nodes (partial to full - -- view, etc.) Some kinds of nodes should be either absent, or can be + -- check/assert. In particular, all expressions must have their proper + -- type, and semantic links should be set between tree nodes (partial to + -- full view, etc.). Some kinds of nodes should be either absent, or can be -- ignored by the formal verification backend: -- N_Object_Renaming_Declaration: can be ignored safely
reply other threads:[~2022-07-12 12:25 UTC|newest] Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20220712122500.BF5073857806@sourceware.org \ --to=pmderodat@gcc.gnu.org \ --cc=gcc-cvs@gcc.gnu.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).