-- --
-- B o d y --
-- --
--- Copyright (C) 2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2015-2019, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Exp_Prag; use Exp_Prag;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
+with Freeze; use Freeze;
+with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Sem_Ch6; use Sem_Ch6;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Snames; use Snames;
+with Stand; use Stand;
with Stringt; use Stringt;
with Tbuild; use Tbuild;
package body Contracts is
- procedure Analyze_Contracts
- (L : List_Id;
- Freeze_Nod : Node_Id;
- Freeze_Id : Entity_Id);
- -- Subsidiary to the one parameter version of Analyze_Contracts and routine
- -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in
- -- the list L. If Freeze_Nod is set, then the analysis stops when the node
- -- is reached. Freeze_Id is the entity of some related context which caused
- -- freezing up to node Freeze_Nod.
+ procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of package
+ -- instantiation Inst_Id as if they appear at the end of a declarative
+ -- region. The pragmas in question are:
+ --
+ -- Part_Of
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- Local variables
- Prag_Nam : Name_Id;
-
- -- Start of processing for Add_Contract_Item
-
- begin
-- A contract must contain only pragmas
pragma Assert (Nkind (Prag) = N_Pragma);
- Prag_Nam := Pragma_Name (Prag);
+ Prag_Nam : constant Name_Id := Pragma_Name (Prag);
+ -- Start of processing for Add_Contract_Item
+
+ begin
-- Create a new contract when adding the first item
if No (Items) then
-- Initializes
-- Part_Of (instantiation only)
- elsif Ekind_In (Id, E_Generic_Package, E_Package) then
+ elsif Is_Package_Or_Generic_Package (Id) then
if Nam_In (Prag_Nam, Name_Abstract_State,
Name_Initial_Condition,
Name_Initializes)
-- Effective_Reads
-- Effective_Writes
-- Global
+ -- No_Caching
-- Part_Of
elsif Ekind (Id) = E_Variable then
Name_Effective_Reads,
Name_Effective_Writes,
Name_Global,
+ Name_No_Caching,
Name_Part_Of)
then
Add_Classification;
-----------------------
procedure Analyze_Contracts (L : List_Id) is
- begin
- Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
- end Analyze_Contracts;
-
- procedure Analyze_Contracts
- (L : List_Id;
- Freeze_Nod : Node_Id;
- Freeze_Id : Entity_Id)
- is
Decl : Node_Id;
begin
Decl := First (L);
while Present (Decl) loop
- -- The caller requests that the traversal stops at a particular node
- -- that causes contract "freezing".
-
- if Present (Freeze_Nod) and then Decl = Freeze_Nod then
- exit;
- end if;
-
-- Entry or subprogram declarations
if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
- Analyze_Entry_Or_Subprogram_Contract
- (Subp_Id => Defining_Entity (Decl),
- Freeze_Id => Freeze_Id);
+ declare
+ Subp_Id : constant Entity_Id := Defining_Entity (Decl);
+
+ begin
+ Analyze_Entry_Or_Subprogram_Contract (Subp_Id);
+
+ -- If analysis of a class-wide pre/postcondition indicates
+ -- that a class-wide clone is needed, analyze its declaration
+ -- now. Its body is created when the body of the original
+ -- operation is analyzed (and rewritten).
+
+ if Is_Subprogram (Subp_Id)
+ and then Present (Class_Wide_Clone (Subp_Id))
+ then
+ Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id)));
+ end if;
+ end;
-- Entry or subprogram bodies
-- Objects
elsif Nkind (Decl) = N_Object_Declaration then
- Analyze_Object_Contract
- (Obj_Id => Defining_Entity (Decl),
- Freeze_Id => Freeze_Id);
+ Analyze_Object_Contract (Defining_Entity (Decl));
+
+ -- Package instantiation
- -- Protected untis
+ elsif Nkind (Decl) = N_Package_Instantiation then
+ Analyze_Package_Instantiation_Contract (Defining_Entity (Decl));
+
+ -- Protected units
elsif Nkind_In (Decl, N_Protected_Type_Declaration,
N_Single_Protected_Declaration)
N_Task_Type_Declaration)
then
Analyze_Task_Contract (Defining_Entity (Decl));
+
+ -- For type declarations, we need to do the preanalysis of Iterable
+ -- aspect specifications.
+
+ -- Other type aspects need to be resolved here???
+
+ elsif Nkind (Decl) = N_Private_Type_Declaration
+ and then Present (Aspect_Specifications (Decl))
+ then
+ declare
+ E : constant Entity_Id := Defining_Identifier (Decl);
+ It : constant Node_Id := Find_Aspect (E, Aspect_Iterable);
+
+ begin
+ if Present (It) then
+ Validate_Iterable_Aspect (E, It);
+ end if;
+ end;
end if;
Next (Decl);
-- Analyze_Entry_Or_Subprogram_Body_Contract --
-----------------------------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
Items : constant Node_Id := Contract (Body_Id);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
- Mode : SPARK_Mode_Type;
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
begin
-- When a subprogram body declaration is illegal, its defining entity is
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
+ Set_SPARK_Mode (Body_Id);
-- Ensure that the contract cases or postconditions mention 'Result or
-- define a post-state.
-- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
-- check is relevant only when SPARK_Mode is on, as it is not a standard
-- legality rule. The check is performed here because Volatile_Function
- -- is processed after the analysis of the related subprogram body.
+ -- is processed after the analysis of the related subprogram body. The
+ -- check only applies to source subprograms and not to generated TSS
+ -- subprograms.
if SPARK_Mode = On
and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+ and then Comes_From_Source (Spec_Id)
and then not Is_Volatile_Function (Body_Id)
then
Check_Nonvolatile_Function_Profile (Body_Id);
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic subprogram body now that
-- the contract has been analyzed.
-- Analyze_Entry_Or_Subprogram_Contract --
------------------------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Entry_Or_Subprogram_Contract
(Subp_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
Items : constant Node_Id := Contract (Subp_Id);
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
Skip_Assert_Exprs : constant Boolean :=
Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
and then not ASIS_Mode
Depends : Node_Id := Empty;
Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+ Set_SPARK_Mode (Subp_Id);
-- All subprograms carry a contract, but for some it is not significant
-- and should not be processed.
if Skip_Assert_Exprs then
null;
- -- Otherwise analyze the pre/postconditions
+ -- Otherwise analyze the pre/postconditions.
+ -- If these come from an aspect specification, their expressions
+ -- might include references to types that are not frozen yet, in the
+ -- case where the body is a rewritten expression function that is a
+ -- completion, so freeze all types within before constructing the
+ -- contract code.
else
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
- Prag := Next_Pragma (Prag);
- end loop;
+ declare
+ Bod : Node_Id;
+ Freeze_Types : Boolean := False;
+
+ begin
+ if Present (Freeze_Id) then
+ Bod := Unit_Declaration_Node (Freeze_Id);
+
+ if Nkind (Bod) = N_Subprogram_Body
+ and then Was_Expression_Function (Bod)
+ and then Ekind (Subp_Id) = E_Function
+ and then Chars (Subp_Id) = Chars (Freeze_Id)
+ and then Subp_Id /= Freeze_Id
+ then
+ Freeze_Types := True;
+ end if;
+ end if;
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Freeze_Types
+ and then Present (Corresponding_Aspect (Prag))
+ then
+ Freeze_Expr_Types
+ (Def_Id => Subp_Id,
+ Typ => Standard_Boolean,
+ Expr => Expression (Corresponding_Aspect (Prag)),
+ N => Bod);
+ end if;
+
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end;
end if;
-- Analyze contract-cases and test-cases
if SPARK_Mode = On
and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+ and then Comes_From_Source (Subp_Id)
and then not Is_Volatile_Function (Subp_Id)
then
Check_Nonvolatile_Function_Profile (Subp_Id);
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic subprogram now that the
-- contract has been analyzed.
-- Analyze_Object_Contract --
-----------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Object_Contract
(Obj_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
is
- Obj_Typ : constant Entity_Id := Etype (Obj_Id);
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- Encap_Id : Entity_Id;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Items : Node_Id;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Ref_Elmt : Elmt_Id;
- Restore_Mode : Boolean := False;
- Seen : Boolean := False;
+ Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ NC_Val : Boolean := False;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Ref_Elmt : Elmt_Id;
+ Seen : Boolean := False;
begin
-- The loop parameter in an element iterator over a formal container
if Is_Single_Concurrent_Object (Obj_Id)
and then Present (SPARK_Pragma (Obj_Id))
then
- Restore_Mode := True;
- Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+ Set_SPARK_Mode (Obj_Id);
end if;
-- Constant-related checks
Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
end if;
+ -- Analyze the non-external volatility property No_Caching
+
+ Prag := Get_Pragma (Obj_Id, Pragma_No_Caching);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
+ end if;
+
-- The anonymous object created for a single concurrent type carries
-- pragmas Depends and Globat of the type.
if not Is_Library_Level_Entity (Obj_Id) then
Error_Msg_N
- ("volatile variable & must be declared at library level",
- Obj_Id);
+ ("volatile variable & must be declared at library level "
+ & "(SPARK RM 7.1.3(3))", Obj_Id);
-- An object of a discriminated type cannot be effectively
-- volatile except for protected objects (SPARK RM 7.1.3(5)).
then
Error_Msg_N
("discriminated object & cannot be volatile", Obj_Id);
-
- -- An object of a tagged type cannot be effectively volatile
- -- (SPARK RM C.6(5)).
-
- elsif Is_Tagged_Type (Obj_Typ) then
- Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
end if;
-- The object is not effectively volatile
Obj_Id);
end if;
end if;
-
- -- A variable whose Part_Of pragma specifies a single concurrent
- -- type as encapsulator must be (SPARK RM 9.4):
- -- * Of a type that defines full default initialization, or
- -- * Declared with a default value, or
- -- * Imported
-
- Encap_Id := Encapsulating_State (Obj_Id);
-
- if Present (Encap_Id)
- and then Is_Single_Concurrent_Object (Encap_Id)
- and then not Has_Full_Default_Initialization (Etype (Obj_Id))
- and then not Has_Initial_Value (Obj_Id)
- and then not Is_Imported (Obj_Id)
- then
- Error_Msg_N ("& requires full default initialization", Obj_Id);
-
- Error_Msg_Name_1 := Chars (Encap_Id);
- Error_Msg_N
- (Fix_Msg (Encap_Id, "\object acts as constituent of single "
- & "protected type %"), Obj_Id);
- end if;
end if;
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- if Restore_Mode then
- Restore_SPARK_Mode (Mode);
- end if;
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Object_Contract;
-----------------------------------
-- Analyze_Package_Body_Contract --
-----------------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty)
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
Items : constant Node_Id := Contract (Body_Id);
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
- Mode : SPARK_Mode_Type;
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
Ref_State : Node_Id;
begin
-- context. To remedy this, restore the original SPARK_Mode of the
-- related package body.
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
+ Set_SPARK_Mode (Body_Id);
Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
if Present (Ref_State) then
Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
-
- -- State refinement is required when the package declaration defines at
- -- least one abstract state. Null states are not considered. Refinement
- -- is not enforced when SPARK checks are turned off.
-
- elsif SPARK_Mode /= Off
- and then Requires_State_Refinement (Spec_Id, Body_Id)
- then
- Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic package body now that the
-- contract has been analyzed.
-- Analyze_Package_Contract --
------------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
Items : constant Node_Id := Contract (Pack_Id);
Pack_Decl : constant Node_Id := Unit_Declaration_Node (Pack_Id);
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
Init : Node_Id := Empty;
Init_Cond : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
Prag : Node_Id;
Prag_Nam : Name_Id;
-- context. To remedy this, restore the original SPARK_Mode of the
-- related package.
- Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+ Set_SPARK_Mode (Pack_Id);
if Present (Items) then
end if;
end if;
- -- Check whether the lack of indicator Part_Of agrees with the placement
- -- of the package instantiation with respect to the state space.
-
- if Is_Generic_Instance (Pack_Id) then
- Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
-
- if No (Prag) then
- Check_Missing_Part_Of (Pack_Id);
- end if;
- end if;
-
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-- Capture all global references in a generic package now that the
-- contract has been analyzed.
end if;
end Analyze_Package_Contract;
- --------------------------------
- -- Analyze_Previous_Contracts --
- --------------------------------
+ --------------------------------------------
+ -- Analyze_Package_Instantiation_Contract --
+ --------------------------------------------
- procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is
- Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
- Par : Node_Id;
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
+ procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is
+ Inst_Spec : constant Node_Id :=
+ Instance_Spec (Unit_Declaration_Node (Inst_Id));
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
+ Pack_Id : Entity_Id;
+ Prag : Node_Id;
begin
- -- A body that is in the process of being inlined appears from source,
- -- but carries name _parent. Such a body does not cause "freezing" of
- -- contracts.
+ -- Nothing to do when the package instantiation is erroneous or left
+ -- partially decorated.
- if Chars (Body_Id) = Name_uParent then
+ if No (Inst_Spec) then
return;
end if;
- -- Climb the parent chain looking for an enclosing package body. Do not
- -- use the scope stack, as a body uses the entity of its corresponding
- -- spec.
+ Pack_Id := Defining_Entity (Inst_Spec);
+ Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
- Par := Parent (Body_Decl);
- while Present (Par) loop
- if Nkind (Par) = N_Package_Body then
- Analyze_Package_Body_Contract
- (Body_Id => Defining_Entity (Par),
- Freeze_Id => Defining_Entity (Body_Decl));
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related package.
- exit;
- end if;
+ Set_SPARK_Mode (Pack_Id);
- Par := Parent (Par);
- end loop;
+ -- Check whether the lack of indicator Part_Of agrees with the placement
+ -- of the package instantiation with respect to the state space. Nested
+ -- package instantiations do not need to be checked because they inherit
+ -- Part_Of indicator of the outermost package instantiation (see routine
+ -- Propagate_Part_Of in Sem_Prag).
- -- Analyze the contracts of all eligible construct up to the body which
- -- caused the "freezing".
+ if In_Instance then
+ null;
- if Is_List_Member (Body_Decl) then
- Analyze_Contracts
- (L => List_Containing (Body_Decl),
- Freeze_Nod => Body_Decl,
- Freeze_Id => Body_Id);
+ elsif No (Prag) then
+ Check_Missing_Part_Of (Pack_Id);
end if;
- end Analyze_Previous_Contracts;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ end Analyze_Package_Instantiation_Contract;
--------------------------------
-- Analyze_Protected_Contract --
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
Items : constant Node_Id := Contract (Prot_Id);
- Mode : SPARK_Mode_Type;
begin
-- Do not analyze a contract multiple times
Set_Analyzed (Items);
end if;
end if;
-
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related protected unit.
-
- Save_SPARK_Mode_And_Set (Prot_Id, Mode);
-
- -- A protected type must define full default initialization
- -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as
- -- it is not a standard Ada legality rule.
-
- if SPARK_Mode = On
- and then not Has_Full_Default_Initialization (Prot_Id)
- then
- Error_Msg_N
- ("protected type & must define full default initialization",
- Prot_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
end Analyze_Protected_Contract;
-------------------------------------------
-- Analyze_Task_Contract --
---------------------------
+ -- WARNING: This routine manages SPARK regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- SPARK mode.
+
procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
Items : constant Node_Id := Contract (Task_Id);
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
+
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save the SPARK_Mode-related data to restore on exit
+
+ Prag : Node_Id;
begin
-- Do not analyze a contract multiple times
-- context. To remedy this, restore the original SPARK_Mode of the
-- related task unit.
- Save_SPARK_Mode_And_Set (Task_Id, Mode);
+ Set_SPARK_Mode (Task_Id);
-- Analyze Global first, as Depends may mention items classified in the
-- global categorization.
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
- Restore_SPARK_Mode (Mode);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Task_Contract;
-----------------------------
-------------------------
function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
- function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
- -- Determine whether the body of procedure Proc_Id contains a sole
- -- null statement, possibly followed by an optional return.
-
function Has_Public_Visibility_Of_Subprogram return Boolean;
-- Determine whether type Typ has public visibility of subprogram
-- Subp_Id.
- -------------------
- -- Has_Null_Body --
- -------------------
-
- function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
- Body_Id : Entity_Id;
- Decl : Node_Id;
- Spec : Node_Id;
- Stmt1 : Node_Id;
- Stmt2 : Node_Id;
-
- begin
- Spec := Parent (Proc_Id);
- Decl := Parent (Spec);
-
- -- Retrieve the entity of the invariant procedure body
-
- if Nkind (Spec) = N_Procedure_Specification
- and then Nkind (Decl) = N_Subprogram_Declaration
- then
- Body_Id := Corresponding_Body (Decl);
-
- -- The body acts as a spec
-
- else
- Body_Id := Proc_Id;
- end if;
-
- -- The body will be generated later
-
- if No (Body_Id) then
- return False;
- end if;
-
- Spec := Parent (Body_Id);
- Decl := Parent (Spec);
-
- pragma Assert
- (Nkind (Spec) = N_Procedure_Specification
- and then Nkind (Decl) = N_Subprogram_Body);
-
- Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
-
- -- Look for a null statement followed by an optional return
- -- statement.
-
- if Nkind (Stmt1) = N_Null_Statement then
- Stmt2 := Next (Stmt1);
-
- if Present (Stmt2) then
- return Nkind (Stmt2) = N_Simple_Return_Statement;
- else
- return True;
- end if;
- end if;
-
- return False;
- end Has_Null_Body;
-
-----------------------------------------
-- Has_Public_Visibility_Of_Subprogram --
-----------------------------------------
return False;
-- Determine whether the subprogram is declared in the visible
- -- declarations of the package containing the type.
+ -- declarations of the package containing the type, or in the
+ -- visible declaration of a child unit of that package.
else
- return List_Containing (Subp_Decl) =
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Scope (Typ))));
+ declare
+ Decls : constant List_Id :=
+ List_Containing (Subp_Decl);
+ Subp_Scope : constant Entity_Id :=
+ Scope (Defining_Entity (Subp_Decl));
+ Typ_Scope : constant Entity_Id := Scope (Typ);
+
+ begin
+ return
+ Decls = Visible_Declarations
+ (Specification (Unit_Declaration_Node (Typ_Scope)))
+
+ or else
+ (Ekind (Subp_Scope) = E_Package
+ and then Typ_Scope /= Subp_Scope
+ and then Is_Child_Unit (Subp_Scope)
+ and then
+ Is_Ancestor_Package (Typ_Scope, Subp_Scope)
+ and then
+ Decls = Visible_Declarations
+ (Specification
+ (Unit_Declaration_Node (Subp_Scope))));
+ end;
end if;
end Has_Public_Visibility_Of_Subprogram;
-- Local variables
- Loc : constant Source_Ptr := Sloc (Body_Decl);
- Params : List_Id := No_List;
- Proc_Bod : Node_Id;
- Proc_Id : Entity_Id;
+ 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;
-- Start of processing for Build_Postconditions_Procedure
Set_Debug_Info_Needed (Proc_Id);
Set_Postconditions_Proc (Subp_Id, Proc_Id);
+ -- Force the front-end inlining of _Postconditions when generating C
+ -- code, since its body may have references to itypes defined in the
+ -- enclosing subprogram, which would cause problems for unnesting
+ -- routines in the absence of inlining.
+
+ if Modify_Tree_For_C then
+ Set_Has_Pragma_Inline (Proc_Id);
+ Set_Has_Pragma_Inline_Always (Proc_Id);
+ Set_Is_Inlined (Proc_Id);
+ end if;
+
-- The related subprogram is a function: create the specification of
-- parameter _Result.
New_Occurrence_Of (Etype (Result), Loc)));
end if;
+ Proc_Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => Params);
+
+ Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
+
-- Insert _Postconditions before the first source declaration of the
-- body. This ensures that the body will not cause any premature
-- freezing, as it may mention types:
-- 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);
+
-- 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
Proc_Bod :=
Make_Subprogram_Body (Loc,
Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => Params),
-
+ Copy_Subprogram_Spec (Proc_Spec),
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => Stmts,
End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
- Insert_Before_First_Source_Declaration (Proc_Bod);
- Analyze (Proc_Bod);
+ Insert_After_And_Analyze (Proc_Decl, Proc_Bod);
end Build_Postconditions_Procedure;
----------------------------
if Present (Items) then
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
+ if Pragma_Name (Prag) = Name_Contract_Cases
+ and then Is_Checked (Prag)
+ then
Expand_Pragma_Contract_Cases
(CCs => Prag,
Subp_Id => Subp_Id,
end if;
end Process_Contract_Cases_For;
+ pragma Unmodified (Stmts);
+ -- Stmts is passed as IN OUT to signal that the list can be updated,
+ -- even if the corresponding integer value representing the list does
+ -- not change.
+
-- Start of processing for Process_Contract_Cases
begin
if Present (Items) then
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Post_Nam then
+ if Pragma_Name (Prag) = Post_Nam
+ and then Is_Checked (Prag)
+ then
Append_Enabled_Item
(Item => Build_Pragma_Check_Equivalent (Prag),
List => Stmts);
-- Note that non-matching pragmas are skipped
if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Post_Nam then
+ if Pragma_Name (Decl) = Post_Nam
+ and then Is_Checked (Decl)
+ then
Append_Enabled_Item
(Item => Build_Pragma_Check_Equivalent (Decl),
List => Stmts);
procedure Process_Spec_Postconditions is
Subps : constant Subprogram_List :=
Inherited_Subprograms (Spec_Id);
+ Item : Node_Id;
Items : Node_Id;
Prag : Node_Id;
Subp_Id : Entity_Id;
if Present (Items) then
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition then
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then Is_Checked (Prag)
+ then
Append_Enabled_Item
(Item => Build_Pragma_Check_Equivalent (Prag),
List => Stmts);
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);
+ Item :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id);
+
+ -- The pragma Check equivalent of the class-wide
+ -- postcondition is still created even though the
+ -- pragma may be ignored because the equivalent
+ -- performs semantic checks.
+
+ if Is_Checked (Prag) then
+ Append_Enabled_Item (Item, Stmts);
+ end if;
end if;
Prag := Next_Pragma (Prag);
end loop;
end Process_Spec_Postconditions;
+ pragma Unmodified (Stmts);
+ -- Stmts is passed as IN OUT to signal that the list can be updated,
+ -- even if the corresponding integer value representing the list does
+ -- not change.
+
-- Start of processing for Process_Postconditions
begin
-- The insertion node after which all pragma Check equivalents are
-- inserted.
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
+ -- Determine whether arbitrary declaration Decl denotes a renaming of
+ -- a discriminant or protection field _object.
+
procedure 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
-- Collect all preconditions of subprogram Subp_Id and prepend their
-- pragma Check equivalents to the declarations of the body.
+ --------------------------
+ -- Is_Prologue_Renaming --
+ --------------------------
+
+ function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
+ Nam : Node_Id;
+ Obj : Entity_Id;
+ Pref : Node_Id;
+ Sel : Node_Id;
+
+ begin
+ if Nkind (Decl) = N_Object_Renaming_Declaration then
+ Obj := Defining_Entity (Decl);
+ Nam := Name (Decl);
+
+ if Nkind (Nam) = N_Selected_Component then
+ Pref := Prefix (Nam);
+ Sel := Selector_Name (Nam);
+
+ -- A discriminant renaming appears as
+ -- Discr : constant ... := Prefix.Discr;
+
+ if Ekind (Obj) = E_Constant
+ and then Is_Entity_Name (Sel)
+ and then Present (Entity (Sel))
+ and then Ekind (Entity (Sel)) = E_Discriminant
+ then
+ return True;
+
+ -- A protection field renaming appears as
+ -- Prot : ... := _object._object;
+
+ -- A renamed private component is just a component of
+ -- _object, with an arbitrary name.
+
+ elsif Ekind (Obj) = 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;
+
+ return False;
+ end Is_Prologue_Renaming;
+
-------------------------
-- Merge_Preconditions --
-------------------------
----------------------
procedure Prepend_To_Decls (Item : Node_Id) is
- Decls : List_Id := Declarations (Body_Decl);
+ Decls : List_Id;
begin
+ Decls := Declarations (Body_Decl);
+
-- Ensure that the body has a declarative list
if No (Decls) then
-------------------------------------
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;
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+
+ Item : Node_Id;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
begin
-- Process the contracts of all inherited subprograms, looking for
if Pragma_Name (Prag) = Name_Precondition
and then Class_Present (Prag)
then
- Check_Prag :=
+ Item :=
Build_Pragma_Check_Equivalent
(Prag => Prag,
Subp_Id => Spec_Id,
Inher_Id => Subp_Id);
- -- The spec of an inherited subprogram already yielded
- -- a class-wide precondition. Merge the existing
- -- precondition with the current one using "or else".
+ -- The pragma Check equivalent of the class-wide
+ -- precondition is still created even though the
+ -- pragma may be ignored because the equivalent
+ -- performs semantic checks.
+
+ if Is_Checked (Prag) then
- if Present (Class_Pre) then
- Merge_Preconditions (Check_Prag, Class_Pre);
- else
- Class_Pre := Check_Prag;
+ -- The spec of an inherited subprogram already
+ -- yielded a class-wide precondition. Merge the
+ -- existing precondition with the current one
+ -- using "or else".
+
+ if Present (Class_Pre) then
+ Merge_Preconditions (Item, Class_Pre);
+ else
+ Class_Pre := Item;
+ end if;
end if;
end if;
procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
Items : constant Node_Id := Contract (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
Decl : Node_Id;
+ Freeze_T : Boolean;
Prag : Node_Id;
- Subp_Decl : Node_Id;
begin
- -- Process the contract
+ -- Process the contract. If the body is an expression function
+ -- that is a completion, freeze types within, because this may
+ -- not have been done yet, when the subprogram declaration and
+ -- its completion by an expression function appear in distinct
+ -- declarative lists of the same unit (visible and private).
+
+ Freeze_T :=
+ Was_Expression_Function (Body_Decl)
+ and then Sloc (Body_Id) /= Sloc (Subp_Id)
+ and then In_Same_Source_Unit (Body_Id, Subp_Id)
+ and then List_Containing (Body_Decl) /=
+ List_Containing (Subp_Decl)
+ and then not In_Instance;
if Present (Items) then
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition then
+ if Pragma_Name (Prag) = Name_Precondition
+ and then Is_Checked (Prag)
+ then
+ if Freeze_T
+ and then Present (Corresponding_Aspect (Prag))
+ then
+ Freeze_Expr_Types
+ (Def_Id => Subp_Id,
+ Typ => Standard_Boolean,
+ Expr => Expression (Corresponding_Aspect (Prag)),
+ N => Body_Decl);
+ end if;
+
Prepend_To_Decls_Or_Save (Prag);
end if;
-- 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
-- Note that non-matching pragmas are skipped
if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Name_Precondition then
+ if Pragma_Name (Decl) = Name_Precondition
+ and then Is_Checked (Decl)
+ then
Prepend_To_Decls_Or_Save (Decl);
end if;
-- Start of processing for Process_Preconditions
begin
- -- Find the last internally generated declaration, starting from the
- -- top of the body declarations. This ensures that discriminals and
- -- subtypes are properly visible to the pragma Check equivalents.
+ -- Find the proper insertion point for all pragma Check equivalents
if Present (Decls) then
Decl := First (Decls);
while Present (Decl) loop
- exit when Comes_From_Source (Decl);
- Insert_Node := Decl;
+
+ -- First source declaration terminates the search, because all
+ -- preconditions must be evaluated prior to it, by definition.
+
+ if Comes_From_Source (Decl) then
+ exit;
+
+ -- 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.
+
+ elsif Is_Prologue_Renaming (Decl) then
+ while Present (Next (Decl))
+ and then Is_Prologue_Renaming (Next (Decl))
+ loop
+ Next (Decl);
+ end loop;
+
+ Insert_Node := Decl;
+
+ -- 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.
+
+ else
+ exit;
+ end if;
+
Next (Decl);
end loop;
end if;
elsif Is_Ignored_Ghost_Entity (Subp_Id) then
return;
- 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).
- if Has_Expanded_Contract (Subp_Id) then
+ elsif Has_Expanded_Contract (Subp_Id) then
return;
+ end if;
- -- Otherwise mark the subprogram
+ -- Prevent multiple expansion attempts of the same contract
- else
- Set_Has_Expanded_Contract (Subp_Id);
- end if;
+ Set_Has_Expanded_Contract (Subp_Id);
-- Ensure that the formal parameters are visible when expanding all
-- contract items.
end if;
end Expand_Subprogram_Contract;
+ -------------------------------
+ -- Freeze_Previous_Contracts --
+ -------------------------------
+
+ procedure Freeze_Previous_Contracts (Body_Decl : Node_Id) is
+ function Causes_Contract_Freezing (N : Node_Id) return Boolean;
+ pragma Inline (Causes_Contract_Freezing);
+ -- Determine whether arbitrary node N causes contract freezing
+
+ procedure Freeze_Contracts;
+ pragma Inline (Freeze_Contracts);
+ -- Freeze the contracts of all eligible constructs which precede body
+ -- Body_Decl.
+
+ procedure Freeze_Enclosing_Package_Body;
+ pragma Inline (Freeze_Enclosing_Package_Body);
+ -- Freeze the contract of the nearest package body (if any) which
+ -- encloses body Body_Decl.
+
+ ------------------------------
+ -- Causes_Contract_Freezing --
+ ------------------------------
+
+ function Causes_Contract_Freezing (N : Node_Id) return Boolean is
+ begin
+ return Nkind_In (N, N_Entry_Body,
+ N_Package_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub,
+ N_Task_Body);
+ end Causes_Contract_Freezing;
+
+ ----------------------
+ -- Freeze_Contracts --
+ ----------------------
+
+ procedure Freeze_Contracts is
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+ Decl : Node_Id;
+
+ begin
+ -- Nothing to do when the body which causes freezing does not appear
+ -- in a declarative list because there cannot possibly be constructs
+ -- with contracts.
+
+ if not Is_List_Member (Body_Decl) then
+ return;
+ end if;
+
+ -- Inspect the declarations preceding the body, and freeze individual
+ -- contracts of eligible constructs.
+
+ Decl := Prev (Body_Decl);
+ while Present (Decl) loop
+
+ -- Stop the traversal when a preceding construct that causes
+ -- freezing is encountered as there is no point in refreezing
+ -- the already frozen constructs.
+
+ if Causes_Contract_Freezing (Decl) then
+ exit;
+
+ -- Entry or subprogram declarations
+
+ elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id => Defining_Entity (Decl),
+ Freeze_Id => Body_Id);
+
+ -- Objects
+
+ elsif Nkind (Decl) = N_Object_Declaration then
+ Analyze_Object_Contract
+ (Obj_Id => Defining_Entity (Decl),
+ Freeze_Id => Body_Id);
+
+ -- Protected units
+
+ elsif Nkind_In (Decl, N_Protected_Type_Declaration,
+ N_Single_Protected_Declaration)
+ then
+ Analyze_Protected_Contract (Defining_Entity (Decl));
+
+ -- Subprogram body stubs
+
+ elsif Nkind (Decl) = N_Subprogram_Body_Stub then
+ Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+
+ -- Task units
+
+ elsif Nkind_In (Decl, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
+ Analyze_Task_Contract (Defining_Entity (Decl));
+ end if;
+
+ Prev (Decl);
+ end loop;
+ end Freeze_Contracts;
+
+ -----------------------------------
+ -- Freeze_Enclosing_Package_Body --
+ -----------------------------------
+
+ procedure Freeze_Enclosing_Package_Body is
+ Orig_Decl : constant Node_Id := Original_Node (Body_Decl);
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for an enclosing package body. Do
+ -- not use the scope stack, because a body utilizes the entity of its
+ -- corresponding spec.
+
+ Par := Parent (Body_Decl);
+ while Present (Par) loop
+ if Nkind (Par) = N_Package_Body then
+ Analyze_Package_Body_Contract
+ (Body_Id => Defining_Entity (Par),
+ Freeze_Id => Defining_Entity (Body_Decl));
+
+ exit;
+
+ -- Do not look for an enclosing package body when the construct
+ -- which causes freezing is a body generated for an expression
+ -- function and it appears within a package spec. This ensures
+ -- that the traversal will not reach too far up the parent chain
+ -- and attempt to freeze a package body which must not be frozen.
+
+ -- package body Enclosing_Body
+ -- with Refined_State => (State => Var)
+ -- is
+ -- package Nested is
+ -- type Some_Type is ...;
+ -- function Cause_Freezing return ...;
+ -- private
+ -- function Cause_Freezing is (...);
+ -- end Nested;
+ --
+ -- Var : Nested.Some_Type;
+
+ elsif Nkind (Par) = N_Package_Declaration
+ and then Nkind (Orig_Decl) = N_Expression_Function
+ then
+ exit;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+ end Freeze_Enclosing_Package_Body;
+
+ -- Local variables
+
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+
+ -- Start of processing for Freeze_Previous_Contracts
+
+ begin
+ pragma Assert (Causes_Contract_Freezing (Body_Decl));
+
+ -- A body that is in the process of being inlined appears from source,
+ -- but carries name _parent. Such a body does not cause freezing of
+ -- contracts.
+
+ if Chars (Body_Id) = Name_uParent then
+ return;
+ end if;
+
+ Freeze_Enclosing_Package_Body;
+ Freeze_Contracts;
+ end Freeze_Previous_Contracts;
+
---------------------------------
-- Inherit_Subprogram_Contract --
---------------------------------
projects / thirdparty / gcc.git / blobdiff