X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=gcc%2Fada%2Fsem_ch6.adb;h=1f3a4c50dd78e9654292c7778fc43c1d3c3655b0;hb=220d1fd9dfd8d7abcb9d5cc38f5ee8e5ba7c2a64;hp=7d947c8ae0a76c84ca35b04e7ecd7e3d48e34c5f;hpb=ddb8a2c7c199ce0f49375bb6d947a45f0f439e6b;p=gcc.git diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 7d947c8ae0a..1f3a4c50dd7 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, 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- -- @@ -23,6 +23,7 @@ -- -- ------------------------------------------------------------------------------ +with Aspects; use Aspects; with Atree; use Atree; with Checks; use Checks; with Debug; use Debug; @@ -192,7 +193,10 @@ package body Sem_Ch6 is -- must appear before the type is frozen, and have the same visibility as -- that of the type. This procedure checks that this rule is met, and -- otherwise emits an error on the subprogram declaration and a warning - -- on the earlier freeze point if it is easy to locate. + -- on the earlier freeze point if it is easy to locate. In Ada 2012 mode, + -- this routine outputs errors (or warnings if -gnatd.E is set). In earlier + -- versions of Ada, warnings are output if Warn_On_Ada_2012_Incompatibility + -- is set, otherwise the call has no effect. procedure Enter_Overloaded_Entity (S : Entity_Id); -- This procedure makes S, a new overloaded entity, into the first visible @@ -211,21 +215,6 @@ package body Sem_Ch6 is -- Create the declaration for an inequality operator that is implicitly -- created by a user-defined equality operator that yields a boolean. - procedure May_Need_Actuals (Fun : Entity_Id); - -- Flag functions that can be called without parameters, i.e. those that - -- have no parameters, or those for which defaults exist for all parameters - - procedure Process_PPCs - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id); - -- Called from Analyze[_Generic]_Subprogram_Body to deal with scanning post - -- conditions for the body and assembling and inserting the _postconditions - -- procedure. N is the node for the subprogram body and Body_Id/Spec_Id are - -- the entities for the body and separate spec (if there is no separate - -- spec, Spec_Id is Empty). Note that invariants and predicates may also - -- provide postconditions, and are also handled in this procedure. - procedure Set_Formal_Validity (Formal_Id : Entity_Id); -- Formal_Id is an formal parameter entity. This procedure deals with -- setting the proper validity status for this entity, which depends on @@ -320,26 +309,31 @@ package body Sem_Ch6 is if Present (Parameter_Specifications (New_Spec)) then declare Formal_Spec : Node_Id; + Def : Entity_Id; + begin Formal_Spec := First (Parameter_Specifications (New_Spec)); + + -- Create a new formal parameter at the same source position + while Present (Formal_Spec) loop - Set_Defining_Identifier - (Formal_Spec, - Make_Defining_Identifier (Sloc (Formal_Spec), - Chars => Chars (Defining_Identifier (Formal_Spec)))); + Def := Defining_Identifier (Formal_Spec); + Set_Defining_Identifier (Formal_Spec, + Make_Defining_Identifier (Sloc (Def), + Chars => Chars (Def))); Next (Formal_Spec); end loop; end; end if; - Prev := Current_Entity_In_Scope (Defining_Entity (Spec)); + Prev := Current_Entity_In_Scope (Defining_Entity (Spec)); -- If there are previous overloadable entities with the same name, -- check whether any of them is completed by the expression function. if Present (Prev) and then Is_Overloadable (Prev) then - Def_Id := Analyze_Subprogram_Specification (Spec); - Prev := Find_Corresponding_Spec (N); + Def_Id := Analyze_Subprogram_Specification (Spec); + Prev := Find_Corresponding_Spec (N); end if; Ret := Make_Simple_Return_Statement (LocX, Expression (N)); @@ -352,15 +346,25 @@ package body Sem_Ch6 is Make_Handled_Sequence_Of_Statements (LocX, Statements => New_List (Ret))); + -- If the expression completes a generic subprogram, we must create a + -- separate node for the body, because at instantiation the original + -- node of the generic copy must be a generic subprogram body, and + -- cannot be a expression function. Otherwise we just rewrite the + -- expression with the non-generic body. + if Present (Prev) and then Ekind (Prev) = E_Generic_Function then + Insert_After (N, New_Body); - -- If the expression completes a generic subprogram, we must create a - -- separate node for the body, because at instantiation the original - -- node of the generic copy must be a generic subprogram body, and - -- cannot be a expression function. Otherwise we just rewrite the - -- expression with the non-generic body. + -- Propagate any aspects or pragmas that apply to the expression + -- function to the proper body when the expression function acts + -- as a completion. + + if Has_Aspects (N) then + Move_Aspects (N, To => New_Body); + end if; + + Relocate_Pragmas_To_Body (New_Body); - Insert_After (N, New_Body); Rewrite (N, Make_Null_Statement (Loc)); Set_Has_Completion (Prev, False); Analyze (N); @@ -370,10 +374,37 @@ package body Sem_Ch6 is elsif Present (Prev) and then Comes_From_Source (Prev) then Set_Has_Completion (Prev, False); + -- An expression function that is a completion freezes the + -- expression. This means freezing the return type, and if it is + -- an access type, freezing its designated type as well. + + -- Note that we cannot defer this freezing to the analysis of the + -- expression itself, because a freeze node might appear in a nested + -- scope, leading to an elaboration order issue in gigi. + + Freeze_Before (N, Etype (Prev)); + + if Is_Access_Type (Etype (Prev)) then + Freeze_Before (N, Designated_Type (Etype (Prev))); + end if; + -- For navigation purposes, indicate that the function is a body Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True); Rewrite (N, New_Body); + + -- Correct the parent pointer of the aspect specification list to + -- reference the rewritten node. + + if Has_Aspects (N) then + Set_Parent (Aspect_Specifications (N), N); + end if; + + -- Propagate any pragmas that apply to the expression function to the + -- proper body when the expression function acts as a completion. + -- Aspects are automatically transfered because of node rewriting. + + Relocate_Pragmas_To_Body (N); Analyze (N); -- Prev is the previous entity with the same name, but it is can @@ -424,13 +455,25 @@ package body Sem_Ch6 is Make_Subprogram_Declaration (Loc, Specification => Spec); Rewrite (N, New_Decl); + + -- Correct the parent pointer of the aspect specification list to + -- reference the rewritten node. + + if Has_Aspects (N) then + Set_Parent (Aspect_Specifications (N), N); + end if; + Analyze (N); Set_Is_Inlined (Defining_Entity (New_Decl)); -- To prevent premature freeze action, insert the new body at the end -- of the current declarations, or at the end of the package spec. -- However, resolve usage names now, to prevent spurious visibility - -- on later entities. + -- on later entities. Note that the function can now be called in + -- the current declarative part, which will appear to be prior to + -- the presence of the body in the code. There are nevertheless no + -- order of elaboration issues because all name resolution has taken + -- place at the point of declaration. declare Decls : List_Id := List_Containing (N); @@ -450,15 +493,19 @@ package body Sem_Ch6 is Push_Scope (Id); Install_Formals (Id); - -- Do a preanalysis of the expression on a separate copy, to - -- prevent visibility issues later with operators in instances. - -- Attach copy to tree so that parent links are available. + -- Preanalyze the expression for name capture, except in an + -- instance, where this has been done during generic analysis, + -- and will be redone when analyzing the body. declare - Expr : constant Node_Id := New_Copy_Tree (Expression (Ret)); + Expr : constant Node_Id := Expression (Ret); + begin Set_Parent (Expr, Ret); - Preanalyze_Spec_Expression (Expr, Etype (Id)); + + if not In_Instance then + Preanalyze_Spec_Expression (Expr, Etype (Id)); + end if; end; End_Scope; @@ -478,6 +525,7 @@ package body Sem_Ch6 is procedure Analyze_Extended_Return_Statement (N : Node_Id) is begin + Check_Compiler_Unit ("extended return statement", N); Analyze_Return_Statement (N); end Analyze_Extended_Return_Statement; @@ -584,7 +632,7 @@ package body Sem_Ch6 is ("(Ada 2005) cannot copy object of a limited type " & "(RM-2005 6.5(5.5/2))", Expr); - if Is_Immutably_Limited_Type (R_Type) then + if Is_Limited_View (R_Type) then Error_Msg_N ("\return by reference not permitted in Ada 2005", Expr); end if; @@ -604,7 +652,7 @@ package body Sem_Ch6 is ("return of limited object not permitted in Ada 2005 " & "(RM-2005 6.5(5.5/2))?y?", Expr); - elsif Is_Immutably_Limited_Type (R_Type) then + elsif Is_Limited_View (R_Type) then Error_Msg_N ("return by reference not permitted in Ada 2005 " & "(RM-2005 6.5(5.5/2))?y?", Expr); @@ -641,25 +689,44 @@ package body Sem_Ch6 is Subtype_Ind : constant Node_Id := Object_Definition (Original_Node (Obj_Decl)); - R_Type_Is_Anon_Access : - constant Boolean := - Ekind (R_Type) = E_Anonymous_Access_Subprogram_Type - or else - Ekind (R_Type) = E_Anonymous_Access_Protected_Subprogram_Type - or else - Ekind (R_Type) = E_Anonymous_Access_Type; + R_Type_Is_Anon_Access : constant Boolean := + Ekind_In (R_Type, + E_Anonymous_Access_Subprogram_Type, + E_Anonymous_Access_Protected_Subprogram_Type, + E_Anonymous_Access_Type); -- True if return type of the function is an anonymous access type -- Can't we make Is_Anonymous_Access_Type in einfo ??? - R_Stm_Type_Is_Anon_Access : - constant Boolean := - Ekind (R_Stm_Type) = E_Anonymous_Access_Subprogram_Type - or else - Ekind (R_Stm_Type) = E_Anonymous_Access_Protected_Subprogram_Type - or else - Ekind (R_Stm_Type) = E_Anonymous_Access_Type; + R_Stm_Type_Is_Anon_Access : constant Boolean := + Ekind_In (R_Stm_Type, + E_Anonymous_Access_Subprogram_Type, + E_Anonymous_Access_Protected_Subprogram_Type, + E_Anonymous_Access_Type); -- True if type of the return object is an anonymous access type + procedure Error_No_Match (N : Node_Id); + -- Output error messages for case where types do not statically + -- match. N is the location for the messages. + + -------------------- + -- Error_No_Match -- + -------------------- + + procedure Error_No_Match (N : Node_Id) is + begin + Error_Msg_N + ("subtype must statically match function result subtype", N); + + if not Predicates_Match (R_Stm_Type, R_Type) then + Error_Msg_Node_2 := R_Type; + Error_Msg_NE + ("\predicate of & does not match predicate of &", + N, R_Stm_Type); + end if; + end Error_No_Match; + + -- Start of processing for Check_Return_Subtype_Indication + begin -- First, avoid cascaded errors @@ -680,9 +747,7 @@ package body Sem_Ch6 is Base_Type (Designated_Type (R_Type)) or else not Subtypes_Statically_Match (R_Stm_Type, R_Type) then - Error_Msg_N - ("subtype must statically match function result subtype", - Subtype_Mark (Subtype_Ind)); + Error_No_Match (Subtype_Mark (Subtype_Ind)); end if; else @@ -692,9 +757,7 @@ package body Sem_Ch6 is if not Conforming_Types (R_Stm_Type, R_Type, Fully_Conformant) then - Error_Msg_N - ("subtype must statically match function result subtype", - Subtype_Ind); + Error_No_Match (Subtype_Ind); end if; end if; @@ -735,9 +798,7 @@ package body Sem_Ch6 is or else Null_Exclusion_Present (Parent (Scope_Id))) /= Can_Never_Be_Null (R_Stm_Type) then - Error_Msg_N - ("subtype must statically match function result subtype", - Subtype_Ind); + Error_No_Match (Subtype_Ind); end if; -- AI05-103: for elementary types, subtypes must statically match @@ -746,9 +807,7 @@ package body Sem_Ch6 is or else Is_Access_Type (R_Type) then if not Subtypes_Statically_Match (R_Stm_Type, R_Type) then - Error_Msg_N - ("subtype must statically match function result subtype", - Subtype_Ind); + Error_No_Match (Subtype_Ind); end if; end if; @@ -875,10 +934,10 @@ package body Sem_Ch6 is -- Can it really happen (extended return???) Error_Msg_N - ("aliased only allowed for limited" - & " return objects in Ada 2012?", N); + ("aliased only allowed for limited return objects " + & "in Ada 2012??", N); - elsif not Is_Immutably_Limited_Type (R_Type) then + elsif not Is_Limited_View (R_Type) then Error_Msg_N ("aliased only allowed for limited" & " return objects", N); end if; @@ -961,7 +1020,7 @@ package body Sem_Ch6 is -- check the static cases. if (Ada_Version < Ada_2005 or else Debug_Flag_Dot_L) - and then Is_Immutably_Limited_Type (Etype (Scope_Id)) + and then Is_Limited_View (Etype (Scope_Id)) and then Object_Access_Level (Expr) > Subprogram_Access_Level (Scope_Id) then @@ -977,11 +1036,9 @@ package body Sem_Ch6 is Reason => PE_Accessibility_Check_Failed)); Analyze (N); - Error_Msg_N - ("cannot return a local value by reference??", N); - Error_Msg_NE - ("\& will be raised at run time??", - N, Standard_Program_Error); + Error_Msg_Warn := SPARK_Mode /= On; + Error_Msg_N ("cannot return a local value by reference<<", N); + Error_Msg_NE ("\& [<<", N, Standard_Program_Error); end if; end if; @@ -1107,6 +1164,7 @@ package body Sem_Ch6 is -- Visible generic entity is callable within its own body Set_Ekind (Gen_Id, Ekind (Body_Id)); + Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Set_Ekind (Body_Id, E_Subprogram_Body); Set_Convention (Body_Id, Convention (Gen_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id)); @@ -1142,13 +1200,14 @@ package body Sem_Ch6 is Set_Actual_Subtypes (N, Current_Scope); - -- Deal with preconditions and postconditions. In formal verification - -- mode, we keep pre- and postconditions attached to entities rather - -- than inserted in the code, in order to facilitate a distinct - -- treatment for them. + -- Deal with [refined] preconditions, postconditions, Contract_Cases, + -- invariants and predicates associated with the body and its spec. + -- Note that this is not pure expansion as Expand_Subprogram_Contract + -- prepares the contract assertions for generic subprograms or for + -- ASIS. Do not generate contract checks in SPARK mode. - if not Alfa_Mode then - Process_PPCs (N, Gen_Id, Body_Id); + if not GNATprove_Mode then + Expand_Subprogram_Contract (N, Gen_Id, Body_Id); end if; -- If the generic unit carries pre- or post-conditions, copy them @@ -1180,6 +1239,11 @@ package body Sem_Ch6 is end loop; end; + Check_SPARK_Mode_In_Generic (N); + + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id, True); + Analyze_Declarations (Declarations (N)); Check_Completion; Analyze (Handled_Statement_Sequence (N)); @@ -1237,7 +1301,7 @@ package body Sem_Ch6 is Null_Body := Make_Subprogram_Body (Loc, Specification => New_Copy_Tree (Spec), - Declarations => New_List, + Declarations => New_List, Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, Statements => New_List (Make_Null_Statement (Loc)))); @@ -1272,7 +1336,6 @@ package body Sem_Ch6 is return; else - -- Resolve the types of the formals now, because the freeze point -- may appear in a different context, e.g. an instantiation. @@ -1358,13 +1421,11 @@ package body Sem_Ch6 is Par : constant Node_Id := Parent (N); begin - if (Nkind (Par) = N_Function_Call - and then N = Name (Par)) + if (Nkind (Par) = N_Function_Call and then N = Name (Par)) or else Nkind (Par) = N_Function_Instantiation - or else (Nkind (Par) = N_Indexed_Component - and then N = Prefix (Par)) + or else (Nkind (Par) = N_Indexed_Component and then N = Prefix (Par)) or else (Nkind (Par) = N_Pragma_Argument_Association - and then not Is_Pragma_String_Literal (Par)) + and then not Is_Pragma_String_Literal (Par)) or else Nkind (Par) = N_Subprogram_Renaming_Declaration or else (Nkind (Par) = N_Attribute_Reference and then Attribute_Name (Par) /= Name_Value) @@ -1894,10 +1955,9 @@ package body Sem_Ch6 is if Is_Tagged_Type (Typ) then null; - elsif Nkind_In (Parent (Parent (N)), - N_Accept_Statement, - N_Entry_Body, - N_Subprogram_Body) + elsif Nkind (Parent (N)) = N_Subprogram_Body + or else Nkind_In (Parent (Parent (N)), N_Accept_Statement, + N_Entry_Body) then Error_Msg_NE ("invalid use of untagged incomplete type&", @@ -1905,7 +1965,7 @@ package body Sem_Ch6 is end if; -- The type must be completed in the current package. This - -- is checked at the end of the package declaraton, when + -- is checked at the end of the package declaration when -- Taft-amendment types are identified. If the return type -- is class-wide, there is no required check, the type can -- be a bona fide TAT. @@ -1967,6 +2027,106 @@ package body Sem_Ch6 is end if; end Analyze_Subprogram_Body; + -------------------------------------- + -- Analyze_Subprogram_Body_Contract -- + -------------------------------------- + + procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is + Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Ref_Depends : Node_Id := Empty; + Ref_Global : Node_Id := Empty; + Spec_Id : Entity_Id; + + begin + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related subprogram body. + + Save_SPARK_Mode_And_Set (Body_Id, Mode); + + -- When a subprogram body declaration is illegal, its defining entity is + -- left unanalyzed. There is nothing left to do in this case because the + -- body lacks a contract, or even a proper Ekind. + + if Ekind (Body_Id) = E_Void then + return; + end if; + + if Nkind (Body_Decl) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + else + Spec_Id := Corresponding_Spec (Body_Decl); + end if; + + -- Locate and store pragmas Refined_Depends and Refined_Global since + -- their order of analysis matters. + + Prag := Classifications (Contract (Body_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Refined_Depends then + Ref_Depends := Prag; + elsif Pragma_Name (Prag) = Name_Refined_Global then + Ref_Global := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze Refined_Global first as Refined_Depends may mention items + -- classified in the global refinement. + + if Present (Ref_Global) then + Analyze_Refined_Global_In_Decl_Part (Ref_Global); + + -- When the corresponding Global aspect/pragma references a state with + -- visible refinement, the body requires Refined_Global. Refinement is + -- not required when SPARK checks are suppressed. + + elsif Present (Spec_Id) then + Prag := Get_Pragma (Spec_Id, Pragma_Global); + + if SPARK_Mode /= Off + and then Present (Prag) + and then Contains_Refined_State (Prag) + then + Error_Msg_NE + ("body of subprogram & requires global refinement", + Body_Decl, Spec_Id); + end if; + end if; + + -- Refined_Depends must be analyzed after Refined_Global in order to see + -- the modes of all global refinements. + + if Present (Ref_Depends) then + Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); + + -- When the corresponding Depends aspect/pragma references a state with + -- visible refinement, the body requires Refined_Depends. Refinement is + -- not required when SPARK checks are suppressed. + + elsif Present (Spec_Id) then + Prag := Get_Pragma (Spec_Id, Pragma_Depends); + + if SPARK_Mode /= Off + and then Present (Prag) + and then Contains_Refined_State (Prag) + then + Error_Msg_NE + ("body of subprogram & requires dependance refinement", + Body_Decl, Spec_Id); + end if; + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Mode); + end Analyze_Subprogram_Body_Contract; + ------------------------------------ -- Analyze_Subprogram_Body_Helper -- ------------------------------------ @@ -2007,6 +2167,10 @@ package body Sem_Ch6 is -- chained beyond that point. It is initialized to Empty to deal with -- the case where there is no separate spec. + procedure Analyze_Aspects_On_Body_Or_Stub; + -- Analyze the aspect specifications of a subprogram body [stub]. It is + -- assumed that N has aspects. + procedure Check_Anonymous_Return; -- Ada 2005: if a function returns an access type that denotes a task, -- or a type that contains tasks, we must create a master entity for @@ -2058,6 +2222,127 @@ package body Sem_Ch6 is -- indicator, check that it is consistent with the known status of the -- entity. + ------------------------------------- + -- Analyze_Aspects_On_Body_Or_Stub -- + ------------------------------------- + + procedure Analyze_Aspects_On_Body_Or_Stub is + procedure Diagnose_Misplaced_Aspects; + -- Subprogram body [stub] N has aspects, but they are not properly + -- placed. Provide precise diagnostics depending on the aspects + -- involved. + + -------------------------------- + -- Diagnose_Misplaced_Aspects -- + -------------------------------- + + procedure Diagnose_Misplaced_Aspects is + Asp : Node_Id; + Asp_Nam : Name_Id; + Asp_Id : Aspect_Id; + -- The current aspect along with its name and id + + procedure SPARK_Aspect_Error (Ref_Nam : Name_Id); + -- Emit an error message concerning SPARK aspect Asp. Ref_Nam is + -- the name of the refined version of the aspect. + + ------------------------ + -- SPARK_Aspect_Error -- + ------------------------ + + procedure SPARK_Aspect_Error (Ref_Nam : Name_Id) is + begin + -- The corresponding spec already contains the aspect in + -- question and the one appearing on the body must be the + -- refined form: + + -- procedure P with Global ...; + -- procedure P with Global ... is ... end P; + -- ^ + -- Refined_Global + + if Has_Aspect (Spec_Id, Asp_Id) then + Error_Msg_Name_1 := Asp_Nam; + + -- Subunits cannot carry aspects that apply to a subprogram + -- declaration. + + if Nkind (Parent (N)) = N_Subunit then + Error_Msg_N ("aspect % cannot apply to a subunit", Asp); + + else + Error_Msg_Name_2 := Ref_Nam; + Error_Msg_N ("aspect % should be %", Asp); + end if; + + -- Otherwise the aspect must appear in the spec, not in the + -- body: + + -- procedure P; + -- procedure P with Global ... is ... end P; + + else + Error_Msg_N + ("aspect specification must appear in subprogram " + & "declaration", Asp); + end if; + end SPARK_Aspect_Error; + + -- Start of processing for Diagnose_Misplaced_Aspects + + begin + -- Iterate over the aspect specifications and emit specific errors + -- where applicable. + + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + Asp_Nam := Chars (Identifier (Asp)); + Asp_Id := Get_Aspect_Id (Asp_Nam); + + -- Do not emit errors on aspects that can appear on a + -- subprogram body. This scenario occurs when the aspect + -- specification list contains both misplaced and properly + -- placed aspects. + + if Aspect_On_Body_Or_Stub_OK (Asp_Id) then + null; + + -- Special diagnostics for SPARK aspects + + elsif Asp_Nam = Name_Depends then + SPARK_Aspect_Error (Name_Refined_Depends); + + elsif Asp_Nam = Name_Global then + SPARK_Aspect_Error (Name_Refined_Global); + + elsif Asp_Nam = Name_Post then + SPARK_Aspect_Error (Name_Refined_Post); + + else + Error_Msg_N + ("aspect specification must appear in subprogram " + & "declaration", Asp); + end if; + + Next (Asp); + end loop; + end Diagnose_Misplaced_Aspects; + + -- Start of processing for Analyze_Aspects_On_Body_Or_Stub + + begin + -- Language-defined aspects cannot be associated with a subprogram + -- body [stub] if the subprogram has a spec. Certain implementation + -- defined aspects are allowed to break this rule (for list, see + -- table Aspect_On_Body_Or_Stub_OK). + + if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then + Diagnose_Misplaced_Aspects; + else + Analyze_Aspect_Specifications (N, Body_Id); + end if; + end Analyze_Aspects_On_Body_Or_Stub; + ---------------------------- -- Check_Anonymous_Return -- ---------------------------- @@ -2095,10 +2380,10 @@ package body Sem_Ch6 is Make_Defining_Identifier (Loc, Name_uMaster), Constant_Present => True, Object_Definition => - New_Reference_To (RTE (RE_Master_Id), Loc), + New_Occurrence_Of (RTE (RE_Master_Id), Loc), Expression => Make_Explicit_Dereference (Loc, - New_Reference_To (RTE (RE_Current_Master), Loc))); + New_Occurrence_Of (RTE (RE_Current_Master), Loc))); if Present (Declarations (N)) then Prepend (Decl, Declarations (N)); @@ -2220,6 +2505,15 @@ package body Sem_Ch6 is Set_Has_Pragma_Inline_Always (Subp); end if; + -- Prior to copying the subprogram body to create a template + -- for it for subsequent inlining, remove the pragma from + -- the current body so that the copy that will produce the + -- new body will start from a completely unanalyzed tree. + + if Nkind (Parent (Prag)) = N_Subprogram_Body then + Rewrite (Prag, Make_Null_Statement (Sloc (Prag))); + end if; + Spec := Subp; end; end if; @@ -2423,7 +2717,7 @@ package body Sem_Ch6 is begin if Ekind (Typ) = E_Incomplete_Type - and then From_With_Type (Typ) + and then From_Limited_With (Typ) and then Present (Non_Limited_View (Typ)) then Set_Etype (Id, Non_Limited_View (Typ)); @@ -2535,6 +2829,16 @@ package body Sem_Ch6 is elsif not Present (Overridden_Operation (Spec_Id)) then Error_Msg_NE ("subprogram& is not overriding", Body_Spec, Spec_Id); + + -- Overriding indicators aren't allowed for protected subprogram + -- bodies (see the Confirmation in Ada Comment AC95-00213). Change + -- this to a warning if -gnatd.E is enabled. + + elsif Ekind (Scope (Spec_Id)) = E_Protected_Type then + Error_Msg_Warn := Error_To_Warning; + Error_Msg_N + ("< False, Force => True); Install_Formals (Body_Id); + Push_Scope (Body_Id); end if; @@ -2948,6 +3260,11 @@ package body Sem_Ch6 is Generate_Reference_To_Formals (Body_Id); end if; + -- Set SPARK_Mode from context + + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id, True); + -- If the return type is an anonymous access type whose designated type -- is the limited view of a class-wide type and the non-limited view is -- available, update the return type accordingly. @@ -2963,7 +3280,9 @@ package body Sem_Ch6 is if Ekind (Rtyp) = E_Anonymous_Access_Type then Etyp := Directly_Designated_Type (Rtyp); - if Is_Class_Wide_Type (Etyp) and then From_With_Type (Etyp) then + if Is_Class_Wide_Type (Etyp) + and then From_Limited_With (Etyp) + then Set_Directly_Designated_Type (Etype (Current_Scope), Available_View (Etyp)); end if; @@ -3012,6 +3331,17 @@ package body Sem_Ch6 is Check_Eliminated (Body_Id); if Nkind (N) = N_Subprogram_Body_Stub then + + -- Analyze any aspect specifications that appear on the subprogram + -- body stub. + + if Has_Aspects (N) then + Analyze_Aspects_On_Body_Or_Stub; + end if; + + -- Stop the analysis now as the stub cannot be inlined, plus it does + -- not have declarative or statement lists. + return; end if; @@ -3085,27 +3415,18 @@ package body Sem_Ch6 is HSS := Handled_Statement_Sequence (N); Set_Actual_Subtypes (N, Current_Scope); - -- Deal with preconditions and postconditions. In formal verification - -- mode, we keep pre- and postconditions attached to entities rather - -- than inserted in the code, in order to facilitate a distinct - -- treatment for them. - - if not Alfa_Mode then - Process_PPCs (N, Spec_Id, Body_Id); - end if; - -- Add a declaration for the Protection object, renaming declarations -- for discriminals and privals and finally a declaration for the entry -- family index (if applicable). This form of early expansion is done -- when the Expander is active because Install_Private_Data_Declarations -- references entities which were created during regular expansion. The - -- body may be the rewritting of an expression function, and we need to - -- verify that the original node is in the source. + -- subprogram entity must come from source, and not be an internally + -- generated subprogram. - if Full_Expander_Active - and then Comes_From_Source (Original_Node (N)) + if Expander_Active and then Present (Prot_Typ) and then Present (Spec_Id) + and then Comes_From_Source (Spec_Id) and then not Is_Eliminated (Spec_Id) then Install_Private_Data_Declarations @@ -3121,12 +3442,56 @@ package body Sem_Ch6 is Exchange_Limited_Views (Spec_Id); end if; + -- Analyze any aspect specifications that appear on the subprogram body + + if Has_Aspects (N) then + Analyze_Aspects_On_Body_Or_Stub; + end if; + + -- Deal with [refined] preconditions, postconditions, Contract_Cases, + -- invariants and predicates associated with the body and its spec. + -- Note that this is not pure expansion as Expand_Subprogram_Contract + -- prepares the contract assertions for generic subprograms or for ASIS. + -- Do not generate contract checks in SPARK mode. + + if not GNATprove_Mode then + Expand_Subprogram_Contract (N, Spec_Id, Body_Id); + end if; + -- Analyze the declarations (this call will analyze the precondition -- Check pragmas we prepended to the list, as well as the declaration -- of the _Postconditions procedure). Analyze_Declarations (Declarations (N)); + -- After declarations have been analyzed, the body has been set + -- its final value of SPARK_Mode. Check that SPARK_Mode for body + -- is consistent with SPARK_Mode for spec. + + if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then + if Present (SPARK_Pragma (Spec_Id)) then + if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off + and then + Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On + then + Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); + Error_Msg_N ("incorrect application of SPARK_Mode#", N); + Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id)); + Error_Msg_NE + ("\value Off was set for SPARK_Mode on&#", N, Spec_Id); + end if; + + elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then + null; + + else + Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); + Error_Msg_N ("incorrect application of SPARK_Mode#", N); + Error_Msg_Sloc := Sloc (Spec_Id); + Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id); + end if; + end if; + -- Check completion, and analyze the statements Check_Completion; @@ -3200,12 +3565,11 @@ package body Sem_Ch6 is -- the body of the procedure. But first we deal with a special case -- where we want to modify this check. If the body of the subprogram -- starts with a raise statement or its equivalent, or if the body - -- consists entirely of a null statement, then it is pretty obvious - -- that it is OK to not reference the parameters. For example, this - -- might be the following common idiom for a stubbed function: - -- statement of the procedure raises an exception. In particular this - -- deals with the common idiom of a stubbed function, which might - -- appear as something like: + -- consists entirely of a null statement, then it is pretty obvious that + -- it is OK to not reference the parameters. For example, this might be + -- the following common idiom for a stubbed function: statement of the + -- procedure raises an exception. In particular this deals with the + -- common idiom of a stubbed function, which appears something like: -- function F (A : Integer) return Some_Type; -- X : Some_Type; @@ -3216,7 +3580,7 @@ package body Sem_Ch6 is -- Here the purpose of X is simply to satisfy the annoying requirement -- in Ada that there be at least one return, and we certainly do not - -- want to go posting warnings on X that it is not initialized! On + -- want to go posting warnings on X that it is not initialized. On -- the other hand, if X is entirely unreferenced that should still -- get a warning. @@ -3320,70 +3684,229 @@ package body Sem_Ch6 is end; end Analyze_Subprogram_Body_Helper; - ------------------------------------ - -- Analyze_Subprogram_Declaration -- - ------------------------------------ + --------------------------------- + -- Analyze_Subprogram_Contract -- + --------------------------------- - procedure Analyze_Subprogram_Declaration (N : Node_Id) is - Scop : constant Entity_Id := Current_Scope; - Designator : Entity_Id; - Is_Completion : Boolean; - -- Indicates whether a null procedure declaration is a completion + procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is + Items : constant Node_Id := Contract (Subp); + Case_Prag : Node_Id := Empty; + Depends : Node_Id := Empty; + Global : Node_Id := Empty; + Mode : SPARK_Mode_Type; + Nam : Name_Id; + Post_Prag : Node_Id := Empty; + Prag : Node_Id; + Seen_In_Case : Boolean := False; + Seen_In_Post : Boolean := False; begin - -- Null procedures are not allowed in SPARK + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related subprogram body. - if Nkind (Specification (N)) = N_Procedure_Specification - and then Null_Present (Specification (N)) - then - Check_SPARK_Restriction ("null procedure is not allowed", N); + Save_SPARK_Mode_And_Set (Subp, Mode); - if Is_Protected_Type (Current_Scope) then - Error_Msg_N ("protected operation cannot be a null procedure", N); - end if; + if Present (Items) then - Analyze_Null_Procedure (N, Is_Completion); + -- Analyze pre- and postconditions - if Is_Completion then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp); - -- The null procedure acts as a body, nothing further is needed. + -- Verify whether a postcondition mentions attribute 'Result and + -- its expression introduces a post-state. - return; - end if; - end if; + if Warn_On_Suspicious_Contract + and then Pragma_Name (Prag) = Name_Postcondition + then + Post_Prag := Prag; + Check_Result_And_Post_State (Prag, Seen_In_Post); + end if; - Designator := Analyze_Subprogram_Specification (Specification (N)); + Prag := Next_Pragma (Prag); + end loop; - -- A reference may already have been generated for the unit name, in - -- which case the following call is redundant. However it is needed for - -- declarations that are the rewriting of an expression function. + -- Analyze contract-cases and test-cases - Generate_Definition (Designator); + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + Nam := Pragma_Name (Prag); - if Debug_Flag_C then - Write_Str ("==> subprogram spec "); - Write_Name (Chars (Designator)); - Write_Str (" from "); - Write_Location (Sloc (N)); - Write_Eol; - Indent; - end if; + if Nam = Name_Contract_Cases then + Analyze_Contract_Cases_In_Decl_Part (Prag); - Validate_RCI_Subprogram_Declaration (N); - New_Overloaded_Entity (Designator); - Check_Delayed_Subprogram (Designator); + -- Verify whether contract-cases mention attribute 'Result and + -- its expression introduces a post-state. Perform the check + -- only when the pragma is legal. - -- If the type of the first formal of the current subprogram is a - -- non-generic tagged private type, mark the subprogram as being a - -- private primitive. Ditto if this is a function with controlling - -- result, and the return type is currently private. In both cases, - -- the type of the controlling argument or result must be in the - -- current scope for the operation to be primitive. + if Warn_On_Suspicious_Contract + and then not Error_Posted (Prag) + then + Case_Prag := Prag; + Check_Result_And_Post_State (Prag, Seen_In_Case); + end if; - if Has_Controlling_Result (Designator) - and then Is_Private_Type (Etype (Designator)) - and then Scope (Etype (Designator)) = Current_Scope - and then not Is_Generic_Actual_Type (Etype (Designator)) + else + pragma Assert (Nam = Name_Test_Case); + Analyze_Test_Case_In_Decl_Part (Prag, Subp); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze classification pragmas + + Prag := Classifications (Items); + while Present (Prag) loop + Nam := Pragma_Name (Prag); + + if Nam = Name_Depends then + Depends := Prag; + else pragma Assert (Nam = Name_Global); + Global := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Analyze Global first as Depends may mention items classified in + -- the global categorization. + + if Present (Global) then + Analyze_Global_In_Decl_Part (Global); + end if; + + -- Depends must be analyzed after Global in order to see the modes of + -- all global items. + + if Present (Depends) then + Analyze_Depends_In_Decl_Part (Depends); + end if; + end if; + + -- Emit an error when neither the postconditions nor the contract-cases + -- mention attribute 'Result in the context of a function. + + if Warn_On_Suspicious_Contract + and then Ekind_In (Subp, E_Function, E_Generic_Function) + then + if Present (Case_Prag) + and then not Seen_In_Case + and then Present (Post_Prag) + and then not Seen_In_Post + then + Error_Msg_N + ("neither function postcondition nor contract cases mention " + & "result?T?", Post_Prag); + + elsif Present (Case_Prag) and then not Seen_In_Case then + Error_Msg_N + ("contract cases do not mention result?T?", Case_Prag); + + -- OK if we have at least one IN OUT parameter + + elsif Present (Post_Prag) and then not Seen_In_Post then + declare + F : Entity_Id; + begin + F := First_Formal (Subp); + while Present (F) loop + if Ekind (F) = E_In_Out_Parameter then + return; + else + Next_Formal (F); + end if; + end loop; + end; + + -- If no in-out parameters and no mention of Result, the contract + -- is certainly suspicious. + + Error_Msg_N + ("function postcondition does not mention result?T?", Post_Prag); + end if; + end if; + + -- Restore the SPARK_Mode of the enclosing context after all delayed + -- pragmas have been analyzed. + + Restore_SPARK_Mode (Mode); + end Analyze_Subprogram_Contract; + + ------------------------------------ + -- Analyze_Subprogram_Declaration -- + ------------------------------------ + + procedure Analyze_Subprogram_Declaration (N : Node_Id) is + Scop : constant Entity_Id := Current_Scope; + Designator : Entity_Id; + + Is_Completion : Boolean; + -- Indicates whether a null procedure declaration is a completion + + begin + -- Null procedures are not allowed in SPARK + + if Nkind (Specification (N)) = N_Procedure_Specification + and then Null_Present (Specification (N)) + then + Check_SPARK_Restriction ("null procedure is not allowed", N); + + if Is_Protected_Type (Current_Scope) then + Error_Msg_N ("protected operation cannot be a null procedure", N); + end if; + + Analyze_Null_Procedure (N, Is_Completion); + + if Is_Completion then + + -- The null procedure acts as a body, nothing further is needed. + + return; + end if; + end if; + + Designator := Analyze_Subprogram_Specification (Specification (N)); + + -- A reference may already have been generated for the unit name, in + -- which case the following call is redundant. However it is needed for + -- declarations that are the rewriting of an expression function. + + Generate_Definition (Designator); + + -- Set SPARK mode from current context (may be overwritten later with + -- explicit pragma). + + Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Designator, True); + + if Debug_Flag_C then + Write_Str ("==> subprogram spec "); + Write_Name (Chars (Designator)); + Write_Str (" from "); + Write_Location (Sloc (N)); + Write_Eol; + Indent; + end if; + + Validate_RCI_Subprogram_Declaration (N); + New_Overloaded_Entity (Designator); + Check_Delayed_Subprogram (Designator); + + -- If the type of the first formal of the current subprogram is a non- + -- generic tagged private type, mark the subprogram as being a private + -- primitive. Ditto if this is a function with controlling result, and + -- the return type is currently private. In both cases, the type of the + -- controlling argument or result must be in the current scope for the + -- operation to be primitive. + + if Has_Controlling_Result (Designator) + and then Is_Private_Type (Etype (Designator)) + and then Scope (Etype (Designator)) = Current_Scope + and then not Is_Generic_Actual_Type (Etype (Designator)) then Set_Is_Private_Primitive (Designator); @@ -4267,7 +4790,7 @@ package body Sem_Ch6 is -- Emit a warning if this is a call to a runtime subprogram -- which is located inside a generic. Previously this call - -- was silently skipped! + -- was silently skipped. if Is_Generic_Instance (Subp) then declare @@ -4726,7 +5249,7 @@ package body Sem_Ch6 is elsif Is_Entity_Name (Orig_Expr) and then Ekind (Entity (Orig_Expr)) = E_Constant - and then Is_Static_Expression (Orig_Expr) + and then Is_OK_Static_Expression (Orig_Expr) then return OK; else @@ -5010,7 +5533,7 @@ package body Sem_Ch6 is -- Compiling with optimizations enabled else - -- Procedures are never frontend inlined in this case! + -- Procedures are never frontend inlined in this case if Ekind (Subp) /= E_Function then return False; @@ -5213,7 +5736,7 @@ package body Sem_Ch6 is Null_Exclusion_Present => Null_Exclusion_Present (Parent (Formal)), Parameter_Type => - New_Reference_To (Etype (Formal), Loc), + New_Occurrence_Of (Etype (Formal), Loc), Expression => Copy_Separate_Tree (Expression (Parent (Formal))))); @@ -5307,11 +5830,11 @@ package body Sem_Ch6 is begin Append_To (Actual_List, - New_Reference_To (Defining_Identifier (New_Obj), Loc)); + New_Occurrence_Of (Defining_Identifier (New_Obj), Loc)); Formal := First_Formal (Spec_Id); while Present (Formal) loop - Append_To (Actual_List, New_Reference_To (Formal, Loc)); + Append_To (Actual_List, New_Occurrence_Of (Formal, Loc)); -- Avoid spurious warning on unreferenced formals @@ -5321,7 +5844,7 @@ package body Sem_Ch6 is Proc_Call := Make_Procedure_Call_Statement (Loc, - Name => New_Reference_To (Proc_Id, Loc), + Name => New_Occurrence_Of (Proc_Id, Loc), Parameter_Associations => Actual_List); end; @@ -5345,7 +5868,7 @@ package body Sem_Ch6 is Make_Simple_Return_Statement (Loc, Expression => - New_Reference_To + New_Occurrence_Of (Defining_Identifier (New_Obj), Loc))))); Rewrite (Ret_Node, Blk_Stmt); @@ -5397,7 +5920,7 @@ package body Sem_Ch6 is end; end if; - -- Build the body to inline only if really needed! + -- Build the body to inline only if really needed if Check_Body_To_Inline (N, Spec_Id) and then Serious_Errors_Detected = 0 @@ -5541,7 +6064,16 @@ package body Sem_Ch6 is null; elsif not Conforming_Types (Old_Type, New_Type, Ctype, Get_Inst) then - Conformance_Error ("\return type does not match!", New_Id); + if Ctype >= Subtype_Conformant + and then not Predicates_Match (Old_Type, New_Type) + then + Conformance_Error + ("\predicate of return type does not match!", New_Id); + else + Conformance_Error + ("\return type does not match!", New_Id); + end if; + return; end if; @@ -5607,7 +6139,7 @@ package body Sem_Ch6 is -- Note: we use the entity information, rather than going directly -- to the specification in the tree. This is not only simpler, but -- absolutely necessary for some cases of conformance tests between - -- operators, where the declaration tree simply does not exist! + -- operators, where the declaration tree simply does not exist. Old_Formal := First_Formal (Old_Id); New_Formal := First_Formal (New_Id); @@ -5778,7 +6310,16 @@ package body Sem_Ch6 is if Errmsg and then Old_Formal_Base = Any_Type then Conforms := False; else - Conformance_Error ("\type of & does not match!", New_Formal); + if Ctype >= Subtype_Conformant + and then + not Predicates_Match (Old_Formal_Base, New_Formal_Base) + then + Conformance_Error + ("\predicate of & does not match!", New_Formal); + else + Conformance_Error + ("\type of & does not match!", New_Formal); + end if; end if; return; @@ -6015,26 +6556,51 @@ package body Sem_Ch6 is ---------------------- procedure Check_Convention (Op : Entity_Id) is + function Convention_Of (Id : Entity_Id) return Convention_Id; + -- Given an entity, return its convention. The function treats Ghost + -- as convention Ada because the two have the same dynamic semantics. + + ------------------- + -- Convention_Of -- + ------------------- + + function Convention_Of (Id : Entity_Id) return Convention_Id is + Conv : constant Convention_Id := Convention (Id); + begin + if Conv = Convention_Ghost then + return Convention_Ada; + else + return Conv; + end if; + end Convention_Of; + + -- Local variables + + Op_Conv : constant Convention_Id := Convention_Of (Op); + Iface_Conv : Convention_Id; Iface_Elmt : Elmt_Id; Iface_Prim_Elmt : Elmt_Id; Iface_Prim : Entity_Id; + -- Start of processing for Check_Convention + begin Iface_Elmt := First_Elmt (Ifaces_List); while Present (Iface_Elmt) loop Iface_Prim_Elmt := - First_Elmt (Primitive_Operations (Node (Iface_Elmt))); + First_Elmt (Primitive_Operations (Node (Iface_Elmt))); while Present (Iface_Prim_Elmt) loop Iface_Prim := Node (Iface_Prim_Elmt); + Iface_Conv := Convention_Of (Iface_Prim); if Is_Interface_Conformant (Typ, Iface_Prim, Op) - and then Convention (Iface_Prim) /= Convention (Op) + and then Iface_Conv /= Op_Conv then Error_Msg_N ("inconsistent conventions in primitive operations", Typ); Error_Msg_Name_1 := Chars (Op); - Error_Msg_Name_2 := Get_Convention_Name (Convention (Op)); + Error_Msg_Name_2 := Get_Convention_Name (Op_Conv); Error_Msg_Sloc := Sloc (Op); if Comes_From_Source (Op) or else No (Alias (Op)) then @@ -6054,9 +6620,8 @@ package body Sem_Ch6 is end if; Error_Msg_Name_1 := Chars (Op); - Error_Msg_Name_2 := - Get_Convention_Name (Convention (Iface_Prim)); - Error_Msg_Sloc := Sloc (Iface_Prim); + Error_Msg_Name_2 := Get_Convention_Name (Iface_Conv); + Error_Msg_Sloc := Sloc (Iface_Prim); Error_Msg_N ("\\overridden operation % with " & "convention % defined #", Typ); @@ -6135,7 +6700,9 @@ package body Sem_Ch6 is then Set_Has_Delayed_Freeze (Designator); - elsif Ekind (T) = E_Incomplete_Type and then From_With_Type (T) then + elsif Ekind (T) = E_Incomplete_Type + and then From_Limited_With (T) + then Set_Has_Delayed_Freeze (Designator); -- AI05-0151: In Ada 2012, Incomplete types can appear in the profile @@ -6177,7 +6744,7 @@ package body Sem_Ch6 is Typ : constant Entity_Id := Etype (Designator); Utyp : constant Entity_Id := Underlying_Type (Typ); begin - if Is_Immutably_Limited_Type (Typ) then + if Is_Limited_View (Typ) then Set_Returns_By_Ref (Designator); elsif Present (Utyp) and then CW_Or_Has_Controlled_Part (Utyp) then Set_Returns_By_Ref (Designator); @@ -6552,11 +7119,6 @@ package body Sem_Ch6 is else Set_Overridden_Operation (Subp, Overridden_Subp); end if; - - -- Ensure that a ghost function is not overriding another routine - - elsif Is_Ghost_Function (Subp) then - Error_Msg_N ("ghost function & cannot be overriding", Subp); end if; end if; @@ -6687,10 +7249,45 @@ package body Sem_Ch6 is Stm : Node_Id; Kind : Node_Kind; + function Assert_False return Boolean; + -- Returns True if Last_Stm is a pragma Assert (False) that has been + -- rewritten as a null statement when assertions are off. The assert + -- is not active, but it is still enough to kill the warning. + + ------------------ + -- Assert_False -- + ------------------ + + function Assert_False return Boolean is + Orig : constant Node_Id := Original_Node (Last_Stm); + + begin + if Nkind (Orig) = N_Pragma + and then Pragma_Name (Orig) = Name_Assert + and then not Error_Posted (Orig) + then + declare + Arg : constant Node_Id := + First (Pragma_Argument_Associations (Orig)); + Exp : constant Node_Id := Expression (Arg); + begin + return Nkind (Exp) = N_Identifier + and then Chars (Exp) = Name_False; + end; + + else + return False; + end if; + end Assert_False; + + -- Local variables + Raise_Exception_Call : Boolean; -- Set True if statement sequence terminated by Raise_Exception call -- or a Reraise_Occurrence call. + -- Start of processing for Check_Statement_Sequence + begin Raise_Exception_Call := False; @@ -6935,7 +7532,7 @@ package body Sem_Ch6 is -- Note: if both ECA and DCA are missing the return, then we -- post only one message, should be enough to fix the bugs. -- If not we will get a message next time on the DCA when the - -- ECA is fixed! + -- ECA is fixed. elsif No (Statements (DCA)) then Last_Stm := DCA; @@ -6980,13 +7577,25 @@ package body Sem_Ch6 is -- If we fall through, issue appropriate message if Mode = 'F' then - if not Raise_Exception_Call then + + -- Kill warning if last statement is a raise exception call, + -- or a pragma Assert (False). Note that with assertions enabled, + -- such a pragma has been converted into a raise exception call + -- already, so the Assert_False is for the assertions off case. + + if not Raise_Exception_Call and then not Assert_False then + + -- In GNATprove mode, it is an error to have a missing return + + Error_Msg_Warn := SPARK_Mode /= On; + + -- Issue error message or warning + Error_Msg_N - ("RETURN statement missing following this statement??!", + ("RETURN statement missing following this statement< S2 in the sense required by this test, + -- for example nameab < namec, but name2 < name10. - -- We ignore postconditions "True" or "False" and contract-cases which - -- have similar consequence expressions, which we call "trivial", when - -- issuing warnings, since these postconditions and contract-cases - -- purposedly ignore the post-state. + ----------------------------- + -- Subprogram_Name_Greater -- + ----------------------------- - Last_Postcondition : Node_Id := Empty; - -- Last non-trivial postcondition on the subprogram, or else Empty if - -- either no non-trivial postcondition or only inherited postconditions. + function Subprogram_Name_Greater (S1, S2 : String) return Boolean is + L1, L2 : Positive; + N1, N2 : Natural; - Last_Contract_Cases : Node_Id := Empty; - -- Last non-trivial contract-cases on the subprogram, or else Empty + begin + -- Deal with special case where names are identical except for a + -- numerical suffix. These are handled specially, taking the numeric + -- ordering from the suffix into account. - Attribute_Result_Mentioned : Boolean := False; - -- Whether attribute 'Result is mentioned in a non-trivial postcondition - -- or contract-cases. + L1 := S1'Last; + while S1 (L1) in '0' .. '9' loop + L1 := L1 - 1; + end loop; - No_Warning_On_Some_Postcondition : Boolean := False; - -- Whether there exists a non-trivial postcondition or contract-cases - -- without a corresponding warning. + L2 := S2'Last; + while S2 (L2) in '0' .. '9' loop + L2 := L2 - 1; + end loop; - Post_State_Mentioned : Boolean := False; - -- Whether some expression mentioned in a postcondition or - -- contract-cases can have a different value in the post-state than - -- in the pre-state. + -- If non-numeric parts non-equal, do straight compare - function Check_Attr_Result (N : Node_Id) return Traverse_Result; - -- Check if N is a reference to the attribute 'Result, and if so set - -- Attribute_Result_Mentioned and return Abandon. Otherwise return OK. + if S1 (S1'First .. L1) /= S2 (S2'First .. L2) then + return S1 > S2; - function Check_Post_State (N : Node_Id) return Traverse_Result; - -- Check whether the value of evaluating N can be different in the - -- post-state, compared to the same evaluation in the pre-state, and - -- if so set Post_State_Mentioned and return Abandon. Return Skip on - -- reference to attribute 'Old, in order to ignore its prefix, which - -- is precisely evaluated in the pre-state. Otherwise return OK. + -- If non-numeric parts equal, compare suffixed numeric parts. Note + -- that a missing suffix is treated as numeric zero in this test. - function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean; - -- Return True if node N is trivially "True" or "False", and it comes - -- from source. In particular, nodes that are statically known "True" or - -- "False" by the compiler but not written as such in source code are - -- not considered as trivial. + else + N1 := 0; + while L1 < S1'Last loop + L1 := L1 + 1; + N1 := N1 * 10 + Character'Pos (S1 (L1)) - Character'Pos ('0'); + end loop; - procedure Process_Contract_Cases (Spec : Node_Id); - -- This processes the Spec_CTC_List from Spec, processing any contract - -- case from the list. The caller has checked that Spec_CTC_List is - -- non-Empty. + N2 := 0; + while L2 < S2'Last loop + L2 := L2 + 1; + N2 := N2 * 10 + Character'Pos (S2 (L2)) - Character'Pos ('0'); + end loop; - procedure Process_Post_Conditions (Spec : Node_Id; Class : Boolean); - -- This processes the Spec_PPC_List from Spec, processing any - -- postcondition from the list. If Class is True, then only - -- postconditions marked with Class_Present are considered. The - -- caller has checked that Spec_PPC_List is non-Empty. + return N1 > N2; + end if; + end Subprogram_Name_Greater; - function Find_Attribute_Result is new Traverse_Func (Check_Attr_Result); + -- Start of processing for Check_Subprogram_Order - function Find_Post_State is new Traverse_Func (Check_Post_State); + begin + -- Check body in alpha order if this is option - ----------------------- - -- Check_Attr_Result -- - ----------------------- + if Style_Check + and then Style_Check_Order_Subprograms + and then Nkind (N) = N_Subprogram_Body + and then Comes_From_Source (N) + and then In_Extended_Main_Source_Unit (N) + then + declare + LSN : String_Ptr + renames Scope_Stack.Table + (Scope_Stack.Last).Last_Subprogram_Name; - function Check_Attr_Result (N : Node_Id) return Traverse_Result is - begin - if Nkind (N) = N_Attribute_Reference - and then Get_Attribute_Id (Attribute_Name (N)) = Attribute_Result - then - Attribute_Result_Mentioned := True; - return Abandon; - else - return OK; - end if; - end Check_Attr_Result; + Body_Id : constant Entity_Id := + Defining_Entity (Specification (N)); - ---------------------- - -- Check_Post_State -- - ---------------------- + begin + Get_Decoded_Name_String (Chars (Body_Id)); - function Check_Post_State (N : Node_Id) return Traverse_Result is - Found : Boolean := False; + if LSN /= null then + if Subprogram_Name_Greater + (LSN.all, Name_Buffer (1 .. Name_Len)) + then + Style.Subprogram_Not_In_Alpha_Order (Body_Id); + end if; - begin - case Nkind (N) is - when N_Function_Call | - N_Explicit_Dereference => - Found := True; + Free (LSN); + end if; - when N_Identifier | - N_Expanded_Name => + LSN := new String'(Name_Buffer (1 .. Name_Len)); + end; + end if; + end Check_Subprogram_Order; - declare - E : constant Entity_Id := Entity (N); - - begin - -- ???Quantified expressions get analyzed later, so E can - -- be empty at this point. In this case, we suppress the - -- warning, just in case E is assignable. It seems better to - -- have false negatives than false positives. At some point, - -- we should make the warning more accurate, either by - -- analyzing quantified expressions earlier, or moving - -- this processing later. - - if No (E) - or else - (Is_Entity_Name (N) - and then Ekind (E) in Assignable_Kind) - then - Found := True; - end if; - end; - - when N_Attribute_Reference => - case Get_Attribute_Id (Attribute_Name (N)) is - when Attribute_Old => - return Skip; - when Attribute_Result => - Found := True; - when others => - null; - end case; - - when others => - null; - end case; - - if Found then - Post_State_Mentioned := True; - return Abandon; - else - return OK; - end if; - end Check_Post_State; - - -------------------------------- - -- Is_Trivial_Post_Or_Ensures -- - -------------------------------- - - function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is - begin - return Is_Entity_Name (N) - and then (Entity (N) = Standard_True - or else - Entity (N) = Standard_False) - and then Comes_From_Source (N); - end Is_Trivial_Post_Or_Ensures; - - ---------------------------- - -- Process_Contract_Cases -- - ---------------------------- - - procedure Process_Contract_Cases (Spec : Node_Id) is - Prag : Node_Id; - Aggr : Node_Id; - Conseq : Node_Id; - Post_Case : Node_Id; - - Ignored : Traverse_Final_Result; - pragma Unreferenced (Ignored); - - begin - Prag := Spec_CTC_List (Contract (Spec)); - loop - if Pragma_Name (Prag) = Name_Contract_Cases then - Aggr := - Expression (First (Pragma_Argument_Associations (Prag))); - - Post_Case := First (Component_Associations (Aggr)); - while Present (Post_Case) loop - Conseq := Expression (Post_Case); - - -- Ignore trivial contract-cases when consequence is "True" - -- or "False". - - if not Is_Trivial_Post_Or_Ensures (Conseq) then - - Last_Contract_Cases := Prag; - - -- For functions, look for presence of 'Result in - -- consequence expression. - - if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then - Ignored := Find_Attribute_Result (Conseq); - end if; - - -- For each individual case, look for presence of an - -- expression that could be evaluated differently in - -- post-state. - - Post_State_Mentioned := False; - Ignored := Find_Post_State (Conseq); - - if Post_State_Mentioned then - No_Warning_On_Some_Postcondition := True; - else - Error_Msg_N - ("contract case refers only to pre-state?T?", - Conseq); - end if; - end if; - - Next (Post_Case); - end loop; - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Contract_Cases; - - ----------------------------- - -- Process_Post_Conditions -- - ----------------------------- - - procedure Process_Post_Conditions - (Spec : Node_Id; - Class : Boolean) - is - Prag : Node_Id; - Arg : Node_Id; - Ignored : Traverse_Final_Result; - pragma Unreferenced (Ignored); - - begin - Prag := Spec_PPC_List (Contract (Spec)); - loop - Arg := First (Pragma_Argument_Associations (Prag)); - - -- Ignore trivial postcondition of "True" or "False" - - if Pragma_Name (Prag) = Name_Postcondition - and then not Is_Trivial_Post_Or_Ensures (Expression (Arg)) - then - -- Since pre- and post-conditions are listed in reverse order, - -- the first postcondition in the list is last in the source. - - if not Class and then No (Last_Postcondition) then - Last_Postcondition := Prag; - end if; - - -- For functions, look for presence of 'Result in postcondition - - if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then - Ignored := Find_Attribute_Result (Arg); - end if; - - -- For each individual non-inherited postcondition, look - -- for presence of an expression that could be evaluated - -- differently in post-state. - - if not Class then - Post_State_Mentioned := False; - Ignored := Find_Post_State (Arg); - - if Post_State_Mentioned then - No_Warning_On_Some_Postcondition := True; - else - Error_Msg_N - ("postcondition refers only to pre-state?T?", Prag); - end if; - end if; - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Post_Conditions; - - -- Start of processing for Check_Subprogram_Contract - - begin - if not Warn_On_Suspicious_Contract then - return; - end if; - - -- Process spec postconditions - - if Present (Spec_PPC_List (Contract (Spec_Id))) then - Process_Post_Conditions (Spec_Id, Class => False); - end if; - - -- Process inherited postconditions - - -- Code is currently commented out as, in some cases, it causes crashes - -- because Direct_Primitive_Operations is not available for a private - -- type. This may cause more warnings to be issued than necessary. ??? - --- for J in Inherited'Range loop --- if Present (Spec_PPC_List (Contract (Inherited (J)))) then --- Process_Post_Conditions (Inherited (J), Class => True); --- end if; --- end loop; - - -- Process contract cases - - if Present (Spec_CTC_List (Contract (Spec_Id))) then - Process_Contract_Cases (Spec_Id); - end if; - - -- Issue warning for functions whose postcondition does not mention - -- 'Result after all postconditions have been processed, and provided - -- all postconditions do not already get a warning that they only refer - -- to pre-state. - - if Ekind_In (Spec_Id, E_Function, E_Generic_Function) - and then (Present (Last_Postcondition) - or else Present (Last_Contract_Cases)) - and then not Attribute_Result_Mentioned - and then No_Warning_On_Some_Postcondition - then - if Present (Last_Postcondition) then - if Present (Last_Contract_Cases) then - Error_Msg_N - ("neither function postcondition nor " - & "contract cases mention result?T?", Last_Postcondition); - - else - Error_Msg_N - ("function postcondition does not mention result?T?", - Last_Postcondition); - end if; - else - Error_Msg_N - ("contract cases do not mention result?T?", Last_Contract_Cases); - end if; - end if; - end Check_Subprogram_Contract; - - ---------------------------- - -- Check_Subprogram_Order -- - ---------------------------- - - procedure Check_Subprogram_Order (N : Node_Id) is - - function Subprogram_Name_Greater (S1, S2 : String) return Boolean; - -- This is used to check if S1 > S2 in the sense required by this test, - -- for example nameab < namec, but name2 < name10. - - ----------------------------- - -- Subprogram_Name_Greater -- - ----------------------------- - - function Subprogram_Name_Greater (S1, S2 : String) return Boolean is - L1, L2 : Positive; - N1, N2 : Natural; - - begin - -- Deal with special case where names are identical except for a - -- numerical suffix. These are handled specially, taking the numeric - -- ordering from the suffix into account. - - L1 := S1'Last; - while S1 (L1) in '0' .. '9' loop - L1 := L1 - 1; - end loop; - - L2 := S2'Last; - while S2 (L2) in '0' .. '9' loop - L2 := L2 - 1; - end loop; - - -- If non-numeric parts non-equal, do straight compare - - if S1 (S1'First .. L1) /= S2 (S2'First .. L2) then - return S1 > S2; - - -- If non-numeric parts equal, compare suffixed numeric parts. Note - -- that a missing suffix is treated as numeric zero in this test. - - else - N1 := 0; - while L1 < S1'Last loop - L1 := L1 + 1; - N1 := N1 * 10 + Character'Pos (S1 (L1)) - Character'Pos ('0'); - end loop; - - N2 := 0; - while L2 < S2'Last loop - L2 := L2 + 1; - N2 := N2 * 10 + Character'Pos (S2 (L2)) - Character'Pos ('0'); - end loop; - - return N1 > N2; - end if; - end Subprogram_Name_Greater; - - -- Start of processing for Check_Subprogram_Order - - begin - -- Check body in alpha order if this is option - - if Style_Check - and then Style_Check_Order_Subprograms - and then Nkind (N) = N_Subprogram_Body - and then Comes_From_Source (N) - and then In_Extended_Main_Source_Unit (N) - then - declare - LSN : String_Ptr - renames Scope_Stack.Table - (Scope_Stack.Last).Last_Subprogram_Name; - - Body_Id : constant Entity_Id := - Defining_Entity (Specification (N)); - - begin - Get_Decoded_Name_String (Chars (Body_Id)); - - if LSN /= null then - if Subprogram_Name_Greater - (LSN.all, Name_Buffer (1 .. Name_Len)) - then - Style.Subprogram_Not_In_Alpha_Order (Body_Id); - end if; - - Free (LSN); - end if; - - LSN := new String'(Name_Buffer (1 .. Name_Len)); - end; - end if; - end Check_Subprogram_Order; - - ------------------------------ - -- Check_Subtype_Conformant -- - ------------------------------ + ------------------------------ + -- Check_Subtype_Conformant -- + ------------------------------ procedure Check_Subtype_Conformant (New_Id : Entity_Id; @@ -7592,8 +7866,8 @@ package body Sem_Ch6 is or else Scope (T1) /= Scope (T2); -- If T2 is a generic actual type it is declared as the subtype of - -- the actual. If that actual is itself a subtype we need to use - -- its own base type to check for compatibility. + -- the actual. If that actual is itself a subtype we need to use its + -- own base type to check for compatibility. elsif Ekind (BT2) = Ekind (T2) and then BT1 = Base_Type (BT2) then return True; @@ -7645,14 +7919,14 @@ package body Sem_Ch6 is -- access-to-class-wide type in a formal. Both entities designate the -- same type. - if From_With_Type (T1) and then T2 = Available_View (T1) then + if From_Limited_With (T1) and then T2 = Available_View (T1) then return True; - elsif From_With_Type (T2) and then T1 = Available_View (T2) then + elsif From_Limited_With (T2) and then T1 = Available_View (T2) then return True; - elsif From_With_Type (T1) - and then From_With_Type (T2) + elsif From_Limited_With (T1) + and then From_Limited_With (T2) and then Available_View (T1) = Available_View (T2) then return True; @@ -7708,13 +7982,16 @@ package body Sem_Ch6 is end if; -- Ada 2005 (AI-254): Anonymous access-to-subprogram types must be - -- treated recursively because they carry a signature. + -- treated recursively because they carry a signature. As far as + -- conformance is concerned, convention plays no role, and either + -- or both could be access to protected subprograms. Are_Anonymous_Access_To_Subprogram_Types := - Ekind (Type_1) = Ekind (Type_2) + Ekind_In (Type_1, E_Anonymous_Access_Subprogram_Type, + E_Anonymous_Access_Protected_Subprogram_Type) and then - Ekind_In (Type_1, E_Anonymous_Access_Subprogram_Type, - E_Anonymous_Access_Protected_Subprogram_Type); + Ekind_In (Type_2, E_Anonymous_Access_Subprogram_Type, + E_Anonymous_Access_Protected_Subprogram_Type); -- Test anonymous access type case. For this case, static subtype -- matching is required for mode conformance (RM 6.3.1(15)). We check @@ -7983,13 +8260,19 @@ package body Sem_Ch6 is -- on discriminants and others do not (and requiring the extra -- formal would introduce distributed overhead). + -- If the type does not have a completion yet, treat as prior to + -- Ada 2012 for consistency. + if Has_Discriminants (Formal_Type) and then not Is_Constrained (Formal_Type) and then not Is_Indefinite_Subtype (Formal_Type) and then (Ada_Version < Ada_2012 - or else - not (Is_Tagged_Type (Underlying_Type (Formal_Type)) - and then Is_Limited_Type (Formal_Type))) + or else No (Underlying_Type (Formal_Type)) + or else not + (Is_Limited_Type (Formal_Type) + and then + (Is_Tagged_Type + (Underlying_Type (Formal_Type))))) then Set_Extra_Constrained (Formal, Add_Extra_Formal (Formal, Standard_Boolean, E, "O")); @@ -8137,7 +8420,8 @@ package body Sem_Ch6 is -- the designated type comes from the limited view (for back-end -- purposes). - Set_From_With_Type (Formal_Typ, From_With_Type (Result_Subt)); + Set_From_Limited_With + (Formal_Typ, From_Limited_With (Result_Subt)); Layout_Type (Formal_Typ); @@ -8258,63 +8542,140 @@ package body Sem_Ch6 is Obj_Decl : Node_Id; begin - if Nkind (Decl) = N_Subprogram_Declaration - and then Is_Record_Type (Typ) - and then not Is_Tagged_Type (Typ) + -- This check applies only if we have a subprogram declaration with a + -- non-tagged record type. + + if Nkind (Decl) /= N_Subprogram_Declaration + or else not Is_Record_Type (Typ) + or else Is_Tagged_Type (Typ) then - -- If the type is not declared in a package, or if we are in the - -- body of the package or in some other scope, the new operation is - -- not primitive, and therefore legal, though suspicious. If the - -- type is a generic actual (sub)type, the operation is not primitive - -- either because the base type is declared elsewhere. - - if Is_Frozen (Typ) then - if Ekind (Scope (Typ)) /= E_Package - or else Scope (Typ) /= Current_Scope - then - null; + return; + end if; - elsif Is_Generic_Actual_Type (Typ) then - null; + -- In Ada 2012 case, we will output errors or warnings depending on + -- the setting of debug flag -gnatd.E. + + if Ada_Version >= Ada_2012 then + Error_Msg_Warn := Debug_Flag_Dot_EE; + + -- In earlier versions of Ada, nothing to do unless we are warning on + -- Ada 2012 incompatibilities (Warn_On_Ada_2012_Incompatibility set). + + else + if not Warn_On_Ada_2012_Compatibility then + return; + end if; + end if; + + -- Cases where the type has already been frozen + + if Is_Frozen (Typ) then + + -- If the type is not declared in a package, or if we are in the body + -- of the package or in some other scope, the new operation is not + -- primitive, and therefore legal, though suspicious. Should we + -- generate a warning in this case ??? + + if Ekind (Scope (Typ)) /= E_Package + or else Scope (Typ) /= Current_Scope + then + return; + + -- If the type is a generic actual (sub)type, the operation is not + -- primitive either because the base type is declared elsewhere. + + elsif Is_Generic_Actual_Type (Typ) then + return; + + -- Here we have a definite error of declaration after freezing - elsif In_Package_Body (Scope (Typ)) then + else + if Ada_Version >= Ada_2012 then Error_Msg_NE - ("equality operator must be declared " - & "before type& is frozen", Eq_Op, Typ); - Error_Msg_N - ("\move declaration to package spec", Eq_Op); + ("equality operator must be declared before type& is " + & "frozen (RM 4.5.2 (9.8)) (Ada 2012)<<", Eq_Op, Typ); + + -- In Ada 2012 mode with error turned to warning, output one + -- more warning to warn that the equality operation may not + -- compose. This is the consequence of ignoring the error. + + if Error_Msg_Warn then + Error_Msg_N ("\equality operation may not compose??", Eq_Op); + end if; else Error_Msg_NE - ("equality operator must be declared " - & "before type& is frozen", Eq_Op, Typ); + ("equality operator must be declared before type& is " + & "frozen (RM 4.5.2 (9.8)) (Ada 2012)?y?", Eq_Op, Typ); + end if; + + -- If we are in the package body, we could just move the + -- declaration to the package spec, so add a message saying that. + + if In_Package_Body (Scope (Typ)) then + if Ada_Version >= Ada_2012 then + Error_Msg_N + ("\move declaration to package spec<<", Eq_Op); + else + Error_Msg_N + ("\move declaration to package spec (Ada 2012)?y?", Eq_Op); + end if; + -- Otherwise try to find the freezing point + + else Obj_Decl := Next (Parent (Typ)); while Present (Obj_Decl) and then Obj_Decl /= Decl loop if Nkind (Obj_Decl) = N_Object_Declaration and then Etype (Defining_Identifier (Obj_Decl)) = Typ then - Error_Msg_NE - ("type& is frozen by declaration??", Obj_Decl, Typ); - Error_Msg_N - ("\an equality operator cannot be declared after this " - & "point (RM 4.5.2 (9.8)) (Ada 2012))??", Obj_Decl); + -- Freezing point, output warnings + + if Ada_Version >= Ada_2012 then + Error_Msg_NE + ("type& is frozen by declaration??", Obj_Decl, Typ); + Error_Msg_N + ("\an equality operator cannot be declared after " + & "this point??", + Obj_Decl); + else + Error_Msg_NE + ("type& is frozen by declaration (Ada 2012)?y?", + Obj_Decl, Typ); + Error_Msg_N + ("\an equality operator cannot be declared after " + & "this point (Ada 2012)?y?", + Obj_Decl); + end if; + exit; end if; Next (Obj_Decl); end loop; end if; + end if; - elsif not In_Same_List (Parent (Typ), Decl) - and then not Is_Limited_Type (Typ) - then + -- Here if type is not frozen yet. It is illegal to have a primitive + -- equality declared in the private part if the type is visible. - -- This makes it illegal to have a primitive equality declared in - -- the private part if the type is visible. + elsif not In_Same_List (Parent (Typ), Decl) + and then not Is_Limited_Type (Typ) + then + -- Shouldn't we give an RM reference here??? - Error_Msg_N ("equality operator appears too late", Eq_Op); - end if; + if Ada_Version >= Ada_2012 then + Error_Msg_N + ("equality operator appears too late<<", Eq_Op); + else + Error_Msg_N + ("equality operator appears too late (Ada 2012)?y?", Eq_Op); + end if; + + -- No error detected + + else + return; end if; end Check_Untagged_Equality; @@ -8343,10 +8704,35 @@ package body Sem_Ch6 is function Different_Generic_Profile (E : Entity_Id) return Boolean is F1, F2 : Entity_Id; + function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean; + -- Check that the types of corresponding formals have the same + -- generic actual if any. We have to account for subtypes of a + -- generic formal, declared between a spec and a body, which may + -- appear distinct in an instance but matched in the generic. + + ------------------------- + -- Same_Generic_Actual -- + ------------------------- + + function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean is + begin + return Is_Generic_Actual_Type (T1) = Is_Generic_Actual_Type (T2) + or else + (Present (Parent (T1)) + and then Comes_From_Source (Parent (T1)) + and then Nkind (Parent (T1)) = N_Subtype_Declaration + and then Is_Entity_Name (Subtype_Indication (Parent (T1))) + and then Entity (Subtype_Indication (Parent (T1))) = T2); + end Same_Generic_Actual; + + -- Start of processing for Different_Generic_Profile + begin - if Ekind (E) = E_Function - and then Is_Generic_Actual_Type (Etype (E)) /= - Is_Generic_Actual_Type (Etype (Designator)) + if not In_Instance then + return False; + + elsif Ekind (E) = E_Function + and then not Same_Generic_Actual (Etype (E), Etype (Designator)) then return True; end if; @@ -8354,9 +8740,7 @@ package body Sem_Ch6 is F1 := First_Formal (Designator); F2 := First_Formal (E); while Present (F1) loop - if Is_Generic_Actual_Type (Etype (F1)) /= - Is_Generic_Actual_Type (Etype (F2)) - then + if not Same_Generic_Actual (Etype (F1), Etype (F2)) then return True; end if; @@ -8453,7 +8837,7 @@ package body Sem_Ch6 is -- If E is an internal function with a controlling result that -- was created for an operation inherited by a null extension, -- it may be overridden by a body without a previous spec (one - -- more reason why these should be shunned). In that case + -- more reason why these should be shunned). In that case we -- remove the generated body if present, because the current -- one is the explicit overriding. @@ -8589,7 +8973,7 @@ package body Sem_Ch6 is end if; -- Compare two lists, skipping rewrite insertions (we want to compare - -- the original trees, not the expanded versions!) + -- the original trees, not the expanded versions). loop if Is_Rewrite_Insertion (N1) then @@ -8645,7 +9029,7 @@ package body Sem_Ch6 is begin -- Non-conformant if paren count does not match. Note: if some idiot -- complains that we don't do this right for more than 3 levels of - -- parentheses, they will be treated with the respect they deserve! + -- parentheses, they will be treated with the respect they deserve. if Paren_Count (E1) /= Paren_Count (E2) then return False; @@ -8993,9 +9377,9 @@ package body Sem_Ch6 is -- All other node types cannot appear in this context. Strictly -- we should raise a fatal internal error. Instead we just ignore -- the nodes. This means that if anyone makes a mistake in the - -- expander and mucks an expression tree irretrievably, the - -- result will be a failure to detect a (probably very obscure) - -- case of non-conformance, which is better than bombing on some + -- expander and mucks an expression tree irretrievably, the result + -- will be a failure to detect a (probably very obscure) case + -- of non-conformance, which is better than bombing on some -- case where two expressions do in fact conform. when others => @@ -9111,7 +9495,12 @@ package body Sem_Ch6 is Iface_Prim : Entity_Id; Prim : Entity_Id) return Boolean is - Iface : constant Entity_Id := Find_Dispatching_Type (Iface_Prim); + -- The operation may in fact be an inherited (implicit) operation + -- rather than the original interface primitive, so retrieve the + -- ultimate ancestor. + + Iface : constant Entity_Id := + Find_Dispatching_Type (Ultimate_Alias (Iface_Prim)); Typ : constant Entity_Id := Find_Dispatching_Type (Prim); function Controlling_Formal (Prim : Entity_Id) return Entity_Id; @@ -9122,9 +9511,10 @@ package body Sem_Ch6 is ------------------------ function Controlling_Formal (Prim : Entity_Id) return Entity_Id is - E : Entity_Id := First_Entity (Prim); + E : Entity_Id; begin + E := First_Entity (Prim); while Present (E) loop if Is_Formal (E) and then Is_Controlling_Formal (E) then return E; @@ -9169,8 +9559,8 @@ package body Sem_Ch6 is -- The mode of the controlling formals must match elsif Present (Iface_Ctrl_F) - and then Present (Prim_Ctrl_F) - and then Ekind (Iface_Ctrl_F) /= Ekind (Prim_Ctrl_F) + and then Present (Prim_Ctrl_F) + and then Ekind (Iface_Ctrl_F) /= Ekind (Prim_Ctrl_F) then return False; @@ -9185,8 +9575,8 @@ package body Sem_Ch6 is return Type_Conformant (Iface_Prim, Prim, Skip_Controlling_Formals => True); - -- Case of a function returning an interface, or an access to one. - -- Check that the return types correspond. + -- Case of a function returning an interface, or an access to one. Check + -- that the return types correspond. elsif Implements_Interface (Typ, Iface) then if (Ekind (Etype (Prim)) = E_Anonymous_Access_Type) @@ -9196,7 +9586,7 @@ package body Sem_Ch6 is return False; else return - Type_Conformant (Prim, Iface_Prim, + Type_Conformant (Prim, Ultimate_Alias (Iface_Prim), Skip_Controlling_Formals => True); end if; @@ -9407,8 +9797,8 @@ package body Sem_Ch6 is Next_Elmt (Prim_Elt); end loop; - -- If no match found, then the new subprogram does not - -- override in the generic (nor in the instance). + -- If no match found, then the new subprogram does not override + -- in the generic (nor in the instance). -- If the type in question is not abstract, and the subprogram -- is, this will be an error if the new operation is in the @@ -9449,7 +9839,7 @@ package body Sem_Ch6 is begin for J in Inherited'Range loop - P := Spec_PPC_List (Contract (Inherited (J))); + P := Pre_Post_Conditions (Contract (Inherited (J))); while Present (P) loop Error_Msg_Sloc := Sloc (P); @@ -9513,13 +9903,13 @@ package body Sem_Ch6 is Make_Parameter_Specification (Loc, Defining_Identifier => A, Parameter_Type => - New_Reference_To (Etype (First_Formal (S)), + New_Occurrence_Of (Etype (First_Formal (S)), Sloc (Etype (First_Formal (S))))), Make_Parameter_Specification (Loc, Defining_Identifier => B, Parameter_Type => - New_Reference_To (Etype (Next_Formal (First_Formal (S))), + New_Occurrence_Of (Etype (Next_Formal (First_Formal (S))), Sloc (Etype (Next_Formal (First_Formal (S))))))); Decl := @@ -9529,13 +9919,13 @@ package body Sem_Ch6 is Defining_Unit_Name => Op_Name, Parameter_Specifications => Formals, Result_Definition => - New_Reference_To (Standard_Boolean, Loc))); + New_Occurrence_Of (Standard_Boolean, Loc))); -- Insert inequality right after equality if it is explicit or after -- the derived type when implicit. These entities are created only - -- for visibility purposes, and eventually replaced in the course of - -- expansion, so they do not need to be attached to the tree and seen - -- by the back-end. Keeping them internal also avoids spurious + -- for visibility purposes, and eventually replaced in the course + -- of expansion, so they do not need to be attached to the tree and + -- seen by the back-end. Keeping them internal also avoids spurious -- freezing problems. The declaration is inserted in the tree for -- analysis, and removed afterwards. If the equality operator comes -- from an explicit declaration, attach the inequality immediately @@ -9644,9 +10034,9 @@ package body Sem_Ch6 is New_E : Entity_Id) return Boolean; -- Check whether new subprogram and old subprogram are both inherited -- from subprograms that have distinct dispatch table entries. This can - -- occur with derivations from instances with accidental homonyms. - -- The function is conservative given that the converse is only true - -- within instances that contain accidental overloadings. + -- occur with derivations from instances with accidental homonyms. The + -- function is conservative given that the converse is only true within + -- instances that contain accidental overloadings. ------------------------------------ -- Check_For_Primitive_Subprogram -- @@ -10214,8 +10604,7 @@ package body Sem_Ch6 is and then In_Private_Part (Current_Scope) then Priv_Decls := - Private_Declarations - (Specification (Unit_Declaration_Node (Current_Scope))); + Private_Declarations (Package_Specification (Current_Scope)); return In_Package_Body (Current_Scope) or else @@ -10313,8 +10702,8 @@ package body Sem_Ch6 is Check_Dispatching_Operation (S, Empty); Check_For_Primitive_Subprogram (Is_Primitive_Subp); - -- If subprogram has an explicit declaration, check whether it - -- has an overriding indicator. + -- If subprogram has an explicit declaration, check whether it has an + -- overriding indicator. if Comes_From_Source (S) then Check_Synchronized_Overriding (S, Overridden_Subp); @@ -10405,11 +10794,21 @@ package body Sem_Ch6 is if Scope (E) /= Current_Scope then null; - -- Ada 2012 (AI05-0165): For internally generated bodies of - -- null procedures locate the internally generated spec. We - -- enforce mode conformance since a tagged type may inherit - -- from interfaces several null primitives which differ only - -- in the mode of the formals. + -- A function can overload the name of an abstract state. The + -- state can be viewed as a function with a profile that cannot + -- be matched by anything. + + elsif Ekind (S) = E_Function + and then Ekind (E) = E_Abstract_State + then + Enter_Overloaded_Entity (S); + return; + + -- Ada 2012 (AI05-0165): For internally generated bodies of null + -- procedures locate the internally generated spec. We enforce + -- mode conformance since a tagged type may inherit from + -- interfaces several null primitives which differ only in + -- the mode of the formals. elsif not Comes_From_Source (S) and then Is_Null_Procedure (S) @@ -10818,10 +11217,7 @@ package body Sem_Ch6 is and then not Is_Dispatching_Operation (S) then Make_Inequality_Operator (S); - - if Ada_Version >= Ada_2012 then - Check_Untagged_Equality (S); - end if; + Check_Untagged_Equality (S); end if; end New_Overloaded_Entity; @@ -10843,7 +11239,7 @@ package body Sem_Ch6 is First_Out_Param : Entity_Id := Empty; -- Used for setting Is_Only_Out_Parameter - function Designates_From_With_Type (Typ : Entity_Id) return Boolean; + function Designates_From_Limited_With (Typ : Entity_Id) return Boolean; -- Determine whether an access type designates a type coming from a -- limited view. @@ -10852,11 +11248,11 @@ package body Sem_Ch6 is -- default has the type of the formal, so we must also check explicitly -- for an access attribute. - ------------------------------- - -- Designates_From_With_Type -- - ------------------------------- + ---------------------------------- + -- Designates_From_Limited_With -- + ---------------------------------- - function Designates_From_With_Type (Typ : Entity_Id) return Boolean is + function Designates_From_Limited_With (Typ : Entity_Id) return Boolean is Desig : Entity_Id := Typ; begin @@ -10869,8 +11265,9 @@ package body Sem_Ch6 is end if; return - Ekind (Desig) = E_Incomplete_Type and then From_With_Type (Desig); - end Designates_From_With_Type; + Ekind (Desig) = E_Incomplete_Type + and then From_Limited_With (Desig); + end Designates_From_Limited_With; --------------------------- -- Is_Class_Wide_Default -- @@ -10924,11 +11321,17 @@ package body Sem_Ch6 is -- Ada 2012: tagged incomplete types are allowed as generic -- formal types. They do not introduce dependencies and the -- corresponding generic subprogram does not have a delayed - -- freeze, because it does not need a freeze node. - - if Is_Tagged_Type (Formal_Type) then + -- freeze, because it does not need a freeze node. However, + -- it is still the case that untagged incomplete types cannot + -- be Taft-amendment types and must be completed in private + -- part, so the subprogram must appear in the list of private + -- dependents of the type. + + if Is_Tagged_Type (Formal_Type) + or else Ada_Version >= Ada_2012 + then if Ekind (Scope (Current_Scope)) = E_Package - and then not From_With_Type (Formal_Type) + and then not From_Limited_With (Formal_Type) and then not Is_Generic_Type (Formal_Type) and then not Is_Class_Wide_Type (Formal_Type) then @@ -11111,7 +11514,7 @@ package body Sem_Ch6 is -- is also class-wide. if Ekind (Formal_Type) = E_Anonymous_Access_Type - and then not Designates_From_With_Type (Formal_Type) + and then not Designates_From_Limited_With (Formal_Type) and then Is_Class_Wide_Default (Default) and then not Is_Class_Wide_Type (Designated_Type (Formal_Type)) then @@ -11138,6 +11541,41 @@ package body Sem_Ch6 is Null_Exclusion_Static_Checks (Param_Spec); end if; + -- The following checks are relevant when SPARK_Mode is on as these + -- are not standard Ada legality rules. + + if SPARK_Mode = On then + if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then + + -- A function cannot have a parameter of mode IN OUT or OUT + -- (SPARK RM 6.1). + + if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then + Error_Msg_N + ("function cannot have parameter of mode `OUT` or " + & "`IN OUT`", Formal); + + -- A function cannot have a volatile formal parameter + -- (SPARK RM 7.1.3(10)). + + elsif Is_SPARK_Volatile (Formal) then + Error_Msg_N + ("function cannot have a volatile formal parameter", + Formal); + end if; + + -- A procedure cannot have a formal parameter of mode IN because + -- it behaves as a constant (SPARK RM 7.1.3(6)). + + elsif Ekind (Scope (Formal)) = E_Procedure + and then Ekind (Formal) = E_In_Parameter + and then Is_SPARK_Volatile (Formal) + then + Error_Msg_N + ("formal parameter of mode `IN` cannot be volatile", Formal); + end if; + end if; + <> Next (Param_Spec); end loop; @@ -11204,7 +11642,7 @@ package body Sem_Ch6 is if Convention (Formal_Type) = Convention_Ada_Pass_By_Copy then Error_Msg_N - ("cannot pass aliased parameter & by copy?", Formal); + ("cannot pass aliased parameter & by copy??", Formal); end if; -- Force mechanism if type has Convention Ada_Pass_By_Ref/Copy @@ -11225,1235 +11663,6 @@ package body Sem_Ch6 is end if; end Process_Formals; - ------------------ - -- Process_PPCs -- - ------------------ - - procedure Process_PPCs - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id) - is - Loc : constant Source_Ptr := Sloc (N); - Prag : Node_Id; - Parms : List_Id; - - Designator : Entity_Id; - -- Subprogram designator, set from Spec_Id if present, else Body_Id - - Precond : Node_Id := Empty; - -- Set non-Empty if we prepend precondition to the declarations. This - -- is used to hook up inherited preconditions (adding the condition - -- expression with OR ELSE, and adding the message). - - Inherited_Precond : Node_Id; - -- Precondition inherited from parent subprogram - - Inherited : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - -- List of subprograms inherited by this subprogram - - Plist : List_Id := No_List; - -- List of generated postconditions - - procedure Check_Access_Invariants (E : Entity_Id); - -- If the subprogram returns an access to a type with invariants, or - -- has access parameters whose designated type has an invariant, then - -- under the same visibility conditions as for other invariant checks, - -- the type invariant must be applied to the returned value. - - procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id); - -- Given pragma Contract_Cases CCs, create the circuitry needed to - -- evaluate case guards and trigger consequence expressions. Subp_Id - -- denotes the related subprogram. - - function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id; - -- Prag contains an analyzed precondition or postcondition pragma. This - -- function copies the pragma, changes it to the corresponding Check - -- pragma and returns the Check pragma as the result. If Pspec is non- - -- empty, this is the case of inheriting a PPC, where we must change - -- references to parameters of the inherited subprogram to point to the - -- corresponding parameters of the current subprogram. - - procedure Insert_After_Last_Declaration (Nod : Node_Id); - -- Insert node Nod after the last declaration of the context - - function Invariants_Or_Predicates_Present return Boolean; - -- Determines if any invariants or predicates are present for any OUT - -- or IN OUT parameters of the subprogram, or (for a function) if the - -- return value has an invariant. - - function Is_Public_Subprogram_For (T : Entity_Id) return Boolean; - -- T is the entity for a private type for which invariants are defined. - -- This function returns True if the procedure corresponding to the - -- value of Designator is a public procedure from the point of view of - -- this type (i.e. its spec is in the visible part of the package that - -- contains the declaration of the private type). A True value means - -- that an invariant check is required (for an IN OUT parameter, or - -- the returned value of a function. - - ----------------------------- - -- Check_Access_Invariants -- - ----------------------------- - - procedure Check_Access_Invariants (E : Entity_Id) is - Call : Node_Id; - Obj : Node_Id; - Typ : Entity_Id; - - begin - if Is_Access_Type (Etype (E)) - and then not Is_Access_Constant (Etype (E)) - then - Typ := Designated_Type (Etype (E)); - - if Has_Invariants (Typ) - and then Present (Invariant_Procedure (Typ)) - and then Is_Public_Subprogram_For (Typ) - then - Obj := - Make_Explicit_Dereference (Loc, - Prefix => New_Occurrence_Of (E, Loc)); - Set_Etype (Obj, Typ); - - Call := Make_Invariant_Call (Obj); - - Append_To (Plist, - Make_If_Statement (Loc, - Condition => - Make_Op_Ne (Loc, - Left_Opnd => Make_Null (Loc), - Right_Opnd => New_Occurrence_Of (E, Loc)), - Then_Statements => New_List (Call))); - end if; - end if; - end Check_Access_Invariants; - - --------------------------- - -- Expand_Contract_Cases -- - --------------------------- - - -- Pragma Contract_Cases is expanded in the following manner: - - -- subprogram S is - -- Flag_1 : Boolean := False; - -- . . . - -- Flag_N : Boolean := False; - -- Flag_N+1 : Boolean := False; -- when "others" present - -- Count : Natural := 0; - - -- - - -- if Case_Guard_1 then - -- Flag_1 := True; - -- Count := Count + 1; - -- end if; - -- . . . - -- if Case_Guard_N then - -- Flag_N := True; - -- Count := Count + 1; - -- end if; - - -- if Count = 0 then - -- raise Assertion_Error with "contract cases incomplete"; - -- - -- Flag_N+1 := True; -- when "others" present - - -- elsif Count > 1 then - -- declare - -- Str0 : constant String := - -- "contract cases overlap for subprogram ABC"; - -- Str1 : constant String := - -- (if Flag_1 then - -- Str0 & "case guard at xxx evaluates to True" - -- else Str0); - -- StrN : constant String := - -- (if Flag_N then - -- StrN-1 & "case guard at xxx evaluates to True" - -- else StrN-1); - -- begin - -- raise Assertion_Error with StrN; - -- end; - -- end if; - - -- procedure _Postconditions is - -- begin - -- - - -- if Flag_1 and then not Consequence_1 then - -- raise Assertion_Error with "failed contract case at xxx"; - -- end if; - -- . . . - -- if Flag_N[+1] and then not Consequence_N[+1] then - -- raise Assertion_Error with "failed contract case at xxx"; - -- end if; - -- end _Postconditions; - -- begin - -- . . . - -- end S; - - procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id) is - Loc : constant Source_Ptr := Sloc (CCs); - - procedure Case_Guard_Error - (Decls : List_Id; - Flag : Entity_Id; - Error_Loc : Source_Ptr; - Msg : in out Entity_Id); - -- Given a declarative list Decls, status flag Flag, the location of - -- the error and a string Msg, construct the following check: - -- Msg : constant String := - -- (if Flag then - -- Msg & "case guard at Error_Loc evaluates to True" - -- else Msg); - -- The resulting code is added to Decls - - procedure Consequence_Error - (Checks : in out Node_Id; - Flag : Entity_Id; - Conseq : Node_Id); - -- Given an if statement Checks, status flag Flag and a consequence - -- Conseq, construct the following check: - -- [els]if Flag and then not Conseq then - -- raise Assertion_Error - -- with "failed contract case at Sloc (Conseq)"; - -- [end if;] - -- The resulting code is added to Checks - - function Declaration_Of (Id : Entity_Id) return Node_Id; - -- Given the entity Id of a boolean flag, generate: - -- Id : Boolean := False; - - function Increment (Id : Entity_Id) return Node_Id; - -- Given the entity Id of a numerical variable, generate: - -- Id := Id + 1; - - function Set (Id : Entity_Id) return Node_Id; - -- Given the entity Id of a boolean variable, generate: - -- Id := True; - - ---------------------- - -- Case_Guard_Error -- - ---------------------- - - procedure Case_Guard_Error - (Decls : List_Id; - Flag : Entity_Id; - Error_Loc : Source_Ptr; - Msg : in out Entity_Id) - is - New_Line : constant Character := Character'Val (10); - New_Msg : constant Entity_Id := Make_Temporary (Loc, 'S'); - - begin - Start_String; - Store_String_Char (New_Line); - Store_String_Chars (" case guard at "); - Store_String_Chars (Build_Location_String (Error_Loc)); - Store_String_Chars (" evaluates to True"); - - -- Generate: - -- New_Msg : constant String := - -- (if Flag then - -- Msg & "case guard at Error_Loc evaluates to True" - -- else Msg); - - Append_To (Decls, - Make_Object_Declaration (Loc, - Defining_Identifier => New_Msg, - Constant_Present => True, - Object_Definition => New_Reference_To (Standard_String, Loc), - Expression => - Make_If_Expression (Loc, - Expressions => New_List ( - New_Reference_To (Flag, Loc), - - Make_Op_Concat (Loc, - Left_Opnd => New_Reference_To (Msg, Loc), - Right_Opnd => Make_String_Literal (Loc, End_String)), - - New_Reference_To (Msg, Loc))))); - - Msg := New_Msg; - end Case_Guard_Error; - - ----------------------- - -- Consequence_Error -- - ----------------------- - - procedure Consequence_Error - (Checks : in out Node_Id; - Flag : Entity_Id; - Conseq : Node_Id) - is - Cond : Node_Id; - Error : Node_Id; - - begin - -- Generate: - -- Flag and then not Conseq - - Cond := - Make_And_Then (Loc, - Left_Opnd => New_Reference_To (Flag, Loc), - Right_Opnd => - Make_Op_Not (Loc, - Right_Opnd => Relocate_Node (Conseq))); - - -- Generate: - -- raise Assertion_Error - -- with "failed contract case at Sloc (Conseq)"; - - Start_String; - Store_String_Chars ("failed contract case at "); - Store_String_Chars (Build_Location_String (Sloc (Conseq))); - - Error := - Make_Procedure_Call_Statement (Loc, - Name => - New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc), - Parameter_Associations => New_List ( - Make_String_Literal (Loc, End_String))); - - if No (Checks) then - Checks := - Make_If_Statement (Loc, - Condition => Cond, - Then_Statements => New_List (Error)); - - else - if No (Elsif_Parts (Checks)) then - Set_Elsif_Parts (Checks, New_List); - end if; - - Append_To (Elsif_Parts (Checks), - Make_Elsif_Part (Loc, - Condition => Cond, - Then_Statements => New_List (Error))); - end if; - end Consequence_Error; - - -------------------- - -- Declaration_Of -- - -------------------- - - function Declaration_Of (Id : Entity_Id) return Node_Id is - begin - return - Make_Object_Declaration (Loc, - Defining_Identifier => Id, - Object_Definition => - New_Reference_To (Standard_Boolean, Loc), - Expression => - New_Reference_To (Standard_False, Loc)); - end Declaration_Of; - - --------------- - -- Increment -- - --------------- - - function Increment (Id : Entity_Id) return Node_Id is - begin - return - Make_Assignment_Statement (Loc, - Name => New_Reference_To (Id, Loc), - Expression => - Make_Op_Add (Loc, - Left_Opnd => New_Reference_To (Id, Loc), - Right_Opnd => Make_Integer_Literal (Loc, 1))); - end Increment; - - --------- - -- Set -- - --------- - - function Set (Id : Entity_Id) return Node_Id is - begin - return - Make_Assignment_Statement (Loc, - Name => New_Reference_To (Id, Loc), - Expression => New_Reference_To (Standard_True, Loc)); - end Set; - - -- Local variables - - Aggr : constant Node_Id := - Expression (First - (Pragma_Argument_Associations (CCs))); - Decls : constant List_Id := Declarations (N); - Multiple_PCs : constant Boolean := - List_Length (Component_Associations (Aggr)) > 1; - Case_Guard : Node_Id; - CG_Checks : Node_Id; - CG_Stmts : List_Id; - Conseq : Node_Id; - Conseq_Checks : Node_Id := Empty; - Count : Entity_Id; - Error_Decls : List_Id; - Flag : Entity_Id; - Msg_Str : Entity_Id; - Others_Flag : Entity_Id := Empty; - Post_Case : Node_Id; - - -- Start of processing for Expand_Contract_Cases - - begin - -- Create the counter which tracks the number of case guards that - -- evaluate to True. - - -- Count : Natural := 0; - - Count := Make_Temporary (Loc, 'C'); - - Prepend_To (Decls, - Make_Object_Declaration (Loc, - Defining_Identifier => Count, - Object_Definition => New_Reference_To (Standard_Natural, Loc), - Expression => Make_Integer_Literal (Loc, 0))); - - -- Create the base error message for multiple overlapping case - -- guards. - - -- Msg_Str : constant String := - -- "contract cases overlap for subprogram Subp_Id"; - - if Multiple_PCs then - Msg_Str := Make_Temporary (Loc, 'S'); - - Start_String; - Store_String_Chars ("contract cases overlap for subprogram "); - Store_String_Chars (Get_Name_String (Chars (Subp_Id))); - - Error_Decls := New_List ( - Make_Object_Declaration (Loc, - Defining_Identifier => Msg_Str, - Constant_Present => True, - Object_Definition => New_Reference_To (Standard_String, Loc), - Expression => Make_String_Literal (Loc, End_String))); - end if; - - -- Process individual post cases - - Post_Case := First (Component_Associations (Aggr)); - while Present (Post_Case) loop - Case_Guard := First (Choices (Post_Case)); - Conseq := Expression (Post_Case); - - -- The "others" choice requires special processing - - if Nkind (Case_Guard) = N_Others_Choice then - Others_Flag := Make_Temporary (Loc, 'F'); - Prepend_To (Decls, Declaration_Of (Others_Flag)); - - -- Check possible overlap between a case guard and "others" - - if Multiple_PCs then - Case_Guard_Error - (Decls => Error_Decls, - Flag => Others_Flag, - Error_Loc => Sloc (Case_Guard), - Msg => Msg_Str); - end if; - - -- Check the corresponding consequence of "others" - - Consequence_Error - (Checks => Conseq_Checks, - Flag => Others_Flag, - Conseq => Conseq); - - -- Regular post case - - else - -- Create the flag which tracks the state of its associated - -- case guard. - - Flag := Make_Temporary (Loc, 'F'); - Prepend_To (Decls, Declaration_Of (Flag)); - - -- The flag is set when the case guard is evaluated to True - -- if Case_Guard then - -- Flag := True; - -- Count := Count + 1; - -- end if; - - Append_To (Decls, - Make_If_Statement (Loc, - Condition => Relocate_Node (Case_Guard), - Then_Statements => New_List ( - Set (Flag), - Increment (Count)))); - - -- Check whether this case guard overlaps with another case - -- guard. - - if Multiple_PCs then - Case_Guard_Error - (Decls => Error_Decls, - Flag => Flag, - Error_Loc => Sloc (Case_Guard), - Msg => Msg_Str); - end if; - - -- The corresponding consequence of the case guard which - -- evaluated to True must hold on exit from the subprogram. - - Consequence_Error (Conseq_Checks, Flag, Conseq); - end if; - - Next (Post_Case); - end loop; - - -- Raise Assertion_Error when none of the case guards evaluate to - -- True. The only exception is when we have "others", in which case - -- there is no error because "others" acts as a default True. - - -- Generate: - -- Flag := True; - - if Present (Others_Flag) then - CG_Stmts := New_List (Set (Others_Flag)); - - -- Generate: - -- raise Assetion_Error with "contract cases incomplete"; - - else - Start_String; - Store_String_Chars ("contract cases incomplete"); - - CG_Stmts := New_List ( - Make_Procedure_Call_Statement (Loc, - Name => - New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc), - Parameter_Associations => New_List ( - Make_String_Literal (Loc, End_String)))); - end if; - - CG_Checks := - Make_If_Statement (Loc, - Condition => - Make_Op_Eq (Loc, - Left_Opnd => New_Reference_To (Count, Loc), - Right_Opnd => Make_Integer_Literal (Loc, 0)), - Then_Statements => CG_Stmts); - - -- Detect a possible failure due to several case guards evaluating to - -- True. - - -- Generate: - -- elsif Count > 0 then - -- declare - -- - -- begin - -- raise Assertion_Error with ; - -- end if; - - if Multiple_PCs then - Set_Elsif_Parts (CG_Checks, New_List ( - Make_Elsif_Part (Loc, - Condition => - Make_Op_Gt (Loc, - Left_Opnd => New_Reference_To (Count, Loc), - Right_Opnd => Make_Integer_Literal (Loc, 1)), - - Then_Statements => New_List ( - Make_Block_Statement (Loc, - Declarations => Error_Decls, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List ( - Make_Procedure_Call_Statement (Loc, - Name => - New_Reference_To - (RTE (RE_Raise_Assert_Failure), Loc), - Parameter_Associations => New_List ( - New_Reference_To (Msg_Str, Loc)))))))))); - end if; - - Append_To (Decls, CG_Checks); - - -- Raise Assertion_Error when the corresponding consequence of a case - -- guard that evaluated to True fails. - - if No (Plist) then - Plist := New_List; - end if; - - Append_To (Plist, Conseq_Checks); - end Expand_Contract_Cases; - - -------------- - -- Grab_PPC -- - -------------- - - function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is - Nam : constant Name_Id := Pragma_Name (Prag); - Map : Elist_Id; - CP : Node_Id; - - Ename : Name_Id; - -- Effective name of pragma (maybe Pre/Post rather than Precondition/ - -- Postcodition if the pragma came from a Pre/Post aspect). We need - -- the name right when we generate the Check pragma, since we want - -- the right set of check policies to apply. - - begin - -- Prepare map if this is the case where we have to map entities of - -- arguments in the overridden subprogram to corresponding entities - -- of the current subprogram. - - if No (Pspec) then - Map := No_Elist; - - else - declare - PF : Entity_Id; - CF : Entity_Id; - - begin - Map := New_Elmt_List; - PF := First_Formal (Pspec); - CF := First_Formal (Designator); - while Present (PF) loop - Append_Elmt (PF, Map); - Append_Elmt (CF, Map); - Next_Formal (PF); - Next_Formal (CF); - end loop; - end; - end if; - - -- Now we can copy the tree, doing any required substitutions - - CP := New_Copy_Tree (Prag, Map => Map, New_Scope => Current_Scope); - - -- Set Analyzed to false, since we want to reanalyze the check - -- procedure. Note that it is only at the outer level that we - -- do this fiddling, for the spec cases, the already preanalyzed - -- parameters are not affected. - - Set_Analyzed (CP, False); - - -- We also make sure Comes_From_Source is False for the copy - - Set_Comes_From_Source (CP, False); - - -- For a postcondition pragma within a generic, preserve the pragma - -- for later expansion. This is also used when an error was detected, - -- thus setting Expander_Active to False. - - if Nam = Name_Postcondition - and then not Expander_Active - then - return CP; - end if; - - -- Get effective name of aspect - - if Present (Corresponding_Aspect (Prag)) then - Ename := Chars (Identifier (Corresponding_Aspect (Prag))); - else - Ename := Nam; - end if; - - -- Change copy of pragma into corresponding pragma Check - - Prepend_To (Pragma_Argument_Associations (CP), - Make_Pragma_Argument_Association (Sloc (Prag), - Expression => Make_Identifier (Loc, Ename))); - Set_Pragma_Identifier (CP, Make_Identifier (Sloc (Prag), Name_Check)); - - -- If this is inherited case and the current message starts with - -- "failed p", we change it to "failed inherited p...". - - if Present (Pspec) then - declare - Msg : constant Node_Id := - Last (Pragma_Argument_Associations (CP)); - - begin - if Chars (Msg) = Name_Message then - String_To_Name_Buffer (Strval (Expression (Msg))); - - if Name_Buffer (1 .. 8) = "failed p" then - Insert_Str_In_Name_Buffer ("inherited ", 8); - Set_Strval - (Expression (Last (Pragma_Argument_Associations (CP))), - String_From_Name_Buffer); - end if; - end if; - end; - end if; - - -- Return the check pragma - - return CP; - end Grab_PPC; - - ----------------------------------- - -- Insert_After_Last_Declaration -- - ----------------------------------- - - procedure Insert_After_Last_Declaration (Nod : Node_Id) is - Decls : constant List_Id := Declarations (N); - - begin - if No (Decls) then - Set_Declarations (N, New_List (Nod)); - else - Append_To (Decls, Nod); - end if; - end Insert_After_Last_Declaration; - - -------------------------------------- - -- Invariants_Or_Predicates_Present -- - -------------------------------------- - - function Invariants_Or_Predicates_Present return Boolean is - Formal : Entity_Id; - - begin - -- Check function return result. If result is an access type there - -- may be invariants on the designated type. - - if Ekind (Designator) /= E_Procedure - and then Has_Invariants (Etype (Designator)) - then - return True; - - elsif Ekind (Designator) /= E_Procedure - and then Is_Access_Type (Etype (Designator)) - and then Has_Invariants (Designated_Type (Etype (Designator))) - then - return True; - end if; - - -- Check parameters - - Formal := First_Formal (Designator); - while Present (Formal) loop - if Ekind (Formal) /= E_In_Parameter - and then (Has_Invariants (Etype (Formal)) - or else Present (Predicate_Function (Etype (Formal)))) - then - return True; - - elsif Is_Access_Type (Etype (Formal)) - and then Has_Invariants (Designated_Type (Etype (Formal))) - then - return True; - end if; - - Next_Formal (Formal); - end loop; - - return False; - end Invariants_Or_Predicates_Present; - - ------------------------------ - -- Is_Public_Subprogram_For -- - ------------------------------ - - -- The type T is a private type, its declaration is therefore in - -- the list of public declarations of some package. The test for a - -- public subprogram is that its declaration is in this same list - -- of declarations for the same package (note that all the public - -- declarations are in one list, and all the private declarations - -- in another, so this deals with the public/private distinction). - - function Is_Public_Subprogram_For (T : Entity_Id) return Boolean is - DD : constant Node_Id := Unit_Declaration_Node (Designator); - -- The subprogram declaration for the subprogram in question - - TL : constant List_Id := - Visible_Declarations - (Specification (Unit_Declaration_Node (Scope (T)))); - -- The list of declarations containing the private declaration of - -- the type. We know it is a private type, so we know its scope is - -- the package in question, and we know it must be in the visible - -- declarations of this package. - - begin - -- If the subprogram declaration is not a list member, it must be - -- an Init_Proc, in which case we want to consider it to be a - -- public subprogram, since we do get initializations to deal with. - -- Other internally generated subprograms are not public. - - if not Is_List_Member (DD) - and then Is_Init_Proc (Defining_Entity (DD)) - then - return True; - - -- The declaration may have been generated for an expression function - -- so check whether that function comes from source. - - elsif not Comes_From_Source (DD) - and then - (Nkind (Original_Node (DD)) /= N_Expression_Function - or else not Comes_From_Source (Defining_Entity (DD))) - then - return False; - - -- Otherwise we test whether the subprogram is declared in the - -- visible declarations of the package containing the type. - - else - return TL = List_Containing (DD); - end if; - end Is_Public_Subprogram_For; - - -- Start of processing for Process_PPCs - - begin - -- Capture designator from spec if present, else from body - - if Present (Spec_Id) then - Designator := Spec_Id; - else - Designator := Body_Id; - end if; - - -- Internally generated subprograms, such as type-specific functions, - -- don't get assertion checks. - - if Get_TSS_Name (Designator) /= TSS_Null then - return; - end if; - - -- Grab preconditions from spec - - if Present (Spec_Id) then - - -- Loop through PPC pragmas from spec. Note that preconditions from - -- the body will be analyzed and converted when we scan the body - -- declarations below. - - Prag := Spec_PPC_List (Contract (Spec_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition then - - -- For Pre (or Precondition pragma), we simply prepend the - -- pragma to the list of declarations right away so that it - -- will be executed at the start of the procedure. Note that - -- this processing reverses the order of the list, which is - -- what we want since new entries were chained to the head of - -- the list. There can be more than one precondition when we - -- use pragma Precondition. - - if not Class_Present (Prag) then - Prepend (Grab_PPC, Declarations (N)); - - -- For Pre'Class there can only be one pragma, and we save - -- it in Precond for now. We will add inherited Pre'Class - -- stuff before inserting this pragma in the declarations. - else - Precond := Grab_PPC; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - - -- Now deal with inherited preconditions - - for J in Inherited'Range loop - Prag := Spec_PPC_List (Contract (Inherited (J))); - - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Inherited_Precond := Grab_PPC (Inherited (J)); - - -- No precondition so far, so establish this as the first - - if No (Precond) then - Precond := Inherited_Precond; - - -- Here we already have a precondition, add inherited one - - else - -- Add new precondition to old one using OR ELSE - - declare - New_Expr : constant Node_Id := - Get_Pragma_Arg - (Next - (First - (Pragma_Argument_Associations - (Inherited_Precond)))); - Old_Expr : constant Node_Id := - Get_Pragma_Arg - (Next - (First - (Pragma_Argument_Associations - (Precond)))); - - begin - if Paren_Count (Old_Expr) = 0 then - Set_Paren_Count (Old_Expr, 1); - end if; - - if Paren_Count (New_Expr) = 0 then - Set_Paren_Count (New_Expr, 1); - end if; - - Rewrite (Old_Expr, - Make_Or_Else (Sloc (Old_Expr), - Left_Opnd => Relocate_Node (Old_Expr), - Right_Opnd => New_Expr)); - end; - - -- Add new message in the form: - - -- failed precondition from bla - -- also failed inherited precondition from bla - -- ... - - -- Skip this if exception locations are suppressed - - if not Exception_Locations_Suppressed then - declare - New_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Inherited_Precond))); - Old_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Precond))); - begin - Start_String (Strval (Old_Msg)); - Store_String_Chars (ASCII.LF & " also "); - Store_String_Chars (Strval (New_Msg)); - Set_Strval (Old_Msg, End_String); - end; - end if; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - end loop; - - -- If we have built a precondition for Pre'Class (including any - -- Pre'Class aspects inherited from parent subprograms), then we - -- insert this composite precondition at this stage. - - if Present (Precond) then - Prepend (Precond, Declarations (N)); - end if; - end if; - - -- Build postconditions procedure if needed and prepend the following - -- declaration to the start of the declarations for the subprogram. - - -- procedure _postconditions [(_Result : resulttype)] is - -- begin - -- pragma Check (Postcondition, condition [,message]); - -- pragma Check (Postcondition, condition [,message]); - -- ... - -- Invariant_Procedure (_Result) ... - -- Invariant_Procedure (Arg1) - -- ... - -- end; - - -- First we deal with the postconditions in the body - - if Is_Non_Empty_List (Declarations (N)) then - - -- Loop through declarations - - Prag := First (Declarations (N)); - while Present (Prag) loop - if Nkind (Prag) = N_Pragma then - Check_Applicable_Policy (Prag); - - -- If pragma, capture if postconditions enabled, else ignore - - if Pragma_Name (Prag) = Name_Postcondition - and then not Is_Ignored (Prag) - then - if Plist = No_List then - Plist := Empty_List; - end if; - - Analyze (Prag); - - -- If expansion is disabled, as in a generic unit, save - -- pragma for later expansion. - - if not Expander_Active then - Prepend (Grab_PPC, Declarations (N)); - else - Append (Grab_PPC, Plist); - end if; - end if; - - Next (Prag); - - -- Not a pragma, if comes from source, then end scan - - elsif Comes_From_Source (Prag) then - exit; - - -- Skip stuff not coming from source - - else - Next (Prag); - end if; - end loop; - end if; - - -- Now deal with any postconditions from the spec - - if Present (Spec_Id) then - Spec_Postconditions : declare - procedure Process_Contract_Cases (Spec : Node_Id); - -- This processes the Spec_CTC_List from Spec, processing any - -- contract-cases from the list. The caller has checked that - -- Spec_CTC_List is non-Empty. - - procedure Process_Post_Conditions - (Spec : Node_Id; - Class : Boolean); - -- This processes the Spec_PPC_List from Spec, processing any - -- postconditions from the list. If Class is True, then only - -- postconditions marked with Class_Present are considered. - -- The caller has checked that Spec_PPC_List is non-Empty. - - ---------------------------- - -- Process_Contract_Cases -- - ---------------------------- - - procedure Process_Contract_Cases (Spec : Node_Id) is - begin - -- Loop through Contract_Cases pragmas from spec - - Prag := Spec_CTC_List (Contract (Spec)); - loop - if Pragma_Name (Prag) = Name_Contract_Cases then - Expand_Contract_Cases (Prag, Spec_Id); - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Contract_Cases; - - ----------------------------- - -- Process_Post_Conditions -- - ----------------------------- - - procedure Process_Post_Conditions - (Spec : Node_Id; - Class : Boolean) - is - Pspec : Node_Id; - - begin - if Class then - Pspec := Spec; - else - Pspec := Empty; - end if; - - -- Loop through PPC pragmas from spec - - Prag := Spec_PPC_List (Contract (Spec)); - loop - if Pragma_Name (Prag) = Name_Postcondition - and then (not Class or else Class_Present (Prag)) - then - if Plist = No_List then - Plist := Empty_List; - end if; - - if not Expander_Active then - Prepend - (Grab_PPC (Pspec), Declarations (N)); - else - Append (Grab_PPC (Pspec), Plist); - end if; - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Post_Conditions; - - -- Start of processing for Spec_Postconditions - - begin - -- Process postconditions expressed as contract-cases - - if Present (Spec_CTC_List (Contract (Spec_Id))) then - Process_Contract_Cases (Spec_Id); - end if; - - -- Process spec postconditions - - if Present (Spec_PPC_List (Contract (Spec_Id))) then - Process_Post_Conditions (Spec_Id, Class => False); - end if; - - -- Process inherited postconditions - - for J in Inherited'Range loop - if Present (Spec_PPC_List (Contract (Inherited (J)))) then - Process_Post_Conditions (Inherited (J), Class => True); - end if; - end loop; - end Spec_Postconditions; - end if; - - -- If we had any postconditions and expansion is enabled, or if the - -- subprogram has invariants, then build the _Postconditions procedure. - - if (Present (Plist) or else Invariants_Or_Predicates_Present) - and then Expander_Active - then - if No (Plist) then - Plist := Empty_List; - end if; - - -- Special processing for function return - - if Ekind (Designator) /= E_Procedure then - declare - Rent : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_uResult); - Ftyp : constant Entity_Id := Etype (Designator); - - begin - Set_Etype (Rent, Ftyp); - - -- Add argument for return - - Parms := - New_List ( - Make_Parameter_Specification (Loc, - Parameter_Type => New_Occurrence_Of (Ftyp, Loc), - Defining_Identifier => Rent)); - - -- Add invariant call if returning type with invariants and - -- this is a public function, i.e. a function declared in the - -- visible part of the package defining the private type. - - if Has_Invariants (Etype (Rent)) - and then Present (Invariant_Procedure (Etype (Rent))) - and then Is_Public_Subprogram_For (Etype (Rent)) - then - Append_To (Plist, - Make_Invariant_Call (New_Occurrence_Of (Rent, Loc))); - end if; - - -- Same if return value is an access to type with invariants - - Check_Access_Invariants (Rent); - end; - - -- Procedure rather than a function - - else - Parms := No_List; - end if; - - -- Add invariant calls and predicate calls for parameters. Note that - -- this is done for functions as well, since in Ada 2012 they can - -- have IN OUT args. - - declare - Formal : Entity_Id; - Ftype : Entity_Id; - - begin - Formal := First_Formal (Designator); - while Present (Formal) loop - if Ekind (Formal) /= E_In_Parameter - or else Is_Access_Type (Etype (Formal)) - then - Ftype := Etype (Formal); - - if Has_Invariants (Ftype) - and then Present (Invariant_Procedure (Ftype)) - and then Is_Public_Subprogram_For (Ftype) - then - Append_To (Plist, - Make_Invariant_Call - (New_Occurrence_Of (Formal, Loc))); - end if; - - Check_Access_Invariants (Formal); - - if Present (Predicate_Function (Ftype)) then - Append_To (Plist, - Make_Predicate_Check - (Ftype, New_Occurrence_Of (Formal, Loc))); - end if; - end if; - - Next_Formal (Formal); - end loop; - end; - - -- Build and insert postcondition procedure - - declare - Post_Proc : constant Entity_Id := - Make_Defining_Identifier (Loc, - Chars => Name_uPostconditions); - -- The entity for the _Postconditions procedure - - begin - -- Insert the corresponding body of a post condition pragma after - -- the last declaration of the context. This ensures that the body - -- will not cause any premature freezing as it may mention types: - - -- procedure Proc (Obj : Array_Typ) is - -- procedure _postconditions is - -- begin - -- ... Obj ... - -- end _postconditions; - - -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); - -- begin - - -- In the example above, Obj is of type T but the incorrect - -- placement of _postconditions will cause a crash in gigi due to - -- an out of order reference. The body of _postconditions must be - -- placed after the declaration of Temp to preserve correct - -- visibility. - - Insert_After_Last_Declaration ( - Make_Subprogram_Body (Loc, - Specification => - Make_Procedure_Specification (Loc, - Defining_Unit_Name => Post_Proc, - Parameter_Specifications => Parms), - - Declarations => Empty_List, - - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => Plist))); - - Set_Ekind (Post_Proc, E_Procedure); - - -- If this is a procedure, set the Postcondition_Proc attribute on - -- the proper defining entity for the subprogram. - - if Ekind (Designator) = E_Procedure then - Set_Postcondition_Proc (Designator, Post_Proc); - end if; - end; - - Set_Has_Postconditions (Designator); - end if; - end Process_PPCs; - ---------------------------- -- Reference_Body_Formals -- ---------------------------- @@ -12515,7 +11724,7 @@ package body Sem_Ch6 is AS_Needed := False; -- If we have unknown discriminants, then we do not need an actual - -- subtype, or more accurately we cannot figure it out! Note that + -- subtype, or more accurately we cannot figure it out. Note that -- all class-wide types have unknown discriminants. elsif Has_Unknown_Discriminants (T) then @@ -12567,7 +11776,7 @@ package body Sem_Ch6 is -- parameter block, and it is this local variable that may -- require an actual subtype. - if Full_Expander_Active then + if Expander_Active then Decl := Build_Actual_Subtype (T, Renamed_Object (Formal)); else Decl := Build_Actual_Subtype (T, Formal); @@ -12603,10 +11812,17 @@ package body Sem_Ch6 is if Present (First_Stmt) then Insert_List_Before_And_Analyze (First_Stmt, Freeze_Entity (Defining_Identifier (Decl), N)); + + -- Ditto if the type has a dynamic predicate, because the + -- generated function will mention the actual subtype. + + elsif Has_Dynamic_Predicate_Aspect (T) then + Insert_List_Before_And_Analyze (Decl, + Freeze_Entity (Defining_Identifier (Decl), N)); end if; if Nkind (N) = N_Accept_Statement - and then Full_Expander_Active + and then Expander_Active then Set_Actual_Subtype (Renamed_Object (Formal), Defining_Identifier (Decl)); @@ -12632,9 +11848,8 @@ package body Sem_Ch6 is -- point of the call. if Out_Present (Spec) then - if Ekind (Scope (Formal_Id)) = E_Function - or else Ekind (Scope (Formal_Id)) = E_Generic_Function - then + if Ekind_In (Scope (Formal_Id), E_Function, E_Generic_Function) then + -- [IN] OUT parameters allowed for functions in Ada 2012 if Ada_Version >= Ada_2012 then @@ -12651,6 +11866,8 @@ package body Sem_Ch6 is Set_Ekind (Formal_Id, E_Out_Parameter); end if; + Set_Has_Out_Or_In_Out_Parameter (Scope (Formal_Id), True); + -- But not in earlier versions of Ada else @@ -12800,6 +12017,15 @@ package body Sem_Ch6 is Error_Msg_N ("default values not allowed for operator parameters", Parent (F)); + + -- For function instantiations that are operators, we must check + -- separately that the corresponding generic only has in-parameters. + -- For subprogram declarations this is done in Set_Formal_Mode. + -- Such an error could not arise in earlier versions of the language. + + elsif Ekind (F) /= E_In_Parameter then + Error_Msg_N + ("operators can only have IN parameters", F); end if; Next_Formal (F);