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