From f24745230fe28ddd92d28ff681bd95d10578e3b0 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 27 Apr 2017 12:55:17 +0200 Subject: [PATCH] [multiple changes] 2017-04-27 Steve Baird * exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel flag when it is declared in order to avoid confusing CodePeer about the possibility of an uninitialized variable read. 2017-04-27 Ed Schonberg * sem_dim.adb (Analyze_Dimension_Object_Declaration): There is no dimensionality error if the subtype of the expression is identical to the nominal subtype in the declaration, even though the expression itself may have been constant-folded and lack a dimension vector. * sem_dim.ads: Add comments on setting of dimension vectors and its interaction with node rewritings and side-effect removal. 2017-04-27 Bob Duff * debug.adb: Minor comment correction. * sem_dim.ads: Minor reformatting and typo fixes. 2017-04-27 Bob Duff * g-table.adb, g-table.adsa, scos.h: From the C side, access First and Last of the tables via function calls, rather than relying on layout of data structures. 2017-04-27 Ed Schonberg * exp_util.adb: No wrapper in GNATprove mode. 2017-04-27 Yannick Moy * sem_res.adb (Resolve_Comparison_Op): Always evaluate comparisons between values of universal types. 2017-04-27 Hristian Kirtchev * sem_elab.adb (Check_Internal_Call_Continue): Do not generate an elaboration counter nor a check when in GNATprove mode. * sem_util.adb (Build_Elaboration_Entity): Do not create an elaboration counter when in GNATprove mode. From-SVN: r247317 --- gcc/ada/ChangeLog | 43 +++++++++++++++++++++++++++++++++++++++++++ gcc/ada/debug.adb | 4 ++-- gcc/ada/exp_ch9.adb | 11 ++++++++++- gcc/ada/exp_util.adb | 9 ++++++--- gcc/ada/g-table.adb | 11 ++++++++++- gcc/ada/g-table.ads | 7 ++++--- gcc/ada/scos.h | 18 +++++++++--------- gcc/ada/sem_dim.adb | 6 ++++++ gcc/ada/sem_dim.ads | 12 +++++++++++- gcc/ada/sem_elab.adb | 8 +++++++- gcc/ada/sem_res.adb | 11 +++++++++-- gcc/ada/sem_util.adb | 8 +++++++- 12 files changed, 124 insertions(+), 24 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f06d94eff59..3e64117e84b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,46 @@ +2017-04-27 Steve Baird + + * exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel + flag when it is declared in order to avoid confusing CodePeer about + the possibility of an uninitialized variable read. + +2017-04-27 Ed Schonberg + + * sem_dim.adb (Analyze_Dimension_Object_Declaration): There is + no dimensionality error if the subtype of the expression is + identical to the nominal subtype in the declaration, even though + the expression itself may have been constant-folded and lack a + dimension vector. + * sem_dim.ads: Add comments on setting of dimension vectors and + its interaction with node rewritings and side-effect removal. + +2017-04-27 Bob Duff + + * debug.adb: Minor comment correction. + * sem_dim.ads: Minor reformatting and typo fixes. + +2017-04-27 Bob Duff + + * g-table.adb, g-table.adsa, scos.h: From the C side, access First and + Last of the tables via function calls, rather than relying on layout + of data structures. + +2017-04-27 Ed Schonberg + + * exp_util.adb: No wrapper in GNATprove mode. + +2017-04-27 Yannick Moy + + * sem_res.adb (Resolve_Comparison_Op): Always + evaluate comparisons between values of universal types. + +2017-04-27 Hristian Kirtchev + + * sem_elab.adb (Check_Internal_Call_Continue): Do not generate + an elaboration counter nor a check when in GNATprove mode. + * sem_util.adb (Build_Elaboration_Entity): Do not create an + elaboration counter when in GNATprove mode. + 2017-04-27 Ed Schonberg * freeze.adb: copy-paste typo. diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index c289c98e604..8822265c928 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -848,8 +848,8 @@ package body Debug is -- prefer specs with no bodies to specs with bodies, and between two -- specs with bodies, prefers the one whose body is closer to being -- able to be elaborated. This is a clear improvement, but we provide - -- this debug flag in case of regressions. Note: -gnatdo is even older - -- than -gnatdp. + -- this debug flag in case of regressions. Note: -do is even older + -- than -dp. -- dp Use old elaboration order preference. The new preference rules -- elaborate all units within a strongly connected component together, diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 89f9e71ac9f..6a6766d8692 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -7515,7 +7515,16 @@ package body Exp_Ch9 is Make_Object_Declaration (Loc, Defining_Identifier => Cancel_Param, Object_Definition => - New_Occurrence_Of (Standard_Boolean, Loc))); + New_Occurrence_Of (Standard_Boolean, Loc), + Expression => + New_Occurrence_Of (Standard_False, Loc), + -- True would work equally well here. This initialization + -- should be dead, but only because of things (e.g., + -- abortion deferral) that CodePeer doesn't know about. + -- We want to avoid CodePeer complaints about a possible read + -- of an uninitialized variable when this variable is read, + -- so we initialize it here. + Has_Init_Expression => True)); -- Remove and save the call to Call_Simple diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 8c05d9956c4..c9e099e4511 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1114,10 +1114,13 @@ package body Exp_Util is if Present (New_E) then Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); - -- If the entity is an overridden primitive, we must build a - -- wrapper for the current inherited operation. + -- If the entity is an overridden primitive and we are not + -- in proof mode, we must build a wrapper for the current + -- inherited operation. - if Is_Subprogram (New_E) then + if Is_Subprogram (New_E) + and then not GNATprove_Mode + then Needs_Wrapper := True; end if; end if; diff --git a/gcc/ada/g-table.adb b/gcc/ada/g-table.adb index e12e84f7578..c5c5891336a 100644 --- a/gcc/ada/g-table.adb +++ b/gcc/ada/g-table.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1998-2014, AdaCore -- +-- Copyright (C) 1998-2017, AdaCore -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -116,6 +116,15 @@ package body GNAT.Table is Last_Val := Last_Val - 1; end Decrement_Last; + ----------- + -- First -- + ----------- + + function First return Table_Index_Type is + begin + return Table_Low_Bound; + end First; + -------------- -- For_Each -- -------------- diff --git a/gcc/ada/g-table.ads b/gcc/ada/g-table.ads index 1b4b04c492d..d27b3224224 100644 --- a/gcc/ada/g-table.ads +++ b/gcc/ada/g-table.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1998-2015, AdaCore -- +-- Copyright (C) 1998-2017, AdaCore -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -154,8 +154,9 @@ package GNAT.Table is -- Free all allocated memory for the table. A call to Init is required -- before any use of this table after calling Free. - First : constant Table_Index_Type := Table_Low_Bound; - -- Export First as synonym for Low_Bound (parallel with use of Last) + function First return Table_Index_Type; + pragma Inline (First); + -- Export First as synonym for Table_Low_Bound (parallel with use of Last) procedure Set_Last (New_Val : Table_Index_Type); pragma Inline (Set_Last); diff --git a/gcc/ada/scos.h b/gcc/ada/scos.h index f7b4aba403c..6c1f545af95 100644 --- a/gcc/ada/scos.h +++ b/gcc/ada/scos.h @@ -6,7 +6,7 @@ * * * C Header File * * * - * Copyright (C) 2014, Free Software Foundation, Inc. * + * Copyright (C) 2014-2017, Free Software Foundation, Inc. * * * * GNAT is free software; you can redistribute it and/or modify it under * * terms of the GNU General Public License as published by the Free Soft- * @@ -48,11 +48,11 @@ typedef struct SCO_Unit_Table_Entry *SCO_Unit_Table_Type; extern SCO_Unit_Table_Type scos__sco_unit_table__table; #define SCO_Unit_Table scos__sco_unit_table__table -extern Int scos__sco_unit_table__min; -#define SCO_Unit_Table_Min scos__sco_unit_table__min +extern Int scos__sco_unit_table__first(void); +#define SCO_Unit_Table_First scos__sco_unit_table__first -extern Int scos__sco_unit_table__last_val; -#define SCO_Unit_Table_Last_Val scos__sco_unit_table__last_val +extern Int scos__sco_unit_table__last(void); +#define SCO_Unit_Table_Last scos__sco_unit_table__last /* SCOs table: */ @@ -77,11 +77,11 @@ typedef struct SCO_Table_Entry *SCO_Table_Type; extern SCO_Table_Type scos__sco_table__table; #define SCO_Table scos__sco_table__table -extern Int scos__sco_table__min; -#define SCO_Table_Min scos__sco_table__min +extern Int scos__sco_table__first(void); +#define SCO_Table_First scos__sco_table__first -extern Int scos__sco_table__last_val; -#define SCO_Table_Last_Val scos__sco_table__last_val +extern Int scos__sco_table__last(void); +#define SCO_Table_Last scos__sco_table__last #ifdef __cplusplus } diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb index 01689bffa67..cac2af53011 100644 --- a/gcc/ada/sem_dim.adb +++ b/gcc/ada/sem_dim.adb @@ -2171,6 +2171,12 @@ package body Sem_Dim is Set_Dimensions (Id, Dim_Of_Expr); + -- Expression may have been constant-folded. If nominal type + -- has dimensions, verify that expression has same type. + + elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then + null; + -- For all other cases, issue an error message else diff --git a/gcc/ada/sem_dim.ads b/gcc/ada/sem_dim.ads index fc484eaffdb..bad3bf22b85 100644 --- a/gcc/ada/sem_dim.ads +++ b/gcc/ada/sem_dim.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2011-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2011-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -83,6 +83,16 @@ -- Phase 2 is called only when the node allows a dimension (see body of -- Sem_Dim to get the list of nodes that permit dimensions). +-- In principle every node that is a component of a floating-point expression +-- may have a dimension vector. However, the dimensionality checking is for +-- the most part a bottom-up tree traversal, and the dimensions of operands +-- become irrelevant once the dimensions of an operation have been computed. +-- To minimize space use, the dimensions of operands are removed after the +-- computation of the dimensions of the parent operation. This may complicate +-- the analysis of nodes that have been constant-folded or otherwise rewritten +-- when removing side effects. In such cases, the (sub)type of the expression +-- is used to determine the applicable dimensions. + with Types; use Types; package Sem_Dim is diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 676c1460161..6bf6dfdb728 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -2573,9 +2573,15 @@ package body Sem_Elab is -- Call is not at outer level else + -- Do not generate elaboration checks in GNATprove mode because the + -- elaboration counter and the check are both forms of expansion. + + if GNATprove_Mode then + null; + -- Deal with dynamic elaboration check - if not Elaboration_Checks_Suppressed (E) then + elsif not Elaboration_Checks_Suppressed (E) then Set_Elaboration_Entity_Required (E); -- Case of no elaboration entity allocated yet diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 383a5a95519..132fe67dada 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6927,8 +6927,15 @@ package body Sem_Res is -- this Eval call may change N to True/False. Skip this evaluation -- inside assertions, in order to keep assertions as written by users -- for tools that rely on these, e.g. GNATprove for loop invariants. - - if In_Assertion_Expr = 0 then + -- Except evaluation is still performed even inside assertions for + -- comparisons between values of universal type, which are useless + -- for static analysis tools, and not supported even by GNATprove. + + if In_Assertion_Expr = 0 + or else (Is_Universal_Numeric_Type (Etype (L)) + and then + Is_Universal_Numeric_Type (Etype (R))) + then Eval_Relational_Op (N); end if; end Resolve_Comparison_Op; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index e158905b0f2..200417a5de0 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -1584,7 +1584,13 @@ package body Sem_Util is elsif ASIS_Mode then return; - -- See if we need elaboration entity. + -- Do not generate an elaboration entity in GNATprove move because the + -- elaboration counter is a form of expansion. + + elsif GNATprove_Mode then + return; + + -- See if we need elaboration entity -- We always need an elaboration entity when preserving control flow, as -- we want to remain explicit about the unit's elaboration order. -- 2.30.2