From e24329cdf00e258cfb48e84f55bbd4903cc48939 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 2 Aug 2011 10:21:47 +0000 Subject: [PATCH] par-ch6.adb: Correct obsolete name in comments 2011-08-02 Yannick Moy * par-ch6.adb: Correct obsolete name in comments * restrict.adb, restrict.ads (Check_Formal_Restriction): new function which takes two message arguments (existing function takes one), with second message used for continuation. * sem_ch5.adb (Analyze_Block_Statement): in formal mode, only reject block statements that originate from a source block statement, not generated block statements * sem_ch6.adb (Analyze_Function_Call): rename L into Actuals, for symmetry with procedure case * sem_ch7.adb (Check_One_Tagged_Type_Or_Extension_At_Most): new function to issue an error in formal mode if a package specification contains more than one tagged type or type extension. * sem_res.adb (Resolve_Actuals): in formal mode, check that actual parameters matching formals of tagged types are objects (or ancestor type conversions of objects), not general expressions. Issue an error on view conversions that are not involving ancestor conversion of an extended type. (Resolve_Type_Conversion): in formal mode, issue an error on the operand of an ancestor type conversion which is not an object * sem_util.adb, sem_util.ads (Find_Actual): extend the behavior of the procedure so that it works also for actuals of function calls (Is_Actual_Tagged_Parameter): new function which determines if its argument is an actual parameter of a formal of tagged type in a subprogram call (Is_SPARK_Object_Reference): new function which determines if the tree referenced by its argument represents an object in SPARK From-SVN: r177125 --- gcc/ada/ChangeLog | 29 +++++++++++++++ gcc/ada/par-ch6.adb | 8 ++--- gcc/ada/restrict.adb | 12 +++++++ gcc/ada/restrict.ads | 4 +++ gcc/ada/sem_ch5.adb | 7 +++- gcc/ada/sem_ch6.adb | 10 +++--- gcc/ada/sem_ch7.adb | 58 ++++++++++++++++++++++++++++++ gcc/ada/sem_res.adb | 86 +++++++++++++++++++++++++++++++++++--------- gcc/ada/sem_util.adb | 37 ++++++++++++++++++- gcc/ada/sem_util.ads | 19 ++++++---- 10 files changed, 237 insertions(+), 33 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 712f5f77ac2..6507dea5a22 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2011-08-02 Yannick Moy + + * par-ch6.adb: Correct obsolete name in comments + * restrict.adb, restrict.ads (Check_Formal_Restriction): new function + which takes two message arguments (existing function takes one), with + second message used for continuation. + * sem_ch5.adb (Analyze_Block_Statement): in formal mode, only reject + block statements that originate from a source block statement, not + generated block statements + * sem_ch6.adb (Analyze_Function_Call): rename L into Actuals, for + symmetry with procedure case + * sem_ch7.adb (Check_One_Tagged_Type_Or_Extension_At_Most): new + function to issue an error in formal mode if a package specification + contains more than one tagged type or type extension. + * sem_res.adb (Resolve_Actuals): in formal mode, check that actual + parameters matching formals of tagged types are objects (or ancestor + type conversions of objects), not general expressions. Issue an error + on view conversions that are not involving ancestor conversion of an + extended type. + (Resolve_Type_Conversion): in formal mode, issue an error on the + operand of an ancestor type conversion which is not an object + * sem_util.adb, sem_util.ads (Find_Actual): extend the behavior of the + procedure so that it works also for actuals of function calls + (Is_Actual_Tagged_Parameter): new function which determines if its + argument is an actual parameter of a formal of tagged type in a + subprogram call + (Is_SPARK_Object_Reference): new function which determines if the tree + referenced by its argument represents an object in SPARK + 2011-08-02 Robert Dewar * sem_ch3.adb: Minor reformatting diff --git a/gcc/ada/par-ch6.adb b/gcc/ada/par-ch6.adb index fae8304f410..bcb6161fdd4 100644 --- a/gcc/ada/par-ch6.adb +++ b/gcc/ada/par-ch6.adb @@ -1492,25 +1492,25 @@ package body Ch6 is -- 6.4 Function Call -- ------------------------ - -- Parsed by P_Call_Or_Name (4.1) + -- Parsed by P_Name (4.1) -------------------------------- -- 6.4 Actual Parameter Part -- -------------------------------- - -- Parsed by P_Call_Or_Name (4.1) + -- Parsed by P_Name (4.1) -------------------------------- -- 6.4 Parameter Association -- -------------------------------- - -- Parsed by P_Call_Or_Name (4.1) + -- Parsed by P_Name (4.1) ------------------------------------ -- 6.4 Explicit Actual Parameter -- ------------------------------------ - -- Parsed by P_Call_Or_Name (4.1) + -- Parsed by P_Name (4.1) --------------------------- -- 6.5 Return Statement -- diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 42746f111ca..5a9f0b24cc3 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -118,6 +118,18 @@ package body Restrict is end if; end Check_Formal_Restriction; + procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is + begin + pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\'); + + if Formal_Verification_Mode + and then Comes_From_Source (Original_Node (N)) + then + Error_Msg_F ("|~~" & Msg1, N); + Error_Msg_F (Msg2, N); + end if; + end Check_Formal_Restriction; + ----------------------------------------- -- Check_Implicit_Dynamic_Code_Allowed -- ----------------------------------------- diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads index c491ca94f9a..c006fd6feb1 100644 --- a/gcc/ada/restrict.ads +++ b/gcc/ada/restrict.ads @@ -225,6 +225,10 @@ package Restrict is -- "|~~" (error not serious, language prepended). Call has no effect if -- not in formal mode, or if N does not come originally from source. + procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id); + -- Same as Check_Formal_Restriction except there is a continuation message + -- Msg2 following the initial message Msg1. + procedure Check_Implicit_Dynamic_Code_Allowed (N : Node_Id); -- Tests to see if dynamic code generation (dynamically generated -- trampolines, in particular) is allowed by the current restrictions diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 0780140cdd8..2bf33832515 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -807,7 +807,12 @@ package body Sem_Ch5 is HSS : constant Node_Id := Handled_Statement_Sequence (N); begin - Check_Formal_Restriction ("block statement is not allowed", N); + -- Only reject block statements that originate from a source block + -- statement, in formal mode. + + if Nkind (Original_Node (N)) = N_Block_Statement then + Check_Formal_Restriction ("block statement is not allowed", N); + end if; -- If no handled statement sequence is present, things are really messed -- up, and we just return immediately (defence against previous errors). diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 140113cbf44..c0b17fe325f 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -325,9 +325,9 @@ package body Sem_Ch6 is ---------------------------- procedure Analyze_Function_Call (N : Node_Id) is - P : constant Node_Id := Name (N); - L : constant List_Id := Parameter_Associations (N); - Actual : Node_Id; + P : constant Node_Id := Name (N); + Actuals : constant List_Id := Parameter_Associations (N); + Actual : Node_Id; begin Analyze (P); @@ -353,8 +353,8 @@ package body Sem_Ch6 is -- Otherwise analyze the parameters - if Present (L) then - Actual := First (L); + if Present (Actuals) then + Actual := First (Actuals); while Present (Actual) loop Analyze (Actual); Check_Parameterless_Call (Actual); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index b36c60069a5..1fbaacd0b8d 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -43,6 +43,7 @@ with Nmake; use Nmake; with Nlists; use Nlists; with Opt; use Opt; with Output; use Output; +with Restrict; use Restrict; with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Cat; use Sem_Cat; @@ -873,6 +874,11 @@ package body Sem_Ch7 is -- private_with_clauses, and remove them at the end of the nested -- package. + procedure Check_One_Tagged_Type_Or_Extension_At_Most; + -- Issue an error in formal mode if a package specification contains + -- more than one tagged type or type extension. This is a restriction of + -- SPARK. + procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id); -- Clears constant indications (Never_Set_In_Source, Constant_Value, and -- Is_True_Constant) on all variables that are entities of Id, and on @@ -901,6 +907,56 @@ package body Sem_Ch7 is -- private part rather than being done in Sem_Ch12.Install_Parent -- (which is where the parents' visible declarations are installed). + ------------------------------------------------ + -- Check_One_Tagged_Type_Or_Extension_At_Most -- + ------------------------------------------------ + + procedure Check_One_Tagged_Type_Or_Extension_At_Most is + Previous : Node_Id; + + procedure Check_Decls (Decls : List_Id); + -- Check that either Previous is Empty and Decls does not contain + -- more than one tagged type or type extension, or Previous is + -- already set and Decls contains no tagged type or type extension. + + ----------------- + -- Check_Decls -- + ----------------- + + procedure Check_Decls (Decls : List_Id) is + Decl : Node_Id; + begin + Decl := First (Decls); + while Present (Decl) loop + if Nkind (Decl) = N_Full_Type_Declaration + and then Is_Tagged_Type (Defining_Identifier (Decl)) + then + if No (Previous) then + Previous := Decl; + else + Error_Msg_Sloc := Sloc (Previous); + Check_Formal_Restriction + ("at most one tagged type or type extension allowed", + "\\ previous declaration#", + Decl); + end if; + end if; + + Next (Decl); + end loop; + end Check_Decls; + + -- Start of processing for Check_One_Tagged_Type_Or_Extension_At_Most + + begin + Previous := Empty; + Check_Decls (Vis_Decls); + + if Present (Priv_Decls) then + Check_Decls (Priv_Decls); + end if; + end Check_One_Tagged_Type_Or_Extension_At_Most; + --------------------- -- Clear_Constants -- --------------------- @@ -1383,6 +1439,8 @@ package body Sem_Ch7 is Clear_Constants (Id, First_Entity (Id)); Clear_Constants (Id, First_Private_Entity (Id)); end if; + + Check_One_Tagged_Type_Or_Extension_At_Most; end Analyze_Package_Specification; -------------------------------------- diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index a94ecc27171..fa938c188d1 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3585,29 +3585,70 @@ package body Sem_Res is A_Typ := Etype (A); F_Typ := Etype (F); - -- In SPARK or ALFA, the only view conversions are those involving - -- ancestor conversion of an extended type. - - if Nkind (A) = N_Type_Conversion - and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) + if Comes_From_Source (Original_Node (N)) + and then Nkind_In (Original_Node (N), + N_Function_Call, + N_Procedure_Call_Statement) then - declare - Operand : constant Node_Id := Expression (A); - Operand_Typ : constant Entity_Id := Etype (Operand); - Target_Typ : constant Entity_Id := A_Typ; + -- In formal mode, check that actual parameters matching + -- formals of tagged types are objects (or ancestor type + -- conversions of objects), not general expressions. - begin - if not (Is_Tagged_Type (Target_Typ) + if Is_Actual_Tagged_Parameter (A) then + if Is_SPARK_Object_Reference (A) then + null; + + elsif Nkind (A) = N_Type_Conversion then + declare + Operand : constant Node_Id := Expression (A); + Operand_Typ : constant Entity_Id := Etype (Operand); + Target_Typ : constant Entity_Id := A_Typ; + + begin + if not Is_SPARK_Object_Reference (Operand) then + Check_Formal_Restriction + ("object required", Operand); + + -- In formal mode, the only view conversions are those + -- involving ancestor conversion of an extended type. + + elsif not + (Is_Tagged_Type (Target_Typ) and then not Is_Class_Wide_Type (Target_Typ) and then Is_Tagged_Type (Operand_Typ) and then not Is_Class_Wide_Type (Operand_Typ) and then Is_Ancestor (Target_Typ, Operand_Typ)) - then - Check_Formal_Restriction - ("ancestor conversion is the only permitted view " - & "conversion", A); + then + if Ekind_In + (F, E_Out_Parameter, E_In_Out_Parameter) + then + Check_Formal_Restriction + ("ancestor conversion is the only permitted " + & "view conversion", A); + else + Check_Formal_Restriction + ("ancestor conversion required", A); + end if; + + else + null; + end if; + end; + + else + Check_Formal_Restriction ("object required", A); end if; - end; + + -- In formal mode, the only view conversions are those + -- involving ancestor conversion of an extended type. + + elsif Nkind (A) = N_Type_Conversion + and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) + then + Check_Formal_Restriction + ("ancestor conversion is the only permitted view " + & "conversion", A); + end if; end if; -- Save actual for subsequent check on order dependence, and @@ -9056,6 +9097,19 @@ package body Sem_Res is ("array types should have matching static bounds", N); end if; + -- In formal mode, the operand of an ancestor type conversion must be an + -- object (not an expression). + + if Is_Tagged_Type (Target_Typ) + and then not Is_Class_Wide_Type (Target_Typ) + and then Is_Tagged_Type (Operand_Typ) + and then not Is_Class_Wide_Type (Operand_Typ) + and then Is_Ancestor (Target_Typ, Operand_Typ) + and then not Is_SPARK_Object_Reference (Operand) + then + Check_Formal_Restriction ("object required", Operand); + end if; + -- Note: we do the Eval_Type_Conversion call before applying the -- required checks for a subtype conversion. This is important, since -- both are prepared under certain circumstances to change the type diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 14824ca385b..15e978f4892 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3359,7 +3359,7 @@ package body Sem_Util is then Call := Parent (Parnt); - elsif Nkind (Parnt) = N_Procedure_Call_Statement then + elsif Nkind_In (Parnt, N_Procedure_Call_Statement, N_Function_Call) then Call := Parnt; else @@ -5883,6 +5883,18 @@ package body Sem_Util is end case; end Is_Actual_Parameter; + -------------------------------- + -- Is_Actual_Tagged_Parameter -- + -------------------------------- + + function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean is + Formal : Entity_Id; + Call : Node_Id; + begin + Find_Actual (N, Formal, Call); + return Present (Formal) and then Is_Tagged_Type (Etype (Formal)); + end Is_Actual_Tagged_Parameter; + --------------------- -- Is_Aliased_View -- --------------------- @@ -6833,6 +6845,29 @@ package body Sem_Util is end if; end Is_Object_Reference; + ------------------------------- + -- Is_SPARK_Object_Reference -- + ------------------------------- + + function Is_SPARK_Object_Reference (N : Node_Id) return Boolean is + begin + if Is_Entity_Name (N) then + return Present (Entity (N)) + and then + (Ekind_In (Entity (N), E_Constant, E_Variable) + or else Ekind (Entity (N)) in Formal_Kind); + + else + case Nkind (N) is + when N_Selected_Component => + return Is_SPARK_Object_Reference (Prefix (N)); + + when others => + return False; + end case; + end if; + end Is_SPARK_Object_Reference; + ----------------------------------- -- Is_OK_Variable_For_Out_Formal -- ----------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 6410db4a9b5..c908d885361 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -353,12 +353,12 @@ package Sem_Util is (N : Node_Id; Formal : out Entity_Id; Call : out Node_Id); - -- Determines if the node N is an actual parameter of a procedure call. If - -- so, then Formal points to the entity for the formal (whose Ekind is one - -- of E_In_Parameter, E_Out_Parameter, E_In_Out_Parameter) and Call is set - -- to the node for the corresponding call. If the node N is not an actual - -- parameter, or is an actual parameter of a function call, then Formal and - -- Call are set to Empty. + -- Determines if the node N is an actual parameter of a function of a + -- procedure call. If so, then Formal points to the entity for the formal + -- (whose Ekind is one of E_In_Parameter, E_Out_Parameter, + -- E_In_Out_Parameter) and Call is set to the node for the corresponding + -- call. If the node N is not an actual parameter then Formal and Call are + -- set to Empty. function Find_Corresponding_Discriminant (Id : Node_Id; @@ -677,6 +677,10 @@ package Sem_Util is function Is_Actual_Parameter (N : Node_Id) return Boolean; -- Determines if N is an actual parameter in a subprogram call + function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean; + -- Determines if N is an actual parameter of a formal of tagged type in a + -- subprogram call. + function Is_Aliased_View (Obj : Node_Id) return Boolean; -- Determine if Obj is an aliased view, i.e. the name of an object to which -- 'Access or 'Unchecked_Access can apply. @@ -763,6 +767,9 @@ package Sem_Util is -- Determines if the tree referenced by N represents an object. Both -- variable and constant objects return True (compare Is_Variable). + function Is_SPARK_Object_Reference (N : Node_Id) return Boolean; + -- Determines if the tree referenced by N represents an object in SPARK. + function Is_OK_Variable_For_Out_Formal (AV : Node_Id) return Boolean; -- Used to test if AV is an acceptable formal for an OUT or IN OUT formal. -- Note that the Is_Variable function is not quite the right test because