diff options
Diffstat (limited to 'gcc/ada/contracts.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 1563 |
1 files changed, 1348 insertions, 215 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 705f197..2726486 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -47,6 +47,8 @@ with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; with Sem_Disp; use Sem_Disp; with Sem_Prag; use Sem_Prag; +with Sem_Res; use Sem_Res; +with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; @@ -66,6 +68,16 @@ package body Contracts is -- -- Part_Of + procedure Check_Class_Condition + (Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Is_Precondition : Boolean); + -- Perform checking of class-wide pre/postcondition Cond inherited by Subp + -- from Par_Subp. Is_Precondition enables check specific for preconditions. + -- In SPARK_Mode, an inherited operation that is not overridden but has + -- inherited modified conditions pre/postconditions is illegal. + procedure Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id : Entity_Id); -- Perform checking of external properties pragmas that is common to both @@ -77,6 +89,12 @@ package body Contracts is -- well as Contract_Cases, Subprogram_Variant, invariants and predicates. -- Body_Id denotes the entity of the subprogram body. + procedure Set_Class_Condition + (Kind : Condition_Kind; + Subp : Entity_Id; + Cond : Node_Id); + -- Set the class-wide Kind condition of Subp + ----------------------- -- Add_Contract_Item -- ----------------------- @@ -386,23 +404,7 @@ package body Contracts is | N_Generic_Subprogram_Declaration | N_Subprogram_Declaration then - declare - Subp_Id : constant Entity_Id := Defining_Entity (Decl); - - begin - Analyze_Entry_Or_Subprogram_Contract (Subp_Id); - - -- If analysis of a class-wide pre/postcondition indicates - -- that a class-wide clone is needed, analyze its declaration - -- now. Its body is created when the body of the original - -- operation is analyzed (and rewritten). - - if Is_Subprogram (Subp_Id) - and then Present (Class_Wide_Clone (Subp_Id)) - then - Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id))); - end if; - end; + Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl)); -- Entry or subprogram bodies @@ -1491,6 +1493,141 @@ package body Contracts is (Type_Or_Obj_Id => Type_Id); end Analyze_Type_Contract; + --------------------------- + -- Check_Class_Condition -- + --------------------------- + + procedure Check_Class_Condition + (Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Is_Precondition : Boolean) + is + function Check_Entity (N : Node_Id) return Traverse_Result; + -- Check reference to formal of inherited operation or to primitive + -- operation of root type. + + ------------------ + -- Check_Entity -- + ------------------ + + function Check_Entity (N : Node_Id) return Traverse_Result is + New_E : Entity_Id; + Orig_E : Entity_Id; + + begin + if Nkind (N) = N_Identifier + and then Present (Entity (N)) + and then + (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) + and then + (Nkind (Parent (N)) /= N_Attribute_Reference + or else Attribute_Name (Parent (N)) /= Name_Class) + then + -- These checks do not apply to dispatching calls within the + -- condition, but only to calls whose static tag is that of + -- the parent type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + and then Present (Controlling_Argument (Parent (N))) + then + return OK; + end if; + + -- Determine whether entity has a renaming + + Orig_E := Entity (N); + New_E := Get_Mapped_Entity (Orig_E); + + if Present (New_E) then + + -- AI12-0166: A precondition for a protected operation + -- cannot include an internal call to a protected function + -- of the type. In the case of an inherited condition for an + -- overriding operation, both the operation and the function + -- are given by primitive wrappers. + + if Is_Precondition + and then Ekind (New_E) = E_Function + and then Is_Primitive_Wrapper (New_E) + and then Is_Primitive_Wrapper (Subp) + and then Scope (Subp) = Scope (New_E) + then + Error_Msg_Node_2 := Wrapped_Entity (Subp); + Error_Msg_NE + ("internal call to& cannot appear in inherited " + & "precondition of protected operation&", + Subp, Wrapped_Entity (New_E)); + end if; + end if; + + -- Check that there are no calls left to abstract operations if + -- the current subprogram is not abstract. + + if Present (New_E) + and then Nkind (Parent (N)) = N_Function_Call + and then N = Name (Parent (N)) + then + if not Is_Abstract_Subprogram (Subp) + and then Is_Abstract_Subprogram (New_E) + then + Error_Msg_Sloc := Sloc (Current_Scope); + Error_Msg_Node_2 := Subp; + + if Comes_From_Source (Subp) then + Error_Msg_NE + ("cannot call abstract subprogram & in inherited " + & "condition for&#", Subp, New_E); + else + Error_Msg_NE + ("cannot call abstract subprogram & in inherited " + & "condition for inherited&#", Subp, New_E); + end if; + + -- In SPARK mode, report error on inherited condition for an + -- inherited operation if it contains a call to an overriding + -- operation, because this implies that the pre/postconditions + -- of the inherited operation have changed silently. + + elsif SPARK_Mode = On + and then Warn_On_Suspicious_Contract + and then Present (Alias (Subp)) + and then Present (New_E) + and then Comes_From_Source (New_E) + then + Error_Msg_N + ("cannot modify inherited condition (SPARK RM 6.1.1(1))", + Parent (Subp)); + Error_Msg_Sloc := Sloc (New_E); + Error_Msg_Node_2 := Subp; + Error_Msg_NE + ("\overriding of&# forces overriding of&", + Parent (Subp), New_E); + end if; + end if; + end if; + + return OK; + end Check_Entity; + + procedure Check_Condition_Entities is + new Traverse_Proc (Check_Entity); + + -- Start of processing for Check_Class_Condition + + begin + -- No check required if the subprograms match + + if Par_Subp = Subp then + return; + end if; + + Update_Primitives_Mapping (Par_Subp, Subp); + Map_Formals (Par_Subp, Subp); + Check_Condition_Entities (Cond); + end Check_Class_Condition; + ----------------------------- -- Create_Generic_Contract -- ----------------------------- @@ -1900,7 +2037,7 @@ package body Contracts is procedure Add_Stable_Property_Contracts (Subp_Id : Entity_Id; Class_Present : Boolean) is - Loc : constant Source_Ptr := Sloc (Subp_Id); + Loc : constant Source_Ptr := Sloc (Subp_Id); procedure Insert_Stable_Property_Check (Formal : Entity_Id; Property_Function : Entity_Id); @@ -2552,13 +2689,38 @@ package body Contracts is --------------------------------- procedure Process_Spec_Postconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Seen : Subprogram_List (Subps'Range) := (others => Empty); + + function Seen_Subp (Subp_Id : Entity_Id) return Boolean; + -- Return True if the contract of subprogram Subp_Id has been + -- processed. + + --------------- + -- Seen_Subp -- + --------------- + + function Seen_Subp (Subp_Id : Entity_Id) return Boolean is + begin + for Index in Seen'Range loop + if Seen (Index) = Subp_Id then + return True; + end if; + end loop; + + return False; + end Seen_Subp; + + -- Local variables + Item : Node_Id; Items : Node_Id; Prag : Node_Id; Subp_Id : Entity_Id; + -- Start of processing for Process_Spec_Postconditions + begin -- Process the contract @@ -2589,7 +2751,7 @@ package body Contracts is Subp_Id := Ultimate_Alias (Subp_Id); end if; - -- Wrappers of class-wide pre/post conditions reference the + -- Wrappers of class-wide pre/postconditions reference the -- parent primitive that has the inherited contract. if Is_Wrapper (Subp_Id) @@ -2600,7 +2762,9 @@ package body Contracts is Items := Contract (Subp_Id); - if Present (Items) then + if not Seen_Subp (Subp_Id) and then Present (Items) then + Seen (Index) := Subp_Id; + Prag := Pre_Post_Conditions (Items); while Present (Prag) loop if Pragma_Name (Prag) = Name_Postcondition @@ -2657,10 +2821,6 @@ package body Contracts is --------------------------- procedure Process_Preconditions is - Class_Pre : Node_Id := Empty; - -- The sole [inherited] class-wide precondition pragma that applies - -- to the subprogram. - Insert_Node : Node_Id := Empty; -- The insertion node after which all pragma Check equivalents are -- inserted. @@ -2669,21 +2829,12 @@ package body Contracts is -- Determine whether arbitrary declaration Decl denotes a renaming of -- a discriminant or protection field _object. - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); - -- Merge two class-wide preconditions by "or else"-ing them. The - -- changes are accumulated in parameter Into. Update the error - -- message of Into. - procedure Prepend_To_Decls (Item : Node_Id); -- Prepend a single item to the declarations of the subprogram body - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); - -- Save a class-wide precondition into Class_Pre, or prepend a normal - -- precondition to the declarations of the body and analyze it. - - procedure Process_Inherited_Preconditions; - -- Collect all inherited class-wide preconditions and merge them into - -- one big precondition to be evaluated as pragma Check. + procedure Prepend_Pragma_To_Decls (Prag : Node_Id); + -- Prepend a normal precondition to the declarations of the body and + -- analyze it. procedure Process_Preconditions_For (Subp_Id : Entity_Id); -- Collect all preconditions of subprogram Subp_Id and prepend their @@ -2737,78 +2888,6 @@ package body Contracts is return False; end Is_Prologue_Renaming; - ------------------------- - -- Merge_Preconditions -- - ------------------------- - - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is - function Expression_Arg (Prag : Node_Id) return Node_Id; - -- Return the boolean expression argument of a precondition while - -- updating its parentheses count for the subsequent merge. - - function Message_Arg (Prag : Node_Id) return Node_Id; - -- Return the message argument of a precondition - - -------------------- - -- Expression_Arg -- - -------------------- - - function Expression_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); - - begin - if Paren_Count (Arg) = 0 then - Set_Paren_Count (Arg, 1); - end if; - - return Arg; - end Expression_Arg; - - ----------------- - -- Message_Arg -- - ----------------- - - function Message_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - begin - return Get_Pragma_Arg (Last (Args)); - end Message_Arg; - - -- Local variables - - From_Expr : constant Node_Id := Expression_Arg (From); - From_Msg : constant Node_Id := Message_Arg (From); - Into_Expr : constant Node_Id := Expression_Arg (Into); - Into_Msg : constant Node_Id := Message_Arg (Into); - Loc : constant Source_Ptr := Sloc (Into); - - -- Start of processing for Merge_Preconditions - - begin - -- Merge the two preconditions by "or else"-ing them - - Rewrite (Into_Expr, - Make_Or_Else (Loc, - Right_Opnd => Relocate_Node (Into_Expr), - Left_Opnd => From_Expr)); - - -- Merge the two error messages to produce a single message of the - -- form: - - -- failed precondition from ... - -- also failed inherited precondition from ... - - if not Exception_Locations_Suppressed then - Start_String (Strval (Into_Msg)); - Store_String_Char (ASCII.LF); - Store_String_Chars (" also "); - Store_String_Chars (Strval (From_Msg)); - - Set_Strval (Into_Msg, End_String); - end if; - end Merge_Preconditions; - ---------------------- -- Prepend_To_Decls -- ---------------------- @@ -2829,28 +2908,27 @@ package body Contracts is Prepend_To (Decls, Item); end Prepend_To_Decls; - ------------------------------ - -- Prepend_To_Decls_Or_Save -- - ------------------------------ + ----------------------------- + -- Prepend_Pragma_To_Decls -- + ----------------------------- - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is + procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is Check_Prag : Node_Id; begin - Check_Prag := Build_Pragma_Check_Equivalent (Prag); - - -- Save the sole class-wide precondition (if any) for the next - -- step, where it will be merged with inherited preconditions. + -- Skip the sole class-wide precondition (if any) since it is + -- processed by Merge_Class_Conditions. if Class_Present (Prag) then - pragma Assert (No (Class_Pre)); - Class_Pre := Check_Prag; + null; -- Accumulate the corresponding Check pragmas at the top of the -- declarations. Prepending the items ensures that they will be -- evaluated in their original order. else + Check_Prag := Build_Pragma_Check_Equivalent (Prag); + if Present (Insert_Node) then Insert_After (Insert_Node, Check_Prag); else @@ -2859,87 +2937,7 @@ package body Contracts is Analyze (Check_Prag); end if; - end Prepend_To_Decls_Or_Save; - - ------------------------------------- - -- Process_Inherited_Preconditions -- - ------------------------------------- - - procedure Process_Inherited_Preconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - - Item : Node_Id; - Items : Node_Id; - Prag : Node_Id; - Subp_Id : Entity_Id; - - begin - -- Process the contracts of all inherited subprograms, looking for - -- class-wide preconditions. - - for Index in Subps'Range loop - Subp_Id := Subps (Index); - - if Present (Alias (Subp_Id)) then - Subp_Id := Ultimate_Alias (Subp_Id); - end if; - - -- Wrappers of class-wide pre/post conditions reference the - -- parent primitive that has the inherited contract. - - if Is_Wrapper (Subp_Id) - and then Present (LSP_Subprogram (Subp_Id)) - then - Subp_Id := LSP_Subprogram (Subp_Id); - end if; - - Items := Contract (Subp_Id); - - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Item := - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Spec_Id, - Inher_Id => Subp_Id); - - -- The pragma Check equivalent of the class-wide - -- precondition is still created even though the - -- pragma may be ignored because the equivalent - -- performs semantic checks. - - if Is_Checked (Prag) then - - -- The spec of an inherited subprogram already - -- yielded a class-wide precondition. Merge the - -- existing precondition with the current one - -- using "or else". - - if Present (Class_Pre) then - Merge_Preconditions (Item, Class_Pre); - else - Class_Pre := Item; - end if; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - end if; - end loop; - - -- Add the merged class-wide preconditions - - if Present (Class_Pre) then - Prepend_To_Decls (Class_Pre); - Analyze (Class_Pre); - end if; - end Process_Inherited_Preconditions; + end Prepend_Pragma_To_Decls; ------------------------------- -- Process_Preconditions_For -- @@ -2983,7 +2981,7 @@ package body Contracts is N => Body_Decl); end if; - Prepend_To_Decls_Or_Save (Prag); + Prepend_Pragma_To_Decls (Prag); end if; Prag := Next_Pragma (Prag); @@ -3008,7 +3006,7 @@ package body Contracts is if Pragma_Name (Decl) = Name_Precondition and then Is_Checked (Decl) then - Prepend_To_Decls_Or_Save (Decl); + Prepend_Pragma_To_Decls (Decl); end if; -- Skip internally generated code @@ -3073,22 +3071,21 @@ package body Contracts is Next (Decl); end loop; - end if; - -- The processing of preconditions is done in reverse order (body - -- first), because each pragma Check equivalent is inserted at the - -- top of the declarations. This ensures that the final order is - -- consistent with following diagram: + -- The processing of preconditions is done in reverse order (body + -- first), because each pragma Check equivalent is inserted at the + -- top of the declarations. This ensures that the final order is + -- consistent with following diagram: - -- <inherited preconditions> - -- <preconditions from spec> - -- <preconditions from body> + -- <inherited preconditions> + -- <preconditions from spec> + -- <preconditions from body> - Process_Preconditions_For (Body_Id); + Process_Preconditions_For (Body_Id); + end if; if Present (Spec_Id) then Process_Preconditions_For (Spec_Id); - Process_Inherited_Preconditions; end if; end Process_Preconditions; @@ -3139,6 +3136,12 @@ package body Contracts is elsif Is_Ignored_Ghost_Entity (Subp_Id) then return; + -- No action needed for helpers and indirect-call wrapper built to + -- support class-wide preconditions. + + elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then + return; + -- Do not re-expand the same contract. This scenario occurs when a -- construct is rewritten into something else during its analysis -- (expression functions for instance). @@ -3605,6 +3608,1112 @@ package body Contracts is end if; end Instantiate_Subprogram_Contract; + ----------------------------------- + -- Make_Class_Precondition_Subps -- + ----------------------------------- + + procedure Make_Class_Precondition_Subps + (Subp_Id : Entity_Id; + Late_Overriding : Boolean := False) + is + Loc : constant Source_Ptr := Sloc (Subp_Id); + Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id); + + procedure Add_Indirect_Call_Wrapper; + -- Build the indirect-call wrapper and append it to the freezing actions + -- of Tagged_Type. + + procedure Add_Call_Helper + (Helper_Id : Entity_Id; + Is_Dynamic : Boolean); + -- Factorizes code for building a call helper with the given identifier + -- and append it to the freezing actions of Tagged_Type. Is_Dynamic + -- controls building the static or dynamic version of the helper. + + ------------------------------- + -- Add_Indirect_Call_Wrapper -- + ------------------------------- + + procedure Add_Indirect_Call_Wrapper is + + function Build_ICW_Body return Node_Id; + -- Build the body of the indirect call wrapper + + function Build_ICW_Decl return Node_Id; + -- Build the declaration of the indirect call wrapper + + -------------------- + -- Build_ICW_Body -- + -------------------- + + function Build_ICW_Body return Node_Id is + ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id); + Spec : constant Node_Id := Parent (ICW_Id); + Body_Spec : Node_Id; + Call : Node_Id; + ICW_Body : Node_Id; + + begin + Body_Spec := Copy_Subprogram_Spec (Spec); + + -- Build call to wrapped subprogram + + declare + Actuals : constant List_Id := Empty_List; + Formal_Spec : Entity_Id := + First (Parameter_Specifications (Spec)); + begin + -- Build parameter association & call + + while Present (Formal_Spec) loop + Append_To (Actuals, + New_Occurrence_Of + (Defining_Identifier (Formal_Spec), Loc)); + Next (Formal_Spec); + end loop; + + if Ekind (ICW_Id) = E_Procedure then + Call := + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Subp_Id, Loc), + Parameter_Associations => Actuals); + else + Call := + Make_Simple_Return_Statement (Loc, + Expression => + Make_Function_Call (Loc, + Name => New_Occurrence_Of (Subp_Id, Loc), + Parameter_Associations => Actuals)); + end if; + end; + + ICW_Body := + Make_Subprogram_Body (Loc, + Specification => Body_Spec, + Declarations => New_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List (Call))); + + -- The new operation is internal and overriding indicators do not + -- apply. + + Set_Must_Override (Body_Spec, False); + + return ICW_Body; + end Build_ICW_Body; + + -------------------- + -- Build_ICW_Decl -- + -------------------- + + function Build_ICW_Decl return Node_Id is + ICW_Id : constant Entity_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "ICW", + Suffix_Index => Source_Offset (Loc))); + Decl : Node_Id; + Spec : Node_Id; + + begin + Spec := Copy_Subprogram_Spec (Parent (Subp_Id)); + Set_Must_Override (Spec, False); + Set_Must_Not_Override (Spec, False); + Set_Defining_Unit_Name (Spec, ICW_Id); + Mutate_Ekind (ICW_Id, Ekind (Subp_Id)); + Set_Is_Public (ICW_Id); + + -- The indirect call wrapper is commonly used for indirect calls + -- but inlined for direct calls performed from the DTW. + + Set_Is_Inlined (ICW_Id); + + if Nkind (Spec) = N_Procedure_Specification then + Set_Null_Present (Spec, False); + end if; + + Decl := Make_Subprogram_Declaration (Loc, Spec); + + -- Link original subprogram to indirect wrapper and vice versa + + Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id); + Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id); + + -- Inherit debug info flag to allow debugging the wrapper + + if Needs_Debug_Info (Subp_Id) then + Set_Debug_Info_Needed (ICW_Id); + end if; + + return Decl; + end Build_ICW_Decl; + + -- Local Variables + + ICW_Body : Node_Id; + ICW_Decl : Node_Id; + + -- Start of processing for Add_Indirect_Call_Wrapper + + begin + pragma Assert (No (Indirect_Call_Wrapper (Subp_Id))); + + ICW_Decl := Build_ICW_Decl; + + Ensure_Freeze_Node (Tagged_Type); + Append_Freeze_Action (Tagged_Type, ICW_Decl); + Analyze (ICW_Decl); + + ICW_Body := Build_ICW_Body; + Append_Freeze_Action (Tagged_Type, ICW_Body); + + -- We cannot defer the analysis of this ICW wrapper when it is + -- built as a consequence of building its partner DTW wrapper + -- at the freezing point of the tagged type. + + if Is_Dispatch_Table_Wrapper (Subp_Id) then + Analyze (ICW_Body); + end if; + end Add_Indirect_Call_Wrapper; + + --------------------- + -- Add_Call_Helper -- + --------------------- + + procedure Add_Call_Helper + (Helper_Id : Entity_Id; + Is_Dynamic : Boolean) + is + function Build_Call_Helper_Body return Node_Id; + -- Build the body of a call helper + + function Build_Call_Helper_Decl return Node_Id; + -- Build the declaration of a call helper + + function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id; + -- Build the specification of the helper + + ---------------------------- + -- Build_Call_Helper_Body -- + ---------------------------- + + function Build_Call_Helper_Body return Node_Id is + + function Copy_And_Update_References + (Expr : Node_Id) return Node_Id; + -- Copy Expr updating references to formals of Helper_Id; update + -- also references to loop identifiers of quantified expressions. + + -------------------------------- + -- Copy_And_Update_References -- + -------------------------------- + + function Copy_And_Update_References + (Expr : Node_Id) return Node_Id + is + Assoc_List : constant Elist_Id := New_Elmt_List; + + procedure Map_Quantified_Expression_Loop_Identifiers; + -- Traverse Expr and append to Assoc_List the mapping of loop + -- identifers of quantified expressions with its new copy. + + ------------------------------------------------ + -- Map_Quantified_Expression_Loop_Identifiers -- + ------------------------------------------------ + + procedure Map_Quantified_Expression_Loop_Identifiers is + function Map_Loop_Param (N : Node_Id) return Traverse_Result; + -- Append to Assoc_List the mapping of loop identifers of + -- quantified expressions with its new copy. + + -------------------- + -- Map_Loop_Param -- + -------------------- + + function Map_Loop_Param (N : Node_Id) return Traverse_Result + is + begin + if Nkind (N) = N_Loop_Parameter_Specification + and then Nkind (Parent (N)) = N_Quantified_Expression + then + declare + Def_Id : constant Entity_Id := + Defining_Identifier (N); + begin + Append_Elmt (Def_Id, Assoc_List); + Append_Elmt (New_Copy (Def_Id), Assoc_List); + end; + end if; + + return OK; + end Map_Loop_Param; + + procedure Map_Quantified_Expressions is + new Traverse_Proc (Map_Loop_Param); + + begin + Map_Quantified_Expressions (Expr); + end Map_Quantified_Expression_Loop_Identifiers; + + -- Local variables + + Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id); + Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id); + + -- Start of processing for Copy_And_Update_References + + begin + while Present (Subp_Formal_Id) loop + Append_Elmt (Subp_Formal_Id, Assoc_List); + Append_Elmt (Helper_Formal_Id, Assoc_List); + + Next_Formal (Subp_Formal_Id); + Next_Formal (Helper_Formal_Id); + end loop; + + Map_Quantified_Expression_Loop_Identifiers; + + return New_Copy_Tree (Expr, Map => Assoc_List); + end Copy_And_Update_References; + + -- Local variables + + Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id)); + Body_Id : Entity_Id; + Body_Spec : Node_Id; + Body_Stmts : Node_Id; + Helper_Body : Node_Id; + Return_Expr : Node_Id; + + -- Start of processing for Build_Call_Helper_Body + + begin + pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id))); + pragma Assert (No (Corresponding_Body (Helper_Decl))); + + Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id)); + Body_Spec := Build_Call_Helper_Spec (Body_Id); + + Set_Corresponding_Body (Helper_Decl, Body_Id); + Set_Must_Override (Body_Spec, False); + + if Present (Class_Preconditions (Subp_Id)) then + Return_Expr := + Copy_And_Update_References (Class_Preconditions (Subp_Id)); + + -- When the subprogram is compiled with assertions disabled the + -- helper just returns True; done to avoid reporting errors at + -- link time since a unit may be compiled with assertions disabled + -- and another (which depends on it) compiled with assertions + -- enabled. + + else + pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id))); + Return_Expr := New_Occurrence_Of (Standard_True, Loc); + end if; + + Body_Stmts := + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Make_Simple_Return_Statement (Loc, Return_Expr))); + + Helper_Body := + Make_Subprogram_Body (Loc, + Specification => Body_Spec, + Declarations => New_List, + Handled_Statement_Sequence => Body_Stmts); + + return Helper_Body; + end Build_Call_Helper_Body; + + ---------------------------- + -- Build_Call_Helper_Decl -- + ---------------------------- + + function Build_Call_Helper_Decl return Node_Id is + Decl : Node_Id; + Spec : Node_Id; + + begin + Spec := Build_Call_Helper_Spec (Helper_Id); + Set_Must_Override (Spec, False); + Set_Must_Not_Override (Spec, False); + Set_Is_Inlined (Helper_Id); + Set_Is_Public (Helper_Id); + + Decl := Make_Subprogram_Declaration (Loc, Spec); + + -- Inherit debug info flag from Subp_Id to Helper_Id to allow + -- debugging of the helper subprogram. + + if Needs_Debug_Info (Subp_Id) then + Set_Debug_Info_Needed (Helper_Id); + end if; + + return Decl; + end Build_Call_Helper_Decl; + + ---------------------------- + -- Build_Call_Helper_Spec -- + ---------------------------- + + function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id + is + Spec : constant Node_Id := Parent (Subp_Id); + Def_Id : constant Node_Id := Defining_Unit_Name (Spec); + Formal : Entity_Id; + Func_Formals : constant List_Id := New_List; + P_Spec : constant List_Id := Parameter_Specifications (Spec); + Par_Formal : Node_Id; + Param : Node_Id; + Param_Type : Node_Id; + + begin + -- Create a list of formal parameters with the same types as the + -- original subprogram but changing the controlling formal. + + Param := First (P_Spec); + Formal := First_Formal (Def_Id); + while Present (Formal) loop + Par_Formal := Parent (Formal); + + if Is_Dynamic and then Is_Controlling_Formal (Formal) then + if Nkind (Parameter_Type (Par_Formal)) + = N_Access_Definition + then + Param_Type := + Copy_Separate_Tree (Parameter_Type (Par_Formal)); + Rewrite (Subtype_Mark (Param_Type), + Make_Attribute_Reference (Loc, + Prefix => Relocate_Node (Subtype_Mark (Param_Type)), + Attribute_Name => Name_Class)); + + else + Param_Type := + Make_Attribute_Reference (Loc, + Prefix => New_Occurrence_Of (Etype (Formal), Loc), + Attribute_Name => Name_Class); + end if; + else + Param_Type := New_Occurrence_Of (Etype (Formal), Loc); + end if; + + Append_To (Func_Formals, + Make_Parameter_Specification (Loc, + Defining_Identifier => + Make_Defining_Identifier (Loc, Chars (Formal)), + In_Present => In_Present (Par_Formal), + Out_Present => Out_Present (Par_Formal), + Null_Exclusion_Present => Null_Exclusion_Present + (Par_Formal), + Parameter_Type => Param_Type)); + + Next (Param); + Next_Formal (Formal); + end loop; + + return + Make_Function_Specification (Loc, + Defining_Unit_Name => Spec_Id, + Parameter_Specifications => Func_Formals, + Result_Definition => + New_Occurrence_Of (Standard_Boolean, Loc)); + end Build_Call_Helper_Spec; + + -- Local variables + + Helper_Body : Node_Id; + Helper_Decl : Node_Id; + + -- Start of processing for Add_Call_Helper + + begin + Helper_Decl := Build_Call_Helper_Decl; + Mutate_Ekind (Helper_Id, Ekind (Subp_Id)); + + -- Add the helper to the freezing actions of the tagged type + + Ensure_Freeze_Node (Tagged_Type); + Append_Freeze_Action (Tagged_Type, Helper_Decl); + Analyze (Helper_Decl); + + Helper_Body := Build_Call_Helper_Body; + Append_Freeze_Action (Tagged_Type, Helper_Body); + + -- If this helper is built as part of building the DTW at the + -- freezing point of its tagged type then we cannot defer + -- its analysis. + + if Late_Overriding then + pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id)); + Analyze (Helper_Body); + end if; + end Add_Call_Helper; + + -- Local variables + + Helper_Id : Entity_Id; + + -- Start of processing for Make_Class_Precondition_Subps + + begin + if Present (Class_Preconditions (Subp_Id)) + or Present (Ignored_Class_Preconditions (Subp_Id)) + then + pragma Assert + (Comes_From_Source (Subp_Id) + or else Is_Dispatch_Table_Wrapper (Subp_Id)); + + if No (Dynamic_Call_Helper (Subp_Id)) then + + -- Build and add to the freezing actions of Tagged_Type its + -- dynamic-call helper. + + Helper_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "DP", + Suffix_Index => Source_Offset (Loc))); + Add_Call_Helper (Helper_Id, Is_Dynamic => True); + + -- Link original subprogram to helper and vice versa + + Set_Dynamic_Call_Helper (Subp_Id, Helper_Id); + Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); + end if; + + if not Is_Abstract_Subprogram (Subp_Id) + and then No (Static_Call_Helper (Subp_Id)) + then + -- Build and add to the freezing actions of Tagged_Type its + -- static-call helper. + + Helper_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "SP", + Suffix_Index => Source_Offset (Loc))); + + Add_Call_Helper (Helper_Id, Is_Dynamic => False); + + -- Link original subprogram to helper and vice versa + + Set_Static_Call_Helper (Subp_Id, Helper_Id); + Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); + + -- Build and add to the freezing actions of Tagged_Type the + -- indirect-call wrapper. + + Add_Indirect_Call_Wrapper; + end if; + end if; + end Make_Class_Precondition_Subps; + + ---------------------------------------------- + -- Process_Class_Conditions_At_Freeze_Point -- + ---------------------------------------------- + + procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is + + procedure Check_Class_Conditions (Spec_Id : Entity_Id); + -- Check class-wide pre/postconditions of Spec_Id + + function Has_Class_Postconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean; + -- Return True if Spec_Id has (or inherits) a postconditions subprogram. + + function Has_Class_Preconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean; + -- Return True if Spec_Id has (or inherits) a preconditions subprogram. + + ---------------------------- + -- Check_Class_Conditions -- + ---------------------------- + + procedure Check_Class_Conditions (Spec_Id : Entity_Id) is + Par_Subp : Entity_Id; + + begin + for Kind in Condition_Kind loop + Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id); + + if Present (Par_Subp) then + Check_Class_Condition + (Cond => Class_Condition (Kind, Par_Subp), + Subp => Spec_Id, + Par_Subp => Par_Subp, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + end if; + end loop; + end Check_Class_Conditions; + + ----------------------------------------- + -- Has_Class_Postconditions_Subprogram -- + ----------------------------------------- + + function Has_Class_Postconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean is + begin + return + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Class_Postcondition)) + or else + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Ignored_Class_Postcondition)); + end Has_Class_Postconditions_Subprogram; + + ---------------------------------------- + -- Has_Class_Preconditions_Subprogram -- + ---------------------------------------- + + function Has_Class_Preconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean is + begin + return + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Class_Precondition)) + or else + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Ignored_Class_Precondition)); + end Has_Class_Preconditions_Subprogram; + + -- Local variables + + Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ)); + Prim : Entity_Id; + + -- Start of processing for Process_Class_Conditions_At_Freeze_Point + + begin + while Present (Prim_Elmt) loop + Prim := Node (Prim_Elmt); + + if Has_Class_Preconditions_Subprogram (Prim) + or else Has_Class_Postconditions_Subprogram (Prim) + then + if Comes_From_Source (Prim) then + if Has_Significant_Contract (Prim) then + Merge_Class_Conditions (Prim); + end if; + + -- Handle wrapper of protected operation + + elsif Is_Primitive_Wrapper (Prim) then + Merge_Class_Conditions (Prim); + + -- Check inherited class-wide conditions, excluding internal + -- entities built for mapping of interface primitives. + + elsif Is_Derived_Type (Typ) + and then Present (Alias (Prim)) + and then No (Interface_Alias (Prim)) + then + Check_Class_Conditions (Prim); + end if; + end if; + + Next_Elmt (Prim_Elmt); + end loop; + end Process_Class_Conditions_At_Freeze_Point; + + ---------------------------- + -- Merge_Class_Conditions -- + ---------------------------- + + procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is + + procedure Preanalyze_Condition + (Subp : Entity_Id; + Expr : Node_Id); + -- Preanalyze the class-wide condition Expr of Subp + + procedure Process_Inherited_Conditions (Kind : Condition_Kind); + -- Collect all inherited class-wide conditions of Spec_Id and merge + -- them into one big condition. + + -------------------------- + -- Preanalyze_Condition -- + -------------------------- + + procedure Preanalyze_Condition + (Subp : Entity_Id; + Expr : Node_Id) + is + procedure Clear_Unset_References; + -- Clear unset references on formals of Subp since preanalysis + -- occurs in a place unrelated to the actual code. + + procedure Remove_Controlling_Arguments; + -- Traverse Expr and clear the Controlling_Argument of calls to + -- nonabstract functions. + + procedure Remove_Formals (Id : Entity_Id); + -- Remove formals from homonym chains and make them not visible + + ---------------------------- + -- Clear_Unset_References -- + ---------------------------- + + procedure Clear_Unset_References is + F : Entity_Id := First_Formal (Subp); + + begin + while Present (F) loop + Set_Unset_Reference (F, Empty); + Next_Formal (F); + end loop; + end Clear_Unset_References; + + ---------------------------------- + -- Remove_Controlling_Arguments -- + ---------------------------------- + + procedure Remove_Controlling_Arguments is + function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result; + -- Reset the Controlling_Argument of calls to nonabstract + -- function calls. + + --------------------- + -- Remove_Ctrl_Arg -- + --------------------- + + function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is + begin + if Nkind (N) = N_Function_Call + and then Present (Controlling_Argument (N)) + and then not Is_Abstract_Subprogram (Entity (Name (N))) + then + Set_Controlling_Argument (N, Empty); + end if; + + return OK; + end Remove_Ctrl_Arg; + + procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg); + begin + Remove_Ctrl_Args (Expr); + end Remove_Controlling_Arguments; + + -------------------- + -- Remove_Formals -- + -------------------- + + procedure Remove_Formals (Id : Entity_Id) is + F : Entity_Id := First_Formal (Id); + + begin + while Present (F) loop + Set_Is_Immediately_Visible (F, False); + Remove_Homonym (F); + Next_Formal (F); + end loop; + end Remove_Formals; + + -- Start of processing for Preanalyze_Condition + + begin + pragma Assert (Present (Expr)); + pragma Assert (Inside_Class_Condition_Preanalysis = False); + + Push_Scope (Subp); + Install_Formals (Subp); + Inside_Class_Condition_Preanalysis := True; + + Preanalyze_And_Resolve (Expr, Standard_Boolean); + + Inside_Class_Condition_Preanalysis := False; + Remove_Formals (Subp); + Pop_Scope; + + -- Traverse Expr and clear the Controlling_Argument of calls to + -- nonabstract functions. Required since the preanalyzed condition + -- is not yet installed on its definite context and will be cloned + -- and extended in derivations with additional conditions. + + Remove_Controlling_Arguments; + + -- Clear also attribute Unset_Reference; again because preanalysis + -- occurs in a place unrelated to the actual code. + + Clear_Unset_References; + end Preanalyze_Condition; + + ---------------------------------- + -- Process_Inherited_Conditions -- + ---------------------------------- + + procedure Process_Inherited_Conditions (Kind : Condition_Kind) is + Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id); + Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id); + Seen : Subprogram_List (Subps'Range) := (others => Empty); + + function Inherit_Condition + (Par_Subp : Entity_Id; + Subp : Entity_Id) return Node_Id; + -- Inherit the class-wide condition from Par_Subp to Subp and adjust + -- all the references to formals in the inherited condition. + + procedure Merge_Conditions (From : Node_Id; Into : Node_Id); + -- Merge two class-wide preconditions or postconditions (the former + -- are merged using "or else", and the latter are merged using "and- + -- then"). The changes are accumulated in parameter Into. + + function Seen_Subp (Id : Entity_Id) return Boolean; + -- Return True if the contract of subprogram Id has been processed + + ----------------------- + -- Inherit_Condition -- + ----------------------- + + function Inherit_Condition + (Par_Subp : Entity_Id; + Subp : Entity_Id) return Node_Id + is + Installed_Calls : constant Elist_Id := New_Elmt_List; + + procedure Install_Original_Selected_Component (Expr : Node_Id); + -- Traverse the given expression searching for dispatching calls + -- to functions whose original nodes was a selected component, + -- and replacing them temporarily by a copy of their original + -- node. Modified calls are stored in the list Installed_Calls + -- (to undo this work later). + + procedure Restore_Dispatching_Calls (Expr : Node_Id); + -- Undo the work done by Install_Original_Selected_Component. + + ----------------------------------------- + -- Install_Original_Selected_Component -- + ----------------------------------------- + + procedure Install_Original_Selected_Component (Expr : Node_Id) is + function Install_Node (N : Node_Id) return Traverse_Result; + -- Process a single node + + ------------------ + -- Install_Node -- + ------------------ + + function Install_Node (N : Node_Id) return Traverse_Result is + New_N : Node_Id; + Orig_Nod : Node_Id; + + begin + if Nkind (N) = N_Function_Call + and then Nkind (Original_Node (N)) = N_Selected_Component + and then Is_Dispatching_Operation (Entity (Name (N))) + then + Orig_Nod := Original_Node (N); + + -- Temporarily use the original node field to keep the + -- reference to this node (to undo this work later!). + + New_N := New_Copy (N); + Set_Original_Node (New_N, Orig_Nod); + Append_Elmt (New_N, Installed_Calls); + + Rewrite (N, Orig_Nod); + Set_Original_Node (N, New_N); + end if; + + return OK; + end Install_Node; + + procedure Install_Nodes is new Traverse_Proc (Install_Node); + + begin + Install_Nodes (Expr); + end Install_Original_Selected_Component; + + ------------------------------- + -- Restore_Dispatching_Calls -- + ------------------------------- + + procedure Restore_Dispatching_Calls (Expr : Node_Id) is + function Restore_Node (N : Node_Id) return Traverse_Result; + -- Process a single node + + ------------------ + -- Restore_Node -- + ------------------ + + function Restore_Node (N : Node_Id) return Traverse_Result is + Orig_Sel_N : Node_Id; + + begin + if Nkind (N) = N_Selected_Component + and then Nkind (Original_Node (N)) = N_Function_Call + and then Contains (Installed_Calls, Original_Node (N)) + then + Orig_Sel_N := Original_Node (Original_Node (N)); + pragma Assert (Nkind (Orig_Sel_N) = N_Selected_Component); + Rewrite (N, Original_Node (N)); + Set_Original_Node (N, Orig_Sel_N); + end if; + + return OK; + end Restore_Node; + + procedure Restore_Nodes is new Traverse_Proc (Restore_Node); + + begin + Restore_Nodes (Expr); + end Restore_Dispatching_Calls; + + -- Local variables + + Assoc_List : constant Elist_Id := New_Elmt_List; + Par_Formal_Id : Entity_Id := First_Formal (Par_Subp); + Subp_Formal_Id : Entity_Id := First_Formal (Subp); + New_Expr : Node_Id; + Class_Cond : Node_Id; + + -- Start of processing for Inherit_Condition + + begin + while Present (Par_Formal_Id) loop + Append_Elmt (Par_Formal_Id, Assoc_List); + Append_Elmt (Subp_Formal_Id, Assoc_List); + + Next_Formal (Par_Formal_Id); + Next_Formal (Subp_Formal_Id); + end loop; + + -- In order to properly preanalyze an inherited preanalyzed + -- condition that has occurrences of the Object.Operation + -- notation we must restore the original node; otherwise we + -- would report spurious errors. + + Class_Cond := Class_Condition (Kind, Par_Subp); + + Install_Original_Selected_Component (Class_Cond); + New_Expr := New_Copy_Tree (Class_Cond); + Restore_Dispatching_Calls (Class_Cond); + + return New_Copy_Tree (New_Expr, Map => Assoc_List); + end Inherit_Condition; + + ---------------------- + -- Merge_Conditions -- + ---------------------- + + procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is + function Expression_Arg (Expr : Node_Id) return Node_Id; + -- Return the boolean expression argument of a condition while + -- updating its parentheses count for the subsequent merge. + + -------------------- + -- Expression_Arg -- + -------------------- + + function Expression_Arg (Expr : Node_Id) return Node_Id is + begin + if Paren_Count (Expr) = 0 then + Set_Paren_Count (Expr, 1); + end if; + + return Expr; + end Expression_Arg; + + -- Local variables + + From_Expr : constant Node_Id := Expression_Arg (From); + Into_Expr : constant Node_Id := Expression_Arg (Into); + Loc : constant Source_Ptr := Sloc (Into); + + -- Start of processing for Merge_Conditions + + begin + case Kind is + + -- Merge the two preconditions by "or else"-ing them + + when Ignored_Class_Precondition + | Class_Precondition + => + Rewrite (Into_Expr, + Make_Or_Else (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); + + -- Merge the two postconditions by "and then"-ing them + + when Ignored_Class_Postcondition + | Class_Postcondition + => + Rewrite (Into_Expr, + Make_And_Then (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); + end case; + end Merge_Conditions; + + --------------- + -- Seen_Subp -- + --------------- + + function Seen_Subp (Id : Entity_Id) return Boolean is + begin + for Index in Seen'Range loop + if Seen (Index) = Id then + return True; + end if; + end loop; + + return False; + end Seen_Subp; + + -- Local variables + + Class_Cond : Node_Id; + Cond : Node_Id; + Subp_Id : Entity_Id; + Par_Prim : Entity_Id := Empty; + Par_Iface_Prims : Elist_Id := No_Elist; + + -- Start of processing for Process_Inherited_Conditions + + begin + Class_Cond := Class_Condition (Kind, Spec_Id); + + -- Process parent primitives looking for nearest ancestor with + -- class-wide conditions. + + for Index in Subps'Range loop + Subp_Id := Subps (Index); + + if No (Par_Prim) + and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ) + then + if Present (Alias (Subp_Id)) then + Subp_Id := Ultimate_Alias (Subp_Id); + end if; + + -- Wrappers of class-wide pre/postconditions reference the + -- parent primitive that has the inherited contract and help + -- us to climb fast. + + if Is_Wrapper (Subp_Id) + and then Present (LSP_Subprogram (Subp_Id)) + then + Subp_Id := LSP_Subprogram (Subp_Id); + end if; + + if not Seen_Subp (Subp_Id) + and then Present (Class_Condition (Kind, Subp_Id)) + then + Seen (Index) := Subp_Id; + Par_Prim := Subp_Id; + Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim); + + Cond := Inherit_Condition + (Subp => Spec_Id, + Par_Subp => Subp_Id); + + if Present (Class_Cond) then + Merge_Conditions (Cond, Class_Cond); + else + Class_Cond := Cond; + end if; + + Check_Class_Condition + (Cond => Class_Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + Build_Class_Wide_Expression + (Pragma_Or_Expr => Class_Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Adjust_Sloc => False); + + -- We are done as soon as we process the nearest ancestor + + exit; + end if; + end if; + end loop; + + -- Process the contract of interface primitives not covered by + -- the nearest ancestor. + + for Index in Subps'Range loop + Subp_Id := Subps (Index); + + if Is_Interface (Find_Dispatching_Type (Subp_Id)) then + if Present (Alias (Subp_Id)) then + Subp_Id := Ultimate_Alias (Subp_Id); + end if; + + if not Seen_Subp (Subp_Id) + and then Present (Class_Condition (Kind, Subp_Id)) + and then not Contains (Par_Iface_Prims, Subp_Id) + then + Seen (Index) := Subp_Id; + + Cond := Inherit_Condition + (Subp => Spec_Id, + Par_Subp => Subp_Id); + + Check_Class_Condition + (Cond => Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + Build_Class_Wide_Expression + (Pragma_Or_Expr => Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Adjust_Sloc => False); + + if Present (Class_Cond) then + Merge_Conditions (Cond, Class_Cond); + else + Class_Cond := Cond; + end if; + end if; + end if; + end loop; + + Set_Class_Condition (Kind, Spec_Id, Class_Cond); + end Process_Inherited_Conditions; + + -- Local variables + + Cond : Node_Id; + + -- Start of processing for Merge_Class_Conditions + + begin + for Kind in Condition_Kind loop + Cond := Class_Condition (Kind, Spec_Id); + + -- If this subprogram has class-wide conditions then preanalyze + -- them before processing inherited conditions since conditions + -- are checked and merged from right to left. + + if Present (Cond) then + Preanalyze_Condition (Spec_Id, Cond); + end if; + + Process_Inherited_Conditions (Kind); + + -- Preanalyze merged inherited conditions + + if Cond /= Class_Condition (Kind, Spec_Id) then + Preanalyze_Condition (Spec_Id, + Class_Condition (Kind, Spec_Id)); + end if; + end loop; + end Merge_Class_Conditions; + ---------------------------------------- -- Save_Global_References_In_Contract -- ---------------------------------------- @@ -3622,10 +4731,9 @@ package body Contracts is ------------------------------------ procedure Save_Global_References_In_List (First_Prag : Node_Id) is - Prag : Node_Id; + Prag : Node_Id := First_Prag; begin - Prag := First_Prag; while Present (Prag) loop if Is_Generic_Contract_Pragma (Prag) then Save_Global_References (Prag); @@ -3662,4 +4770,29 @@ package body Contracts is Pop_Scope; end Save_Global_References_In_Contract; + ------------------------- + -- Set_Class_Condition -- + ------------------------- + + procedure Set_Class_Condition + (Kind : Condition_Kind; + Subp : Entity_Id; + Cond : Node_Id) + is + begin + case Kind is + when Class_Postcondition => + Set_Class_Postconditions (Subp, Cond); + + when Class_Precondition => + Set_Class_Preconditions (Subp, Cond); + + when Ignored_Class_Postcondition => + Set_Ignored_Class_Postconditions (Subp, Cond); + + when Ignored_Class_Precondition => + Set_Ignored_Class_Preconditions (Subp, Cond); + end case; + end Set_Class_Condition; + end Contracts; |