package body Contracts is
- procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id);
- -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
- -- contract-only subprogram body of eligible subprograms found in L, adds
- -- them to their corresponding list of declarations, and analyzes them.
-
procedure Analyze_Contracts
(L : List_Id;
Freeze_Nod : Node_Id;
-- is reached. Freeze_Id is the entity of some related context which caused
-- freezing up to node Freeze_Nod.
+ procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id);
+ -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
+ -- contract-only subprogram body of eligible subprograms found in L, adds
+ -- them to their corresponding list of declarations, and analyzes them.
+
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
Restore_SPARK_Mode (Mode);
end Analyze_Task_Contract;
- -----------------------------
- -- Create_Generic_Contract --
- -----------------------------
+ -------------------------------------------------
+ -- Build_And_Analyze_Contract_Only_Subprograms --
+ -------------------------------------------------
- procedure Create_Generic_Contract (Unit : Node_Id) is
- Templ : constant Node_Id := Original_Node (Unit);
- Templ_Id : constant Entity_Id := Defining_Entity (Templ);
+ procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
+ procedure Analyze_Contract_Only_Subprograms;
+ -- Analyze the contract-only subprograms of L
- procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
- -- Add a single contract-related source pragma Prag to the contract of
- -- generic template Templ_Id.
+ procedure Append_Contract_Only_Subprograms (Subp_List : List_Id);
+ -- Append the contract-only bodies of Subp_List to its declarations list
- ---------------------------------
- -- Add_Generic_Contract_Pragma --
- ---------------------------------
+ function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id;
+ -- If E is an entity for a non-imported subprogram specification with
+ -- pre/postconditions and we are compiling with CodePeer mode, then
+ -- this procedure will create a wrapper to help Gnat2scil process its
+ -- contracts. Return Empty if the wrapper cannot be built.
- procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
- Prag_Templ : Node_Id;
+ function Build_Contract_Only_Subprograms (L : List_Id) return List_Id;
+ -- Build the contract-only subprograms of all eligible subprograms found
+ -- in list L.
- begin
- -- Mark the pragma to prevent the premature capture of global
- -- references when capturing global references of the context
- -- (see Save_References_In_Pragma).
+ function Has_Private_Declarations (N : Node_Id) return Boolean;
+ -- Return True for package specs, task definitions, and protected type
+ -- definitions whose list of private declarations is not empty.
- Set_Is_Generic_Contract_Pragma (Prag);
+ ---------------------------------------
+ -- Analyze_Contract_Only_Subprograms --
+ ---------------------------------------
- -- Pragmas that apply to a generic subprogram declaration are not
- -- part of the semantic structure of the generic template:
+ procedure Analyze_Contract_Only_Subprograms is
+ procedure Analyze_Contract_Only_Bodies;
+ -- Analyze all the contract-only bodies of L
- -- generic
- -- procedure Example (Formal : Integer);
- -- pragma Precondition (Formal > 0);
+ ----------------------------------
+ -- Analyze_Contract_Only_Bodies --
+ ----------------------------------
- -- Create a generic template for such pragmas and link the template
- -- of the pragma with the generic template.
+ procedure Analyze_Contract_Only_Bodies is
+ Decl : Node_Id;
- if Nkind (Templ) = N_Generic_Subprogram_Declaration then
- Rewrite
- (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
- Prag_Templ := Original_Node (Prag);
+ begin
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Subprogram_Body
+ and then Is_Contract_Only_Body
+ (Defining_Unit_Name (Specification (Decl)))
+ then
+ Analyze (Decl);
+ end if;
- Set_Is_Generic_Contract_Pragma (Prag_Templ);
- Add_Contract_Item (Prag_Templ, Templ_Id);
+ Next (Decl);
+ end loop;
+ end Analyze_Contract_Only_Bodies;
- -- Otherwise link the pragma with the generic template
+ -- Start of processing for Analyze_Contract_Only_Subprograms
+
+ begin
+ if Ekind (Current_Scope) /= E_Package then
+ Analyze_Contract_Only_Bodies;
else
- Add_Contract_Item (Prag, Templ_Id);
- end if;
- end Add_Generic_Contract_Pragma;
+ declare
+ Pkg_Spec : constant Node_Id :=
+ Package_Specification (Current_Scope);
- -- Local variables
+ begin
+ if not Has_Private_Declarations (Pkg_Spec) then
+ Analyze_Contract_Only_Bodies;
- Context : constant Node_Id := Parent (Unit);
- Decl : Node_Id := Empty;
+ -- For packages with private declarations, the contract-only
+ -- bodies of subprograms defined in the visible part of the
+ -- package are added to its private declarations (to ensure
+ -- that they do not cause premature freezing of types and also
+ -- that they are analyzed with proper visibility). Hence they
+ -- will be analyzed later.
- -- Start of processing for Create_Generic_Contract
+ elsif Visible_Declarations (Pkg_Spec) = L then
+ null;
- begin
- -- A generic package declaration carries contract-related source pragmas
- -- in its visible declarations.
+ elsif Private_Declarations (Pkg_Spec) = L then
+ Analyze_Contract_Only_Bodies;
+ end if;
+ end;
+ end if;
+ end Analyze_Contract_Only_Subprograms;
- if Nkind (Templ) = N_Generic_Package_Declaration then
- Set_Ekind (Templ_Id, E_Generic_Package);
+ --------------------------------------
+ -- Append_Contract_Only_Subprograms --
+ --------------------------------------
- if Present (Visible_Declarations (Specification (Templ))) then
- Decl := First (Visible_Declarations (Specification (Templ)));
+ procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is
+ begin
+ if No (Subp_List) then
+ return;
end if;
- -- A generic package body carries contract-related source pragmas in its
- -- declarations.
+ if Ekind (Current_Scope) /= E_Package then
+ Append_List (Subp_List, To => L);
- elsif Nkind (Templ) = N_Package_Body then
- Set_Ekind (Templ_Id, E_Package_Body);
+ else
+ declare
+ Pkg_Spec : constant Node_Id :=
+ Package_Specification (Current_Scope);
- if Present (Declarations (Templ)) then
- Decl := First (Declarations (Templ));
- end if;
+ begin
+ if not Has_Private_Declarations (Pkg_Spec) then
+ Append_List (Subp_List, To => L);
- -- Generic subprogram declaration
+ -- If the package has private declarations then append them to
+ -- its private declarations; they will be analyzed when the
+ -- contracts of its private declarations are analyzed.
- elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
- if Nkind (Specification (Templ)) = N_Function_Specification then
- Set_Ekind (Templ_Id, E_Generic_Function);
- else
- Set_Ekind (Templ_Id, E_Generic_Procedure);
+ else
+ Append_List
+ (List => Subp_List,
+ To => Private_Declarations (Pkg_Spec));
+ end if;
+ end;
end if;
+ end Append_Contract_Only_Subprograms;
- -- When the generic subprogram acts as a compilation unit, inspect
- -- the Pragmas_After list for contract-related source pragmas.
+ ------------------------------------
+ -- Build_Contract_Only_Subprogram --
+ ------------------------------------
- if Nkind (Context) = N_Compilation_Unit then
- if Present (Aux_Decls_Node (Context))
- and then Present (Pragmas_After (Aux_Decls_Node (Context)))
- then
- Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
- end if;
+ -- This procedure takes care of building a wrapper to generate better
+ -- analysis results in the case of a call to a subprogram whose body
+ -- is unavailable to CodePeer but whose specification includes Pre/Post
+ -- conditions. The body might be unavailable for any of a number or
+ -- reasons (it is imported, the .adb file is simply missing, or the
+ -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
+ -- pragma). The built subprogram has the following contents:
+ -- * check preconditions
+ -- * call the subprogram
+ -- * check postconditions
- -- Otherwise inspect the successive declarations for contract-related
- -- source pragmas.
+ function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is
+ Loc : constant Source_Ptr := Sloc (E);
- else
- Decl := Next (Unit);
- end if;
+ Missing_Body_Name : constant Name_Id :=
+ New_External_Name (Chars (E), "__missing_body");
- -- A generic subprogram body carries contract-related source pragmas in
- -- its declarations.
+ function Build_Missing_Body_Decls return List_Id;
+ -- Build the declaration of the missing body subprogram and its
+ -- corresponding pragma Import.
- elsif Nkind (Templ) = N_Subprogram_Body then
- Set_Ekind (Templ_Id, E_Subprogram_Body);
+ function Build_Missing_Body_Subprogram_Call return Node_Id;
+ -- Build the call to the missing body subprogram
- if Present (Declarations (Templ)) then
- Decl := First (Declarations (Templ));
- end if;
- end if;
+ function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
+ -- Return True for cases where the wrapper is not needed or we cannot
+ -- build it.
- -- Inspect the relevant declarations looking for contract-related source
- -- pragmas and add them to the contract of the generic unit.
+ ------------------------------
+ -- Build_Missing_Body_Decls --
+ ------------------------------
- while Present (Decl) loop
- if Comes_From_Source (Decl) then
- if Nkind (Decl) = N_Pragma then
+ function Build_Missing_Body_Decls return List_Id is
+ Spec : constant Node_Id := Declaration_Node (E);
+ Decl : Node_Id;
+ Prag : Node_Id;
- -- The source pragma is a contract annotation
+ begin
+ Decl :=
+ Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec));
+ Set_Chars (Defining_Entity (Decl), Missing_Body_Name);
- if Is_Contract_Annotation (Decl) then
- Add_Generic_Contract_Pragma (Decl);
- end if;
+ Prag :=
+ Make_Pragma (Loc,
+ Chars => Name_Import,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Name_Ada)),
- -- The region where a contract-related source pragma may appear
- -- ends with the first source non-pragma declaration or statement.
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Missing_Body_Name))));
- else
- exit;
- end if;
- end if;
+ return New_List (Decl, Prag);
+ end Build_Missing_Body_Decls;
- Next (Decl);
- end loop;
- end Create_Generic_Contract;
+ ----------------------------------------
+ -- Build_Missing_Body_Subprogram_Call --
+ ----------------------------------------
- --------------------------------
- -- Expand_Subprogram_Contract --
- --------------------------------
+ function Build_Missing_Body_Subprogram_Call return Node_Id is
+ Forml : Entity_Id;
+ Parms : List_Id;
- procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
- Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
- Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+ begin
+ Parms := New_List;
- procedure Add_Invariant_And_Predicate_Checks
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id;
- Result : out Node_Id);
- -- Process the result of function Subp_Id (if applicable) and all its
- -- formals. Add invariant and predicate checks where applicable. The
- -- routine appends all the checks to list Stmts. If Subp_Id denotes a
- -- function, Result contains the entity of parameter _Result, to be
- -- used in the creation of procedure _Postconditions.
-
- procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
- -- Append a node to a list. If there is no list, create a new one. When
- -- the item denotes a pragma, it is added to the list only when it is
- -- enabled.
+ -- Build parameter list that we need
- 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.
+ Forml := First_Formal (E);
+ while Present (Forml) loop
+ Append_To (Parms, Make_Identifier (Loc, Chars (Forml)));
+ Next_Formal (Forml);
+ end loop;
- procedure Process_Contract_Cases (Stmts : in out List_Id);
- -- Process pragma Contract_Cases. This routine prepends items to the
- -- body declarations and appends items to list Stmts.
+ -- Build the call to the missing body subprogram
- procedure Process_Postconditions (Stmts : in out List_Id);
- -- Collect all [inherited] spec and body postconditions and accumulate
- -- their pragma Check equivalents in list Stmts.
+ if Ekind_In (E, E_Function, E_Generic_Function) then
+ return
+ Make_Simple_Return_Statement (Loc,
+ Expression =>
+ Make_Function_Call (Loc,
+ Name =>
+ Make_Identifier (Loc, Missing_Body_Name),
+ Parameter_Associations => Parms));
- procedure Process_Preconditions;
- -- Collect all [inherited] spec and body preconditions and prepend their
- -- pragma Check equivalents to the declarations of the body.
+ else
+ return
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ Make_Identifier (Loc, Missing_Body_Name),
+ Parameter_Associations => Parms);
+ end if;
+ end Build_Missing_Body_Subprogram_Call;
- ----------------------------------------
- -- Add_Invariant_And_Predicate_Checks --
- ----------------------------------------
+ -----------------------------------
+ -- Skip_Contract_Only_Subprogram --
+ -----------------------------------
- procedure Add_Invariant_And_Predicate_Checks
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id;
- Result : out Node_Id)
- is
- procedure Add_Invariant_Access_Checks (Id : Entity_Id);
- -- Id denotes the return value of a function or a formal parameter.
- -- Add an invariant check if the type of Id is access to a type with
- -- invariants. The routine appends the generated code to Stmts.
+ function Skip_Contract_Only_Subprogram
+ (E : Entity_Id) return Boolean
+ is
+ function Depends_On_Enclosing_Private_Type return Boolean;
+ -- Return True if some formal of E (or its return type) are
+ -- private types defined in an enclosing package.
- function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ can benefit from invariant checks. To
- -- qualify, the type must have a non-null invariant procedure and
- -- subprogram Subp_Id must appear visible from the point of view of
- -- the type.
+ function Some_Enclosing_Package_Has_Private_Decls return Boolean;
+ -- Return True if some enclosing package of the current scope has
+ -- private declarations.
- ---------------------------------
- -- Add_Invariant_Access_Checks --
- ---------------------------------
+ ---------------------------------------
+ -- Depends_On_Enclosing_Private_Type --
+ ---------------------------------------
- procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
- Loc : constant Source_Ptr := Sloc (Body_Decl);
- Ref : Node_Id;
- Typ : Entity_Id;
+ function Depends_On_Enclosing_Private_Type return Boolean is
+ function Defined_In_Enclosing_Package
+ (Typ : Entity_Id) return Boolean;
+ -- Return True if Typ is an entity defined in an enclosing
+ -- package of the current scope.
- begin
- Typ := Etype (Id);
+ ----------------------------------
+ -- Defined_In_Enclosing_Package --
+ ----------------------------------
- if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
- Typ := Designated_Type (Typ);
+ function Defined_In_Enclosing_Package
+ (Typ : Entity_Id) return Boolean
+ is
+ Scop : Entity_Id := Scope (Current_Scope);
- if Invariant_Checks_OK (Typ) then
- Ref :=
- Make_Explicit_Dereference (Loc,
- Prefix => New_Occurrence_Of (Id, Loc));
- Set_Etype (Ref, Typ);
+ begin
+ while Scop /= Scope (Typ)
+ and then not Is_Compilation_Unit (Scop)
+ loop
+ Scop := Scope (Scop);
+ end loop;
- -- Generate:
- -- if <Id> /= null then
- -- <invariant_call (<Ref>)>
- -- end if;
+ return Scop = Scope (Typ);
+ end Defined_In_Enclosing_Package;
- Append_Enabled_Item
- (Item =>
- Make_If_Statement (Loc,
- Condition =>
- Make_Op_Ne (Loc,
- Left_Opnd => New_Occurrence_Of (Id, Loc),
- Right_Opnd => Make_Null (Loc)),
- Then_Statements => New_List (
- Make_Invariant_Call (Ref))),
- List => Stmts);
- end if;
- end if;
- end Add_Invariant_Access_Checks;
+ -- Local variables
- -------------------------
- -- Invariant_Checks_OK --
- -------------------------
+ Param_E : Entity_Id;
+ Typ : Entity_Id;
- function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
- function Has_Public_Visibility_Of_Subprogram return Boolean;
- -- Determine whether type Typ has public visibility of subprogram
- -- Subp_Id.
+ -- Start of processing for Depends_On_Enclosing_Private_Type
- -----------------------------------------
- -- Has_Public_Visibility_Of_Subprogram --
- -----------------------------------------
+ begin
+ Param_E := First_Entity (E);
+ while Present (Param_E) loop
+ Typ := Etype (Param_E);
- function Has_Public_Visibility_Of_Subprogram return Boolean is
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ if Is_Private_Type (Typ)
+ and then Defined_In_Enclosing_Package (Typ)
+ then
+ return True;
+ end if;
- begin
- -- An Initialization procedure must be considered visible even
- -- though it is internally generated.
+ Next_Entity (Param_E);
+ end loop;
- if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
- return True;
+ return
+ Ekind (E) = E_Function
+ and then Is_Private_Type (Etype (E))
+ and then Defined_In_Enclosing_Package (Etype (E));
+ end Depends_On_Enclosing_Private_Type;
- elsif Ekind (Scope (Typ)) /= E_Package then
- return False;
+ ----------------------------------------------
+ -- Some_Enclosing_Package_Has_Private_Decls --
+ ----------------------------------------------
- -- Internally generated code is never publicly visible except
- -- for a subprogram that is the implementation of an expression
- -- function. In that case the visibility is determined by the
- -- last check.
+ function Some_Enclosing_Package_Has_Private_Decls return Boolean is
+ Scop : Entity_Id := Current_Scope;
+ Pkg_Spec : Node_Id := Package_Specification (Scop);
- elsif not Comes_From_Source (Subp_Decl)
- and then
- (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
- or else not
- Comes_From_Source (Defining_Entity (Subp_Decl)))
- then
- return False;
+ begin
+ loop
+ if Ekind (Scop) = E_Package
+ and then Has_Private_Declarations
+ (Package_Specification (Scop))
+ then
+ Pkg_Spec := Package_Specification (Scop);
+ end if;
- -- Determine whether the subprogram is declared in the visible
- -- declarations of the package containing the type.
+ exit when Is_Compilation_Unit (Scop);
+ Scop := Scope (Scop);
+ end loop;
- else
- return List_Containing (Subp_Decl) =
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Scope (Typ))));
- end if;
- end Has_Public_Visibility_Of_Subprogram;
+ return Pkg_Spec /= Package_Specification (Current_Scope);
+ end Some_Enclosing_Package_Has_Private_Decls;
- -- Start of processing for Invariant_Checks_OK
+ -- Start of processing for Skip_Contract_Only_Subprogram
begin
- return
- Has_Invariants (Typ)
- and then Present (Invariant_Procedure (Typ))
- and then not Has_Null_Body (Invariant_Procedure (Typ))
- and then Has_Public_Visibility_Of_Subprogram;
- end Invariant_Checks_OK;
+ if not CodePeer_Mode
+ or else Inside_A_Generic
+ or else not Is_Subprogram (E)
+ or else Is_Abstract_Subprogram (E)
+ or else Is_Imported (E)
+ or else No (Contract (E))
+ or else No (Pre_Post_Conditions (Contract (E)))
+ or else Is_Contract_Only_Body (E)
+ or else Convention (E) = Convention_Protected
+ then
+ return True;
- -- Local variables
+ -- We do not support building the contract-only subprogram if E
+ -- is a subprogram declared in a nested package that has some
+ -- formal or return type depending on a private type defined in
+ -- an enclosing package.
- Loc : constant Source_Ptr := Sloc (Body_Decl);
- -- Source location of subprogram body contract
+ elsif Ekind (Current_Scope) = E_Package
+ and then Some_Enclosing_Package_Has_Private_Decls
+ and then Depends_On_Enclosing_Private_Type
+ then
+ if Debug_Flag_Dot_KK then
+ declare
+ Saved_Mode : constant Warning_Mode_Type := Warning_Mode;
- Formal : Entity_Id;
- Typ : Entity_Id;
+ begin
+ -- Warnings are disabled by default under CodePeer_Mode
+ -- (see switch-c). Enable them temporarily.
- -- Start of processing for Add_Invariant_And_Predicate_Checks
+ Warning_Mode := Normal;
+ Error_Msg_N
+ ("cannot generate contract-only subprogram?", E);
+ Warning_Mode := Saved_Mode;
+ end;
+ end if;
- begin
- Result := Empty;
+ return True;
+ end if;
- -- Process the result of a function
+ return False;
+ end Skip_Contract_Only_Subprogram;
- if Ekind (Subp_Id) = E_Function then
- Typ := Etype (Subp_Id);
+ -- Start of processing for Build_Contract_Only_Subprogram
- -- Generate _Result which is used in procedure _Postconditions to
- -- verify the return value.
+ begin
+ -- Test cases where the wrapper is not needed and cases where we
+ -- cannot build it.
- Result := Make_Defining_Identifier (Loc, Name_uResult);
- Set_Etype (Result, Typ);
+ if Skip_Contract_Only_Subprogram (E) then
+ return Empty;
+ end if;
- -- Add an invariant check when the return type has invariants and
- -- the related function is visible to the outside.
+ -- Note on calls to Copy_Separate_Tree. The trees we are copying
+ -- here are fully analyzed, but we definitely want fully syntactic
+ -- unanalyzed trees in the body we construct, so that the analysis
+ -- generates the right visibility, and that is exactly what the
+ -- calls to Copy_Separate_Tree give us.
- if Invariant_Checks_OK (Typ) then
- Append_Enabled_Item
- (Item =>
- Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
- List => Stmts);
- end if;
+ declare
+ Name : constant Name_Id :=
+ New_External_Name (Chars (E), "__contract_only");
+ Id : Entity_Id;
+ Bod : Node_Id;
- -- Add an invariant check when the return type is an access to a
- -- type with invariants.
+ begin
+ Bod :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Declaration_Node (E)),
+ Declarations =>
+ Build_Missing_Body_Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Build_Missing_Body_Subprogram_Call),
+ End_Label => Make_Identifier (Loc, Name)));
- Add_Invariant_Access_Checks (Result);
- end if;
+ Id := Defining_Unit_Name (Specification (Bod));
- -- Add invariant and predicates for all formals that qualify
+ -- Copy only the pre/postconditions of the original contract
+ -- since it is what we need, but also because pragmas stored in
+ -- the other fields have N_Pragmas with N_Aspect_Specifications
+ -- that reference their associated pragma (thus causing an endless
+ -- loop when trying to copy the subtree).
- Formal := First_Formal (Subp_Id);
- while Present (Formal) loop
- Typ := Etype (Formal);
+ declare
+ New_Contract : constant Node_Id := Make_Contract (Sloc (E));
- if Ekind (Formal) /= E_In_Parameter
- or else Is_Access_Type (Typ)
- then
- if Invariant_Checks_OK (Typ) then
- Append_Enabled_Item
- (Item =>
- Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
- List => Stmts);
- end if;
+ begin
+ Set_Pre_Post_Conditions (New_Contract,
+ Copy_Separate_Tree (Pre_Post_Conditions (Contract (E))));
+ Set_Contract (Id, New_Contract);
+ end;
- Add_Invariant_Access_Checks (Formal);
+ -- Fix the name of this new subprogram and link the original
+ -- subprogram with its Contract_Only_Body subprogram.
- -- Note: we used to add predicate checks for OUT and IN OUT
- -- formals here, but that was misguided, since such checks are
- -- performed on the caller side, based on the predicate of the
- -- actual, rather than the predicate of the formal.
+ Set_Chars (Id, Name);
+ Set_Is_Contract_Only_Body (Id);
+ Set_Contract_Only_Body (E, Id);
- end if;
+ return Bod;
+ end;
+ end Build_Contract_Only_Subprogram;
- Next_Formal (Formal);
- end loop;
- end Add_Invariant_And_Predicate_Checks;
+ -------------------------------------
+ -- Build_Contract_Only_Subprograms --
+ -------------------------------------
- -------------------------
- -- Append_Enabled_Item --
- -------------------------
+ function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is
+ Decl : Node_Id;
+ New_Subp : Node_Id;
+ Result : List_Id := No_List;
+ Subp_Id : Entity_Id;
- procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
begin
- -- Do not chain ignored or disabled pragmas
-
- if Nkind (Item) = N_Pragma
- and then (Is_Ignored (Item) or else Is_Disabled (Item))
- then
- null;
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Subprogram_Declaration then
+ Subp_Id := Defining_Unit_Name (Specification (Decl));
+ New_Subp := Build_Contract_Only_Subprogram (Subp_Id);
- -- Otherwise, add the item
+ if Present (New_Subp) then
+ if No (Result) then
+ Result := New_List;
+ end if;
- else
- if No (List) then
- List := New_List;
+ Append_To (Result, New_Subp);
+ end if;
end if;
- -- If the pragma is a conjunct in a composite postcondition, it
- -- has been processed in reverse order. In the postcondition body
- -- it must appear before the others.
+ Next (Decl);
+ end loop;
- if Nkind (Item) = N_Pragma
- and then From_Aspect_Specification (Item)
- and then Split_PPC (Item)
- then
- Prepend (Item, List);
- else
- Append (Item, List);
- end if;
- end if;
- end Append_Enabled_Item;
+ return Result;
+ end Build_Contract_Only_Subprograms;
- ------------------------------------
- -- Build_Postconditions_Procedure --
- ------------------------------------
+ ------------------------------
+ -- Has_Private_Declarations --
+ ------------------------------
- procedure Build_Postconditions_Procedure
- (Subp_Id : Entity_Id;
- Stmts : List_Id;
- Result : Entity_Id)
- is
- procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
- -- Insert node Stmt before the first source declaration of the
- -- related subprogram's body. If no such declaration exists, Stmt
- -- becomes the last declaration.
+ function Has_Private_Declarations (N : Node_Id) return Boolean is
+ begin
+ if not Nkind_In (N, N_Package_Specification,
+ N_Protected_Definition,
+ N_Task_Definition)
+ then
+ return False;
+ else
+ return
+ Present (Private_Declarations (N))
+ and then Is_Non_Empty_List (Private_Declarations (N));
+ end if;
+ end Has_Private_Declarations;
- --------------------------------------------
- -- Insert_Before_First_Source_Declaration --
- --------------------------------------------
+ -- Local variables
- procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
- Decls : constant List_Id := Declarations (Body_Decl);
- Decl : Node_Id;
+ Subp_List : List_Id;
- begin
- -- Inspect the declarations of the related subprogram body looking
- -- for the first source declaration.
+ -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
- if Present (Decls) then
- Decl := First (Decls);
- while Present (Decl) loop
- if Comes_From_Source (Decl) then
- Insert_Before (Decl, Stmt);
- return;
- end if;
+ begin
+ Subp_List := Build_Contract_Only_Subprograms (L);
+ Append_Contract_Only_Subprograms (Subp_List);
+ Analyze_Contract_Only_Subprograms;
+ end Build_And_Analyze_Contract_Only_Subprograms;
- Next (Decl);
- end loop;
+ -----------------------------
+ -- Create_Generic_Contract --
+ -----------------------------
- -- If we get there, then the subprogram body lacks any source
- -- declarations. The body of _Postconditions now acts as the
- -- last declaration.
+ procedure Create_Generic_Contract (Unit : Node_Id) is
+ Templ : constant Node_Id := Original_Node (Unit);
+ Templ_Id : constant Entity_Id := Defining_Entity (Templ);
- Append (Stmt, Decls);
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
+ -- Add a single contract-related source pragma Prag to the contract of
+ -- generic template Templ_Id.
- -- Ensure that the body has a declaration list
+ ---------------------------------
+ -- Add_Generic_Contract_Pragma --
+ ---------------------------------
- else
- Set_Declarations (Body_Decl, New_List (Stmt));
- end if;
- end Insert_Before_First_Source_Declaration;
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
+ Prag_Templ : Node_Id;
- -- Local variables
+ begin
+ -- Mark the pragma to prevent the premature capture of global
+ -- references when capturing global references of the context
+ -- (see Save_References_In_Pragma).
- Loc : constant Source_Ptr := Sloc (Body_Decl);
- Params : List_Id := No_List;
- Proc_Bod : Node_Id;
- Proc_Decl : Node_Id;
- Proc_Id : Entity_Id;
- Proc_Spec : Node_Id;
+ Set_Is_Generic_Contract_Pragma (Prag);
- -- Start of processing for Build_Postconditions_Procedure
+ -- Pragmas that apply to a generic subprogram declaration are not
+ -- part of the semantic structure of the generic template:
- begin
- -- Nothing to do if there are no actions to check on exit
+ -- generic
+ -- procedure Example (Formal : Integer);
+ -- pragma Precondition (Formal > 0);
- if No (Stmts) then
- return;
- end if;
+ -- Create a generic template for such pragmas and link the template
+ -- of the pragma with the generic template.
- Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
- Set_Debug_Info_Needed (Proc_Id);
- Set_Postconditions_Proc (Subp_Id, Proc_Id);
+ if Nkind (Templ) = N_Generic_Subprogram_Declaration then
+ Rewrite
+ (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
+ Prag_Templ := Original_Node (Prag);
- -- 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.
+ Set_Is_Generic_Contract_Pragma (Prag_Templ);
+ Add_Contract_Item (Prag_Templ, Templ_Id);
- if Generate_C_Code then
- Set_Has_Pragma_Inline (Proc_Id);
- Set_Has_Pragma_Inline_Always (Proc_Id);
- Set_Is_Inlined (Proc_Id);
+ -- Otherwise link the pragma with the generic template
+
+ else
+ Add_Contract_Item (Prag, Templ_Id);
end if;
+ end Add_Generic_Contract_Pragma;
- -- The related subprogram is a function: create the specification of
- -- parameter _Result.
+ -- Local variables
- if Present (Result) then
- Params := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Result,
- Parameter_Type =>
- New_Occurrence_Of (Etype (Result), Loc)));
- end if;
+ Context : constant Node_Id := Parent (Unit);
+ Decl : Node_Id := Empty;
- Proc_Spec :=
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => Params);
+ -- Start of processing for Create_Generic_Contract
- Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
+ begin
+ -- A generic package declaration carries contract-related source pragmas
+ -- in its visible declarations.
- -- 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:
+ if Nkind (Templ) = N_Generic_Package_Declaration then
+ Set_Ekind (Templ_Id, E_Generic_Package);
- -- 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);
- Analyze (Proc_Decl);
+ if Present (Visible_Declarations (Specification (Templ))) then
+ Decl := First (Visible_Declarations (Specification (Templ)));
+ end if;
- -- 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.
+ -- A generic package body carries contract-related source pragmas in its
+ -- declarations.
- 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))));
+ elsif Nkind (Templ) = N_Package_Body then
+ Set_Ekind (Templ_Id, E_Package_Body);
- Insert_After_And_Analyze (Proc_Decl, Proc_Bod);
- end Build_Postconditions_Procedure;
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
+ end if;
- ----------------------------
- -- Process_Contract_Cases --
- ----------------------------
+ -- Generic subprogram declaration
- procedure Process_Contract_Cases (Stmts : in out List_Id) is
- procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
- -- Process pragma Contract_Cases for subprogram Subp_Id
+ elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
+ if Nkind (Specification (Templ)) = N_Function_Specification then
+ Set_Ekind (Templ_Id, E_Generic_Function);
+ else
+ Set_Ekind (Templ_Id, E_Generic_Procedure);
+ end if;
- --------------------------------
- -- Process_Contract_Cases_For --
- --------------------------------
+ -- When the generic subprogram acts as a compilation unit, inspect
+ -- the Pragmas_After list for contract-related source pragmas.
- procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Subp_Id);
- Prag : Node_Id;
+ if Nkind (Context) = N_Compilation_Unit then
+ if Present (Aux_Decls_Node (Context))
+ and then Present (Pragmas_After (Aux_Decls_Node (Context)))
+ then
+ Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
+ end if;
- begin
- if Present (Items) then
- Prag := Contract_Test_Cases (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Expand_Pragma_Contract_Cases
- (CCs => Prag,
- Subp_Id => Subp_Id,
- Decls => Declarations (Body_Decl),
- Stmts => Stmts);
- end if;
+ -- Otherwise inspect the successive declarations for contract-related
+ -- source pragmas.
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end Process_Contract_Cases_For;
+ else
+ Decl := Next (Unit);
+ end if;
- -- Start of processing for Process_Contract_Cases
+ -- A generic subprogram body carries contract-related source pragmas in
+ -- its declarations.
- begin
- Process_Contract_Cases_For (Body_Id);
+ elsif Nkind (Templ) = N_Subprogram_Body then
+ Set_Ekind (Templ_Id, E_Subprogram_Body);
- if Present (Spec_Id) then
- Process_Contract_Cases_For (Spec_Id);
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
end if;
- end Process_Contract_Cases;
+ end if;
- ----------------------------
- -- Process_Postconditions --
- ----------------------------
+ -- Inspect the relevant declarations looking for contract-related source
+ -- pragmas and add them to the contract of the generic unit.
- procedure Process_Postconditions (Stmts : in out List_Id) is
- procedure Process_Body_Postconditions (Post_Nam : Name_Id);
- -- Collect all [refined] postconditions of a specific kind denoted
- -- by Post_Nam that belong to the body, and generate pragma Check
- -- equivalents in list Stmts.
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ if Nkind (Decl) = N_Pragma then
- procedure Process_Spec_Postconditions;
- -- Collect all [inherited] postconditions of the spec, and generate
- -- pragma Check equivalents in list Stmts.
+ -- The source pragma is a contract annotation
- ---------------------------------
- -- Process_Body_Postconditions --
- ---------------------------------
+ if Is_Contract_Annotation (Decl) then
+ Add_Generic_Contract_Pragma (Decl);
+ end if;
- procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
- Items : constant Node_Id := Contract (Body_Id);
- Unit_Decl : constant Node_Id := Parent (Body_Decl);
- Decl : Node_Id;
- Prag : Node_Id;
+ -- The region where a contract-related source pragma may appear
+ -- ends with the first source non-pragma declaration or statement.
- begin
- -- Process the contract
+ else
+ exit;
+ end if;
+ end if;
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Post_Nam then
- Append_Enabled_Item
- (Item => Build_Pragma_Check_Equivalent (Prag),
- List => Stmts);
- end if;
+ Next (Decl);
+ end loop;
+ end Create_Generic_Contract;
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
+ --------------------------------
+ -- Expand_Subprogram_Contract --
+ --------------------------------
- -- The subprogram body being processed is actually the proper body
- -- of a stub with a corresponding spec. The subprogram stub may
- -- carry a postcondition pragma, in which case it must be taken
- -- into account. The pragma appears after the stub.
+ procedure Expand_Subprogram_Contract (Body_Id : Entity_Id) is
+ Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
- if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
- Decl := Next (Corresponding_Stub (Unit_Decl));
- while Present (Decl) loop
+ procedure Add_Invariant_And_Predicate_Checks
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id;
+ Result : out Node_Id);
+ -- Process the result of function Subp_Id (if applicable) and all its
+ -- formals. Add invariant and predicate checks where applicable. The
+ -- routine appends all the checks to list Stmts. If Subp_Id denotes a
+ -- function, Result contains the entity of parameter _Result, to be
+ -- used in the creation of procedure _Postconditions.
- -- Note that non-matching pragmas are skipped
+ procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
+ -- Append a node to a list. If there is no list, create a new one. When
+ -- the item denotes a pragma, it is added to the list only when it is
+ -- enabled.
- if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Post_Nam then
- Append_Enabled_Item
- (Item => Build_Pragma_Check_Equivalent (Decl),
- List => Stmts);
- end if;
+ 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.
- -- Skip internally generated code
+ procedure Process_Contract_Cases (Stmts : in out List_Id);
+ -- Process pragma Contract_Cases. This routine prepends items to the
+ -- body declarations and appends items to list Stmts.
- elsif not Comes_From_Source (Decl) then
- null;
+ procedure Process_Postconditions (Stmts : in out List_Id);
+ -- Collect all [inherited] spec and body postconditions and accumulate
+ -- their pragma Check equivalents in list Stmts.
- -- Postcondition pragmas are usually grouped together. There
- -- is no need to inspect the whole declarative list.
+ procedure Process_Preconditions;
+ -- Collect all [inherited] spec and body preconditions and prepend their
+ -- pragma Check equivalents to the declarations of the body.
- else
- exit;
- end if;
+ ----------------------------------------
+ -- Add_Invariant_And_Predicate_Checks --
+ ----------------------------------------
- Next (Decl);
- end loop;
- end if;
- end Process_Body_Postconditions;
+ procedure Add_Invariant_And_Predicate_Checks
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id;
+ Result : out Node_Id)
+ is
+ procedure Add_Invariant_Access_Checks (Id : Entity_Id);
+ -- Id denotes the return value of a function or a formal parameter.
+ -- Add an invariant check if the type of Id is access to a type with
+ -- invariants. The routine appends the generated code to Stmts.
+
+ function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ can benefit from invariant checks. To
+ -- qualify, the type must have a non-null invariant procedure and
+ -- subprogram Subp_Id must appear visible from the point of view of
+ -- the type.
---------------------------------
- -- Process_Spec_Postconditions --
+ -- Add_Invariant_Access_Checks --
---------------------------------
- procedure Process_Spec_Postconditions is
- Subps : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- Items : Node_Id;
- Prag : Node_Id;
- Subp_Id : Entity_Id;
+ procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ Ref : Node_Id;
+ Typ : Entity_Id;
begin
- -- Process the contract
-
- Items := Contract (Spec_Id);
+ Typ := Etype (Id);
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition then
- Append_Enabled_Item
- (Item => Build_Pragma_Check_Equivalent (Prag),
- List => Stmts);
- end if;
+ if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
+ Typ := Designated_Type (Typ);
- Prag := Next_Pragma (Prag);
- end loop;
+ if Invariant_Checks_OK (Typ) then
+ Ref :=
+ Make_Explicit_Dereference (Loc,
+ Prefix => New_Occurrence_Of (Id, Loc));
+ Set_Etype (Ref, Typ);
+
+ -- Generate:
+ -- if <Id> /= null then
+ -- <invariant_call (<Ref>)>
+ -- end if;
+
+ Append_Enabled_Item
+ (Item =>
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => New_Occurrence_Of (Id, Loc),
+ Right_Opnd => Make_Null (Loc)),
+ Then_Statements => New_List (
+ Make_Invariant_Call (Ref))),
+ List => Stmts);
+ end if;
end if;
+ end Add_Invariant_Access_Checks;
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide postconditions.
+ -------------------------
+ -- Invariant_Checks_OK --
+ -------------------------
- for Index in Subps'Range loop
- Subp_Id := Subps (Index);
- Items := Contract (Subp_Id);
+ function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
+ function Has_Public_Visibility_Of_Subprogram return Boolean;
+ -- Determine whether type Typ has public visibility of subprogram
+ -- Subp_Id.
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition
- and then Class_Present (Prag)
- then
- Append_Enabled_Item
- (Item =>
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Spec_Id,
- Inher_Id => Subp_Id),
- List => Stmts);
- end if;
+ -----------------------------------------
+ -- Has_Public_Visibility_Of_Subprogram --
+ -----------------------------------------
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end loop;
- end Process_Spec_Postconditions;
+ function Has_Public_Visibility_Of_Subprogram return Boolean is
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- -- Start of processing for Process_Postconditions
+ begin
+ -- An Initialization procedure must be considered visible even
+ -- though it is internally generated.
- begin
- -- The processing of postconditions is done in reverse order (body
- -- first) to ensure the following arrangement:
+ if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
+ return True;
- -- <refined postconditions from body>
- -- <postconditions from body>
- -- <postconditions from spec>
- -- <inherited postconditions>
+ elsif Ekind (Scope (Typ)) /= E_Package then
+ return False;
- Process_Body_Postconditions (Name_Refined_Post);
- Process_Body_Postconditions (Name_Postcondition);
+ -- Internally generated code is never publicly visible except
+ -- for a subprogram that is the implementation of an expression
+ -- function. In that case the visibility is determined by the
+ -- last check.
- if Present (Spec_Id) then
- Process_Spec_Postconditions;
- end if;
- end Process_Postconditions;
+ elsif not Comes_From_Source (Subp_Decl)
+ and then
+ (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
+ or else not
+ Comes_From_Source (Defining_Entity (Subp_Decl)))
+ then
+ return False;
- ---------------------------
- -- Process_Preconditions --
- ---------------------------
+ -- Determine whether the subprogram is declared in the visible
+ -- declarations of the package containing the type.
- procedure Process_Preconditions is
- Class_Pre : Node_Id := Empty;
- -- The sole [inherited] class-wide precondition pragma that applies
- -- to the subprogram.
+ else
+ return List_Containing (Subp_Decl) =
+ Visible_Declarations
+ (Specification (Unit_Declaration_Node (Scope (Typ))));
+ end if;
+ end Has_Public_Visibility_Of_Subprogram;
- Insert_Node : Node_Id := Empty;
- -- The insertion node after which all pragma Check equivalents are
- -- inserted.
+ -- Start of processing for Invariant_Checks_OK
- function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
- -- Determine whether arbitrary declaration Decl denotes a renaming of
- -- a discriminant or protection field _object.
+ begin
+ return
+ Has_Invariants (Typ)
+ and then Present (Invariant_Procedure (Typ))
+ and then not Has_Null_Body (Invariant_Procedure (Typ))
+ and then Has_Public_Visibility_Of_Subprogram;
+ end Invariant_Checks_OK;
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
- -- Merge two class-wide preconditions by "or else"-ing them. The
- -- changes are accumulated in parameter Into. Update the error
- -- message of Into.
+ -- Local variables
- procedure Prepend_To_Decls (Item : Node_Id);
- -- Prepend a single item to the declarations of the subprogram body
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ -- Source location of subprogram body contract
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
- -- Save a class-wide precondition into Class_Pre, or prepend a normal
- -- precondition to the declarations of the body and analyze it.
+ Formal : Entity_Id;
+ Typ : Entity_Id;
- procedure Process_Inherited_Preconditions;
- -- Collect all inherited class-wide preconditions and merge them into
- -- one big precondition to be evaluated as pragma Check.
+ -- Start of processing for Add_Invariant_And_Predicate_Checks
- procedure Process_Preconditions_For (Subp_Id : Entity_Id);
- -- Collect all preconditions of subprogram Subp_Id and prepend their
- -- pragma Check equivalents to the declarations of the body.
+ begin
+ Result := Empty;
- --------------------------
- -- Is_Prologue_Renaming --
- --------------------------
+ -- Process the result of a function
- function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
- Nam : Node_Id;
- Obj : Entity_Id;
- Pref : Node_Id;
- Sel : Node_Id;
+ if Ekind (Subp_Id) = E_Function then
+ Typ := Etype (Subp_Id);
- begin
- if Nkind (Decl) = N_Object_Renaming_Declaration then
- Obj := Defining_Entity (Decl);
- Nam := Name (Decl);
+ -- Generate _Result which is used in procedure _Postconditions to
+ -- verify the return value.
- if Nkind (Nam) = N_Selected_Component then
- Pref := Prefix (Nam);
- Sel := Selector_Name (Nam);
+ Result := Make_Defining_Identifier (Loc, Name_uResult);
+ Set_Etype (Result, Typ);
- -- A discriminant renaming appears as
- -- Discr : constant ... := Prefix.Discr;
+ -- Add an invariant check when the return type has invariants and
+ -- the related function is visible to the outside.
- 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;
+ if Invariant_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
+ List => Stmts);
+ end if;
- -- A protection field renaming appears as
- -- Prot : ... := _object._object;
+ -- Add an invariant check when the return type is an access to a
+ -- type with invariants.
- -- A renamed private component is just a component of
- -- _object, with an arbitrary name.
+ Add_Invariant_Access_Checks (Result);
+ end if;
- elsif Ekind (Obj) = E_Variable
- and then Nkind (Pref) = N_Identifier
- and then Chars (Pref) = Name_uObject
- and then Nkind (Sel) = N_Identifier
- then
- return True;
- end if;
+ -- Add invariant and predicates for all formals that qualify
+
+ Formal := First_Formal (Subp_Id);
+ while Present (Formal) loop
+ Typ := Etype (Formal);
+
+ if Ekind (Formal) /= E_In_Parameter
+ or else Is_Access_Type (Typ)
+ then
+ if Invariant_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
+ List => Stmts);
end if;
- end if;
- return False;
- end Is_Prologue_Renaming;
+ Add_Invariant_Access_Checks (Formal);
- -------------------------
- -- Merge_Preconditions --
- -------------------------
+ -- Note: we used to add predicate checks for OUT and IN OUT
+ -- formals here, but that was misguided, since such checks are
+ -- performed on the caller side, based on the predicate of the
+ -- actual, rather than the predicate of the formal.
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
- function Expression_Arg (Prag : Node_Id) return Node_Id;
- -- Return the boolean expression argument of a precondition while
- -- updating its parentheses count for the subsequent merge.
+ end if;
- function Message_Arg (Prag : Node_Id) return Node_Id;
- -- Return the message argument of a precondition
+ Next_Formal (Formal);
+ end loop;
+ end Add_Invariant_And_Predicate_Checks;
- --------------------
- -- Expression_Arg --
- --------------------
+ -------------------------
+ -- Append_Enabled_Item --
+ -------------------------
- function Expression_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
+ procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
+ begin
+ -- Do not chain ignored or disabled pragmas
- begin
- if Paren_Count (Arg) = 0 then
- Set_Paren_Count (Arg, 1);
- end if;
+ if Nkind (Item) = N_Pragma
+ and then (Is_Ignored (Item) or else Is_Disabled (Item))
+ then
+ null;
- return Arg;
- end Expression_Arg;
+ -- Otherwise, add the item
- -----------------
- -- Message_Arg --
- -----------------
+ else
+ if No (List) then
+ List := New_List;
+ end if;
- function Message_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- begin
- return Get_Pragma_Arg (Last (Args));
- end Message_Arg;
+ -- If the pragma is a conjunct in a composite postcondition, it
+ -- has been processed in reverse order. In the postcondition body
+ -- it must appear before the others.
- -- Local variables
+ if Nkind (Item) = N_Pragma
+ and then From_Aspect_Specification (Item)
+ and then Split_PPC (Item)
+ then
+ Prepend (Item, List);
+ else
+ Append (Item, List);
+ end if;
+ end if;
+ end Append_Enabled_Item;
- From_Expr : constant Node_Id := Expression_Arg (From);
- From_Msg : constant Node_Id := Message_Arg (From);
- Into_Expr : constant Node_Id := Expression_Arg (Into);
- Into_Msg : constant Node_Id := Message_Arg (Into);
- Loc : constant Source_Ptr := Sloc (Into);
+ ------------------------------------
+ -- Build_Postconditions_Procedure --
+ ------------------------------------
- -- Start of processing for Merge_Preconditions
+ procedure Build_Postconditions_Procedure
+ (Subp_Id : Entity_Id;
+ Stmts : List_Id;
+ Result : Entity_Id)
+ is
+ procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
+ -- Insert node Stmt before the first source declaration of the
+ -- related subprogram's body. If no such declaration exists, Stmt
+ -- becomes the last declaration.
+
+ --------------------------------------------
+ -- Insert_Before_First_Source_Declaration --
+ --------------------------------------------
+
+ procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
+ Decls : constant List_Id := Declarations (Body_Decl);
+ Decl : Node_Id;
begin
- -- Merge the two preconditions by "or else"-ing them
+ -- Inspect the declarations of the related subprogram body looking
+ -- for the first source declaration.
- Rewrite (Into_Expr,
- Make_Or_Else (Loc,
- Right_Opnd => Relocate_Node (Into_Expr),
- Left_Opnd => From_Expr));
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ Insert_Before (Decl, Stmt);
+ return;
+ end if;
- -- Merge the two error messages to produce a single message of the
- -- form:
+ Next (Decl);
+ end loop;
- -- failed precondition from ...
- -- also failed inherited precondition from ...
+ -- If we get there, then the subprogram body lacks any source
+ -- declarations. The body of _Postconditions now acts as the
+ -- last declaration.
- if not Exception_Locations_Suppressed then
- Start_String (Strval (Into_Msg));
- Store_String_Char (ASCII.LF);
- Store_String_Chars (" also ");
- Store_String_Chars (Strval (From_Msg));
+ Append (Stmt, Decls);
- Set_Strval (Into_Msg, End_String);
+ -- Ensure that the body has a declaration list
+
+ else
+ Set_Declarations (Body_Decl, New_List (Stmt));
end if;
- end Merge_Preconditions;
+ end Insert_Before_First_Source_Declaration;
- ----------------------
- -- Prepend_To_Decls --
- ----------------------
+ -- Local variables
- procedure Prepend_To_Decls (Item : Node_Id) is
- Decls : List_Id := Declarations (Body_Decl);
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ Params : List_Id := No_List;
+ Proc_Bod : Node_Id;
+ Proc_Decl : Node_Id;
+ Proc_Id : Entity_Id;
+ Proc_Spec : Node_Id;
- begin
- -- Ensure that the body has a declarative list
+ -- Start of processing for Build_Postconditions_Procedure
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (Body_Decl, Decls);
- end if;
+ begin
+ -- Nothing to do if there are no actions to check on exit
- Prepend_To (Decls, Item);
- end Prepend_To_Decls;
+ if No (Stmts) then
+ return;
+ end if;
- ------------------------------
- -- Prepend_To_Decls_Or_Save --
- ------------------------------
+ Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
+ Set_Debug_Info_Needed (Proc_Id);
+ Set_Postconditions_Proc (Subp_Id, Proc_Id);
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
- Check_Prag : Node_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.
- begin
- Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+ if Generate_C_Code then
+ Set_Has_Pragma_Inline (Proc_Id);
+ Set_Has_Pragma_Inline_Always (Proc_Id);
+ Set_Is_Inlined (Proc_Id);
+ end if;
- -- Save the sole class-wide precondition (if any) for the next
- -- step, where it will be merged with inherited preconditions.
+ -- The related subprogram is a function: create the specification of
+ -- parameter _Result.
- if Class_Present (Prag) then
- pragma Assert (No (Class_Pre));
- Class_Pre := Check_Prag;
+ if Present (Result) then
+ Params := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Result,
+ Parameter_Type =>
+ New_Occurrence_Of (Etype (Result), Loc)));
+ end if;
- -- Accumulate the corresponding Check pragmas at the top of the
- -- declarations. Prepending the items ensures that they will be
- -- evaluated in their original order.
+ Proc_Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => Params);
- else
- if Present (Insert_Node) then
- Insert_After (Insert_Node, Check_Prag);
- else
- Prepend_To_Decls (Check_Prag);
- end if;
+ Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
- Analyze (Check_Prag);
- end if;
- end Prepend_To_Decls_Or_Save;
+ -- 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:
- -------------------------------------
- -- Process_Inherited_Preconditions --
- -------------------------------------
+ -- procedure Proc (Obj : Array_Typ) is
+ -- procedure _postconditions is
+ -- begin
+ -- ... Obj ...
+ -- end _postconditions;
- procedure Process_Inherited_Preconditions is
- Subps : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- Check_Prag : Node_Id;
- Items : Node_Id;
- Prag : Node_Id;
- Subp_Id : Entity_Id;
+ -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
+ -- begin
- begin
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide preconditions.
+ -- 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.
- for Index in Subps'Range loop
- Subp_Id := Subps (Index);
- Items := Contract (Subp_Id);
+ Insert_Before_First_Source_Declaration (Proc_Decl);
+ Analyze (Proc_Decl);
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Check_Prag :=
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Spec_Id,
- Inher_Id => Subp_Id);
+ -- 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.
+
+ 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_After_And_Analyze (Proc_Decl, Proc_Bod);
+ end Build_Postconditions_Procedure;
+
+ ----------------------------
+ -- Process_Contract_Cases --
+ ----------------------------
+
+ procedure Process_Contract_Cases (Stmts : in out List_Id) is
+ procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
+ -- Process pragma Contract_Cases for subprogram Subp_Id
+
+ --------------------------------
+ -- Process_Contract_Cases_For --
+ --------------------------------
+
+ procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Prag : Node_Id;
+
+ begin
+ if Present (Items) then
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Expand_Pragma_Contract_Cases
+ (CCs => Prag,
+ Subp_Id => Subp_Id,
+ Decls => Declarations (Body_Decl),
+ Stmts => Stmts);
+ end if;
- -- The spec of an inherited subprogram already yielded
- -- a class-wide precondition. Merge the existing
- -- precondition with the current one using "or else".
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end Process_Contract_Cases_For;
- if Present (Class_Pre) then
- Merge_Preconditions (Check_Prag, Class_Pre);
- else
- Class_Pre := Check_Prag;
- end if;
- end if;
+ -- Start of processing for Process_Contract_Cases
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end loop;
+ begin
+ Process_Contract_Cases_For (Body_Id);
- -- Add the merged class-wide preconditions
+ if Present (Spec_Id) then
+ Process_Contract_Cases_For (Spec_Id);
+ end if;
+ end Process_Contract_Cases;
- if Present (Class_Pre) then
- Prepend_To_Decls (Class_Pre);
- Analyze (Class_Pre);
- end if;
- end Process_Inherited_Preconditions;
+ ----------------------------
+ -- Process_Postconditions --
+ ----------------------------
- -------------------------------
- -- Process_Preconditions_For --
- -------------------------------
+ procedure Process_Postconditions (Stmts : in out List_Id) is
+ procedure Process_Body_Postconditions (Post_Nam : Name_Id);
+ -- Collect all [refined] postconditions of a specific kind denoted
+ -- by Post_Nam that belong to the body, and generate pragma Check
+ -- equivalents in list Stmts.
- procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Subp_Id);
+ procedure Process_Spec_Postconditions;
+ -- Collect all [inherited] postconditions of the spec, and generate
+ -- pragma Check equivalents in list Stmts.
+
+ ---------------------------------
+ -- Process_Body_Postconditions --
+ ---------------------------------
+
+ procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
+ Items : constant Node_Id := Contract (Body_Id);
+ Unit_Decl : constant Node_Id := Parent (Body_Decl);
Decl : Node_Id;
Prag : Node_Id;
- Subp_Decl : Node_Id;
begin
-- Process the contract
if Present (Items) then
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition then
- Prepend_To_Decls_Or_Save (Prag);
+ if Pragma_Name (Prag) = Post_Nam then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Prag),
+ List => Stmts);
end if;
Prag := Next_Pragma (Prag);
end loop;
end if;
- -- The subprogram declaration being processed is actually a body
- -- stub. The stub may carry a precondition pragma, in which case
- -- it must be taken into account. The pragma appears after the
- -- stub.
-
- Subp_Decl := Unit_Declaration_Node (Subp_Id);
-
- if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
-
- -- Inspect the declarations following the body stub
+ -- The subprogram body being processed is actually the proper body
+ -- of a stub with a corresponding spec. The subprogram stub may
+ -- carry a postcondition pragma, in which case it must be taken
+ -- into account. The pragma appears after the stub.
- Decl := Next (Subp_Decl);
+ if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
+ Decl := Next (Corresponding_Stub (Unit_Decl));
while Present (Decl) loop
-- Note that non-matching pragmas are skipped
if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Name_Precondition then
- Prepend_To_Decls_Or_Save (Decl);
+ if Pragma_Name (Decl) = Post_Nam then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Decl),
+ List => Stmts);
end if;
-- Skip internally generated code
elsif not Comes_From_Source (Decl) then
null;
- -- Preconditions are usually grouped together. There is no
- -- need to inspect the whole declarative list.
+ -- Postcondition pragmas are usually grouped together. There
+ -- is no need to inspect the whole declarative list.
else
exit;
Next (Decl);
end loop;
end if;
- end Process_Preconditions_For;
-
- -- Local variables
-
- Decls : constant List_Id := Declarations (Body_Decl);
- Decl : Node_Id;
+ end Process_Body_Postconditions;
- -- Start of processing for Process_Preconditions
+ ---------------------------------
+ -- Process_Spec_Postconditions --
+ ---------------------------------
- begin
- -- Find the proper insertion point for all pragma Check equivalents
+ procedure Process_Spec_Postconditions is
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
- if Present (Decls) then
- Decl := First (Decls);
- while Present (Decl) loop
+ begin
+ -- Process the contract
- -- First source declaration terminates the search, because all
- -- preconditions must be evaluated prior to it, by definition.
+ Items := Contract (Spec_Id);
- if Comes_From_Source (Decl) then
- exit;
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Prag),
+ List => Stmts);
+ end if;
- -- Certain internally generated object renamings such as those
- -- for discriminants and protection fields must be elaborated
- -- before the preconditions are evaluated, as their expressions
- -- may mention the discriminants. The renamings include those
- -- for private components so we need to find the last such.
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
- elsif Is_Prologue_Renaming (Decl) then
- while Present (Next (Decl))
- and then Is_Prologue_Renaming (Next (Decl))
- loop
- Next (Decl);
- end loop;
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide postconditions.
- Insert_Node := Decl;
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (Subp_Id);
- -- Otherwise the declaration does not come from source. This
- -- also terminates the search, because internal code may raise
- -- exceptions which should not preempt the preconditions.
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then Class_Present (Prag)
+ then
+ Append_Enabled_Item
+ (Item =>
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id),
+ List => Stmts);
+ end if;
- else
- exit;
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
-
- Next (Decl);
end loop;
- end if;
+ end Process_Spec_Postconditions;
- -- The processing of preconditions is done in reverse order (body
- -- first), because each pragma Check equivalent is inserted at the
- -- top of the declarations. This ensures that the final order is
- -- consistent with following diagram:
+ -- Start of processing for Process_Postconditions
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
+ begin
+ -- The processing of postconditions is done in reverse order (body
+ -- first) to ensure the following arrangement:
- Process_Preconditions_For (Body_Id);
+ -- <refined postconditions from body>
+ -- <postconditions from body>
+ -- <postconditions from spec>
+ -- <inherited postconditions>
+
+ Process_Body_Postconditions (Name_Refined_Post);
+ Process_Body_Postconditions (Name_Postcondition);
if Present (Spec_Id) then
- Process_Preconditions_For (Spec_Id);
- Process_Inherited_Preconditions;
+ Process_Spec_Postconditions;
end if;
- end Process_Preconditions;
-
- -- Local variables
-
- Restore_Scope : Boolean := False;
- Result : Entity_Id;
- Stmts : List_Id := No_List;
- Subp_Id : Entity_Id;
-
- -- Start of processing for Expand_Subprogram_Contract
-
- begin
- -- Obtain the entity of the initial declaration
-
- if Present (Spec_Id) then
- Subp_Id := Spec_Id;
- else
- Subp_Id := Body_Id;
- end if;
-
- -- Do not perform expansion activity when it is not needed
-
- if not Expander_Active then
- return;
-
- -- ASIS requires an unaltered tree
-
- elsif ASIS_Mode then
- return;
-
- -- GNATprove does not need the executable semantics of a contract
-
- elsif GNATprove_Mode then
- return;
-
- -- The contract of a generic subprogram or one declared in a generic
- -- context is not expanded, as the corresponding instance will provide
- -- the executable semantics of the contract.
-
- elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
- return;
-
- -- All subprograms carry a contract, but for some it is not significant
- -- and should not be processed. This is a small optimization.
-
- elsif not Has_Significant_Contract (Subp_Id) then
- return;
-
- -- The contract of an ignored Ghost subprogram does not need expansion,
- -- because the subprogram and all calls to it will be removed.
+ end Process_Postconditions;
- elsif Is_Ignored_Ghost_Entity (Subp_Id) then
- return;
- end if;
+ ---------------------------
+ -- Process_Preconditions --
+ ---------------------------
- -- Do not re-expand the same contract. This scenario occurs when a
- -- construct is rewritten into something else during its analysis
- -- (expression functions for instance).
+ procedure Process_Preconditions is
+ Class_Pre : Node_Id := Empty;
+ -- The sole [inherited] class-wide precondition pragma that applies
+ -- to the subprogram.
- if Has_Expanded_Contract (Subp_Id) then
- return;
+ Insert_Node : Node_Id := Empty;
+ -- The insertion node after which all pragma Check equivalents are
+ -- inserted.
- -- Otherwise mark the subprogram
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
+ -- Determine whether arbitrary declaration Decl denotes a renaming of
+ -- a discriminant or protection field _object.
- else
- Set_Has_Expanded_Contract (Subp_Id);
- end if;
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
+ -- Merge two class-wide preconditions by "or else"-ing them. The
+ -- changes are accumulated in parameter Into. Update the error
+ -- message of Into.
- -- Ensure that the formal parameters are visible when expanding all
- -- contract items.
+ procedure Prepend_To_Decls (Item : Node_Id);
+ -- Prepend a single item to the declarations of the subprogram body
- if not In_Open_Scopes (Subp_Id) then
- Restore_Scope := True;
- Push_Scope (Subp_Id);
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
+ -- Save a class-wide precondition into Class_Pre, or prepend a normal
+ -- precondition to the declarations of the body and analyze it.
- if Is_Generic_Subprogram (Subp_Id) then
- Install_Generic_Formals (Subp_Id);
- else
- Install_Formals (Subp_Id);
- end if;
- end if;
+ procedure Process_Inherited_Preconditions;
+ -- Collect all inherited class-wide preconditions and merge them into
+ -- one big precondition to be evaluated as pragma Check.
- -- The expansion of a subprogram contract involves the creation of Check
- -- pragmas to verify the contract assertions of the spec and body in a
- -- particular order. The order is as follows:
+ procedure Process_Preconditions_For (Subp_Id : Entity_Id);
+ -- Collect all preconditions of subprogram Subp_Id and prepend their
+ -- pragma Check equivalents to the declarations of the body.
- -- function Example (...) return ... is
- -- procedure _Postconditions (...) is
- -- begin
- -- <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;
+ --------------------------
+ -- Is_Prologue_Renaming --
+ --------------------------
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
- -- <contract case conditions>
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
+ Nam : Node_Id;
+ Obj : Entity_Id;
+ Pref : Node_Id;
+ Sel : Node_Id;
- -- <source declarations>
- -- begin
- -- <source statements>
+ begin
+ if Nkind (Decl) = N_Object_Renaming_Declaration then
+ Obj := Defining_Entity (Decl);
+ Nam := Name (Decl);
- -- _Preconditions (Result);
- -- return Result;
- -- end Example;
+ if Nkind (Nam) = N_Selected_Component then
+ Pref := Prefix (Nam);
+ Sel := Selector_Name (Nam);
- -- Routine _Postconditions holds all contract assertions that must be
- -- verified on exit from the related subprogram.
+ -- A discriminant renaming appears as
+ -- Discr : constant ... := Prefix.Discr;
- -- Step 1: Handle all preconditions. This action must come before the
- -- processing of pragma Contract_Cases because the pragma prepends items
- -- to the body declarations.
+ 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;
- Process_Preconditions;
+ -- A protection field renaming appears as
+ -- Prot : ... := _object._object;
- -- Step 2: Handle all postconditions. This action must come before the
- -- processing of pragma Contract_Cases because the pragma appends items
- -- to list Stmts.
+ -- A renamed private component is just a component of
+ -- _object, with an arbitrary name.
- Process_Postconditions (Stmts);
+ elsif Ekind (Obj) = E_Variable
+ 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;
- -- Step 3: Handle pragma Contract_Cases. This action must come before
- -- the processing of invariants and predicates because those append
- -- items to list Stmts.
+ return False;
+ end Is_Prologue_Renaming;
- Process_Contract_Cases (Stmts);
+ -------------------------
+ -- Merge_Preconditions --
+ -------------------------
- -- Step 4: Apply invariant and predicate checks on a function result and
- -- all formals. The resulting checks are accumulated in list Stmts.
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
+ function Expression_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the boolean expression argument of a precondition while
+ -- updating its parentheses count for the subsequent merge.
- Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
+ function Message_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the message argument of a precondition
- -- Step 5: Construct procedure _Postconditions
+ --------------------
+ -- Expression_Arg --
+ --------------------
- Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
+ function Expression_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
- if Restore_Scope then
- End_Scope;
- end if;
- end Expand_Subprogram_Contract;
+ begin
+ if Paren_Count (Arg) = 0 then
+ Set_Paren_Count (Arg, 1);
+ end if;
- ---------------------------------
- -- Inherit_Subprogram_Contract --
- ---------------------------------
+ return Arg;
+ end Expression_Arg;
- procedure Inherit_Subprogram_Contract
- (Subp : Entity_Id;
- From_Subp : Entity_Id)
- is
- procedure Inherit_Pragma (Prag_Id : Pragma_Id);
- -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
- -- Subp's contract.
+ -----------------
+ -- Message_Arg --
+ -----------------
- --------------------
- -- Inherit_Pragma --
- --------------------
+ function Message_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ begin
+ return Get_Pragma_Arg (Last (Args));
+ end Message_Arg;
- procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
- Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
- New_Prag : Node_Id;
+ -- Local variables
- begin
- -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
- -- chains, therefore the node must be replicated. The new pragma is
- -- flagged as inherited for distinction purposes.
+ From_Expr : constant Node_Id := Expression_Arg (From);
+ From_Msg : constant Node_Id := Message_Arg (From);
+ Into_Expr : constant Node_Id := Expression_Arg (Into);
+ Into_Msg : constant Node_Id := Message_Arg (Into);
+ Loc : constant Source_Ptr := Sloc (Into);
- if Present (Prag) then
- New_Prag := New_Copy_Tree (Prag);
- Set_Is_Inherited_Pragma (New_Prag);
+ -- Start of processing for Merge_Preconditions
- Add_Contract_Item (New_Prag, Subp);
- end if;
- end Inherit_Pragma;
+ begin
+ -- Merge the two preconditions by "or else"-ing them
- -- Start of processing for Inherit_Subprogram_Contract
+ Rewrite (Into_Expr,
+ Make_Or_Else (Loc,
+ Right_Opnd => Relocate_Node (Into_Expr),
+ Left_Opnd => From_Expr));
- begin
- -- Inheritance is carried out only when both entities are subprograms
- -- with contracts.
+ -- Merge the two error messages to produce a single message of the
+ -- form:
- if Is_Subprogram_Or_Generic_Subprogram (Subp)
- and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
- and then Present (Contract (From_Subp))
- then
- Inherit_Pragma (Pragma_Extensions_Visible);
- end if;
- end Inherit_Subprogram_Contract;
+ -- failed precondition from ...
+ -- also failed inherited precondition from ...
- -------------------------------------
- -- Instantiate_Subprogram_Contract --
- -------------------------------------
+ if not Exception_Locations_Suppressed then
+ Start_String (Strval (Into_Msg));
+ Store_String_Char (ASCII.LF);
+ Store_String_Chars (" also ");
+ Store_String_Chars (Strval (From_Msg));
- procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
- procedure Instantiate_Pragmas (First_Prag : Node_Id);
- -- Instantiate all contract-related source pragmas found in the list,
- -- starting with pragma First_Prag. Each instantiated pragma is added
- -- to list L.
+ Set_Strval (Into_Msg, End_String);
+ end if;
+ end Merge_Preconditions;
- -------------------------
- -- Instantiate_Pragmas --
- -------------------------
+ ----------------------
+ -- Prepend_To_Decls --
+ ----------------------
- procedure Instantiate_Pragmas (First_Prag : Node_Id) is
- Inst_Prag : Node_Id;
- Prag : Node_Id;
+ procedure Prepend_To_Decls (Item : Node_Id) is
+ Decls : List_Id := Declarations (Body_Decl);
- begin
- Prag := First_Prag;
- while Present (Prag) loop
- if Is_Generic_Contract_Pragma (Prag) then
- Inst_Prag :=
- Copy_Generic_Node (Prag, Empty, Instantiating => True);
+ begin
+ -- Ensure that the body has a declarative list
- Set_Analyzed (Inst_Prag, False);
- Append_To (L, Inst_Prag);
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (Body_Decl, Decls);
end if;
- Prag := Next_Pragma (Prag);
- end loop;
- end Instantiate_Pragmas;
-
- -- Local variables
+ Prepend_To (Decls, Item);
+ end Prepend_To_Decls;
- Items : constant Node_Id := Contract (Defining_Entity (Templ));
+ ------------------------------
+ -- Prepend_To_Decls_Or_Save --
+ ------------------------------
- -- Start of processing for Instantiate_Subprogram_Contract
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
+ Check_Prag : Node_Id;
- begin
- if Present (Items) then
- Instantiate_Pragmas (Pre_Post_Conditions (Items));
- Instantiate_Pragmas (Contract_Test_Cases (Items));
- Instantiate_Pragmas (Classifications (Items));
- end if;
- end Instantiate_Subprogram_Contract;
+ begin
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
- ----------------------------------------
- -- Save_Global_References_In_Contract --
- ----------------------------------------
+ -- Save the sole class-wide precondition (if any) for the next
+ -- step, where it will be merged with inherited preconditions.
- procedure Save_Global_References_In_Contract
- (Templ : Node_Id;
- Gen_Id : Entity_Id)
- is
- procedure Save_Global_References_In_List (First_Prag : Node_Id);
- -- Save all global references in contract-related source pragmas found
- -- in the list, starting with pragma First_Prag.
+ if Class_Present (Prag) then
+ pragma Assert (No (Class_Pre));
+ Class_Pre := Check_Prag;
- ------------------------------------
- -- Save_Global_References_In_List --
- ------------------------------------
+ -- Accumulate the corresponding Check pragmas at the top of the
+ -- declarations. Prepending the items ensures that they will be
+ -- evaluated in their original order.
- procedure Save_Global_References_In_List (First_Prag : Node_Id) is
- Prag : Node_Id;
+ else
+ if Present (Insert_Node) then
+ Insert_After (Insert_Node, Check_Prag);
+ else
+ Prepend_To_Decls (Check_Prag);
+ end if;
- begin
- Prag := First_Prag;
- while Present (Prag) loop
- if Is_Generic_Contract_Pragma (Prag) then
- Save_Global_References (Prag);
+ Analyze (Check_Prag);
end if;
+ end Prepend_To_Decls_Or_Save;
- Prag := Next_Pragma (Prag);
- end loop;
- end Save_Global_References_In_List;
-
- -- Local variables
+ -------------------------------------
+ -- Process_Inherited_Preconditions --
+ -------------------------------------
- Items : constant Node_Id := Contract (Defining_Entity (Templ));
+ procedure Process_Inherited_Preconditions is
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Check_Prag : Node_Id;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
- -- Start of processing for Save_Global_References_In_Contract
+ begin
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide preconditions.
- begin
- -- The entity of the analyzed generic copy must be on the scope stack
- -- to ensure proper detection of global references.
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (Subp_Id);
- Push_Scope (Gen_Id);
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition
+ and then Class_Present (Prag)
+ then
+ Check_Prag :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id);
- if Permits_Aspect_Specifications (Templ)
- and then Has_Aspects (Templ)
- then
- Save_Global_References_In_Aspects (Templ);
- end if;
+ -- The spec of an inherited subprogram already yielded
+ -- a class-wide precondition. Merge the existing
+ -- precondition with the current one using "or else".
- if Present (Items) then
- Save_Global_References_In_List (Pre_Post_Conditions (Items));
- Save_Global_References_In_List (Contract_Test_Cases (Items));
- Save_Global_References_In_List (Classifications (Items));
- end if;
+ if Present (Class_Pre) then
+ Merge_Preconditions (Check_Prag, Class_Pre);
+ else
+ Class_Pre := Check_Prag;
+ end if;
+ end if;
- Pop_Scope;
- end Save_Global_References_In_Contract;
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end loop;
- -------------------------------------------------
- -- Build_And_Analyze_Contract_Only_Subprograms --
- -------------------------------------------------
+ -- Add the merged class-wide preconditions
- procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
- procedure Analyze_Contract_Only_Subprograms (L : List_Id);
- -- Analyze the contract-only subprograms of L
+ if Present (Class_Pre) then
+ Prepend_To_Decls (Class_Pre);
+ Analyze (Class_Pre);
+ end if;
+ end Process_Inherited_Preconditions;
- procedure Append_Contract_Only_Subprograms (Subp_List : List_Id);
- -- Append the contract-only bodies of Subp_List to its declarations list
+ -------------------------------
+ -- Process_Preconditions_For --
+ -------------------------------
- function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id;
- -- If E is an entity for a non-imported subprogram specification with
- -- pre/postconditions and we are compiling with CodePeer mode, then this
- -- procedure will create a wrapper to help Gnat2scil process its
- -- contracts. Return Empty if the wrapper cannot be built.
+ procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Decl : Node_Id;
+ Prag : Node_Id;
+ Subp_Decl : Node_Id;
- function Build_Contract_Only_Subprograms (L : List_Id) return List_Id;
- -- Build the contract-only subprograms of all eligible subprograms found
- -- in list L.
+ begin
+ -- Process the contract
- function Has_Private_Declarations (N : Node_Id) return Boolean;
- -- Return True for package specs, task definitions, and protected type
- -- definitions whose list of private declarations is not empty.
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition then
+ Prepend_To_Decls_Or_Save (Prag);
+ end if;
- ---------------------------------------
- -- Analyze_Contract_Only_Subprograms --
- ---------------------------------------
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
- procedure Analyze_Contract_Only_Subprograms (L : List_Id) is
- procedure Analyze_Contract_Only_Bodies;
- -- Analyze all the contract-only bodies of L
+ -- The subprogram declaration being processed is actually a body
+ -- stub. The stub may carry a precondition pragma, in which case
+ -- it must be taken into account. The pragma appears after the
+ -- stub.
- ----------------------------------
- -- Analyze_Contract_Only_Bodies --
- ----------------------------------
+ Subp_Decl := Unit_Declaration_Node (Subp_Id);
- procedure Analyze_Contract_Only_Bodies is
- Decl : Node_Id;
+ if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
- begin
- Decl := First (L);
- while Present (Decl) loop
- if Nkind (Decl) = N_Subprogram_Body
- and then Is_Contract_Only_Body
- (Defining_Unit_Name (Specification (Decl)))
- then
- Analyze (Decl);
- end if;
+ -- Inspect the declarations following the body stub
- Next (Decl);
- end loop;
- end Analyze_Contract_Only_Bodies;
+ Decl := Next (Subp_Decl);
+ while Present (Decl) loop
- -- Start of processing for Analyze_Contract_Only_Subprograms
+ -- Note that non-matching pragmas are skipped
- begin
- if Ekind (Current_Scope) /= E_Package then
- Analyze_Contract_Only_Bodies;
+ if Nkind (Decl) = N_Pragma then
+ if Pragma_Name (Decl) = Name_Precondition then
+ Prepend_To_Decls_Or_Save (Decl);
+ end if;
- else
- declare
- Pkg_Spec : constant Node_Id :=
- Package_Specification (Current_Scope);
+ -- Skip internally generated code
- begin
- if not Has_Private_Declarations (Pkg_Spec) then
- Analyze_Contract_Only_Bodies;
+ elsif not Comes_From_Source (Decl) then
+ null;
- -- For packages with private declarations, the contract-only
- -- bodies of subprograms defined in the visible part of the
- -- package are added to its private declarations (to ensure
- -- that they do not cause premature freezing of types and also
- -- that they are analyzed with proper visibility). Hence they
- -- will be analyzed later.
+ -- Preconditions are usually grouped together. There is no
+ -- need to inspect the whole declarative list.
- elsif Visible_Declarations (Pkg_Spec) = L then
- null;
+ else
+ exit;
+ end if;
- elsif Private_Declarations (Pkg_Spec) = L then
- Analyze_Contract_Only_Bodies;
- end if;
- end;
- end if;
- end Analyze_Contract_Only_Subprograms;
+ Next (Decl);
+ end loop;
+ end if;
+ end Process_Preconditions_For;
- --------------------------------------
- -- Append_Contract_Only_Subprograms --
- --------------------------------------
+ -- Local variables
- procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is
- begin
- if No (Subp_List) then
- return;
- end if;
+ Decls : constant List_Id := Declarations (Body_Decl);
+ Decl : Node_Id;
- if Ekind (Current_Scope) /= E_Package then
- Append_List (Subp_List, To => L);
+ -- Start of processing for Process_Preconditions
- else
- declare
- Pkg_Spec : constant Node_Id :=
- Package_Specification (Current_Scope);
+ begin
+ -- Find the proper insertion point for all pragma Check equivalents
- begin
- if not Has_Private_Declarations (Pkg_Spec) then
- Append_List (Subp_List, To => L);
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
- -- If the package has private declarations then append them to
- -- its private declarations; they will be analyzed when the
- -- contracts of its private declarations are analyzed.
+ -- First source declaration terminates the search, because all
+ -- preconditions must be evaluated prior to it, by definition.
- else
- Append_List
- (List => Subp_List,
- To => Private_Declarations (Pkg_Spec));
- end if;
- end;
- end if;
- end Append_Contract_Only_Subprograms;
+ if Comes_From_Source (Decl) then
+ exit;
- ------------------------------------
- -- Build_Contract_Only_Subprogram --
- ------------------------------------
+ -- Certain internally generated object renamings such as those
+ -- for discriminants and protection fields must be elaborated
+ -- before the preconditions are evaluated, as their expressions
+ -- may mention the discriminants. The renamings include those
+ -- for private components so we need to find the last such.
- -- This procedure takes care of building a wrapper to generate better
- -- analysis results in the case of a call to a subprogram whose body
- -- is unavailable to CodePeer but whose specification includes Pre/Post
- -- conditions. The body might be unavailable for any of a number or
- -- reasons (it is imported, the .adb file is simply missing, or the
- -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
- -- pragma). The built subprogram has the following contents:
- -- * check preconditions
- -- * call the subprogram
- -- * check postconditions
+ elsif Is_Prologue_Renaming (Decl) then
+ while Present (Next (Decl))
+ and then Is_Prologue_Renaming (Next (Decl))
+ loop
+ Next (Decl);
+ end loop;
- function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is
- Loc : constant Source_Ptr := Sloc (E);
+ Insert_Node := Decl;
- function Build_Missing_Body_Decls return List_Id;
- -- Build the declaration of the missing body subprogram and its
- -- corresponding pragma Import.
+ -- Otherwise the declaration does not come from source. This
+ -- also terminates the search, because internal code may raise
+ -- exceptions which should not preempt the preconditions.
- function Build_Missing_Body_Subprogram_Call return Node_Id;
- -- Build the call to the missing body subprogram
+ else
+ exit;
+ end if;
- function Copy_Original_Specification
- (Loc : Source_Ptr;
- Spec : Node_Id) return Node_Id;
- -- Build a copy of the original specification of the given subprogram
- -- specification.
+ Next (Decl);
+ end loop;
+ end if;
- function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
- -- Return True if E is a subprogram declared in a nested package that
- -- has some formal or return type depending on a private type defined
- -- in an enclosing package.
+ -- The processing of preconditions is done in reverse order (body
+ -- first), because each pragma Check equivalent is inserted at the
+ -- top of the declarations. This ensures that the final order is
+ -- consistent with following diagram:
- ------------------------------
- -- Build_Missing_Body_Decls --
- ------------------------------
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
- function Build_Missing_Body_Decls return List_Id is
- Name : constant Name_Id := Get_Contract_Only_Missing_Body_Name (E);
- Spec : constant Node_Id := Declaration_Node (E);
- Decl : Node_Id;
- Prag : Node_Id;
+ Process_Preconditions_For (Body_Id);
- begin
- Decl := Make_Subprogram_Declaration (Loc,
- Copy_Original_Specification (Loc, Spec));
- Set_Chars (Defining_Unit_Name (Specification (Decl)), Name);
+ if Present (Spec_Id) then
+ Process_Preconditions_For (Spec_Id);
+ Process_Inherited_Preconditions;
+ end if;
+ end Process_Preconditions;
- Prag :=
- Make_Pragma (Loc,
- Chars => Name_Import,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Name_Ada)),
+ -- Local variables
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Name))));
+ Restore_Scope : Boolean := False;
+ Result : Entity_Id;
+ Stmts : List_Id := No_List;
+ Subp_Id : Entity_Id;
- return New_List (Decl, Prag);
- end Build_Missing_Body_Decls;
+ -- Start of processing for Expand_Subprogram_Contract
- ----------------------------------------
- -- Build_Missing_Body_Subprogram_Call --
- ----------------------------------------
+ begin
+ -- Obtain the entity of the initial declaration
- function Build_Missing_Body_Subprogram_Call return Node_Id is
- Forml : Entity_Id;
- Parms : List_Id;
+ if Present (Spec_Id) then
+ Subp_Id := Spec_Id;
+ else
+ Subp_Id := Body_Id;
+ end if;
- begin
- -- Build parameter list that we need
+ -- Do not perform expansion activity when it is not needed
- Parms := New_List;
- Forml := First_Formal (E);
- while Present (Forml) loop
- Append_To (Parms, Make_Identifier (Loc, Chars (Forml)));
- Next_Formal (Forml);
- end loop;
+ if not Expander_Active then
+ return;
- -- Build the call to the missing body subprogram
+ -- ASIS requires an unaltered tree
- if Ekind_In (E, E_Function, E_Generic_Function) then
- return
- Make_Simple_Return_Statement (Loc,
- Expression =>
- Make_Function_Call (Loc,
- Name => Make_Identifier (Loc,
- Get_Contract_Only_Missing_Body_Name (E)),
- Parameter_Associations => Parms));
+ elsif ASIS_Mode then
+ return;
- else
- return
- Make_Procedure_Call_Statement (Loc,
- Name => Make_Identifier (Loc,
- Get_Contract_Only_Missing_Body_Name (E)),
- Parameter_Associations => Parms);
- end if;
- end Build_Missing_Body_Subprogram_Call;
+ -- GNATprove does not need the executable semantics of a contract
- ---------------------------------
- -- Copy_Original_Specification --
- ---------------------------------
+ elsif GNATprove_Mode then
+ return;
- function Copy_Original_Specification
- (Loc : Source_Ptr;
- Spec : Node_Id) return Node_Id
- is
- function Copy_Original_Type (N : Node_Id) return Node_Id;
- -- Duplicate the original type of a given formal or function
- -- result type.
+ -- The contract of a generic subprogram or one declared in a generic
+ -- context is not expanded, as the corresponding instance will provide
+ -- the executable semantics of the contract.
- function Copy_Original_Type (N : Node_Id) return Node_Id is
- begin
- -- For expanded names located in instantiations, copy them with
- -- semantic information (avoids visibility problems).
+ elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
+ return;
- if In_Instance
- and then Nkind (N) = N_Expanded_Name
- then
- return New_Copy_Tree (N);
- else
- return Copy_Separate_Tree (Original_Node (N));
- end if;
- end Copy_Original_Type;
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed. This is a small optimization.
- -- Local variables
+ elsif not Has_Significant_Contract (Subp_Id) then
+ return;
- Current_Parameter : Node_Id;
- Current_Identifier : Entity_Id;
- Current_Type : Node_Id;
- New_Identifier : Entity_Id;
- Parameters : List_Id := No_List;
+ -- The contract of an ignored Ghost subprogram does not need expansion,
+ -- because the subprogram and all calls to it will be removed.
- -- Start of processing for Copy_Original_Specification
+ elsif Is_Ignored_Ghost_Entity (Subp_Id) then
+ return;
+ end if;
- begin
- if Present (Parameter_Specifications (Spec)) then
- Parameters := New_List;
- Current_Parameter := First (Parameter_Specifications (Spec));
- while Present (Current_Parameter) loop
- Current_Identifier :=
- Defining_Identifier (Current_Parameter);
- Current_Type :=
- Copy_Original_Type (Parameter_Type (Current_Parameter));
-
- New_Identifier := Make_Defining_Identifier (Loc,
- Chars (Current_Identifier));
-
- Append_To (Parameters,
- Make_Parameter_Specification (Loc,
- Defining_Identifier => New_Identifier,
- Parameter_Type => Current_Type,
- In_Present => In_Present (Current_Parameter),
- Out_Present => Out_Present (Current_Parameter),
- Expression =>
- Copy_Separate_Tree (Expression (Current_Parameter))));
-
- Next (Current_Parameter);
- end loop;
- end if;
+ -- Do not re-expand the same contract. This scenario occurs when a
+ -- construct is rewritten into something else during its analysis
+ -- (expression functions for instance).
- case Nkind (Spec) is
- when N_Function_Specification =>
- return
- Make_Function_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc,
- Chars => Chars (Defining_Unit_Name (Spec))),
- Parameter_Specifications => Parameters,
- Result_Definition =>
- Copy_Original_Type (Result_Definition (Spec)));
-
- when N_Procedure_Specification =>
- return
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc,
- Chars => Chars (Defining_Unit_Name (Spec))),
- Parameter_Specifications => Parameters);
-
- when others =>
- raise Program_Error;
- end case;
- end Copy_Original_Specification;
+ if Has_Expanded_Contract (Subp_Id) then
+ return;
- -----------------------------------
- -- Skip_Contract_Only_Subprogram --
- -----------------------------------
+ -- Otherwise mark the subprogram
- function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean
- is
- function Depends_On_Enclosing_Private_Type return Boolean;
- -- Return True if some formal of E (or its return type) are
- -- private types defined in an enclosing package.
+ else
+ Set_Has_Expanded_Contract (Subp_Id);
+ end if;
- function Some_Enclosing_Package_Has_Private_Decls return Boolean;
- -- Return True if some enclosing package of the current scope has
- -- private declarations.
+ -- Ensure that the formal parameters are visible when expanding all
+ -- contract items.
- ---------------------------------------
- -- Depends_On_Enclosing_Private_Type --
- ---------------------------------------
+ if not In_Open_Scopes (Subp_Id) then
+ Restore_Scope := True;
+ Push_Scope (Subp_Id);
- function Depends_On_Enclosing_Private_Type return Boolean is
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
+ end if;
- function Defined_In_Enclosing_Package
- (Typ : Entity_Id) return Boolean;
- -- Return True if Typ is an entity defined in an enclosing
- -- package of the current scope.
+ -- The expansion of a subprogram contract involves the creation of Check
+ -- pragmas to verify the contract assertions of the spec and body in a
+ -- particular order. The order is as follows:
- ----------------------------------
- -- Defined_In_Enclosing_Package --
- ----------------------------------
+ -- function Example (...) return ... is
+ -- procedure _Postconditions (...) is
+ -- begin
+ -- <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;
- function Defined_In_Enclosing_Package
- (Typ : Entity_Id) return Boolean
- is
- Scop : Entity_Id := Scope (Current_Scope);
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+ -- <contract case conditions>
- begin
- while Scop /= Scope (Typ)
- and then not Is_Compilation_Unit (Scop)
- loop
- Scop := Scope (Scop);
- end loop;
+ -- <source declarations>
+ -- begin
+ -- <source statements>
- return Scop = Scope (Typ);
- end Defined_In_Enclosing_Package;
+ -- _Preconditions (Result);
+ -- return Result;
+ -- end Example;
- -- Local variables
+ -- Routine _Postconditions holds all contract assertions that must be
+ -- verified on exit from the related subprogram.
- Param_E : Entity_Id;
- Typ : Entity_Id;
- begin
- Param_E := First_Entity (E);
- while Present (Param_E) loop
- Typ := Etype (Param_E);
+ -- Step 1: Handle all preconditions. This action must come before the
+ -- processing of pragma Contract_Cases because the pragma prepends items
+ -- to the body declarations.
- if Is_Private_Type (Typ)
- and then Defined_In_Enclosing_Package (Typ)
- then
- return True;
- end if;
+ Process_Preconditions;
+
+ -- Step 2: Handle all postconditions. This action must come before the
+ -- processing of pragma Contract_Cases because the pragma appends items
+ -- to list Stmts.
- Next_Entity (Param_E);
- end loop;
+ Process_Postconditions (Stmts);
- return Ekind (E) = E_Function
- and then Is_Private_Type (Etype (E))
- and then Defined_In_Enclosing_Package (Etype (E));
- end Depends_On_Enclosing_Private_Type;
+ -- Step 3: Handle pragma Contract_Cases. This action must come before
+ -- the processing of invariants and predicates because those append
+ -- items to list Stmts.
- ----------------------------------------------
- -- Some_Enclosing_Package_Has_Private_Decls --
- ----------------------------------------------
+ Process_Contract_Cases (Stmts);
- function Some_Enclosing_Package_Has_Private_Decls return Boolean is
- Scop : Entity_Id := Current_Scope;
- Pkg_Spec : Node_Id := Package_Specification (Scop);
+ -- Step 4: Apply invariant and predicate checks on a function result and
+ -- all formals. The resulting checks are accumulated in list Stmts.
- begin
- loop
- if Ekind (Scop) = E_Package
- and then
- Has_Private_Declarations (Package_Specification (Scop))
- then
- Pkg_Spec := Package_Specification (Scop);
- end if;
+ Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
- exit when Is_Compilation_Unit (Scop);
- Scop := Scope (Scop);
- end loop;
+ -- Step 5: Construct procedure _Postconditions
- return Pkg_Spec /= Package_Specification (Current_Scope);
- end Some_Enclosing_Package_Has_Private_Decls;
+ Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
- -- Start of processing for Skip_Contract_Only_Subprogram
+ if Restore_Scope then
+ End_Scope;
+ end if;
+ end Expand_Subprogram_Contract;
- begin
- if Ekind (Current_Scope) = E_Package
- and then Some_Enclosing_Package_Has_Private_Decls
- and then Depends_On_Enclosing_Private_Type
- then
- if Debug_Flag_Dot_KK then
- declare
- Saved_Mode : constant Warning_Mode_Type := Warning_Mode;
+ ---------------------------------
+ -- Inherit_Subprogram_Contract --
+ ---------------------------------
- begin
- -- Warnings are disabled by default under CodePeer_Mode
- -- (see switch-c). Enable them temporarily.
+ procedure Inherit_Subprogram_Contract
+ (Subp : Entity_Id;
+ From_Subp : Entity_Id)
+ is
+ procedure Inherit_Pragma (Prag_Id : Pragma_Id);
+ -- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
+ -- Subp's contract.
- Warning_Mode := Normal;
- Error_Msg_N
- ("cannot generate contract-only subprogram?", E);
- Warning_Mode := Saved_Mode;
- end;
- end if;
+ --------------------
+ -- Inherit_Pragma --
+ --------------------
- return True;
- end if;
+ procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
+ Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
+ New_Prag : Node_Id;
- return False;
- end Skip_Contract_Only_Subprogram;
+ begin
+ -- A pragma cannot be part of more than one First_Pragma/Next_Pragma
+ -- chains, therefore the node must be replicated. The new pragma is
+ -- flagged as inherited for distinction purposes.
- -- Start of processing for Build_Contract_Only_Subprogram
+ if Present (Prag) then
+ New_Prag := New_Copy_Tree (Prag);
+ Set_Is_Inherited_Pragma (New_Prag);
- begin
- -- Test cases where the wrapper is not needed and cases where we
- -- cannot build the wrapper.
-
- if not CodePeer_Mode
- or else Inside_A_Generic
- or else not Is_Subprogram (E)
- or else Is_Abstract_Subprogram (E)
- or else Is_Imported (E)
- or else No (Contract (E))
- or else No (Pre_Post_Conditions (Contract (E)))
- or else Is_Contract_Only_Body (E)
- or else Skip_Contract_Only_Subprogram (E)
- or else Convention (E) = Convention_Protected
- then
- return Empty;
+ Add_Contract_Item (New_Prag, Subp);
end if;
+ end Inherit_Pragma;
- -- Note on calls to Copy_Separate_Tree. The trees we are copying
- -- here are fully analyzed, but we definitely want fully syntactic
- -- unanalyzed trees in the body we construct, so that the analysis
- -- generates the right visibility, and that is exactly what the
- -- calls to Copy_Separate_Tree give us.
+ -- Start of processing for Inherit_Subprogram_Contract
- declare
- Name : constant Name_Id := Get_Contract_Only_Body_Name (E);
- Id : Entity_Id;
- Bod : Node_Id;
+ begin
+ -- Inheritance is carried out only when both entities are subprograms
+ -- with contracts.
- begin
- Bod :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Original_Specification (Loc, Declaration_Node (E)),
- Declarations =>
- Build_Missing_Body_Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Build_Missing_Body_Subprogram_Call),
- End_Label => Make_Identifier (Loc, Name)));
+ if Is_Subprogram_Or_Generic_Subprogram (Subp)
+ and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
+ and then Present (Contract (From_Subp))
+ then
+ Inherit_Pragma (Pragma_Extensions_Visible);
+ end if;
+ end Inherit_Subprogram_Contract;
- Id := Defining_Unit_Name (Specification (Bod));
+ -------------------------------------
+ -- Instantiate_Subprogram_Contract --
+ -------------------------------------
- -- Copy only the pre/postconditions of the original contract
- -- since it is what we need, but also because pragmas stored in
- -- the other fields have N_Pragmas with N_Aspect_Specifications
- -- that reference their associated pragma (thus causing an endless
- -- loop when trying to copy the subtree).
+ procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
+ procedure Instantiate_Pragmas (First_Prag : Node_Id);
+ -- Instantiate all contract-related source pragmas found in the list,
+ -- starting with pragma First_Prag. Each instantiated pragma is added
+ -- to list L.
- declare
- New_Contract : constant Node_Id := Make_Contract (Sloc (E));
+ -------------------------
+ -- Instantiate_Pragmas --
+ -------------------------
- begin
- Set_Pre_Post_Conditions (New_Contract,
- Copy_Separate_Tree (Pre_Post_Conditions (Contract (E))));
- Set_Contract (Id, New_Contract);
- end;
+ procedure Instantiate_Pragmas (First_Prag : Node_Id) is
+ Inst_Prag : Node_Id;
+ Prag : Node_Id;
- -- Fix the name of this new subprogram and link the original
- -- subprogram with its Contract_Only_Body subprogram.
+ begin
+ Prag := First_Prag;
+ while Present (Prag) loop
+ if Is_Generic_Contract_Pragma (Prag) then
+ Inst_Prag :=
+ Copy_Generic_Node (Prag, Empty, Instantiating => True);
- Set_Chars (Id, Name);
- Set_Is_Contract_Only_Body (Id);
- Set_Contract_Only_Body (E, Id);
+ Set_Analyzed (Inst_Prag, False);
+ Append_To (L, Inst_Prag);
+ end if;
- return Bod;
- end;
- end Build_Contract_Only_Subprogram;
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Instantiate_Pragmas;
- -------------------------------------
- -- Build_Contract_Only_Subprograms --
- -------------------------------------
+ -- Local variables
- function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is
- Decl : Node_Id;
- Subp_Id : Entity_Id;
- New_Subp : Node_Id;
- Result : List_Id := No_List;
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
- begin
- Decl := First (L);
- while Present (Decl) loop
- if Nkind (Decl) = N_Subprogram_Declaration then
- Subp_Id := Defining_Unit_Name (Specification (Decl));
- New_Subp := Build_Contract_Only_Subprogram (Subp_Id);
+ -- Start of processing for Instantiate_Subprogram_Contract
- if Present (New_Subp) then
- if No (Result) then
- Result := New_List;
- end if;
+ begin
+ if Present (Items) then
+ Instantiate_Pragmas (Pre_Post_Conditions (Items));
+ Instantiate_Pragmas (Contract_Test_Cases (Items));
+ Instantiate_Pragmas (Classifications (Items));
+ end if;
+ end Instantiate_Subprogram_Contract;
- Append_To (Result, New_Subp);
- end if;
- end if;
+ ----------------------------------------
+ -- Save_Global_References_In_Contract --
+ ----------------------------------------
- Next (Decl);
- end loop;
+ procedure Save_Global_References_In_Contract
+ (Templ : Node_Id;
+ Gen_Id : Entity_Id)
+ is
+ procedure Save_Global_References_In_List (First_Prag : Node_Id);
+ -- Save all global references in contract-related source pragmas found
+ -- in the list, starting with pragma First_Prag.
- return Result;
- end Build_Contract_Only_Subprograms;
+ ------------------------------------
+ -- Save_Global_References_In_List --
+ ------------------------------------
- ------------------------------
- -- Has_Private_Declarations --
- ------------------------------
+ procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+ Prag : Node_Id;
- function Has_Private_Declarations (N : Node_Id) return Boolean is
begin
- if not Nkind_In (N, N_Package_Specification,
- N_Task_Definition,
- N_Protected_Definition)
- then
- return False;
- else
- return Present (Private_Declarations (N))
- and then Is_Non_Empty_List (Private_Declarations (N));
- end if;
- end Has_Private_Declarations;
+ Prag := First_Prag;
+ while Present (Prag) loop
+ if Is_Generic_Contract_Pragma (Prag) then
+ Save_Global_References (Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Save_Global_References_In_List;
-- Local variables
- Subp_List : List_Id;
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
- -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
+ -- Start of processing for Save_Global_References_In_Contract
begin
- Subp_List := Build_Contract_Only_Subprograms (L);
- Append_Contract_Only_Subprograms (Subp_List);
- Analyze_Contract_Only_Subprograms (L);
- end Build_And_Analyze_Contract_Only_Subprograms;
+ -- The entity of the analyzed generic copy must be on the scope stack
+ -- to ensure proper detection of global references.
+
+ Push_Scope (Gen_Id);
+
+ if Permits_Aspect_Specifications (Templ)
+ and then Has_Aspects (Templ)
+ then
+ Save_Global_References_In_Aspects (Templ);
+ end if;
+
+ if Present (Items) then
+ Save_Global_References_In_List (Pre_Post_Conditions (Items));
+ Save_Global_References_In_List (Contract_Test_Cases (Items));
+ Save_Global_References_In_List (Classifications (Items));
+ end if;
+
+ Pop_Scope;
+ end Save_Global_References_In_Contract;
end Contracts;
projects / gcc.git / commitdiff