--
-- Part_Of
+ procedure Build_Subprogram_Contract_Wrapper
+ (Body_Id : Entity_Id;
+ Stmts : List_Id;
+ Decls : List_Id;
+ Result : Entity_Id);
+ -- Generate a wrapper for a given subprogram body when the expansion of
+ -- postconditions require it by moving its declarations and statements
+ -- into a locally declared subprogram _Wrapped_Statements.
+
+ -- Postcondition and precondition checks then get inserted in place of
+ -- the original statements and declarations along with a call to
+ -- _Wrapped_Statements.
+
procedure Check_Class_Condition
(Cond : Node_Id;
Subp : Entity_Id;
-- In SPARK_Mode, an inherited operation that is not overridden but has
-- inherited modified conditions pre/postconditions is illegal.
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
+ -- Determine whether arbitrary declaration Decl denotes a renaming of
+ -- a discriminant or protection field _object.
+
procedure Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id : Entity_Id);
-- Perform checking of external properties pragmas that is common to both
end loop;
end Analyze_Contracts;
+ -------------------------------------
+ -- Analyze_Pragmas_In_Declarations --
+ -------------------------------------
+
+ procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id) is
+ Curr_Decl : Node_Id;
+
+ begin
+ -- Move through the body's declarations analyzing all pragmas which
+ -- appear at the top of the declarations.
+
+ Curr_Decl := First (Declarations (Unit_Declaration_Node (Body_Id)));
+ while Present (Curr_Decl) loop
+
+ if Nkind (Curr_Decl) = N_Pragma then
+
+ if Pragma_Significant_To_Subprograms
+ (Get_Pragma_Id (Curr_Decl))
+ then
+ Analyze (Curr_Decl);
+ end if;
+
+ -- Skip the renamings of discriminants and protection fields
+
+ elsif Is_Prologue_Renaming (Curr_Decl) then
+ null;
+
+ -- We have reached something which is not a pragma so we can be sure
+ -- there are no more contracts or pragmas which need to be taken into
+ -- account.
+
+ else
+ exit;
+ end if;
+
+ Next (Curr_Decl);
+ end loop;
+ end Analyze_Pragmas_In_Declarations;
+
-----------------------------------------------
-- Analyze_Entry_Or_Subprogram_Body_Contract --
-----------------------------------------------
else
declare
- Bod : Node_Id;
+ Bod : Node_Id := Empty;
Freeze_Types : Boolean := False;
begin
(Type_Or_Obj_Id => Type_Id);
end Analyze_Type_Contract;
+ ---------------------------------------
+ -- Build_Subprogram_Contract_Wrapper --
+ ---------------------------------------
+
+ procedure Build_Subprogram_Contract_Wrapper
+ (Body_Id : Entity_Id;
+ Stmts : List_Id;
+ Decls : List_Id;
+ Result : Entity_Id)
+ is
+ Actuals : constant List_Id := Empty_List;
+ Body_Decl : constant Entity_Id := Unit_Declaration_Node (Body_Id);
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+ Subp_Id : Entity_Id;
+ Ret_Type : Entity_Id;
+
+ Wrapper_Id : Entity_Id;
+ Wrapper_Body : Node_Id;
+ Wrapper_Spec : Node_Id;
+
+ begin
+ -- When there are no postcondition statements we do not need to
+ -- generate a wrapper.
+
+ if No (Stmts) then
+ return;
+ end if;
+
+ -- Obtain the related subprogram id from the body id.
+
+ if Present (Spec_Id) then
+ Subp_Id := Spec_Id;
+ else
+ Subp_Id := Body_Id;
+ end if;
+ Ret_Type := Etype (Subp_Id);
+
+ -- Generate the contracts wrapper by moving the original declarations
+ -- and statements within a local subprogram and calling it within
+ -- an extended return to preserve the result for the purpose of
+ -- evaluating postconditions, contracts, type invariants, etc.
+
+ -- Generate:
+ --
+ -- function Original_Func (X : in out Integer) return Typ is
+ -- <prologue renamings>
+ -- <preconditions>
+ --
+ -- function _Wrapped_Statements return Typ is
+ -- <original declarations>
+ -- begin
+ -- <original statements>
+ -- end;
+ --
+ -- begin
+ -- return
+ -- Result_Obj : constant Typ := _Wrapped_Statements
+ -- do
+ -- <postconditions statments>
+ -- end return;
+ -- end;
+ --
+ -- Or, in the case of a procedure:
+ --
+ -- procedure Original_Proc (X : in out Integer) is
+ -- <prologue renamings>
+ -- <preconditions>
+ --
+ -- procedure _Wrapped_Statements is
+ -- <original declarations>
+ -- begin
+ -- <original statements>
+ -- end;
+ --
+ -- begin
+ -- _Wrapped_Statements;
+ -- <postconditions statments>
+ -- end;
+ --
+
+ -- Create Identifier
+
+ Wrapper_Id := Make_Defining_Identifier (Loc, Name_uWrapped_Statements);
+ Set_Debug_Info_Needed (Wrapper_Id);
+ Set_Wrapped_Statements (Subp_Id, Wrapper_Id);
+
+ -- Create specification and declaration for the wrapper
+
+ if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
+ Wrapper_Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Wrapper_Id);
+ else
+ Wrapper_Spec :=
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name => Wrapper_Id,
+ Result_Definition => New_Occurrence_Of (Ret_Type, Loc));
+ end if;
+
+ -- Create the wrapper body using Body_Id's statements and declarations
+
+ Wrapper_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification => Wrapper_Spec,
+ Declarations => Declarations (Body_Decl),
+ Handled_Statement_Sequence =>
+ Relocate_Node (Handled_Statement_Sequence (Body_Decl)));
+
+ Append_To (Decls, Wrapper_Body);
+ Set_Declarations (Body_Decl, Decls);
+ Set_Handled_Statement_Sequence (Body_Decl,
+ Make_Handled_Sequence_Of_Statements (Loc,
+ End_Label => Make_Identifier (Loc, Chars (Wrapper_Id)),
+ Statements => New_List));
+
+ -- Move certain flags which are relevant to the body
+
+ -- Wouldn't a better way be to perform some sort of copy of Body_Decl
+ -- for Wrapper_Body be less error-prone ???
+
+ if Was_Expression_Function (Body_Decl) then
+ Set_Was_Expression_Function (Body_Decl, False);
+ Set_Was_Expression_Function (Wrapper_Body);
+ end if;
+
+ Set_Has_Pragma_Inline (Wrapper_Id, Has_Pragma_Inline (Subp_Id));
+ Set_Has_Pragma_Inline_Always
+ (Wrapper_Id, Has_Pragma_Inline_Always (Subp_Id));
+
+ -- Generate call to the wrapper
+
+ if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
+ Prepend_To (Stmts,
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Wrapper_Id, Loc)));
+ Set_Statements
+ (Handled_Statement_Sequence (Body_Decl), Stmts);
+
+ -- Generate the post-execution statements and the extended return
+ -- when the subprogram being wrapped is a function.
+
+ else
+ Set_Statements (Handled_Statement_Sequence (Body_Decl), New_List (
+ Make_Extended_Return_Statement (Loc,
+ Return_Object_Declarations => New_List (
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Result,
+ Object_Definition =>
+ New_Occurrence_Of (Ret_Type, Loc),
+ Expression =>
+ Make_Function_Call (Loc,
+ Name =>
+ New_Occurrence_Of (Wrapper_Id, Loc),
+ Parameter_Associations => Actuals))),
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts))));
+ end if;
+ end Build_Subprogram_Contract_Wrapper;
+
+ ----------------------------------
+ -- Build_Entry_Contract_Wrapper --
+ ----------------------------------
+
+ procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
+ Conc_Typ : constant Entity_Id := Scope (E);
+ Loc : constant Source_Ptr := Sloc (E);
+
+ procedure Add_Discriminant_Renamings
+ (Obj_Id : Entity_Id;
+ Decls : List_Id);
+ -- Add renaming declarations for all discriminants of concurrent type
+ -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
+ -- represents the concurrent object.
+
+ procedure Add_Matching_Formals
+ (Formals : List_Id;
+ Actuals : in out List_Id);
+ -- Add formal parameters that match those of entry E to list Formals.
+ -- The routine also adds matching actuals for the new formals to list
+ -- Actuals.
+
+ procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
+ -- Relocate pragma Prag to list To. The routine creates a new list if
+ -- To does not exist.
+
+ --------------------------------
+ -- Add_Discriminant_Renamings --
+ --------------------------------
+
+ procedure Add_Discriminant_Renamings
+ (Obj_Id : Entity_Id;
+ Decls : List_Id)
+ is
+ Discr : Entity_Id;
+ Renaming_Decl : Node_Id;
+
+ begin
+ -- Inspect the discriminants of the concurrent type and generate a
+ -- renaming for each one.
+
+ if Has_Discriminants (Conc_Typ) then
+ Discr := First_Discriminant (Conc_Typ);
+ while Present (Discr) loop
+ Renaming_Decl :=
+ Make_Object_Renaming_Declaration (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc, Chars (Discr)),
+ Subtype_Mark =>
+ New_Occurrence_Of (Etype (Discr), Loc),
+ Name =>
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Selector_Name =>
+ Make_Identifier (Loc, Chars (Discr))));
+
+ Prepend_To (Decls, Renaming_Decl);
+
+ Next_Discriminant (Discr);
+ end loop;
+ end if;
+ end Add_Discriminant_Renamings;
+
+ --------------------------
+ -- Add_Matching_Formals --
+ --------------------------
+
+ procedure Add_Matching_Formals
+ (Formals : List_Id;
+ Actuals : in out List_Id)
+ is
+ Formal : Entity_Id;
+ New_Formal : Entity_Id;
+
+ begin
+ -- Inspect the formal parameters of the entry and generate a new
+ -- matching formal with the same name for the wrapper. A reference
+ -- to the new formal becomes an actual in the entry call.
+
+ Formal := First_Formal (E);
+ while Present (Formal) loop
+ New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
+ Append_To (Formals,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => New_Formal,
+ In_Present => In_Present (Parent (Formal)),
+ Out_Present => Out_Present (Parent (Formal)),
+ Parameter_Type =>
+ New_Occurrence_Of (Etype (Formal), Loc)));
+
+ if No (Actuals) then
+ Actuals := New_List;
+ end if;
+
+ Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
+ Next_Formal (Formal);
+ end loop;
+ end Add_Matching_Formals;
+
+ ---------------------
+ -- Transfer_Pragma --
+ ---------------------
+
+ procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
+ New_Prag : Node_Id;
+
+ begin
+ if No (To) then
+ To := New_List;
+ end if;
+
+ New_Prag := Relocate_Node (Prag);
+
+ Set_Analyzed (New_Prag, False);
+ Append (New_Prag, To);
+ end Transfer_Pragma;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (E);
+ Actuals : List_Id := No_List;
+ Call : Node_Id;
+ Call_Nam : Node_Id;
+ Decls : List_Id := No_List;
+ Formals : List_Id;
+ Has_Pragma : Boolean := False;
+ Index_Id : Entity_Id;
+ Obj_Id : Entity_Id;
+ Prag : Node_Id;
+ Wrapper_Id : Entity_Id;
+
+ -- Start of processing for Build_Entry_Contract_Wrapper
+
+ begin
+ -- This routine generates a specialized wrapper for a protected or task
+ -- entry [family] which implements precondition/postcondition semantics.
+ -- Preconditions and case guards of contract cases are checked before
+ -- the protected action or rendezvous takes place.
+
+ -- procedure Wrapper
+ -- (Obj_Id : Conc_Typ; -- concurrent object
+ -- [Index : Index_Typ;] -- index of entry family
+ -- [Formal_1 : ...; -- parameters of original entry
+ -- Formal_N : ...])
+ -- is
+ -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
+ -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
+
+ -- <contracts pragmas>
+ -- <case guard checks>
+
+ -- begin
+ -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
+ -- end Wrapper;
+
+ -- Create the wrapper only when the entry has at least one executable
+ -- contract item such as contract cases, precondition or postcondition.
+
+ if Present (Items) then
+
+ -- Inspect the list of pre/postconditions and transfer all available
+ -- pragmas to the declarative list of the wrapper.
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name_Unmapped (Prag) in Name_Postcondition
+ | Name_Precondition
+ and then Is_Checked (Prag)
+ then
+ Has_Pragma := True;
+ Transfer_Pragma (Prag, To => Decls);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Inspect the list of test/contract cases and transfer only contract
+ -- cases pragmas to the declarative part of the wrapper.
+
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases
+ and then Is_Checked (Prag)
+ then
+ Has_Pragma := True;
+ Transfer_Pragma (Prag, To => Decls);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- The entry lacks executable contract items and a wrapper is not needed
+
+ if not Has_Pragma then
+ return;
+ end if;
+
+ -- Create the profile of the wrapper. The first formal parameter is the
+ -- concurrent object.
+
+ Obj_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Conc_Typ), 'A'));
+
+ Formals := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Obj_Id,
+ Out_Present => True,
+ In_Present => True,
+ Parameter_Type => New_Occurrence_Of (Conc_Typ, Loc)));
+
+ -- Construct the call to the original entry. The call will be gradually
+ -- augmented with an optional entry index and extra parameters.
+
+ Call_Nam :=
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Selector_Name => New_Occurrence_Of (E, Loc));
+
+ -- When creating a wrapper for an entry family, the second formal is the
+ -- entry index.
+
+ if Ekind (E) = E_Entry_Family then
+ Index_Id := Make_Defining_Identifier (Loc, Name_I);
+
+ Append_To (Formals,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Index_Id,
+ Parameter_Type =>
+ New_Occurrence_Of (Entry_Index_Type (E), Loc)));
+
+ -- The call to the original entry becomes an indexed component to
+ -- accommodate the entry index.
+
+ Call_Nam :=
+ Make_Indexed_Component (Loc,
+ Prefix => Call_Nam,
+ Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
+ end if;
+
+ -- Add formal parameters to match those of the entry and build actuals
+ -- for the entry call.
+
+ Add_Matching_Formals (Formals, Actuals);
+
+ Call :=
+ Make_Procedure_Call_Statement (Loc,
+ Name => Call_Nam,
+ Parameter_Associations => Actuals);
+
+ -- Add renaming declarations for the discriminants of the enclosing type
+ -- as the various contract items may reference them.
+
+ Add_Discriminant_Renamings (Obj_Id, Decls);
+
+ Wrapper_Id :=
+ Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
+ Set_Contract_Wrapper (E, Wrapper_Id);
+ Set_Is_Entry_Wrapper (Wrapper_Id);
+
+ -- The wrapper body is analyzed when the enclosing type is frozen
+
+ Append_Freeze_Action (Defining_Entity (Decl),
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Wrapper_Id,
+ Parameter_Specifications => Formals),
+ Declarations => Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call))));
+ end Build_Entry_Contract_Wrapper;
+
---------------------------
-- Check_Class_Condition --
---------------------------
-- the item denotes a pragma, it is added to the list only when it is
-- enabled.
- procedure Build_Postconditions_Procedure
- (Subp_Id : Entity_Id;
- Stmts : List_Id;
- Result : Entity_Id);
- -- Create the body of procedure _Postconditions which handles various
- -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
- -- of statements to be checked on exit. Parameter Result is the entity
- -- of parameter _Result when Subp_Id denotes a function.
-
- procedure Process_Contract_Cases (Stmts : in out List_Id);
+ procedure Process_Contract_Cases
+ (Stmts : in out List_Id;
+ Decls : List_Id);
-- Process pragma Contract_Cases. This routine prepends items to the
-- body declarations and appends items to list Stmts.
-- Collect all [inherited] spec and body postconditions and accumulate
-- their pragma Check equivalents in list Stmts.
- procedure Process_Preconditions;
+ procedure Process_Preconditions (Decls : in out List_Id);
-- Collect all [inherited] spec and body preconditions and prepend their
-- pragma Check equivalents to the declarations of the body.
end if;
end Append_Enabled_Item;
- ------------------------------------
- -- Build_Postconditions_Procedure --
- ------------------------------------
-
- procedure Build_Postconditions_Procedure
- (Subp_Id : Entity_Id;
- Stmts : List_Id;
- Result : Entity_Id)
- is
- Loc : constant Source_Ptr := Sloc (Body_Decl);
- Last_Decl : Node_Id;
- Params : List_Id := No_List;
- Proc_Bod : Node_Id;
- Proc_Decl : Node_Id;
- Proc_Id : Entity_Id;
- Proc_Spec : Node_Id;
-
- -- Extra declarations needed to handle interactions between
- -- postconditions and finalization.
-
- Postcond_Enabled_Decl : Node_Id;
- Return_Success_Decl : Node_Id;
- Result_Obj_Decl : Node_Id;
- Result_Obj_Type_Decl : Node_Id;
- Result_Obj_Type : Entity_Id;
-
- -- Start of processing for Build_Postconditions_Procedure
-
- begin
- -- Nothing to do if there are no actions to check on exit
-
- if No (Stmts) then
- return;
- end if;
-
- -- Otherwise, we generate the postcondition procedure and add
- -- associated objects and conditions used to coordinate postcondition
- -- evaluation with finalization.
-
- -- Generate:
- --
- -- procedure _postconditions (Return_Exp : Result_Typ);
- --
- -- -- Result_Obj_Type created when Result_Type is non-elementary
- -- [type Result_Obj_Type is access all Result_Typ;]
- --
- -- Result_Obj : Result_Obj_Type;
- --
- -- Postcond_Enabled : Boolean := True;
- -- Return_Success_For_Postcond : Boolean := False;
- --
- -- procedure _postconditions (Return_Exp : Result_Typ) is
- -- begin
- -- if Postcond_Enabled and then Return_Success_For_Postcond then
- -- [stmts];
- -- end if;
- -- end;
-
- Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
- Set_Debug_Info_Needed (Proc_Id);
- Set_Postconditions_Proc (Subp_Id, Proc_Id);
-
- -- Mark it inlined to speed up the call
-
- Set_Is_Inlined (Proc_Id);
-
- -- Force the front-end inlining of _Postconditions when generating C
- -- code, since its body may have references to itypes defined in the
- -- enclosing subprogram, which would cause problems for unnesting
- -- routines in the absence of inlining.
-
- if Modify_Tree_For_C then
- Set_Has_Pragma_Inline (Proc_Id);
- Set_Has_Pragma_Inline_Always (Proc_Id);
- end if;
-
- -- The related subprogram is a function: create the specification of
- -- parameter _Result.
-
- if Present (Result) then
- Params := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Result,
- Parameter_Type =>
- New_Occurrence_Of (Etype (Result), Loc)));
- end if;
-
- Proc_Spec :=
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => Params);
-
- Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
-
- -- Insert _Postconditions before the first source declaration of the
- -- body. This ensures that the body will not cause any premature
- -- freezing, as it may mention types:
-
- -- Generate:
- --
- -- 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_Before_First_Source_Declaration
- (Proc_Decl, Declarations (Body_Decl));
- Analyze (Proc_Decl);
- Last_Decl := Proc_Decl;
-
- -- When Result is present (e.g. the postcondition checks apply to a
- -- function) we make a local object to capture the result, so, if
- -- needed, we can call the generated postconditions procedure during
- -- finalization instead of at the point of return.
-
- -- Note: The placement of the following declarations before the
- -- declaration of the body of the postconditions, but after the
- -- declaration of the postconditions spec is deliberate and required
- -- since other code within the expander expects them to be located
- -- here. Perhaps when more space is available in the tree this will
- -- no longer be necessary ???
-
- if Present (Result) then
- -- Elementary result types mean a copy is cheap and preferred over
- -- using pointers.
-
- if Is_Elementary_Type (Etype (Result)) then
- Result_Obj_Type := Etype (Result);
-
- -- Otherwise, we create a named access type to capture the result
-
- -- Generate:
- --
- -- type Result_Obj_Type is access all [Result_Type];
-
- else
- Result_Obj_Type := Make_Temporary (Loc, 'R');
-
- Result_Obj_Type_Decl :=
- Make_Full_Type_Declaration (Loc,
- Defining_Identifier => Result_Obj_Type,
- Type_Definition =>
- Make_Access_To_Object_Definition (Loc,
- All_Present => True,
- Subtype_Indication => New_Occurrence_Of
- (Etype (Result), Loc)));
- Insert_After_And_Analyze (Proc_Decl, Result_Obj_Type_Decl);
- Last_Decl := Result_Obj_Type_Decl;
- end if;
-
- -- Create the result obj declaration
-
- -- Generate:
- --
- -- Result_Object_For_Postcond : Result_Obj_Type;
-
- Result_Obj_Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier
- (Loc, Name_uResult_Object_For_Postcond),
- Object_Definition =>
- New_Occurrence_Of
- (Result_Obj_Type, Loc));
- Set_No_Initialization (Result_Obj_Decl);
- Insert_After_And_Analyze (Last_Decl, Result_Obj_Decl);
- Last_Decl := Result_Obj_Decl;
- end if;
-
- -- Build the Postcond_Enabled flag used to delay evaluation of
- -- postconditions until finalization has been performed when cleanup
- -- actions are present.
-
- -- NOTE: This flag could be made into a predicate since we should be
- -- able at compile time to recognize when finalization and cleanup
- -- actions occur, but in practice this is not possible ???
-
- -- Generate:
- --
- -- Postcond_Enabled : Boolean := True;
-
- Postcond_Enabled_Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier
- (Loc, Name_uPostcond_Enabled),
- Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
- Expression => New_Occurrence_Of (Standard_True, Loc));
- Insert_After_And_Analyze (Last_Decl, Postcond_Enabled_Decl);
- Last_Decl := Postcond_Enabled_Decl;
-
- -- Create a flag to indicate that return has been reached
-
- -- This is necessary for deciding whether to execute _postconditions
- -- during finalization.
-
- -- Generate:
- --
- -- Return_Success_For_Postcond : Boolean := False;
-
- Return_Success_Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier
- (Loc, Name_uReturn_Success_For_Postcond),
- Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
- Expression => New_Occurrence_Of (Standard_False, Loc));
- Insert_After_And_Analyze (Last_Decl, Return_Success_Decl);
- Last_Decl := Return_Success_Decl;
-
- -- Set an explicit End_Label to override the sloc of the implicit
- -- RETURN statement, and prevent it from inheriting the sloc of one
- -- the postconditions: this would cause confusing debug info to be
- -- produced, interfering with coverage-analysis tools.
-
- -- NOTE: Coverage-analysis and static-analysis tools rely on the
- -- postconditions procedure being free of internally generated code
- -- since some of these tools, like CodePeer, treat _postconditions
- -- as original source.
-
- -- Generate:
- --
- -- procedure _postconditions is
- -- begin
- -- [Stmts];
- -- end;
-
- Proc_Bod :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Subprogram_Spec (Proc_Spec),
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- End_Label => Make_Identifier (Loc, Chars (Proc_Id)),
- Statements => Stmts));
- Insert_After_And_Analyze (Last_Decl, Proc_Bod);
-
- end Build_Postconditions_Procedure;
-
----------------------------
-- Process_Contract_Cases --
----------------------------
- procedure Process_Contract_Cases (Stmts : in out List_Id) is
+ procedure Process_Contract_Cases
+ (Stmts : in out List_Id;
+ Decls : List_Id)
+ is
procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
-- Process pragma Contract_Cases for subprogram Subp_Id
Expand_Pragma_Contract_Cases
(CCs => Prag,
Subp_Id => Subp_Id,
- Decls => Declarations (Body_Decl),
+ Decls => Decls,
Stmts => Stmts);
elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
Expand_Pragma_Subprogram_Variant
(Prag => Prag,
Subp_Id => Subp_Id,
- Body_Decls => Declarations (Body_Decl));
+ Body_Decls => Decls);
end if;
end if;
end if;
end Process_Contract_Cases_For;
- pragma Unmodified (Stmts);
- -- Stmts is passed as IN OUT to signal that the list can be updated,
- -- even if the corresponding integer value representing the list does
- -- not change.
-
-- Start of processing for Process_Contract_Cases
begin
-- Process_Preconditions --
---------------------------
- procedure Process_Preconditions is
+ procedure Process_Preconditions (Decls : in out List_Id) is
Insert_Node : Node_Id := Empty;
-- The insertion node after which all pragma Check equivalents are
-- inserted.
- function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
- -- Determine whether arbitrary declaration Decl denotes a renaming of
- -- a discriminant or protection field _object.
-
procedure Prepend_To_Decls (Item : Node_Id);
-- Prepend a single item to the declarations of the subprogram body
-- Collect all preconditions of subprogram Subp_Id and prepend their
-- pragma Check equivalents to the declarations of the body.
- --------------------------
- -- Is_Prologue_Renaming --
- --------------------------
-
- function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
- Nam : Node_Id;
- Obj : Entity_Id;
- Pref : Node_Id;
- Sel : Node_Id;
-
- begin
- if Nkind (Decl) = N_Object_Renaming_Declaration then
- Obj := Defining_Entity (Decl);
- Nam := Name (Decl);
-
- if Nkind (Nam) = N_Selected_Component then
- Pref := Prefix (Nam);
- Sel := Selector_Name (Nam);
-
- -- A discriminant renaming appears as
- -- Discr : constant ... := Prefix.Discr;
-
- if Ekind (Obj) = E_Constant
- and then Is_Entity_Name (Sel)
- and then Present (Entity (Sel))
- and then Ekind (Entity (Sel)) = E_Discriminant
- then
- return True;
-
- -- A protection field renaming appears as
- -- Prot : ... := _object._object;
-
- -- A renamed private component is just a component of
- -- _object, with an arbitrary name.
-
- elsif Ekind (Obj) in E_Variable | E_Constant
- and then Nkind (Pref) = N_Identifier
- and then Chars (Pref) = Name_uObject
- and then Nkind (Sel) = N_Identifier
- then
- return True;
- end if;
- end if;
- end if;
-
- return False;
- end Is_Prologue_Renaming;
-
----------------------
-- Prepend_To_Decls --
----------------------
procedure Prepend_To_Decls (Item : Node_Id) is
- Decls : List_Id;
-
begin
- Decls := Declarations (Body_Decl);
-
-- Ensure that the body has a declarative list
if No (Decls) then
else
Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+ Prepend_To_Decls (Check_Prag);
- if Present (Insert_Node) then
- Insert_After (Insert_Node, Check_Prag);
- else
- Prepend_To_Decls (Check_Prag);
- end if;
-
- Analyze (Check_Prag);
end if;
end Prepend_Pragma_To_Decls;
-- Local variables
- Decls : constant List_Id := Declarations (Body_Decl);
- Decl : Node_Id;
+ Body_Decls : constant List_Id := Declarations (Body_Decl);
+ Decl : Node_Id;
+ Next_Decl : Node_Id;
-- Start of processing for Process_Preconditions
begin
-- Find the proper insertion point for all pragma Check equivalents
- if Present (Decls) then
- Decl := First (Decls);
+ if Present (Body_Decls) then
+ Decl := First (Body_Decls);
while Present (Decl) loop
-- First source declaration terminates the search, because all
-- <preconditions from body>
Process_Preconditions_For (Body_Id);
+
+ -- Move the generated entry-call prologue renamings into the
+ -- outer declarations for use in the preconditions.
+
+ Decl := First (Body_Decls);
+ while Present (Decl) and then Present (Insert_Node) loop
+ Next_Decl := Next (Decl);
+ Remove (Decl);
+ Prepend_To_Decls (Decl);
+
+ exit when Decl = Insert_Node;
+ Decl := Next_Decl;
+ end loop;
end if;
if Present (Spec_Id) then
Restore_Scope : Boolean := False;
Result : Entity_Id;
Stmts : List_Id := No_List;
+ Decls : List_Id := New_List;
Subp_Id : Entity_Id;
-- Start of processing for Expand_Subprogram_Contract
-- pragmas to verify the contract assertions of the spec and body in a
-- particular order. The order is as follows:
- -- function Example (...) return ... is
- -- procedure _Postconditions (...) is
+ -- function Original_Code (...) return ... is
+ -- <prologue renamings>
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+ -- <contract case conditions>
+
+ -- function _wrapped_statements (...) return ... is
+ -- <source declarations>
-- begin
+ -- <source statements>
+ -- end _wrapped_statements;
+
+ -- begin
+ -- return
+ -- Result : ... := _wrapped_statements
+ -- do
-- <refined postconditions from body>
-- <postconditions from body>
-- <postconditions from spec>
-- <inherited postconditions>
-- <contract case consequences>
-- <invariant check of function result>
- -- <invariant and predicate checks of parameters>
- -- end _Postconditions;
-
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
- -- <contract case conditions>
-
- -- <source declarations>
- -- begin
- -- <source statements>
-
- -- _Preconditions (Result);
- -- return Result;
- -- end Example;
-
- -- Routine _Postconditions holds all contract assertions that must be
- -- verified on exit from the related subprogram.
+ -- <invariant and predicate checks of parameters
+ -- return Result;
+ -- end return;
+ -- end Original_Code;
-- Step 1: augment contracts list with postconditions associated with
-- Stable_Properties and Stable_Properties'Class aspects. This must
-- processing of pragma Contract_Cases because the pragma prepends items
-- to the body declarations.
- Process_Preconditions;
+ Process_Preconditions (Decls);
-- Step 3: Handle all postconditions. This action must come before the
-- processing of pragma Contract_Cases because the pragma appends items
-- the processing of invariants and predicates because those append
-- items to list Stmts.
- Process_Contract_Cases (Stmts);
+ Process_Contract_Cases (Stmts, Decls);
-- Step 5: Apply invariant and predicate checks on a function result and
-- all formals. The resulting checks are accumulated in list Stmts.
Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
- -- Step 6: Construct procedure _Postconditions
+ -- Step 6: Construct subprogram _wrapped_statements
+
+ -- When no statements are present we still need to insert contract
+ -- related declarations.
+
+ if No (Stmts) then
+ Prepend_List_To (Declarations (Body_Decl), Decls);
+
+ -- Otherwise, we need a wrapper
- Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
+ else
+ Build_Subprogram_Contract_Wrapper (Body_Id, Stmts, Decls, Result);
+ end if;
if Restore_Scope then
End_Scope;
Freeze_Contracts;
end Freeze_Previous_Contracts;
- --------------------------
- -- Get_Postcond_Enabled --
- --------------------------
-
- function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id is
- Decl : Node_Id;
- begin
- Decl :=
- Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
- while Present (Decl) loop
-
- if Nkind (Decl) = N_Object_Declaration
- and then Chars (Defining_Identifier (Decl))
- = Name_uPostcond_Enabled
- then
- return Defining_Identifier (Decl);
- end if;
-
- Next (Decl);
- end loop;
-
- return Empty;
- end Get_Postcond_Enabled;
-
- ------------------------------------
- -- Get_Result_Object_For_Postcond --
- ------------------------------------
-
- function Get_Result_Object_For_Postcond
- (Subp : Entity_Id) return Entity_Id
- is
- Decl : Node_Id;
- begin
- Decl :=
- Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
- while Present (Decl) loop
-
- if Nkind (Decl) = N_Object_Declaration
- and then Chars (Defining_Identifier (Decl))
- = Name_uResult_Object_For_Postcond
- then
- return Defining_Identifier (Decl);
- end if;
-
- Next (Decl);
- end loop;
-
- return Empty;
- end Get_Result_Object_For_Postcond;
-
- -------------------------------------
- -- Get_Return_Success_For_Postcond --
- -------------------------------------
-
- function Get_Return_Success_For_Postcond (Subp : Entity_Id) return Entity_Id
- is
- Decl : Node_Id;
- begin
- Decl :=
- Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
- while Present (Decl) loop
-
- if Nkind (Decl) = N_Object_Declaration
- and then Chars (Defining_Identifier (Decl))
- = Name_uReturn_Success_For_Postcond
- then
- return Defining_Identifier (Decl);
- end if;
-
- Next (Decl);
- end loop;
-
- return Empty;
- end Get_Return_Success_For_Postcond;
-
---------------------------------
-- Inherit_Subprogram_Contract --
---------------------------------
end if;
end Instantiate_Subprogram_Contract;
+ --------------------------
+ -- Is_Prologue_Renaming --
+ --------------------------
+
+ -- This should be turned into a flag and set during the expansion of
+ -- task and protected types when the renamings get generated ???
+
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
+ Nam : Node_Id;
+ Obj : Entity_Id;
+ Pref : Node_Id;
+ Sel : Node_Id;
+
+ begin
+ if Nkind (Decl) = N_Object_Renaming_Declaration
+ and then not Comes_From_Source (Decl)
+ then
+ Obj := Defining_Entity (Decl);
+ Nam := Name (Decl);
+
+ if Nkind (Nam) = N_Selected_Component then
+ -- Analyze the renaming declaration so we can further examine it
+
+ if not Analyzed (Decl) then
+ Analyze (Decl);
+ end if;
+
+ Pref := Prefix (Nam);
+ Sel := Selector_Name (Nam);
+
+ -- A discriminant renaming appears as
+ -- Discr : constant ... := Prefix.Discr;
+
+ if Ekind (Obj) = E_Constant
+ and then Is_Entity_Name (Sel)
+ and then Present (Entity (Sel))
+ and then Ekind (Entity (Sel)) = E_Discriminant
+ then
+ return True;
+
+ -- A protection field renaming appears as
+ -- Prot : ... := _object._object;
+
+ -- A renamed private component is just a component of
+ -- _object, with an arbitrary name.
+
+ elsif Ekind (Obj) in E_Variable | E_Constant
+ and then Nkind (Pref) = N_Identifier
+ and then Chars (Pref) = Name_uObject
+ and then Nkind (Sel) = N_Identifier
+ then
+ return True;
+ end if;
+ end if;
+ end if;
+
+ return False;
+ end Is_Prologue_Renaming;
+
-----------------------------------
-- Make_Class_Precondition_Subps --
-----------------------------------
procedure Analyze_Contracts (L : List_Id);
-- Analyze the contracts of all eligible constructs found in list L
+ procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id);
+ -- Perform early analysis of pragmas at the top of a given subprogram's
+ -- declarations.
+ --
+ -- The purpose of this is to analyze contract-related pragmas for later
+ -- processing, but also to handle other such pragmas before these
+ -- declarations get moved to an internal wrapper as part of contract
+ -- expansion. For example, pragmas Inline, Ghost, Volatile all need to
+ -- apply directly to the subprogram and not be moved to a wrapper.
+
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of entry or
-- subprogram body Body_Id as if they appeared at the end of a declarative
-- Depends
-- Global
+ procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
+ -- Build the body of a wrapper procedure for an entry or entry family that
+ -- has contract cases, preconditions, or postconditions, and add it to the
+ -- freeze actions of the related synchronized type.
+ --
+ -- The body first verifies the preconditions and case guards of the
+ -- contract cases, then invokes the entry [family], and finally verifies
+ -- the postconditions and the consequences of the contract cases. E denotes
+ -- the entry family. Decl denotes the declaration of the enclosing
+ -- synchronized type.
+
procedure Create_Generic_Contract (Unit : Node_Id);
-- Create a contract node for a generic package, generic subprogram, or a
-- generic body denoted by Unit by collecting all source contract-related
-- denoted by Body_Decl. In addition, freeze the contract of the nearest
-- enclosing package body.
- function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's Postcond_Enabled
- -- object created during the expansion of the subprogram's postconditions.
-
- function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's
- -- Result_Object_For_Postcond object created during the expansion of the
- -- subprogram's postconditions.
-
- function Get_Return_Success_For_Postcond
- (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's
- -- Return_Success_For_Postcond object created during the expansion of the
- -- subprogram's postconditions.
-
procedure Inherit_Subprogram_Contract
(Subp : Entity_Id;
From_Subp : Entity_Id);
-- fully initialized when the full view is frozen.
-- Postconditions_Proc
--- Defined in functions, procedures, entries, and entry families. Refers
--- to the entity of the _Postconditions procedure used to check contract
--- assertions on exit from a subprogram.
+-- Obsolete field which can be removed once CodePeer is fixed ???
-- Predicate_Function (synthesized)
-- Defined in all types. Set for types for which (Has_Predicates is True)
-- Defined in functions and procedures which have been classified as
-- Is_Primitive_Wrapper. Set to the entity being wrapper.
+-- Wrapped_Statements
+-- Defined in functions, procedures, entries, and entry families. Refers
+-- to the entity of the _Wrapped_Statements procedure which gets
+-- generated as part of the expansion of contracts and postconditions
+-- and contains its enclosing subprogram's original source declarations
+-- and statements.
+
-- LSP_Subprogram
-- Defined in subprogram entities. Set on wrappers created to handle
-- inherited class-wide pre/post conditions that call overridden
-- Protected_Body_Subprogram
-- Barrier_Function
-- Elaboration_Entity
- -- Postconditions_Proc
-- Entry_Parameters_Type
-- First_Entity
-- Alias (for entry only. Empty)
-- Protected_Body_Subprogram
-- Next_Inlined_Subprogram
-- Elaboration_Entity (not implicit /=)
- -- Postconditions_Proc (non-generic case only)
-- DT_Position
-- DTC_Entity
-- First_Entity
-- Protected_Body_Subprogram
-- Next_Inlined_Subprogram
-- Elaboration_Entity
- -- Postconditions_Proc (non-generic case only)
-- DT_Position
-- DTC_Entity
-- First_Entity
use Old_Attr_Util.Indirect_Temps;
begin
-- Generating C code we don't need to expand this attribute when
- -- we are analyzing the internally built nested postconditions
+ -- we are analyzing the internally built nested _Wrapped_Statements
-- procedure since it will be expanded inline (and later it will
-- be removed by Expand_N_Subprogram_Body). It this expansion is
-- performed in such case then the compiler generates unreferenced
-- extra temporaries.
if Modify_Tree_For_C
- and then Chars (Current_Scope) = Name_uPostconditions
+ and then Chars (Current_Scope) = Name_uWrapped_Statements
then
return;
end if;
- -- Climb the parent chain looking for subprogram _Postconditions
+ -- Climb the parent chain looking for subprogram _Wrapped_Statements
Subp := N;
while Present (Subp) loop
exit when Nkind (Subp) = N_Subprogram_Body
- and then Chars (Defining_Entity (Subp)) = Name_uPostconditions;
+ and then Chars (Defining_Entity (Subp))
+ = Name_uWrapped_Statements;
-- If assertions are disabled, no need to create the declaration
-- that preserves the value. The postcondition pragma in which
Subp := Parent (Subp);
end loop;
+ Subp := Empty;
- -- 'Old can only appear in a postcondition, the generated body of
- -- _Postconditions must be in the tree (or inlined if we are
- -- generating C code).
-
- pragma Assert
- (Present (Subp)
- or else (Modify_Tree_For_C and then In_Inlined_Body));
+ -- 'Old can only appear in the case where local contract-related
+ -- wrapper has been generated with the purpose of wrapping the
+ -- original declarations and statements.
Temp := Make_Temporary (Loc, 'T', Pref);
-- No need to push the scope when generating C code since the
-- _Postcondition procedure has been inlined.
- else pragma Assert (Modify_Tree_For_C);
- pragma Assert (In_Inlined_Body);
+ else
null;
end if;
if Present (Subp) then
Ins_Nod := Subp;
- -- Generating C, the postcondition procedure has been inlined and the
- -- temporary is added before the first declaration of the enclosing
- -- subprogram.
+ -- General case where the postcondtion checks occur after the call
+ -- to _Wrapped_Statements.
- else pragma Assert (Modify_Tree_For_C);
+ else
Ins_Nod := N;
while Nkind (Ins_Nod) /= N_Subprogram_Body loop
Ins_Nod := Parent (Ins_Nod);
end loop;
- Ins_Nod := First (Declarations (Ins_Nod));
+ if Present (Corresponding_Spec (Ins_Nod))
+ and then Present
+ (Wrapped_Statements (Corresponding_Spec (Ins_Nod)))
+ then
+ Ins_Nod := Last (Declarations (Ins_Nod));
+ else
+ Ins_Nod := First (Declarations (Ins_Nod));
+ end if;
end if;
if Eligible_For_Conditional_Evaluation (N) then
-- unconditionally) or an evaluation statement (which is
-- to be executed conditionally).
- -------------------------------
- -- Append_For_Indirect_Temp --
- -------------------------------
+ ------------------------------
+ -- Append_For_Indirect_Temp --
+ ------------------------------
procedure Append_For_Indirect_Temp
(N : Node_Id; Is_Eval_Stmt : Boolean)
Declare_Indirect_Temporary
(Attr_Prefix => Pref, Indirect_Temp => Temp);
- Insert_Before_And_Analyze (
+ Insert_After_And_Analyze (
Ins_Nod,
Make_If_Statement
(Sloc => Loc,
with Atree; use Atree;
with Aspects; use Aspects;
with Checks; use Checks;
-with Contracts; use Contracts;
with Debug; use Debug;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
| N_Function_Call
| N_Procedure_Call_Statement);
- -- Check that this is not the call in the body of the wrapper
+ -- Check that this is not the call in the body of the access
+ -- subprogram wrapper or the postconditions wrapper.
if Must_Rewrite_Indirect_Call
and then (not Is_Overloadable (Current_Scope)
- or else not Is_Access_Subprogram_Wrapper (Current_Scope))
+ or else not (Is_Access_Subprogram_Wrapper (Current_Scope)
+ or else
+ (Chars (Current_Scope) = Name_uWrapped_Statements
+ and then Is_Access_Subprogram_Wrapper
+ (Scope (Current_Scope)))))
then
declare
Loc : constant Source_Ptr := Sloc (N);
then
Must_Inline := not In_Extended_Main_Source_Unit (Subp);
- -- Inline calls to _postconditions when generating C code
+ -- Inline calls to _Wrapped_Statements when generating C
elsif Modify_Tree_For_C
and then In_Same_Extended_Unit (Sloc (Bod), Loc)
- and then Chars (Name (Call_Node)) = Name_uPostconditions
+ and then Chars (Name (Call_Node))
+ = Name_uWrapped_Statements
then
Must_Inline := True;
end if;
Append_To (Stmts, Stmt);
Set_Analyzed (Stmt);
- -- Call the _Postconditions procedure if the related subprogram
- -- has contract assertions that need to be verified on exit.
-
- -- Also, mark the successful return to signal that postconditions
- -- need to be evaluated when finalization occurs by setting
- -- Return_Success_For_Postcond to be True.
-
- if Ekind (Spec_Id) = E_Procedure
- and then Present (Postconditions_Proc (Spec_Id))
- then
- -- Generate:
- --
- -- Return_Success_For_Postcond := True;
- -- if Postcond_Enabled then
- -- _postconditions;
- -- end if;
-
- Insert_Action (Stmt,
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Return_Success_For_Postcond (Spec_Id), Loc),
- Expression => New_Occurrence_Of (Standard_True, Loc)));
-
- -- Wrap the call to _postconditions within a test of the
- -- Postcond_Enabled flag to delay postcondition evaluation
- -- until after finalization when required.
-
- Insert_Action (Stmt,
- Make_If_Statement (Loc,
- Condition =>
- New_Occurrence_Of (Get_Postcond_Enabled (Spec_Id), Loc),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postconditions_Proc (Spec_Id), Loc)))));
- end if;
-
-- Ada 2022 (AI12-0279): append the call to 'Yield unless this is
-- a generic subprogram (since in such case it will be added to
-- the instantiations).
Lab_Node : Node_Id;
begin
- -- Call the _Postconditions procedure if the related subprogram has
- -- contract assertions that need to be verified on exit.
-
- -- Also, mark the successful return to signal that postconditions need
- -- to be evaluated when finalization occurs.
-
- if Ekind (Scope_Id) in E_Entry | E_Entry_Family | E_Procedure
- and then Present (Postconditions_Proc (Scope_Id))
- then
- -- Generate:
- --
- -- Return_Success_For_Postcond := True;
- -- if Postcond_Enabled then
- -- _postconditions;
- -- end if;
-
- Insert_Action (N,
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Return_Success_For_Postcond (Scope_Id), Loc),
- Expression => New_Occurrence_Of (Standard_True, Loc)));
-
- -- Wrap the call to _postconditions within a test of the
- -- Postcond_Enabled flag to delay postcondition evaluation until
- -- after finalization when required.
-
- Insert_Action (N,
- Make_If_Statement (Loc,
- Condition =>
- New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postconditions_Proc (Scope_Id), Loc)))));
- end if;
-
-- Ada 2022 (AI12-0279)
if Has_Yield_Aspect (Scope_Id)
end;
end if;
- -- Call the _Postconditions procedure if the related function has
- -- contract assertions that need to be verified on exit.
-
- if Ekind (Scope_Id) = E_Function
- and then Present (Postconditions_Proc (Scope_Id))
- then
- -- In the case of discriminated objects, we have created a
- -- constrained subtype above, and used the underlying type. This
- -- transformation is post-analysis and harmless, except that now the
- -- call to the post-condition will be analyzed and the type kinds
- -- have to match.
-
- if Nkind (Exp) = N_Unchecked_Type_Conversion
- and then Is_Private_Type (R_Type) /= Is_Private_Type (Etype (Exp))
- then
- Rewrite (Exp, Expression (Relocate_Node (Exp)));
- end if;
-
- -- We are going to reference the returned value twice in this case,
- -- once in the call to _Postconditions, and once in the actual return
- -- statement, but we can't have side effects happening twice.
-
- Force_Evaluation (Exp, Mode => Strict);
-
- -- Save the return value or a pointer to the return value since we
- -- may need to call postconditions after finalization when cleanup
- -- actions are present.
-
- -- Generate:
- --
- -- Result_Object_For_Postcond := [Exp]'Unrestricted_Access;
-
- Insert_Action (Exp,
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Result_Object_For_Postcond (Scope_Id), Loc),
- Expression =>
- (if Is_Elementary_Type (Etype (R_Type)) then
- New_Copy_Tree (Exp)
- else
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Unrestricted_Access,
- Prefix => New_Copy_Tree (Exp)))));
-
- -- Mark the successful return to signal that postconditions need to
- -- be evaluated when finalization occurs.
-
- -- Generate:
- --
- -- Return_Success_For_Postcond := True;
- -- if Postcond_Enabled then
- -- _Postconditions ([exp]);
- -- end if;
-
- Insert_Action (Exp,
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Return_Success_For_Postcond (Scope_Id), Loc),
- Expression => New_Occurrence_Of (Standard_True, Loc)));
-
- -- Wrap the call to _postconditions within a test of the
- -- Postcond_Enabled flag to delay postcondition evaluation until
- -- after finalization when required.
-
- Insert_Action (Exp,
- Make_If_Statement (Loc,
- Condition =>
- New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postconditions_Proc (Scope_Id), Loc),
- Parameter_Associations => New_List (New_Copy_Tree (Exp))))));
- end if;
-
-- Ada 2005 (AI-251): If this return statement corresponds with an
-- simple return statement associated with an extended return statement
-- and the type of the returned object is an interface then generate an
-- - transient scopes
with Atree; use Atree;
-with Contracts; use Contracts;
with Debug; use Debug;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
-- such as for task termination. Fin_Id is the finalizer declaration
-- entity.
- procedure Build_Finalizer_Helper
- (N : Node_Id;
- Clean_Stmts : List_Id;
- Mark_Id : Entity_Id;
- Top_Decls : List_Id;
- Defer_Abort : Boolean;
- Fin_Id : out Entity_Id;
- Finalize_Old_Only : Boolean);
- -- An internal routine which does all of the heavy lifting on behalf of
- -- Build_Finalizer.
-
procedure Build_Finalizer_Call (N : Node_Id; Fin_Id : Entity_Id);
-- N is a construct that contains a handled sequence of statements, Fin_Id
-- is the entity of a finalizer. Create an At_End handler that covers the
end;
end Build_Finalization_Master;
- ----------------------------
- -- Build_Finalizer_Helper --
- ----------------------------
+ ---------------------
+ -- Build_Finalizer --
+ ---------------------
- procedure Build_Finalizer_Helper
+ procedure Build_Finalizer
(N : Node_Id;
Clean_Stmts : List_Id;
Mark_Id : Entity_Id;
Top_Decls : List_Id;
Defer_Abort : Boolean;
- Fin_Id : out Entity_Id;
- Finalize_Old_Only : Boolean)
+ Fin_Id : out Entity_Id)
is
Acts_As_Clean : constant Boolean :=
Present (Mark_Id)
-- there will need to be multiple finalization routines in the
-- same scope. See Build_Finalizer for details.
- if Finalize_Old_Only then
- Fin_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Name_uFinalizer_Old));
- else
- Fin_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Name_uFinalizer));
- end if;
+ Fin_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Name_uFinalizer));
-- The visibility semantics of AT_END handlers force a strange
-- separation of spec and body for stack-related finalizers:
Decl := Last_Non_Pragma (Decls);
while Present (Decl) loop
- -- Depending on the value of flag Finalize_Old_Only we determine
- -- which objects get finalized as part of the current finalizer
- -- being built.
-
- -- When True, only temporaries capturing the value of attribute
- -- 'Old are finalized and all other cases are ignored.
-
- -- When False, temporary objects used to capture the value of 'Old
- -- are ignored and all others are considered.
-
- if Finalize_Old_Only
- xor (Nkind (Decl) = N_Object_Declaration
- and then Stores_Attribute_Old_Prefix
- (Defining_Identifier (Decl)))
- then
- null;
-
-- Library-level tagged types
- elsif Nkind (Decl) = N_Full_Type_Declaration then
+ if Nkind (Decl) = N_Full_Type_Declaration then
Typ := Defining_Identifier (Decl);
-- Ignored Ghost types do not need any cleanup actions because
New_Occurrence_Of (DT_Ptr, Loc))));
end Process_Tagged_Type_Declaration;
- -- Start of processing for Build_Finalizer_Helper
+ -- Start of processing for Build_Finalizer
begin
Fin_Id := Empty;
if Acts_As_Clean or Has_Ctrl_Objs or Has_Tagged_Types then
Create_Finalizer;
end if;
- end Build_Finalizer_Helper;
+ end Build_Finalizer;
--------------------------
-- Build_Finalizer_Call --
end Build_Finalizer_Call;
---------------------
- -- Build_Finalizer --
- ---------------------
-
- procedure Build_Finalizer
- (N : Node_Id;
- Clean_Stmts : List_Id;
- Mark_Id : Entity_Id;
- Top_Decls : List_Id;
- Defer_Abort : Boolean;
- Fin_Id : out Entity_Id)
- is
- Def_Ent : constant Entity_Id := Unique_Defining_Entity (N);
- Loc : constant Source_Ptr := Sloc (N);
-
- -- Declarations used for the creation of _finalization_controller
-
- Fin_Old_Id : Entity_Id := Empty;
- Fin_Controller_Id : Entity_Id := Empty;
- Fin_Controller_Decls : List_Id;
- Fin_Controller_Stmts : List_Id;
- Fin_Controller_Body : Node_Id := Empty;
- Fin_Controller_Spec : Node_Id := Empty;
- Postconditions_Call : Node_Id := Empty;
-
- -- Defining identifiers for local objects used to store exception info
-
- Raised_Post_Exception_Id : Entity_Id := Empty;
- Raised_Finalization_Exception_Id : Entity_Id := Empty;
- Saved_Exception_Id : Entity_Id := Empty;
-
- -- Start of processing for Build_Finalizer
-
- begin
- -- Create the general finalization routine
-
- Build_Finalizer_Helper
- (N => N,
- Clean_Stmts => Clean_Stmts,
- Mark_Id => Mark_Id,
- Top_Decls => Top_Decls,
- Defer_Abort => Defer_Abort,
- Fin_Id => Fin_Id,
- Finalize_Old_Only => False);
-
- -- When postconditions are present, expansion gets much more complicated
- -- due to both the fact that they must be called after finalization and
- -- that finalization of 'Old objects must occur after the postconditions
- -- get checked.
-
- -- Additionally, exceptions between general finalization and 'Old
- -- finalization must be propagated correctly and exceptions which happen
- -- during _postconditions need to be saved and reraised after
- -- finalization of 'Old objects.
-
- -- Generate:
- --
- -- Postcond_Enabled := False;
- --
- -- procedure _finalization_controller is
- --
- -- -- Exception capturing and tracking
- --
- -- Saved_Exception : Exception_Occurrence;
- -- Raised_Post_Exception : Boolean := False;
- -- Raised_Finalization_Exception : Boolean := False;
- --
- -- -- Start of processing for _finalization_controller
- --
- -- begin
- -- -- Perform general finalization
- --
- -- begin
- -- _finalizer;
- -- exception
- -- when others =>
- -- -- Save the exception
- --
- -- Raised_Finalization_Exception := True;
- -- Save_Occurrence
- -- (Saved_Exception, Get_Current_Excep.all);
- -- end;
- --
- -- -- Perform postcondition checks after general finalization, but
- -- -- before finalization of 'Old related objects.
- --
- -- if not Raised_Finalization_Exception
- -- and then Return_Success_For_Postcond
- -- then
- -- begin
- -- -- Re-enable postconditions and check them
- --
- -- Postcond_Enabled := True;
- -- _postconditions [(Result_Obj_For_Postcond[.all])];
- -- exception
- -- when others =>
- -- -- Save the exception
- --
- -- Raised_Post_Exception := True;
- -- Save_Occurrence
- -- (Saved_Exception, Get_Current_Excep.all);
- -- end;
- -- end if;
- --
- -- -- Finally finalize 'Old related objects
- --
- -- begin
- -- _finalizer_old;
- -- exception
- -- when others =>
- -- -- Reraise the previous finalization error if there is
- -- -- one.
- --
- -- if Raised_Finalization_Exception then
- -- Reraise_Occurrence (Saved_Exception);
- -- end if;
- --
- -- -- Otherwise, reraise the current one
- --
- -- raise;
- -- end;
- --
- -- -- Reraise any saved exception
- --
- -- if Raised_Finalization_Exception
- -- or else Raised_Post_Exception
- -- then
- -- Reraise_Occurrence (Saved_Exception);
- -- end if;
- -- end _finalization_controller;
-
- if Nkind (N) = N_Subprogram_Body
- and then Present (Postconditions_Proc (Def_Ent))
- then
- Fin_Controller_Stmts := New_List;
- Fin_Controller_Decls := New_List;
-
- -- Build the 'Old finalizer
-
- Build_Finalizer_Helper
- (N => N,
- Clean_Stmts => Empty_List,
- Mark_Id => Mark_Id,
- Top_Decls => Top_Decls,
- Defer_Abort => Defer_Abort,
- Fin_Id => Fin_Old_Id,
- Finalize_Old_Only => True);
-
- -- Create local declarations for _finalization_controller needed for
- -- saving exceptions.
- --
- -- Generate:
- --
- -- Saved_Exception : Exception_Occurrence;
- -- Raised_Post_Exception : Boolean := False;
- -- Raised_Finalization_Exception : Boolean := False;
-
- Saved_Exception_Id := Make_Temporary (Loc, 'S');
- Raised_Post_Exception_Id := Make_Temporary (Loc, 'P');
- Raised_Finalization_Exception_Id := Make_Temporary (Loc, 'F');
-
- Append_List_To (Fin_Controller_Decls, New_List (
- Make_Object_Declaration (Loc,
- Defining_Identifier => Saved_Exception_Id,
- Object_Definition =>
- New_Occurrence_Of (RTE (RE_Exception_Occurrence), Loc)),
- Make_Object_Declaration (Loc,
- Defining_Identifier => Raised_Post_Exception_Id,
- Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
- Expression => New_Occurrence_Of (Standard_False, Loc)),
- Make_Object_Declaration (Loc,
- Defining_Identifier => Raised_Finalization_Exception_Id,
- Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
- Expression => New_Occurrence_Of (Standard_False, Loc))));
-
- -- Call _finalizer and save any exceptions which occur
-
- -- Generate:
- --
- -- begin
- -- _finalizer;
- -- exception
- -- when others =>
- -- Raised_Finalization_Exception := True;
- -- Save_Occurrence
- -- (Saved_Exception, Get_Current_Excep.all);
- -- end;
-
- if Present (Fin_Id) then
- Append_To (Fin_Controller_Stmts,
- Make_Block_Statement (Loc,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Fin_Id, Loc))),
- Exception_Handlers => New_List (
- Make_Exception_Handler (Loc,
- Exception_Choices => New_List (
- Make_Others_Choice (Loc)),
- Statements => New_List (
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Raised_Finalization_Exception_Id, Loc),
- Expression =>
- New_Occurrence_Of (Standard_True, Loc)),
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (RTE (RE_Save_Occurrence), Loc),
- Parameter_Associations => New_List (
- New_Occurrence_Of
- (Saved_Exception_Id, Loc),
- Make_Explicit_Dereference (Loc,
- Prefix =>
- Make_Function_Call (Loc,
- Name =>
- Make_Explicit_Dereference (Loc,
- Prefix =>
- New_Occurrence_Of
- (RTE (RE_Get_Current_Excep),
- Loc))))))))))));
- end if;
-
- -- Create the call to postconditions based on the kind of the current
- -- subprogram, and the type of the Result_Obj_For_Postcond.
-
- -- Generate:
- --
- -- _postconditions (Result_Obj_For_Postcond[.all]);
- --
- -- or
- --
- -- _postconditions;
-
- if Ekind (Def_Ent) = E_Procedure then
- Postconditions_Call :=
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postconditions_Proc (Def_Ent), Loc));
- else
- Postconditions_Call :=
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postconditions_Proc (Def_Ent), Loc),
- Parameter_Associations => New_List (
- (if Is_Elementary_Type (Etype (Def_Ent)) then
- New_Occurrence_Of
- (Get_Result_Object_For_Postcond
- (Def_Ent), Loc)
- else
- Make_Explicit_Dereference (Loc,
- New_Occurrence_Of
- (Get_Result_Object_For_Postcond
- (Def_Ent), Loc)))));
- end if;
-
- -- Call _postconditions when no general finalization exceptions have
- -- occurred taking care to enable the postconditions and save any
- -- exception occurrences.
-
- -- Generate:
- --
- -- if not Raised_Finalization_Exception
- -- and then Return_Success_For_Postcond
- -- then
- -- begin
- -- Postcond_Enabled := True;
- -- _postconditions [(Result_Obj_For_Postcond[.all])];
- -- exception
- -- when others =>
- -- Raised_Post_Exception := True;
- -- Save_Occurrence
- -- (Saved_Exception, Get_Current_Excep.all);
- -- end;
- -- end if;
-
- Append_To (Fin_Controller_Stmts,
- Make_If_Statement (Loc,
- Condition =>
- Make_And_Then (Loc,
- Left_Opnd =>
- Make_Op_Not (Loc,
- Right_Opnd =>
- New_Occurrence_Of
- (Raised_Finalization_Exception_Id, Loc)),
- Right_Opnd =>
- New_Occurrence_Of
- (Get_Return_Success_For_Postcond (Def_Ent), Loc)),
- Then_Statements => New_List (
- Make_Block_Statement (Loc,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Postcond_Enabled (Def_Ent), Loc),
- Expression =>
- New_Occurrence_Of
- (Standard_True, Loc)),
- Postconditions_Call),
- Exception_Handlers => New_List (
- Make_Exception_Handler (Loc,
- Exception_Choices => New_List (
- Make_Others_Choice (Loc)),
- Statements => New_List (
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Raised_Post_Exception_Id, Loc),
- Expression =>
- New_Occurrence_Of (Standard_True, Loc)),
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (RTE (RE_Save_Occurrence), Loc),
- Parameter_Associations => New_List (
- New_Occurrence_Of
- (Saved_Exception_Id, Loc),
- Make_Explicit_Dereference (Loc,
- Prefix =>
- Make_Function_Call (Loc,
- Name =>
- Make_Explicit_Dereference (Loc,
- Prefix =>
- New_Occurrence_Of
- (RTE (RE_Get_Current_Excep),
- Loc))))))))))))));
-
- -- Call _finalizer_old and reraise any exception that occurred during
- -- initial finalization within the exception handler. Otherwise,
- -- propagate the current exception.
-
- -- Generate:
- --
- -- begin
- -- _finalizer_old;
- -- exception
- -- when others =>
- -- if Raised_Finalization_Exception then
- -- Reraise_Occurrence (Saved_Exception);
- -- end if;
- -- raise;
- -- end;
-
- if Present (Fin_Old_Id) then
- Append_To (Fin_Controller_Stmts,
- Make_Block_Statement (Loc,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Fin_Old_Id, Loc))),
- Exception_Handlers => New_List (
- Make_Exception_Handler (Loc,
- Exception_Choices => New_List (
- Make_Others_Choice (Loc)),
- Statements => New_List (
- Make_If_Statement (Loc,
- Condition =>
- New_Occurrence_Of
- (Raised_Finalization_Exception_Id, Loc),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (RTE (RE_Reraise_Occurrence), Loc),
- Parameter_Associations => New_List (
- New_Occurrence_Of
- (Saved_Exception_Id, Loc))))),
- Make_Raise_Statement (Loc)))))));
- end if;
-
- -- Once finalization is complete reraise any pending exceptions
-
- -- Generate:
- --
- -- if Raised_Post_Exception
- -- or else Raised_Finalization_Exception
- -- then
- -- Reraise_Occurrence (Saved_Exception);
- -- end if;
-
- Append_To (Fin_Controller_Stmts,
- Make_If_Statement (Loc,
- Condition =>
- Make_Or_Else (Loc,
- Left_Opnd =>
- New_Occurrence_Of
- (Raised_Post_Exception_Id, Loc),
- Right_Opnd =>
- New_Occurrence_Of
- (Raised_Finalization_Exception_Id, Loc)),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of (RTE (RE_Reraise_Occurrence), Loc),
- Parameter_Associations => New_List (
- New_Occurrence_Of
- (Saved_Exception_Id, Loc))))));
-
- -- Make the finalization controller subprogram body and declaration.
-
- -- Generate:
- -- procedure _finalization_controller;
- --
- -- procedure _finalization_controller is
- -- begin
- -- [Fin_Controller_Stmts];
- -- end;
-
- Fin_Controller_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Name_uFinalization_Controller));
-
- Fin_Controller_Spec :=
- Make_Subprogram_Declaration (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Fin_Controller_Id));
-
- Fin_Controller_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Fin_Controller_Id))),
- Declarations => Fin_Controller_Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Fin_Controller_Stmts));
-
- -- Disable _postconditions calls which get generated before return
- -- statements to delay their evaluation until after finalization.
-
- -- This is done by way of the local Postcond_Enabled object which is
- -- initially assigned to True - we then create an assignment within
- -- the subprogram's declaration to make it False and assign it back
- -- to True before _postconditions is called within
- -- _finalization_controller.
-
- -- Generate:
- --
- -- Postcond_Enable := False;
-
- -- Note that we do not disable early evaluation of postconditions
- -- for return types that are unconstrained or have unconstrained
- -- elements since the temporary result object could get allocated on
- -- the stack and be out of scope at the point where we perform late
- -- evaluation of postconditions - leading to uninitialized memory
- -- reads.
-
- -- This disabling of early evaluation can lead to incorrect run-time
- -- semantics where functions with unconstrained elements will
- -- have their corresponding postconditions evaluated before
- -- finalization. The proper solution here is to generate a wrapper
- -- to capture the result instead of using multiple flags and playing
- -- with flags which does not even work in all cases ???
-
- if not Has_Unconstrained_Elements (Etype (Def_Ent))
- or else (Is_Array_Type (Etype (Def_Ent))
- and then not Is_Constrained (Etype (Def_Ent)))
- then
- Append_To (Top_Decls,
- Make_Assignment_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Get_Postcond_Enabled (Def_Ent), Loc),
- Expression =>
- New_Occurrence_Of
- (Standard_False, Loc)));
- end if;
-
- -- Add the subprogram to the list of declarations an analyze it
-
- Append_To (Top_Decls, Fin_Controller_Spec);
- Analyze (Fin_Controller_Spec);
- Insert_After (Fin_Controller_Spec, Fin_Controller_Body);
- Analyze (Fin_Controller_Body, Suppress => All_Checks);
-
- -- Return the finalization controller as the result Fin_Id
-
- Fin_Id := Fin_Controller_Id;
- end if;
- end Build_Finalizer;
-
- ---------------------
-- Build_Late_Proc --
---------------------
with Atree; use Atree;
with Aspects; use Aspects;
with Checks; use Checks;
+with Contracts; use Contracts;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
-- Build a specification for a function implementing the protected entry
-- barrier of the specified entry body.
- procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
- -- Build the body of a wrapper procedure for an entry or entry family that
- -- has contract cases, preconditions, or postconditions. The body gathers
- -- the executable contract items and expands them in the usual way, and
- -- performs the entry call itself. This way preconditions are evaluated
- -- before the call is queued. E is the entry in question, and Decl is the
- -- enclosing synchronized type declaration at whose freeze point the
- -- generated body is analyzed.
-
function Build_Corresponding_Record
(N : Node_Id;
Ctyp : Entity_Id;
Set_Master_Id (Typ, Master_Id);
end Build_Class_Wide_Master;
- ----------------------------
- -- Build_Contract_Wrapper --
- ----------------------------
-
- procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
- Conc_Typ : constant Entity_Id := Scope (E);
- Loc : constant Source_Ptr := Sloc (E);
-
- procedure Add_Discriminant_Renamings
- (Obj_Id : Entity_Id;
- Decls : List_Id);
- -- Add renaming declarations for all discriminants of concurrent type
- -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
- -- represents the concurrent object.
-
- procedure Add_Matching_Formals
- (Formals : List_Id;
- Actuals : in out List_Id);
- -- Add formal parameters that match those of entry E to list Formals.
- -- The routine also adds matching actuals for the new formals to list
- -- Actuals.
-
- procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
- -- Relocate pragma Prag to list To. The routine creates a new list if
- -- To does not exist.
-
- --------------------------------
- -- Add_Discriminant_Renamings --
- --------------------------------
-
- procedure Add_Discriminant_Renamings
- (Obj_Id : Entity_Id;
- Decls : List_Id)
- is
- Discr : Entity_Id;
-
- begin
- -- Inspect the discriminants of the concurrent type and generate a
- -- renaming for each one.
-
- if Has_Discriminants (Conc_Typ) then
- Discr := First_Discriminant (Conc_Typ);
- while Present (Discr) loop
- Prepend_To (Decls,
- Make_Object_Renaming_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Chars (Discr)),
- Subtype_Mark =>
- New_Occurrence_Of (Etype (Discr), Loc),
- Name =>
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Obj_Id, Loc),
- Selector_Name =>
- Make_Identifier (Loc, Chars (Discr)))));
-
- Next_Discriminant (Discr);
- end loop;
- end if;
- end Add_Discriminant_Renamings;
-
- --------------------------
- -- Add_Matching_Formals --
- --------------------------
-
- procedure Add_Matching_Formals
- (Formals : List_Id;
- Actuals : in out List_Id)
- is
- Formal : Entity_Id;
- New_Formal : Entity_Id;
-
- begin
- -- Inspect the formal parameters of the entry and generate a new
- -- matching formal with the same name for the wrapper. A reference
- -- to the new formal becomes an actual in the entry call.
-
- Formal := First_Formal (E);
- while Present (Formal) loop
- New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
- Append_To (Formals,
- Make_Parameter_Specification (Loc,
- Defining_Identifier => New_Formal,
- In_Present => In_Present (Parent (Formal)),
- Out_Present => Out_Present (Parent (Formal)),
- Parameter_Type =>
- New_Occurrence_Of (Etype (Formal), Loc)));
-
- if No (Actuals) then
- Actuals := New_List;
- end if;
-
- Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
- Next_Formal (Formal);
- end loop;
- end Add_Matching_Formals;
-
- ---------------------
- -- Transfer_Pragma --
- ---------------------
-
- procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
- New_Prag : Node_Id;
-
- begin
- if No (To) then
- To := New_List;
- end if;
-
- New_Prag := Relocate_Node (Prag);
-
- Set_Analyzed (New_Prag, False);
- Append (New_Prag, To);
- end Transfer_Pragma;
-
- -- Local variables
-
- Items : constant Node_Id := Contract (E);
- Actuals : List_Id := No_List;
- Call : Node_Id;
- Call_Nam : Node_Id;
- Decls : List_Id := No_List;
- Formals : List_Id;
- Has_Pragma : Boolean := False;
- Index_Id : Entity_Id;
- Obj_Id : Entity_Id;
- Prag : Node_Id;
- Wrapper_Id : Entity_Id;
-
- -- Start of processing for Build_Contract_Wrapper
-
- begin
- -- This routine generates a specialized wrapper for a protected or task
- -- entry [family] which implements precondition/postcondition semantics.
- -- Preconditions and case guards of contract cases are checked before
- -- the protected action or rendezvous takes place. Postconditions and
- -- consequences of contract cases are checked after the protected action
- -- or rendezvous takes place. The structure of the generated wrapper is
- -- as follows:
-
- -- procedure Wrapper
- -- (Obj_Id : Conc_Typ; -- concurrent object
- -- [Index : Index_Typ;] -- index of entry family
- -- [Formal_1 : ...; -- parameters of original entry
- -- Formal_N : ...])
- -- is
- -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
- -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
-
- -- <precondition checks>
- -- <case guard checks>
-
- -- procedure _Postconditions is
- -- begin
- -- <postcondition checks>
- -- <consequence checks>
- -- end _Postconditions;
-
- -- begin
- -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
- -- _Postconditions;
- -- end Wrapper;
-
- -- Create the wrapper only when the entry has at least one executable
- -- contract item such as contract cases, precondition or postcondition.
-
- if Present (Items) then
-
- -- Inspect the list of pre/postconditions and transfer all available
- -- pragmas to the declarative list of the wrapper.
-
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name_Unmapped (Prag) in Name_Postcondition
- | Name_Precondition
- and then Is_Checked (Prag)
- then
- Has_Pragma := True;
- Transfer_Pragma (Prag, To => Decls);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Inspect the list of test/contract cases and transfer only contract
- -- cases pragmas to the declarative part of the wrapper.
-
- Prag := Contract_Test_Cases (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases
- and then Is_Checked (Prag)
- then
- Has_Pragma := True;
- Transfer_Pragma (Prag, To => Decls);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
-
- -- The entry lacks executable contract items and a wrapper is not needed
-
- if not Has_Pragma then
- return;
- end if;
-
- -- Create the profile of the wrapper. The first formal parameter is the
- -- concurrent object.
-
- Obj_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Conc_Typ), 'A'));
-
- Formals := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Obj_Id,
- Out_Present => True,
- In_Present => True,
- Parameter_Type => New_Occurrence_Of (Conc_Typ, Loc)));
-
- -- Construct the call to the original entry. The call will be gradually
- -- augmented with an optional entry index and extra parameters.
-
- Call_Nam :=
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Obj_Id, Loc),
- Selector_Name => New_Occurrence_Of (E, Loc));
-
- -- When creating a wrapper for an entry family, the second formal is the
- -- entry index.
-
- if Ekind (E) = E_Entry_Family then
- Index_Id := Make_Defining_Identifier (Loc, Name_I);
-
- Append_To (Formals,
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Index_Id,
- Parameter_Type =>
- New_Occurrence_Of (Entry_Index_Type (E), Loc)));
-
- -- The call to the original entry becomes an indexed component to
- -- accommodate the entry index.
-
- Call_Nam :=
- Make_Indexed_Component (Loc,
- Prefix => Call_Nam,
- Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
- end if;
-
- -- Add formal parameters to match those of the entry and build actuals
- -- for the entry call.
-
- Add_Matching_Formals (Formals, Actuals);
-
- Call :=
- Make_Procedure_Call_Statement (Loc,
- Name => Call_Nam,
- Parameter_Associations => Actuals);
-
- -- Add renaming declarations for the discriminants of the enclosing type
- -- as the various contract items may reference them.
-
- Add_Discriminant_Renamings (Obj_Id, Decls);
-
- Wrapper_Id :=
- Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
- Set_Contract_Wrapper (E, Wrapper_Id);
- Set_Is_Entry_Wrapper (Wrapper_Id);
-
- -- The wrapper body is analyzed when the enclosing type is frozen
-
- Append_Freeze_Action (Defining_Entity (Decl),
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Wrapper_Id,
- Parameter_Specifications => Formals),
- Declarations => Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Call))));
- end Build_Contract_Wrapper;
-
--------------------------------
-- Build_Corresponding_Record --
--------------------------------
-- Build a wrapper procedure to handle contract cases, preconditions,
-- and postconditions.
- Build_Contract_Wrapper (Ent_Id, N);
+ Build_Entry_Contract_Wrapper (Ent_Id, N);
-- Create the barrier function
Ent := First_Entity (Tasktyp);
while Present (Ent) loop
if Ekind (Ent) in E_Entry | E_Entry_Family then
- Build_Contract_Wrapper (Ent, N);
+ Build_Entry_Contract_Wrapper (Ent, N);
end if;
Next_Entity (Ent);
Make_Selected_Component (Loc,
Prefix => New_Occurrence_Of (Obj_Ent, Loc),
Selector_Name => Make_Identifier (Loc, Name_uObject)));
+
Add (Decl);
end;
end if;
Make_Selected_Component (Loc,
Prefix => New_Occurrence_Of (Obj_Ent, Loc),
Selector_Name => Make_Identifier (Loc, Chars (D))));
+
Add (Decl);
-- Set debug info needed on this renaming declaration even
Make_Selected_Component (Loc,
Prefix => New_Occurrence_Of (Obj_Ent, Loc),
Selector_Name => Make_Identifier (Loc, Nam)));
+
Add (Decl);
end if;
New_Occurrence_Of (RTE (RE_Assert_Failure),
Loc))))))));
+ Set_Comes_From_Check_Or_Contract (N);
+
-- Case where we call the procedure
else
Name =>
New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
Parameter_Associations => New_List (Relocate_Node (Msg))))));
+
+ Set_Comes_From_Check_Or_Contract (N);
end if;
Analyze (N);
Condition => Cond,
Then_Statements => New_List (Error));
+ Set_Comes_From_Check_Or_Contract (Checks);
+
else
if No (Elsif_Parts (Checks)) then
Set_Elsif_Parts (Checks, New_List);
Condition => New_Occurrence_Of (Flag, Loc),
Then_Statements => Eval_Stmts);
+ Set_Comes_From_Check_Or_Contract (Evals);
+
-- Otherwise generate:
-- elsif Flag then
-- <evaluation statements>
Set (Flag),
Increment (Count)));
+ Set_Comes_From_Check_Or_Contract (If_Stmt);
+
Append_To (Decls, If_Stmt);
Analyze (If_Stmt);
Right_Opnd => Make_Integer_Literal (Loc, 0)),
Then_Statements => CG_Stmts);
+ Set_Comes_From_Check_Or_Contract (CG_Checks);
+
-- Detect a possible failure due to several case guards evaluating to
-- True.
New_Occurrence_Of (Msg_Str, Loc))))))))));
end if;
+ -- Append the checks, but do not analyze them at this point, because
+ -- contracts get potentially expanded as part of a wrapper which gets
+ -- fully analyzed once it is fully formed.
+
Append_To (Decls, CG_Checks);
- Analyze (CG_Checks);
-- Once all case guards are evaluated and checked, evaluate any prefixes
-- of attribute 'Old founds in the selected consequence.
if Present (Old_Evals) then
Append_To (Decls, Old_Evals);
- Analyze (Old_Evals);
end if;
-- Raise Assertion_Error when the corresponding consequence of a case
and then Scope (Test_E) /= Current_Scope
and then Ekind (Test_E) /= E_Constant
then
+ -- Here we deal with the special case of the expansion of
+ -- postconditions. Previously this was handled by the loop below,
+ -- since these postcondition checks got isolated to a separate,
+ -- internally generated, subprogram. Now, however, the postcondition
+ -- checks get contained within their corresponding subprogram
+ -- directly.
+
+ if not Comes_From_Source (N)
+ and then Nkind (N) = N_Pragma
+ and then From_Aspect_Specification (N)
+ and then Is_Valid_Assertion_Kind (Original_Aspect_Pragma_Name (N))
+
+ -- Now, verify the placement of the pragma is within an expanded
+ -- subprogram which contains postcondition expansion - detected
+ -- through the presence of the "Wrapped_Statements" field.
+
+ and then Present (Enclosing_Subprogram (Current_Scope))
+ and then Present (Wrapped_Statements
+ (Enclosing_Subprogram (Current_Scope)))
+ then
+ goto Leave;
+ end if;
+
+ -- Otherwise, loop through scopes checking if an enclosing scope
+ -- comes from source or is a generic.
+
declare
S : Entity_Id;
-- If the parent is a subprogram body, the candidate insertion
-- point is just ahead of it.
- if Nkind (Parent_P) = N_Subprogram_Body
- and then Unique_Defining_Entity (Parent_P) =
- Freeze_Outside_Subp
+ if Nkind (Parent_P) = N_Subprogram_Body
+ and then Unique_Defining_Entity (Parent_P) =
+ Freeze_Outside_Subp
then
P := Parent_P;
exit;
Class_Present,
Classifications,
Cleanup_Actions,
+ Comes_From_Check_Or_Contract,
Comes_From_Extended_Return_Statement,
Compile_Time_Known_Aggregate,
Component_Associations,
Warnings_Off_Used_Unmodified,
Warnings_Off_Used_Unreferenced,
Was_Hidden,
- Wrapped_Entity
+ Wrapped_Entity,
+ Wrapped_Statements
-- End of entity fields.
); -- Opt_Field_Enum
Sm (Thunk_Entity, Node_Id,
Pre => "Is_Thunk (N)"),
Sm (Wrapped_Entity, Node_Id,
- Pre => "Is_Primitive_Wrapper (N)")));
+ Pre => "Is_Primitive_Wrapper (N)"),
+ Sm (Wrapped_Statements, Node_Id)));
Cc (E_Operator, Subprogram_Kind,
-- A predefined operator, appearing in Standard, or an implicitly
Sm (Thunk_Entity, Node_Id,
Pre => "Is_Thunk (N)"),
Sm (Wrapped_Entity, Node_Id,
- Pre => "Is_Primitive_Wrapper (N)")));
+ Pre => "Is_Primitive_Wrapper (N)"),
+ Sm (Wrapped_Statements, Node_Id)));
Cc (E_Abstract_State, Overloadable_Kind,
-- A state abstraction. Used to designate entities introduced by aspect
Sm (Protection_Object, Node_Id),
Sm (Scope_Depth_Value, Unat),
Sm (SPARK_Pragma, Node_Id),
- Sm (SPARK_Pragma_Inherited, Flag)));
+ Sm (SPARK_Pragma_Inherited, Flag),
+ Sm (Wrapped_Statements, Node_Id)));
Cc (E_Entry_Family, Entity_Kind,
-- An entry family, created by an entry family declaration in a
Sm (Renamed_Or_Alias, Node_Id),
Sm (Scope_Depth_Value, Unat),
Sm (SPARK_Pragma, Node_Id),
- Sm (SPARK_Pragma_Inherited, Flag)));
+ Sm (SPARK_Pragma_Inherited, Flag),
+ Sm (Wrapped_Statements, Node_Id)));
Cc (E_Block, Entity_Kind,
-- A block identifier, created by an explicit or implicit label on
Sy (Elsif_Parts, List_Id, Default_No_List),
Sy (Else_Statements, List_Id, Default_No_List),
Sy (End_Span, Unat, Default_Uint_0),
- Sm (From_Conditional_Expression, Flag)));
+ Sm (From_Conditional_Expression, Flag),
+ Sm (Comes_From_Check_Or_Contract, Flag)));
Cc (N_Accept_Alternative, Node_Kind,
(Sy (Accept_Statement, Node_Id),
if Present (Subp_Id) then
- -- The context is the internally built _Postconditions
+ -- The context is the internally built _Wrapped_Statements
-- procedure, which is OK because the real check was done
- -- before expansion activities.
+ -- before contract expansion activities.
- if Chars (Subp_Id) = Name_uPostconditions then
+ if Chars (Subp_Id) = Name_uWrapped_Statements then
return True;
-- The context is the internally built predicate function,
-- but it may still contain references to Ghost entities.
elsif Nkind (Stmt) = N_If_Statement
- and then Nkind (Original_Node (Stmt)) = N_Pragma
- and then Assertion_Expression_Pragma
- (Get_Pragma_Id (Original_Node (Stmt)))
+ and then Comes_From_Check_Or_Contract (Stmt)
then
return True;
end if;
pragma Assert
(Modify_Tree_For_C
and then Is_Subprogram (Enclosing_Subp)
- and then Present (Postconditions_Proc (Enclosing_Subp)));
+ and then Present (Wrapped_Statements (Enclosing_Subp)));
if Ekind (Enclosing_Subp) = E_Function then
if Nkind (First (Parameter_Associations (N))) in
if Modify_Tree_For_C
and then Nkind (N) = N_Procedure_Call_Statement
- and then Chars (Name (N)) = Name_uPostconditions
+ and then Chars (Name (N)) = Name_uWrapped_Statements
then
Declare_Postconditions_Result;
end if;
end if;
end if;
- -- Do not generate references if we are within a postcondition sub-
- -- program, because the reference does not comes from source, and the
- -- preanalysis of the aspect has already created an entry for the ALI
- -- file at the proper source location.
-
- if Chars (Current_Scope) = Name_uPostconditions then
- return;
- end if;
-
-- Never collect references if not in main source unit. However, we omit
-- this test if Typ is 'e' or 'k', since these entries are structural,
-- and it is useful to have them in units that reference packages as
return Is_Predefined_Renaming (Unit);
end In_Predefined_Renaming;
+ ---------
+ -- ipu --
+ ---------
+
+ function ipu (N : Node_Or_Entity_Id) return Boolean is
+ begin
+ return In_Predefined_Unit (N);
+ end ipu;
+
------------------------
-- In_Predefined_Unit --
------------------------
function In_Extended_Main_Source_Unit (Loc : Source_Ptr) return Boolean;
-- Same function as above, but argument is a source pointer
+ function ipu (N : Node_Or_Entity_Id) return Boolean;
+ -- Same as In_Predefined_Unit, but renamed so it can assist debugging.
+ -- Otherwise, there is a disambiguous name conflict in the two versions of
+ -- In_Predefined_Unit which makes it inconvient to set as a breakpoint
+ -- condition.
+
function In_Predefined_Unit (N : Node_Or_Entity_Id) return Boolean;
-- Returns True if the given node or entity appears within the source text
-- of a predefined unit (i.e. within Ada, Interfaces, System or within one
Placement_Error;
end if;
- -- 'Old attribute reference ok in a _Postconditions procedure
+ -- 'Old attribute reference ok in a _Wrapped_Statements procedure
elsif Nkind (Prag) = N_Subprogram_Body
- and then not Comes_From_Source (Prag)
- and then Nkind (Corresponding_Spec (Prag)) = N_Defining_Identifier
- and then Chars (Corresponding_Spec (Prag)) = Name_uPostconditions
+ and then Ekind (Defining_Entity (Prag)) in Subprogram_Kind
+ and then Present (Wrapped_Statements (Defining_Entity (Prag)))
then
null;
if Nkind (Prag) = N_Aspect_Specification then
Subp_Decl := Parent (Prag);
elsif Nkind (Prag) = N_Subprogram_Body then
- declare
- Enclosing_Scope : constant Node_Id :=
- Scope (Corresponding_Spec (Prag));
- begin
- pragma Assert (Postconditions_Proc (Enclosing_Scope)
- = Corresponding_Spec (Prag));
- Subp_Decl := Parent (Parent (Enclosing_Scope));
- end;
+ Subp_Decl := Prag;
else
Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
end if;
+ -- 'Old objects appear in extended return statements as part of
+ -- the expansion of contract wrappers.
+
+ if Nkind (Subp_Decl) = N_Extended_Return_Statement then
+ Subp_Decl := Parent (Parent (Subp_Decl));
+ end if;
+
-- The aspect or pragma where the attribute resides should be
-- associated with a subprogram declaration or a body. If this is not
-- the case, then the aspect or pragma is illegal. Return as analysis
if Modify_Tree_For_C
and then Chars (Spec_Id) = Name_uParent
- and then Chars (Scope (Spec_Id)) = Name_uPostconditions
+ and then Chars (Scope (Spec_Id)) = Name_uWrapped_Statements
then
-- This situation occurs only when analyzing the body-to-inline
if Is_Entry_Wrapper (Spec_Id) then
Legal := True;
- elsif Chars (Spec_Id) = Name_uPostconditions
+ elsif Chars (Spec_Id) = Name_uWrapped_Statements
and then Is_Entry_Wrapper (Scope (Spec_Id))
then
Spec_Id := Scope (Spec_Id);
Error_Attr ("prefix of % attribute must be a function", P);
end if;
- -- Attribute 'Result is part of a _Postconditions procedure. There is
+ -- Attribute 'Result is part of postconditions expansion. There is
-- no need to perform the semantic checks below as they were already
-- verified when the attribute was analyzed in its original context.
-- Instead, rewrite the attribute as a reference to formal parameter
- -- _Result of the _Postconditions procedure.
+ -- _Result of the _Wrapped_Statements procedure.
- if Chars (Spec_Id) = Name_uPostconditions
+ if Chars (Spec_Id) = Name_uWrapped_Statements
or else
(In_Inlined_C_Postcondition
and then Nkind (Parent (Spec_Id)) = N_Block_Statement)
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
-with Snames; use Snames;
with Stand; use Stand;
package body Sem_Ch11 is
-- If the current scope is a subprogram, entry or task body or declare
-- block then this is the right place to check for hanging useless
- -- assignments from the statement sequence. Skip this in the body of a
- -- postcondition, since in that case there are no source references.
+ -- assignments from the statement sequence.
- if (Is_Subprogram_Or_Entry (Current_Scope)
- and then Chars (Current_Scope) /= Name_uPostconditions)
- or else Ekind (Current_Scope) in E_Block | E_Task_Type
+ if Is_Subprogram_Or_Entry (Current_Scope)
+ or else Ekind (Current_Scope) in E_Block | E_Task_Type
then
Warn_On_Useless_Assignments (Current_Scope);
end if;
Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
end if;
- Analyze_Declarations (Declarations (N));
- Check_Completion;
-
- -- Process the contract of the subprogram body after all declarations
- -- have been analyzed. This ensures that any contract-related pragmas
- -- are available through the N_Contract node of the body.
+ -- Process the contract of the subprogram body after analyzing all
+ -- the contract-related pragmas within the declarations.
+ Analyze_Pragmas_In_Declarations (Body_Id);
Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
+ -- Continue on with analyzing the declarations and statements once
+ -- contract expansion is done and we are done expanding contract
+ -- related wrappers.
+
+ Analyze_Declarations (Declarations (N));
+ Check_Completion;
+
Analyze (Handled_Statement_Sequence (N));
Save_Global_References (Original_Node (N));
Conformant : Boolean;
Desig_View : Entity_Id := Empty;
Exch_Views : Elist_Id := No_Elist;
- HSS : Node_Id;
Mask_Types : Elist_Id := No_Elist;
Prot_Typ : Entity_Id := Empty;
Spec_Decl : Node_Id := Empty;
--------------------------
procedure Check_Missing_Return is
+ HSS : constant Node_Id := Handled_Statement_Sequence (N);
+
Id : Entity_Id;
Missing_Ret : Boolean;
-- Move relevant pragmas to the spec
- elsif Pragma_Name_Unmapped (Decl) in Name_Depends
- | Name_Ghost
- | Name_Global
- | Name_Pre
- | Name_Precondition
- | Name_Post
- | Name_Refined_Depends
- | Name_Refined_Global
- | Name_Refined_Post
- | Name_Inline
- | Name_Pure_Function
- | Name_Volatile_Function
+ elsif
+ Pragma_Significant_To_Subprograms
+ (Get_Pragma_Id (Decl))
then
Remove (Decl);
Insert_After (Insert_Nod, Decl);
Analyze_Generic_Subprogram_Body (N, Spec_Id);
if Nkind (N) = N_Subprogram_Body then
- HSS := Handled_Statement_Sequence (N);
Check_Missing_Return;
end if;
end;
end if;
- -- Now we can go on to analyze the body
+ -- Ada 2012 (AI05-0151): Incomplete types coming from a limited context
+ -- may now appear in parameter and result profiles. Since the analysis
+ -- of a subprogram body may use the parameter and result profile of the
+ -- spec, swap any limited views with their non-limited counterpart.
+
+ if Ada_Version >= Ada_2012 and then Present (Spec_Id) then
+ Exch_Views := 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_Subprogram_Body_Or_Stub (N);
+ end if;
+
+ -- Process the contract of the subprogram body after analyzing all the
+ -- contract-related pragmas within the declarations.
+
+ Analyze_Pragmas_In_Declarations (Body_Id);
+ Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
- HSS := Handled_Statement_Sequence (N);
Set_Actual_Subtypes (N, Current_Scope);
-- Add a declaration for the Protection object, renaming declarations
(Sloc (N), Spec_Id, Prot_Typ, N, Declarations (N));
end if;
- -- Ada 2012 (AI05-0151): Incomplete types coming from a limited context
- -- may now appear in parameter and result profiles. Since the analysis
- -- of a subprogram body may use the parameter and result profile of the
- -- spec, swap any limited views with their non-limited counterpart.
-
- if Ada_Version >= Ada_2012 and then Present (Spec_Id) then
- Exch_Views := Exchange_Limited_Views (Spec_Id);
- end if;
-
-- 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.
end;
end if;
- -- Analyze any aspect specifications that appear on the subprogram body
-
- if Has_Aspects (N) then
- Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
- end if;
-
Analyze_Declarations (Declarations (N));
-- Verify that the SPARK_Mode of the body agrees with that of its spec
end if;
end if;
- -- A subprogram body freezes its own contract. Analyze the contract
- -- after the declarations of the body have been processed as pragmas
- -- are now chained on the contract of the subprogram body.
-
- Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
-
-- Check completion, and analyze the statements
Check_Completion;
Inspect_Deferred_Constant_Completion (Declarations (N));
- Analyze (HSS);
+ Analyze (Handled_Statement_Sequence (N));
-- Add the generated minimum accessibility objects to the subprogram
-- body's list of declarations after analysis of the statements and
-- Deal with end of scope processing for the body
- Process_End_Label (HSS, 't', Current_Scope);
+ Process_End_Label
+ (Handled_Statement_Sequence (N), 't', Current_Scope);
Update_Use_Clause_Chain;
End_Scope;
-- the warning.
declare
- Stm : Node_Id := First (Statements (HSS));
+ Stm : Node_Id := First (Statements (Handled_Statement_Sequence (N)));
begin
-- Skip call markers installed by the ABE mechanism, labels, and
-- Push_xxx_Error_Label to find the first real statement.
-- Determine whether arbitrary entity Id denotes a partial invariant
-- procedure.
- function Is_Postconditions_Proc (Id : Entity_Id) return Boolean;
- pragma Inline (Is_Postconditions_Proc);
- -- Determine whether arbitrary entity Id denotes internally generated
- -- routine _Postconditions.
-
function Is_Preelaborated_Unit (Id : Entity_Id) return Boolean;
pragma Inline (Is_Preelaborated_Unit);
-- Determine whether arbitrary entity Id denotes a unit which is subject
elsif Is_Partial_Invariant_Proc (Subp_Id) then
null;
- -- _Postconditions
-
- elsif Is_Postconditions_Proc (Subp_Id) then
- Output_Verification_Call
- (Pred => "postconditions",
- Id => Find_Enclosing_Scope (Call),
- Id_Kind => "subprogram");
-
-- Subprograms must come last because some of the previous cases fall
-- under this category.
elsif Is_Partial_Invariant_Proc (Subp_Id) then
null;
- -- _Postconditions
-
- elsif Is_Postconditions_Proc (Subp_Id) then
- Info_Verification_Call
- (Pred => "postconditions",
- Id => Find_Enclosing_Scope (Call),
- Id_Kind => "subprogram");
-
-- Subprograms must come last because some of the previous cases
-- fall under this category.
(Extra : out Entity_Id;
Kind : out Invocation_Kind)
is
- Targ_Rep : constant Target_Rep_Id :=
- Target_Representation_Of (Targ_Id, In_State);
- Spec_Decl : constant Node_Id := Spec_Declaration (Targ_Rep);
-
begin
-- Accept within a task body
Extra := First_Formal_Type (Targ_Id);
Kind := Invariant_Verification;
- -- Postcondition verification
-
- elsif Is_Postconditions_Proc (Targ_Id) then
- Extra := Find_Enclosing_Scope (Spec_Decl);
- Kind := Postcondition_Verification;
-
-- Protected entry call
elsif Is_Protected_Entry (Targ_Id) then
Is_Default_Initial_Condition_Proc (Id)
or else Is_Initial_Condition_Proc (Id)
or else Is_Invariant_Proc (Id)
- or else Is_Partial_Invariant_Proc (Id)
- or else Is_Postconditions_Proc (Id);
+ or else Is_Partial_Invariant_Proc (Id);
end Is_Assertion_Pragma_Target;
----------------------------
Is_Accept_Alternative_Proc (Id)
or else Is_Finalizer_Proc (Id)
or else Is_Partial_Invariant_Proc (Id)
- or else Is_Postconditions_Proc (Id)
or else Is_TSS (Id, TSS_Deep_Adjust)
or else Is_TSS (Id, TSS_Deep_Finalize)
or else Is_TSS (Id, TSS_Deep_Initialize);
and then Is_Partial_Invariant_Procedure (Id);
end Is_Partial_Invariant_Proc;
- ----------------------------
- -- Is_Postconditions_Proc --
- ----------------------------
-
- function Is_Postconditions_Proc (Id : Entity_Id) return Boolean is
- begin
- -- To qualify, the entity must denote a _Postconditions procedure
-
- return
- Ekind (Id) = E_Procedure and then Chars (Id) = Name_uPostconditions;
- end Is_Postconditions_Proc;
-
---------------------------
-- Is_Preelaborated_Unit --
---------------------------
if Nkind (N) = N_Procedure_Call_Statement
and then Is_Entity_Name (Name (N))
- and then Chars (Entity (Name (N))) = Name_uPostconditions
+ and then Chars (Entity (Name (N))) = Name_uWrapped_Statements
then
return;
end if;
then
OK := True;
+ -- Special case for postconditions wrappers
+
+ elsif Ekind (Scop) in Subprogram_Kind
+ and then Present (Wrapped_Statements (Scop))
+ and then Wrapped_Statements (Scop) = Current_Scope
+ then
+ OK := True;
+
-- Default case, just check that the pragma occurs in the scope
-- of the entity denoted by the name.
then
return;
- -- Do not process internally generated routine _Postconditions
+ -- Do not process internally generated routine _Wrapped_Statements
elsif Ekind (Body_Id) = E_Procedure
- and then Chars (Body_Id) = Name_uPostconditions
+ and then Chars (Body_Id) = Name_uWrapped_Statements
then
return;
end if;
Pragma_Type_Invariant_Class => True,
others => False);
+ -- Should to following constant arrays be renamed to better suit their
+ -- use as a predicate (e.g. Is_Pragma_*) ???
+
-- The following table lists all the implementation-defined pragmas that
-- should apply to the anonymous object produced by the analysis of a
-- single protected or task type. The table should be synchronized with
Pragma_Warnings => False,
others => True);
+ -- The following table lists all pragmas which are relevant to the analysis
+ -- of subprogram bodies.
+
+ Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Contract_Cases => True,
+ Pragma_Depends => True,
+ Pragma_Ghost => True,
+ Pragma_Global => True,
+ Pragma_Inline => True,
+ Pragma_Inline_Always => True,
+ Pragma_Post => True,
+ Pragma_Post_Class => True,
+ Pragma_Postcondition => True,
+ Pragma_Pre => True,
+ Pragma_Pre_Class => True,
+ Pragma_Precondition => True,
+ Pragma_Pure => True,
+ Pragma_Pure_Function => True,
+ Pragma_Refined_Depends => True,
+ Pragma_Refined_Global => True,
+ Pragma_Refined_Post => True,
+ Pragma_Refined_State => True,
+ Pragma_Volatile => True,
+ Pragma_Volatile_Function => True,
+ others => False);
+
-----------------
-- Subprograms --
-----------------
if Is_Entry (Nam)
and then Present (Contract_Wrapper (Nam))
and then Current_Scope /= Contract_Wrapper (Nam)
+ and then Current_Scope /= Wrapped_Statements (Contract_Wrapper (Nam))
then
-- Note the entity being called before rewriting the call, so that
-- it appears used at this point.
-- Anonymous access types
elsif Nkind (Pre) in N_Has_Entity
+ and then Ekind (Entity (Pre)) not in Subprogram_Kind
and then Present (Get_Dynamic_Accessibility (Entity (Pre)))
and then Level = Dynamic_Level
then
if Subp_Nam = Name_uFinalizer then
return False;
- -- _Postconditions procedure
+ -- _Wrapped_Statements procedure which gets generated as part of the
+ -- expansion of postconditions.
- elsif Subp_Nam = Name_uPostconditions then
+ elsif Subp_Nam = Name_uWrapped_Statements then
return False;
-- Predicate function
E : Entity_Id) return Boolean
is
Subp_Alias : constant Entity_Id := Alias (S);
+ Subp : Entity_Id := E;
begin
- return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
+ -- During expansion of subprograms with postconditions the original
+ -- subprogram's declarations and statements get wrapped into a local
+ -- _Wrapped_Statements subprogram.
+
+ if Chars (Subp) = Name_uWrapped_Statements then
+ Subp := Enclosing_Subprogram (Subp);
+ end if;
+
+ return S = Subp
+ or else (Present (Subp_Alias) and then Subp_Alias = Subp);
end Same_Or_Aliased_Subprograms;
---------------
and then Ekind (Scope (T))
in E_Entry | E_Entry_Family | E_Function | E_Procedure
and then
- (Present (Postconditions_Proc (Scope (T)))
+ (Present (Wrapped_Statements (Scope (T)))
or else Present (Contract (Scope (T))))
then
-- ??? Should define a flag for this. We could incorrectly
-- for this purpose, so e.g. in X := (if A then B else C);
-- Paren_Count for the right side will be 1.
+ -- Comes_From_Check_Or_Contract
+ -- This flag is present in all N_If_Statement nodes and
+ -- gets set when an N_If_Statement is generated as part of
+ -- the expansion of a Check, Assert, or contract-related
+ -- pragma.
+
-- Comes_From_Source
-- This flag is present in all nodes. It is set if the
-- node is built by the scanner or parser, and clear if
Name_uMaster : constant Name_Id := N + $;
Name_uObject : constant Name_Id := N + $;
Name_uPost : constant Name_Id := N + $;
- Name_uPostconditions : constant Name_Id := N + $;
Name_uPostcond_Enabled : constant Name_Id := N + $;
Name_uPre : constant Name_Id := N + $;
Name_uPriority : constant Name_Id := N + $;
Name_uTask_Name : constant Name_Id := N + $;
Name_uType_Invariant : constant Name_Id := N + $;
Name_uVariants : constant Name_Id := N + $;
+ Name_uWrapped_Statements : constant Name_Id := N + $;
-- Names of predefined primitives used in the expansion of dispatching
-- requeue and select statements, Abort, 'Callable and 'Terminated.
projects / platform / upstream / gcc.git / commitdiff