end if;
Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
- Set_Debug_Info_Needed (Proc_Id);
- Set_Postconditions_Proc (Subp_Id, Proc_Id);
+ Set_Debug_Info_Needed (Proc_Id);
-- The related subprogram is a function: create the specification of
-- parameter _Result.
-- the postconditions: this would cause confusing debug info to be
-- produced, interfering with coverage-analysis tools.
- Proc_Bod :=
- Make_Subprogram_Body (Loc,
- Specification =>
+ declare
+ Proc_Decl : Node_Id;
+ Proc_Decl_Id : Entity_Id;
+ Proc_Spec : Node_Id;
+ begin
+ Proc_Spec :=
Make_Procedure_Specification (Loc,
Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => Params),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts,
- End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
-
- Insert_Before_First_Source_Declaration (Proc_Bod);
+ Parameter_Specifications => Params);
- -- Force the front-end inlining of _PostConditions when generating
- -- C code, since its body may have references to itypes defined in
- -- the enclosing subprogram, thus causing problems for the unnested
- -- routines. For this purpose its declaration with proper decoration
- -- for inlining is needed.
+ Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
+ Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl));
+ Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id);
- if Generate_C_Code then
- declare
- Proc_Decl : Node_Id;
- Proc_Decl_Id : Entity_Id;
-
- begin
- Proc_Decl :=
- Make_Subprogram_Declaration (Loc,
- Specification =>
- Copy_Subprogram_Spec (Specification (Proc_Bod)));
- Insert_Before (Proc_Bod, Proc_Decl);
+ -- Force the front end inlining of _PostConditions when generating
+ -- C code since its body may have references to itypes defined in
+ -- the enclosing subprogram, thus causing problems to unnesting
+ -- routines.
- Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl));
+ if Generate_C_Code then
Set_Has_Pragma_Inline (Proc_Decl_Id);
Set_Has_Pragma_Inline_Always (Proc_Decl_Id);
Set_Is_Inlined (Proc_Decl_Id);
+ end if;
- Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id);
-
- Analyze (Proc_Decl);
- end;
- end if;
-
- Analyze (Proc_Bod);
+ Insert_Before_First_Source_Declaration (Proc_Decl);
+ Analyze (Proc_Decl);
+
+ Proc_Bod :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Proc_Spec),
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts,
+ End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
+
+ Insert_Before_First_Source_Declaration (Proc_Bod);
+ Analyze (Proc_Bod);
+ end;
end Build_Postconditions_Procedure;
----------------------------
then
Subp_Id := Corresponding_Spec (Decl);
- -- The original context is an expression function that has
- -- been split into a spec and a body. The context is OK as
- -- long as the initial declaration is Ghost.
-
if Present (Subp_Id) then
- Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id));
- if Nkind (Subp_Decl) = N_Expression_Function then
- return Is_Subject_To_Ghost (Subp_Decl);
+ -- The context is the internally built _postconditions
+ -- subprogram, which it is OK because the real check was
+ -- done before expansion activities.
+
+ if Chars (Subp_Id) = Name_uPostconditions then
+ return True;
+
+ else
+ Subp_Decl :=
+ Original_Node (Unit_Declaration_Node (Subp_Id));
+
+ -- The original context is an expression function that
+ -- has been split into a spec and a body. The context is
+ -- OK as long as the initial declaration is Ghost.
+
+ if Nkind (Subp_Decl) = N_Expression_Function then
+ return Is_Subject_To_Ghost (Subp_Decl);
+ end if;
end if;
-- Otherwise this is either an internal body or an internal