From e9ea8f9e56c95c1a36ca24b365de5c2bbb1dfe2a Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Thu, 12 Nov 2015 11:35:30 +0000 Subject: [PATCH] sem_ch10.adb, atree.adb: Minor reformatting. 2015-11-12 Hristian Kirtchev * sem_ch10.adb, atree.adb: Minor reformatting. 2015-11-12 Hristian Kirtchev * sem_elab.adb (Check_A_Call): Add new variable Is_DIC_Proc. Report elaboration issue in SPARK concerning calls to source subprograms or nontrivial Default_Initial_Condition procedures. Add specialized error message to avoid outputting the internal name of the Default_Initial_Condition procedure. * sem_util.ads, sem_util.adb (Is_Non_Trivial_Default_Init_Cond_Procedure): New routine. From-SVN: r230237 --- gcc/ada/ChangeLog | 14 ++++++++++++++ gcc/ada/atree.adb | 9 ++++----- gcc/ada/sem_ch10.adb | 5 ++--- gcc/ada/sem_elab.adb | 31 +++++++++++++++++++++++++++++-- gcc/ada/sem_util.adb | 40 +++++++++++++++++++++++++++++++++++++++- gcc/ada/sem_util.ads | 6 ++++++ 6 files changed, 94 insertions(+), 11 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 63c4f3af4fa..66cde7f47bd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2015-11-12 Hristian Kirtchev + + * sem_ch10.adb, atree.adb: Minor reformatting. + +2015-11-12 Hristian Kirtchev + + * sem_elab.adb (Check_A_Call): Add new variable + Is_DIC_Proc. Report elaboration issue in SPARK concerning calls + to source subprograms or nontrivial Default_Initial_Condition + procedures. Add specialized error message to avoid outputting + the internal name of the Default_Initial_Condition procedure. + * sem_util.ads, sem_util.adb + (Is_Non_Trivial_Default_Init_Cond_Procedure): New routine. + 2015-11-12 Hristian Kirtchev * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index b03da914165..1afaca6908d 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -794,7 +794,7 @@ package body Atree is ------------------------ function Copy_Separate_Tree (Source : Node_Id) return Node_Id is - New_Id : Node_Id; + New_Id : Node_Id; function Copy_Entity (E : Entity_Id) return Entity_Id; -- Copy Entity, copying only the Ekind and Chars fields @@ -803,8 +803,8 @@ package body Atree is -- Copy list function Possible_Copy (Field : Union_Id) return Union_Id; - -- Given a field, returns a copy of the node or list if its parent - -- is the current source node, and otherwise returns the input + -- Given a field, returns a copy of the node or list if its parent is + -- the current source node, and otherwise returns the input. ----------------- -- Copy_Entity -- @@ -871,8 +871,7 @@ package body Atree is begin if Field in Node_Range then - New_N := - Union_Id (Copy_Separate_Tree (Node_Id (Field))); + New_N := Union_Id (Copy_Separate_Tree (Node_Id (Field))); if Parent (Node_Id (Field)) = Source then Set_Parent (Node_Id (New_N), New_Id); diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 5de074e1f25..6ff5f9ebfbc 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -1877,9 +1877,8 @@ package body Sem_Ch10 is -- the extended main unit. if Generate_SCO - and then - In_Extended_Main_Source_Unit - (Cunit_Entity (Current_Sem_Unit)) + and then In_Extended_Main_Source_Unit + (Cunit_Entity (Current_Sem_Unit)) then SCO_Record_Raw (Unum); end if; diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 7f3b42a8530..bab845d359e 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -597,6 +597,11 @@ package body Sem_Elab is -- non-visible unit. This is the scope that is to be investigated to -- see whether an elaboration check is required. + Is_DIC_Proc : Boolean := False; + -- Flag set when the call denotes the Default_Initial_Condition + -- procedure of a private type which wraps a non-trivila assertion + -- expression. + Issue_In_SPARK : Boolean; -- Flag set when a source entity is called during elaboration in SPARK @@ -966,7 +971,16 @@ package body Sem_Elab is return; end if; - Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent); + Is_DIC_Proc := Is_Non_Trivial_Default_Init_Cond_Procedure (Ent); + + -- Elaboration issues in SPARK are reported only for source constructs + -- and for non-trivial Default_Initial_Condition procedures. The latter + -- must be checked because the default initialization of an object of a + -- private type triggers the evaluation of the Default_Initial_Condition + -- expression which in turn may have side effects. + + Issue_In_SPARK := + SPARK_Mode = On and (Comes_From_Source (Ent) or Is_DIC_Proc); -- Now check if an Elaborate_All (or dynamic check) is needed @@ -1016,7 +1030,20 @@ package body Sem_Elab is Ent); elsif Issue_In_SPARK then - Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent); + + -- Emit a specialized error message when the elaboration of an + -- object of a private type evaluates the expression of pragma + -- Default_Initial_Condition. This prevents the internal name + -- of the procedure from appearing in the error message. + + if Is_DIC_Proc then + Error_Msg_N + ("call to Default_Initial_Condition during elaboration in " + & "SPARK", N); + else + Error_Msg_NE + ("call to & during elaboration in SPARK", N, Ent); + end if; else Elab_Warning diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 25ffa96e5d2..f9206ac6c73 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12362,12 +12362,50 @@ package body Sem_Util is end if; end Is_Local_Variable_Reference; + ------------------------------------------------ + -- Is_Non_Trivial_Default_Init_Cond_Procedure -- + ------------------------------------------------ + + function Is_Non_Trivial_Default_Init_Cond_Procedure + (Id : Entity_Id) return Boolean + is + Body_Decl : Node_Id; + Stmt : Node_Id; + + begin + if Ekind (Id) = E_Procedure + and then Is_Default_Init_Cond_Procedure (Id) + then + Body_Decl := + Unit_Declaration_Node + (Corresponding_Body (Unit_Declaration_Node (Id))); + + -- The body of the Default_Initial_Condition procedure must contain + -- at least one statement, otherwise the generation of the subprogram + -- body failed. + + pragma Assert (Present (Handled_Statement_Sequence (Body_Decl))); + + -- To qualify as non-trivial, the first statement of the procedure + -- must be a check in the form of an if statement. If the original + -- Default_Initial_Condition expression was folded, then the first + -- statement is not a check. + + Stmt := First (Statements (Handled_Statement_Sequence (Body_Decl))); + + return + Nkind (Stmt) = N_If_Statement + and then Nkind (Original_Node (Stmt)) = N_Pragma; + end if; + + return False; + end Is_Non_Trivial_Default_Init_Cond_Procedure; + ------------------------- -- Is_Object_Reference -- ------------------------- function Is_Object_Reference (N : Node_Id) return Boolean is - function Is_Internally_Generated_Renaming (N : Node_Id) return Boolean; -- Determine whether N is the name of an internally-generated renaming diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 0f6dd7ceaa4..1aa29e65958 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1433,6 +1433,12 @@ package Sem_Util is -- parameter of the current enclosing subprogram. -- Why are OUT parameters not considered here ??? + function Is_Non_Trivial_Default_Init_Cond_Procedure + (Id : Entity_Id) return Boolean; + -- Determine whether entity Id denotes the procedure which verifies the + -- assertion expression of pragma Default_Initial_Condition and if it does, + -- the encapsulated expression is non-trivial. + function Is_Object_Reference (N : Node_Id) return Boolean; -- Determines if the tree referenced by N represents an object. Both -- variable and constant objects return True (compare Is_Variable). -- 2.30.2