diff mbox series

[Ada] Fix missing Overflow and Range checks

Message ID 20220712122506.GA3404535@adacore.com
State New
Headers show
Series [Ada] Fix missing Overflow and Range checks | expand

Commit Message

Pierre-Marie de Rodat July 12, 2022, 12:25 p.m. UTC 
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.

Tested on x86_64-pc-linux-gnu, committed on trunk

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 mbox series

Patch

diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb
--- 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
--- 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
--- 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