+2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * contracts.ads, contracts.adb: New unit.
+ * exp_ch6.adb Add with and use clauses for Contracts.
+ (Expand_Subprogram_Contract): Moved to Contracts.
+ * exp_ch6.ads (Expand_Subprogram_Contract): Moved to Contracts.
+ * sem_ch3.adb Add with and use clauses for Contracts.
+ (Analyze_Object_Contract): Moved to Contracts.
+ (Analyze_Declarations): Remove local variable Pack_Decl. Do not
+ capture global references in contracts. Check the hidden states
+ of a package body.
+ * sem_ch6.adb Add with and use clauses in Contracts.
+ (Analyze_Generic_Subprogram_Body): Do not capture global
+ references in contracts.
+ (Analyze_Subprogram_Body_Contract):
+ Moved to Contracts.
+ (Analyze_Subprogram_Body_Helper): Freeze the
+ contract of the nearest enclosing package body. Always analyze
+ the subprogram body contract. Do not expand the subprogram
+ body contract.
+ (Analyze_Subprogram_Contract): Moved to Contracts.
+ * sem_ch6.ads (Analyze_Subprogram_Body_Contract): Moved to Contracts.
+ (Analyze_Subprogram_Contract): Moved to Contracts.
+ * sem_ch7.adb Add with and use clauses for Contracts.
+ (Analyze_Package_Body_Contract): Moved to Contracts.
+ (Analyze_Package_Body_Helper): Freeze the contract of the
+ nearest enclosing package body.
+ (Analyze_Package_Contract): Moved to Contracts.
+ * sem_ch7.ads (Analyze_Package_Body_Contract): Moved to Contracts.
+ (Analyze_Package_Contract): Moved to Contracts.
+ * sem_ch10.adb Add with and use clauses for Contracts.
+ (Analyze_Compilation_Unit): Do not capture global references
+ in contracts.
+ (Analyze_Subprogram_Body_Stub_Contract): Moved to Contracts.
+ * sem_ch10.ads (Analyze_Subprogram_Body_Stub_Contract): Moved
+ to Contracts.
+ * sem_ch12.adb Add with and use clauses for Contracts.
+ (Analyze_Subprogram_Instantiation): Update the call to
+ Instantiate_Subprogram_Contract.
+ (Instantiate_Package_Body):
+ Do not copy the entity of the spec when creating an entity
+ for the body. Construct a brand new defining identifier for
+ the body and inherit the Comes_From_Source flag from the spec.
+ (Instantiate_Subprogram_Body): Remove Anon_Id to Act_Decl_Id
+ and update all occurrences. Construct a brand new defining
+ identifier for the body and inherit the Comes_From_Source
+ flag from the spec.
+ (Instantiate_Subprogram_Contract): Moved
+ to Contracts.
+ (Save_Global_References_In_Aspects): Moved to
+ the spec of Sem_Ch12.
+ (Save_Global_References_In_Contract):
+ Moved to Contracts.
+ * sem_ch12.ads (Save_Global_References_In_Aspects): Moved from
+ the body of Sem_Ch12.
+ (Save_Global_References_In_Contract):
+ Moved to Contracts.
+ * sem_prag.adb Add with and use clauses for Contracts.
+ (Add_Item): Removed. All references to this routine have been
+ replaced with calls to Append_New_Elmt.
+ (Analyze_Constituent):
+ Add special diagnostics for errors caused by freezing of
+ contracts.
+ (Analyze_Refined_State_In_Decl_Part): Add formal
+ parameter Freeze_Id. Add new global variable Freeze_Posted.
+ (Collect_Body_States): Removed.
+ (Report_Unused_States): Removed.
+ * sem_prag.ads (Analyze_Defined_State_In_Decl_Part): Add formal
+ parameter Freeze_Id and update comment on usage.
+ * sem_util.adb Remove with and use clauses for
+ Sem_Ch12.
+ (Add_Contract_Item): Moved to Contracts.
+ (Check_Unused_Body_States): New routine.
+ (Collect_Body_States):
+ New routine.
+ (Create_Generic_Contract): Moved to Contracts.
+ (Inherit_Subprogram_Contract): Moved to Contracts.
+ (Report_Unused_Body_States): New routine.
+ * sem_util.ads (Add_Contract_Item): Moved to Contracts.
+ (Check_Unused_Body_States): New routine.
+ (Collect_Body_States): New routine.
+ (Create_Generic_Contract): Moved to Contracts.
+ (Inherit_Subprogram_Contract): Moved to Contracts.
+ (Report_Unused_Body_States): New routine.
+ * sinfo.adb (Is_Expanded_Contract): New routine.
+ (Set_Is_Expanded_Contract): New routine.
+ * sinfo.ads New attribute Is_Expanded_Contract along with
+ placement in nodes.
+ (Is_Expanded_Contract): New routine along
+ with pragma Inline.
+ (Set_Is_Expanded_Contract): New routine
+ along with pragma Inline.
+ * gcc-interface/Make-lang.in: Add entry for contracts.o
+
+2015-10-23 Bob Duff <duff@adacore.com>
+
+ * bindgen.adb, init.c, opt.ads, switch-b.adb: Implement new -Ea and
+ -Es switches.
+ * switch-b.ads: Minor comment fix.
+ * bindusg.adb: Document new -Ea and -Es switches.
+ * s-exctra.ads: Use -Es instead of -E.
+
2015-10-23 Tristan Gingold <gingold@adacore.com>
* gcc-interface/utils2.c (build_call_alloc_dealloc): Check no implicit
-- Num_Interrupt_States : Integer;
-- Unreserve_All_Interrupts : Integer;
-- Exception_Tracebacks : Integer;
+ -- Exception_Tracebacks_Symbolic : Integer;
-- Detect_Blocking : Integer;
-- Default_Stack_Size : Integer;
-- Leap_Seconds_Support : Integer;
-- Unreserve_All_Interrupts is set to one if at least one unit in the
-- partition had a pragma Unreserve_All_Interrupts, and zero otherwise.
- -- Exception_Tracebacks is set to one if the -E parameter was present
- -- in the bind and to zero otherwise. Note that on some targets exception
- -- tracebacks are provided by default, so a value of zero for this
- -- parameter does not necessarily mean no trace backs are available.
+ -- Exception_Tracebacks is set to one if the -Ea or -E parameter was
+ -- present in the bind and to zero otherwise. Note that on some targets
+ -- exception tracebacks are provided by default, so a value of zero for
+ -- this parameter does not necessarily mean no trace backs are available.
+
+ -- Exception_Tracebacks_Symbolic is set to one if the -Es parameter was
+ -- present in the bind and to zero otherwise.
-- Detect_Blocking indicates whether pragma Detect_Blocking is active or
-- not. A value of zero indicates that the pragma is not present, while a
WBI (" pragma Import (C, Unreserve_All_Interrupts, " &
"""__gl_unreserve_all_interrupts"");");
- if Exception_Tracebacks then
+ if Exception_Tracebacks or Exception_Tracebacks_Symbolic then
WBI (" Exception_Tracebacks : Integer;");
WBI (" pragma Import (C, Exception_Tracebacks, " &
"""__gl_exception_tracebacks"");");
+
+ if Exception_Tracebacks_Symbolic then
+ WBI (" Exception_Tracebacks_Symbolic : Integer;");
+ WBI (" pragma Import (C, Exception_Tracebacks_Symbolic, " &
+ """__gl_exception_tracebacks_symbolic"");");
+ end if;
end if;
WBI (" Detect_Blocking : Integer;");
Set_Char (';');
Write_Statement_Buffer;
- if Exception_Tracebacks then
+ if Exception_Tracebacks or Exception_Tracebacks_Symbolic then
WBI (" Exception_Tracebacks := 1;");
+
+ if Exception_Tracebacks_Symbolic then
+ WBI (" Exception_Tracebacks_Symbolic := 1;");
+ end if;
end if;
Set_String (" Detect_Blocking := ");
-- Line for -E switch
- Write_Line (" -E Store tracebacks in exception occurrences");
+ Write_Line (" -Ea Store tracebacks in exception occurrences");
+ Write_Line (" -Es Store tracebacks in exception occurrences,");
+ Write_Line (" and enable symbolic tracebacks");
+ Write_Line (" -E Same as -Ea");
-- The -f switch is voluntarily omitted, because it is obsolete
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- C O N T R A C T S --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2015, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Exp_Prag; use Exp_Prag;
+with Exp_Tss; use Exp_Tss;
+with Exp_Util; use Exp_Util;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch12; use Sem_Ch12;
+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 Stringt; use Stringt;
+with Tbuild; use Tbuild;
+
+package body Contracts is
+
+ 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
+ -- well as Contract_Cases, invariants and predicates. Body_Id denotes the
+ -- entity of the subprogram body.
+
+ -----------------------
+ -- Add_Contract_Item --
+ -----------------------
+
+ procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
+ Items : Node_Id := Contract (Id);
+
+ procedure Add_Classification;
+ -- Prepend Prag to the list of classifications
+
+ procedure Add_Contract_Test_Case;
+ -- Prepend Prag to the list of contract and test cases
+
+ procedure Add_Pre_Post_Condition;
+ -- Prepend Prag to the list of pre- and postconditions
+
+ ------------------------
+ -- Add_Classification --
+ ------------------------
+
+ procedure Add_Classification is
+ begin
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
+ end Add_Classification;
+
+ ----------------------------
+ -- Add_Contract_Test_Case --
+ ----------------------------
+
+ procedure Add_Contract_Test_Case is
+ begin
+ Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
+ Set_Contract_Test_Cases (Items, Prag);
+ end Add_Contract_Test_Case;
+
+ ----------------------------
+ -- Add_Pre_Post_Condition --
+ ----------------------------
+
+ procedure Add_Pre_Post_Condition is
+ begin
+ Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
+ Set_Pre_Post_Conditions (Items, Prag);
+ end Add_Pre_Post_Condition;
+
+ -- 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);
+
+ -- Create a new contract when adding the first item
+
+ if No (Items) then
+ Items := Make_Contract (Sloc (Id));
+ Set_Contract (Id, Items);
+ end if;
+
+ -- Contract items related to constants. Applicable pragmas are:
+ -- Part_Of
+
+ if Ekind (Id) = E_Constant then
+ if Prag_Nam = Name_Part_Of then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to [generic] packages or instantiations. The
+ -- applicable pragmas are:
+ -- Abstract_States
+ -- Initial_Condition
+ -- Initializes
+ -- Part_Of (instantiation only)
+
+ elsif Ekind_In (Id, E_Generic_Package, E_Package) then
+ if Nam_In (Prag_Nam, Name_Abstract_State,
+ Name_Initial_Condition,
+ Name_Initializes)
+ then
+ Add_Classification;
+
+ -- Indicator Part_Of must be associated with a package instantiation
+
+ elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to package bodies. The applicable pragmas are:
+ -- Refined_States
+
+ elsif Ekind (Id) = E_Package_Body then
+ if Prag_Nam = Name_Refined_State then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to subprogram or entry declarations. The
+ -- applicable pragmas are:
+ -- Contract_Cases
+ -- Depends
+ -- Extensions_Visible
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
+ -- Volatile_Function
+
+ elsif Ekind_In (Id, E_Entry, E_Entry_Family)
+ or else Is_Generic_Subprogram (Id)
+ or else Is_Subprogram (Id)
+ then
+ if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
+ Add_Pre_Post_Condition;
+
+ elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
+ Add_Contract_Test_Case;
+
+ elsif Nam_In (Prag_Nam, Name_Depends,
+ Name_Extensions_Visible,
+ Name_Global)
+ then
+ Add_Classification;
+
+ elsif Prag_Nam = Name_Volatile_Function
+ and then Ekind_In (Id, E_Function, E_Generic_Function)
+ then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to subprogram bodies. Applicable pragmas are:
+ -- Postcondition
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+
+ elsif Ekind (Id) = E_Subprogram_Body then
+ if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
+ Add_Classification;
+
+ elsif Nam_In (Prag_Nam, Name_Postcondition,
+ Name_Precondition,
+ Name_Refined_Post)
+ then
+ Add_Pre_Post_Condition;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to variables. Applicable pragmas are:
+ -- Async_Readers
+ -- Async_Writers
+ -- Constant_After_Elaboration
+ -- Effective_Reads
+ -- Effective_Writes
+ -- Part_Of
+
+ elsif Ekind (Id) = E_Variable then
+ if Nam_In (Prag_Nam, Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Constant_After_Elaboration,
+ Name_Effective_Reads,
+ Name_Effective_Writes,
+ Name_Part_Of)
+ then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+ end if;
+ end Add_Contract_Item;
+
+ ---------------------------------------------
+ -- Analyze_Enclosing_Package_Body_Contract --
+ ---------------------------------------------
+
+ procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id) is
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for an enclosing body. Do not use the
+ -- scope stack as a body uses 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));
+
+ return;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+ end Analyze_Enclosing_Package_Body_Contract;
+
+ -----------------------------
+ -- Analyze_Object_Contract --
+ -----------------------------
+
+ procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
+ Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Seen : Boolean := False;
+
+ begin
+ -- The loop parameter in an element iterator over a formal container
+ -- is declared with an object declaration but no contracts apply.
+
+ if Ekind (Obj_Id) = E_Loop_Parameter then
+ return;
+ end if;
+
+ -- Do not analyze a contract mutiple times
+
+ Items := Contract (Obj_Id);
+
+ if Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ Set_Analyzed (Items);
+ end if;
+ end if;
+
+ -- Constant related checks
+
+ if Ekind (Obj_Id) = E_Constant then
+
+ -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
+ -- This check is relevant only when SPARK_Mode is on as it is not a
+ -- standard Ada legality rule. Internally-generated constants that
+ -- map generic formals to actuals in instantiations are allowed to
+ -- be volatile.
+
+ if SPARK_Mode = On
+ and then Comes_From_Source (Obj_Id)
+ and then Is_Effectively_Volatile (Obj_Id)
+ and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
+ then
+ Error_Msg_N ("constant cannot be volatile", Obj_Id);
+ end if;
+
+ -- Variable related checks
+
+ else pragma Assert (Ekind (Obj_Id) = E_Variable);
+
+ -- The following checks are relevant only when SPARK_Mode is on as
+ -- they are not standard Ada legality rules. Internally generated
+ -- temporaries are ignored.
+
+ if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
+ if Is_Effectively_Volatile (Obj_Id) then
+
+ -- The declaration of an effectively volatile object must
+ -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
+
+ if not Is_Library_Level_Entity (Obj_Id) then
+ Error_Msg_N
+ ("volatile variable & must be declared at library level",
+ Obj_Id);
+
+ -- An object of a discriminated type cannot be effectively
+ -- volatile except for protected objects (SPARK RM 7.1.3(5)).
+
+ elsif Has_Discriminants (Obj_Typ)
+ and then not Is_Protected_Type (Obj_Typ)
+ 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
+
+ else
+ -- A non-effectively volatile object cannot have effectively
+ -- volatile components (SPARK RM 7.1.3(6)).
+
+ if not Is_Effectively_Volatile (Obj_Id)
+ and then Has_Volatile_Component (Obj_Typ)
+ then
+ Error_Msg_N
+ ("non-volatile object & cannot have volatile components",
+ Obj_Id);
+ end if;
+ end if;
+ end if;
+
+ if Is_Ghost_Entity (Obj_Id) then
+
+ -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
+
+ if Is_Effectively_Volatile (Obj_Id) then
+ Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+
+ -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
+
+ elsif Is_Imported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
+
+ elsif Is_Exported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
+ end if;
+ end if;
+
+ -- Analyze all external properties
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+ Seen := True;
+ end if;
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+ Seen := True;
+ end if;
+
+ -- Verify the mutual interaction of the various external properties
+
+ if Seen then
+ Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+ end if;
+ end if;
+
+ -- Check whether the lack of indicator Part_Of agrees with the placement
+ -- of the object with respect to the state space.
+
+ Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
+
+ if No (Prag) then
+ Check_Missing_Part_Of (Obj_Id);
+ end if;
+
+ -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
+ -- exception to this is the object that represents the dispatch table of
+ -- a Ghost tagged type as the symbol needs to be exported.
+
+ if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
+ if Is_Exported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
+
+ elsif Is_Imported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ end if;
+ end if;
+ end Analyze_Object_Contract;
+
+ -----------------------------------
+ -- Analyze_Package_Body_Contract --
+ -----------------------------------
+
+ procedure Analyze_Package_Body_Contract
+ (Body_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ 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;
+ Ref_State : Node_Id;
+
+ begin
+ -- Do not analyze a contract mutiple times
+
+ if Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ 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 package body.
+
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
+ Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
+
+ -- The analysis of pragma Refined_State detects whether the spec has
+ -- abstract states available for refinement.
+
+ 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 envorced 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);
+
+ -- Capture all global references in a generic package body now that the
+ -- contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Body_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Body_Decl),
+ Gen_Id => Spec_Id);
+ end if;
+ end Analyze_Package_Body_Contract;
+
+ ------------------------------
+ -- Analyze_Package_Contract --
+ ------------------------------
+
+ 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);
+ Init : Node_Id := Empty;
+ Init_Cond : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+
+ begin
+ -- Do not analyze a contract mutiple times
+
+ if Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ 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 package.
+
+ Save_SPARK_Mode_And_Set (Pack_Id, Mode);
+
+ if Present (Items) then
+
+ -- Locate and store pragmas Initial_Condition and Initializes since
+ -- their order of analysis matters.
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Initial_Condition then
+ Init_Cond := Prag;
+
+ elsif Prag_Nam = Name_Initializes then
+ Init := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze the initialization related pragmas. Initializes must come
+ -- before Initial_Condition due to item dependencies.
+
+ if Present (Init) then
+ Analyze_Initializes_In_Decl_Part (Init);
+ end if;
+
+ if Present (Init_Cond) then
+ Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
+ 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);
+
+ -- Capture all global references in a generic package now that the
+ -- contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Pack_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Pack_Decl),
+ Gen_Id => Pack_Id);
+ end if;
+ end Analyze_Package_Contract;
+
+ --------------------------------------
+ -- Analyze_Subprogram_Body_Contract --
+ --------------------------------------
+
+ procedure Analyze_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 := Corresponding_Spec_Of (Body_Decl);
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+ Ref_Depends : Node_Id := Empty;
+ Ref_Global : Node_Id := Empty;
+
+ begin
+ -- When a subprogram body declaration is illegal, its defining entity is
+ -- left unanalyzed. There is nothing left to do in this case because the
+ -- body lacks a contract, or even a proper Ekind.
+
+ if Ekind (Body_Id) = E_Void then
+ return;
+
+ -- Do not analyze a contract mutiple times
+
+ elsif Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ 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 subprogram body.
+
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
+
+ if not Has_Significant_Contract (Body_Id) then
+ null;
+
+ -- The subprogram body is a completion, analyze all delayed pragmas that
+ -- apply. Note that when the body is stand alone, the pragmas are always
+ -- analyzed on the spot.
+
+ elsif Present (Items) then
+
+ -- Locate and store pragmas Refined_Depends and Refined_Global since
+ -- their order of analysis matters.
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Refined_Depends then
+ Ref_Depends := Prag;
+
+ elsif Prag_Nam = Name_Refined_Global then
+ Ref_Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze Refined_Global first as Refined_Depends may mention items
+ -- classified in the global refinement.
+
+ if Present (Ref_Global) then
+ Analyze_Refined_Global_In_Decl_Part (Ref_Global);
+ end if;
+
+ -- Refined_Depends must be analyzed after Refined_Global in order to
+ -- see the modes of all global refinements.
+
+ if Present (Ref_Depends) then
+ Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+ end if;
+ end if;
+
+ -- Ensure that the contract cases or postconditions mention 'Result or
+ -- define a post-state.
+
+ Check_Result_And_Post_State (Body_Id);
+
+ -- A stand alone non-volatile function body cannot have an effectively
+ -- 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.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Body_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Body_Id);
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+
+ -- Capture all global references in a generic subprogram body now that
+ -- the contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Body_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Body_Decl),
+ Gen_Id => Spec_Id);
+ end if;
+
+ -- Deal with preconditions, [refined] postconditions, Contract_Cases,
+ -- invariants and predicates associated with body and its spec. Do not
+ -- expand the contract of subprogram body stubs.
+
+ if Nkind (Body_Decl) = N_Subprogram_Body then
+ Expand_Subprogram_Contract (Body_Id);
+ end if;
+ end Analyze_Subprogram_Body_Contract;
+
+ ---------------------------------
+ -- Analyze_Subprogram_Contract --
+ ---------------------------------
+
+ procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+
+ begin
+ -- Do not analyze a contract mutiple times
+
+ if Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ 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 subprogram body.
+
+ Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
+
+ if not Has_Significant_Contract (Subp_Id) then
+ null;
+
+ elsif Present (Items) then
+
+ -- Analyze pre- and postconditions
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze contract-cases and test-cases
+
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Contract_Cases then
+ Analyze_Contract_Cases_In_Decl_Part (Prag);
+ else
+ pragma Assert (Prag_Nam = Name_Test_Case);
+ Analyze_Test_Case_In_Decl_Part (Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze classification pragmas
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Depends then
+ Depends := Prag;
+
+ elsif Prag_Nam = Name_Global then
+ Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze Global first as Depends may mention items classified in
+ -- the global categorization.
+
+ if Present (Global) then
+ Analyze_Global_In_Decl_Part (Global);
+ end if;
+
+ -- Depends must be analyzed after Global in order to see the modes of
+ -- all global items.
+
+ if Present (Depends) then
+ Analyze_Depends_In_Decl_Part (Depends);
+ end if;
+
+ -- Ensure that the contract cases or postconditions mention 'Result
+ -- or define a post-state.
+
+ Check_Result_And_Post_State (Subp_Id);
+ end if;
+
+ -- A non-volatile function cannot have an effectively 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 pragma Volatile_Function is processed
+ -- after the analysis of the related subprogram declaration.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Subp_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Subp_Id);
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+
+ -- Capture all global references in a generic subprogram now that the
+ -- contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Subp_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Subp_Decl),
+ Gen_Id => Subp_Id);
+ end if;
+ end Analyze_Subprogram_Contract;
+
+ -------------------------------------------
+ -- Analyze_Subprogram_Body_Stub_Contract --
+ -------------------------------------------
+
+ procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
+ Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
+
+ begin
+ -- A subprogram body stub may act as its own spec or as the completion
+ -- of a previous declaration. Depending on the context, the contract of
+ -- the stub may contain two sets of pragmas.
+
+ -- The stub is a completion, the applicable pragmas are:
+ -- Refined_Depends
+ -- Refined_Global
+
+ if Present (Spec_Id) then
+ Analyze_Subprogram_Body_Contract (Stub_Id);
+
+ -- The stub acts as its own spec, the applicable pragmas are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
+
+ else
+ Analyze_Subprogram_Contract (Stub_Id);
+ end if;
+ end Analyze_Subprogram_Body_Stub_Contract;
+
+ -----------------------------
+ -- Create_Generic_Contract --
+ -----------------------------
+
+ procedure Create_Generic_Contract (Unit : Node_Id) is
+ Templ : constant Node_Id := Original_Node (Unit);
+ Templ_Id : constant Entity_Id := Defining_Entity (Templ);
+
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
+ -- Add a single contract-related source pragma Prag to the contract of
+ -- generic template Templ_Id.
+
+ ---------------------------------
+ -- Add_Generic_Contract_Pragma --
+ ---------------------------------
+
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
+ Prag_Templ : Node_Id;
+
+ begin
+ -- Mark the pragma to prevent the premature capture of global
+ -- references when capturing global references of the context
+ -- (see Save_References_In_Pragma).
+
+ Set_Is_Generic_Contract_Pragma (Prag);
+
+ -- Pragmas that apply to a generic subprogram declaration are not
+ -- part of the semantic structure of the generic template:
+
+ -- generic
+ -- procedure Example (Formal : Integer);
+ -- pragma Precondition (Formal > 0);
+
+ -- Create a generic template for such pragmas and link the template
+ -- of the pragma with the generic template.
+
+ if Nkind (Templ) = N_Generic_Subprogram_Declaration then
+ Rewrite
+ (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
+ Prag_Templ := Original_Node (Prag);
+
+ Set_Is_Generic_Contract_Pragma (Prag_Templ);
+ Add_Contract_Item (Prag_Templ, Templ_Id);
+
+ -- Otherwise link the pragma with the generic template
+
+ else
+ Add_Contract_Item (Prag, Templ_Id);
+ end if;
+ end Add_Generic_Contract_Pragma;
+
+ -- Local variables
+
+ Context : constant Node_Id := Parent (Unit);
+ Decl : Node_Id := Empty;
+
+ -- Start of processing for Create_Generic_Contract
+
+ begin
+ -- A generic package declaration carries contract-related source pragmas
+ -- in its visible declarations.
+
+ if Nkind (Templ) = N_Generic_Package_Declaration then
+ Set_Ekind (Templ_Id, E_Generic_Package);
+
+ if Present (Visible_Declarations (Specification (Templ))) then
+ Decl := First (Visible_Declarations (Specification (Templ)));
+ end if;
+
+ -- A generic package body carries contract-related source pragmas in its
+ -- declarations.
+
+ elsif Nkind (Templ) = N_Package_Body then
+ Set_Ekind (Templ_Id, E_Package_Body);
+
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
+ end if;
+
+ -- Generic subprogram declaration
+
+ 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;
+
+ -- When the generic subprogram acts as a compilation unit, inspect
+ -- the Pragmas_After list for contract-related source pragmas.
+
+ 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;
+
+ -- Otherwise inspect the successive declarations for contract-related
+ -- source pragmas.
+
+ else
+ Decl := Next (Unit);
+ end if;
+
+ -- A generic subprogram body carries contract-related source pragmas in
+ -- its declarations.
+
+ elsif Nkind (Templ) = N_Subprogram_Body then
+ Set_Ekind (Templ_Id, E_Subprogram_Body);
+
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
+ end if;
+ end if;
+
+ -- Inspect the relevant declarations looking for contract-related source
+ -- pragmas and add them to the contract of the generic unit.
+
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ if Nkind (Decl) = N_Pragma then
+
+ -- The source pragma is a contract annotation
+
+ if Is_Contract_Annotation (Decl) then
+ Add_Generic_Contract_Pragma (Decl);
+ end if;
+
+ -- The region where a contract-related source pragma may appear
+ -- ends with the first source non-pragma declaration or statement.
+
+ else
+ exit;
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Create_Generic_Contract;
+
+ --------------------------------
+ -- Expand_Subprogram_Contract --
+ --------------------------------
+
+ 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);
+
+ 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.
+
+ 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.
+
+ function Build_Pragma_Check_Equivalent
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty) return Node_Id;
+ -- Transform a [refined] pre- or postcondition denoted by Prag into an
+ -- equivalent pragma Check. When the pre- or postcondition is inherited,
+ -- the routine corrects the references of all formals of Inher_Id to
+ -- point to the formals of Subp_Id.
+
+ 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.
+
+ procedure Process_Postconditions (Stmts : in out List_Id);
+ -- Collect all [inherited] spec and body postconditions and accumulate
+ -- their pragma Check equivalents in list Stmts.
+
+ procedure Process_Preconditions;
+ -- Collect all [inherited] spec and body preconditions and prepend their
+ -- pragma Check equivalents to the declarations of the body.
+
+ ----------------------------------------
+ -- Add_Invariant_And_Predicate_Checks --
+ ----------------------------------------
+
+ 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.
+
+ ---------------------------------
+ -- Add_Invariant_Access_Checks --
+ ---------------------------------
+
+ procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ Ref : Node_Id;
+ Typ : Entity_Id;
+
+ begin
+ Typ := Etype (Id);
+
+ if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
+ Typ := Designated_Type (Typ);
+
+ 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;
+
+ -------------------------
+ -- Invariant_Checks_OK --
+ -------------------------
+
+ 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 --
+ -----------------------------------------
+
+ function Has_Public_Visibility_Of_Subprogram return Boolean is
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+
+ begin
+ -- An Initialization procedure must be considered visible even
+ -- though it is internally generated.
+
+ if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
+ return True;
+
+ elsif Ekind (Scope (Typ)) /= E_Package then
+ return False;
+
+ -- 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.
+
+ 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;
+
+ -- Determine whether the subprogram is declared in the visible
+ -- declarations of the package containing the type.
+
+ else
+ return List_Containing (Subp_Decl) =
+ Visible_Declarations
+ (Specification (Unit_Declaration_Node (Scope (Typ))));
+ end if;
+ end Has_Public_Visibility_Of_Subprogram;
+
+ -- Start of processing for Invariant_Checks_OK
+
+ 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;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ -- Source location of subprogram body contract
+
+ Formal : Entity_Id;
+ Typ : Entity_Id;
+
+ -- Start of processing for Add_Invariant_And_Predicate_Checks
+
+ begin
+ Result := Empty;
+
+ -- Process the result of a function
+
+ if Ekind (Subp_Id) = E_Function then
+ Typ := Etype (Subp_Id);
+
+ -- Generate _Result which is used in procedure _Postconditions to
+ -- verify the return value.
+
+ Result := Make_Defining_Identifier (Loc, Name_uResult);
+ Set_Etype (Result, Typ);
+
+ -- Add an invariant check when the return type has invariants and
+ -- the related function is visible to the outside.
+
+ if Invariant_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
+ List => Stmts);
+ end if;
+
+ -- Add an invariant check when the return type is an access to a
+ -- type with invariants.
+
+ Add_Invariant_Access_Checks (Result);
+ 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;
+
+ Add_Invariant_Access_Checks (Formal);
+
+ -- 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.
+
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+ end Add_Invariant_And_Predicate_Checks;
+
+ -------------------------
+ -- Append_Enabled_Item --
+ -------------------------
+
+ 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;
+
+ -- Otherwise, add the item
+
+ else
+ if No (List) then
+ List := New_List;
+ end if;
+
+ -- If the pragma is a conjunct in a composite postcondition, it
+ -- has been processed in reverse order. In the postcondition body
+ -- if must appear before the others.
+
+ 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;
+
+ ------------------------------------
+ -- Build_Postconditions_Procedure --
+ ------------------------------------
+
+ 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
+ -- Inspect the declarations of the related subprogram body looking
+ -- for the first source declaration.
+
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ Insert_Before (Decl, Stmt);
+ return;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ -- If we get there, then the subprogram body lacks any source
+ -- declarations. The body of _Postconditions now acts as the
+ -- last declaration.
+
+ Append (Stmt, Decls);
+
+ -- Ensure that the body has a declaration list
+
+ else
+ Set_Declarations (Body_Decl, New_List (Stmt));
+ end if;
+ end Insert_Before_First_Source_Declaration;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (Body_Decl);
+ Params : List_Id := No_List;
+ Proc_Bod : Node_Id;
+ Proc_Id : Entity_Id;
+
+ -- Start of processing for Build_Postconditions_Procedure
+
+ begin
+ -- Nothing to do if there are no actions to check on exit
+
+ if No (Stmts) then
+ return;
+ end if;
+
+ Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
+ Set_Debug_Info_Needed (Proc_Id);
+ Set_Postconditions_Proc (Subp_Id, Proc_Id);
+
+ -- The related subprogram is a function, create the specification of
+ -- parameter _Result.
+
+ if Present (Result) then
+ Params := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Result,
+ Parameter_Type =>
+ New_Occurrence_Of (Etype (Result), Loc)));
+ end if;
+
+ -- 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:
+
+ -- 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.
+
+ -- Set an explicit End_Lavel 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 into to be
+ -- produced, interfering with coverage analysis tools.
+
+ Proc_Bod :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => Params),
+
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts,
+ End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
+
+ Insert_Before_First_Source_Declaration (Proc_Bod);
+ Analyze (Proc_Bod);
+ end Build_Postconditions_Procedure;
+
+ -----------------------------------
+ -- Build_Pragma_Check_Equivalent --
+ -----------------------------------
+
+ function Build_Pragma_Check_Equivalent
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty) return Node_Id
+ is
+ function Suppress_Reference (N : Node_Id) return Traverse_Result;
+ -- Detect whether node N references a formal parameter subject to
+ -- pragma Unreferenced. If this is the case, set Comes_From_Source
+ -- to False to suppress the generation of a reference when analyzing
+ -- N later on.
+
+ ------------------------
+ -- Suppress_Reference --
+ ------------------------
+
+ function Suppress_Reference (N : Node_Id) return Traverse_Result is
+ Formal : Entity_Id;
+
+ begin
+ if Is_Entity_Name (N) and then Present (Entity (N)) then
+ Formal := Entity (N);
+
+ -- The formal parameter is subject to pragma Unreferenced.
+ -- Prevent the generation of a reference by resetting the
+ -- Comes_From_Source flag.
+
+ if Is_Formal (Formal)
+ and then Has_Pragma_Unreferenced (Formal)
+ then
+ Set_Comes_From_Source (N, False);
+ end if;
+ end if;
+
+ return OK;
+ end Suppress_Reference;
+
+ procedure Suppress_References is
+ new Traverse_Proc (Suppress_Reference);
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (Prag);
+ Prag_Nam : constant Name_Id := Pragma_Name (Prag);
+ Check_Prag : Node_Id;
+ Formals_Map : Elist_Id;
+ Inher_Formal : Entity_Id;
+ Msg_Arg : Node_Id;
+ Nam : Name_Id;
+ Subp_Formal : Entity_Id;
+
+ -- Start of processing for Build_Pragma_Check_Equivalent
+
+ begin
+ Formals_Map := No_Elist;
+
+ -- When the pre- or postcondition is inherited, map the formals of
+ -- the inherited subprogram to those of the current subprogram.
+
+ if Present (Inher_Id) then
+ pragma Assert (Present (Subp_Id));
+
+ Formals_Map := New_Elmt_List;
+
+ -- Create a relation <inherited formal> => <subprogram formal>
+
+ Inher_Formal := First_Formal (Inher_Id);
+ Subp_Formal := First_Formal (Subp_Id);
+ while Present (Inher_Formal) and then Present (Subp_Formal) loop
+ Append_Elmt (Inher_Formal, Formals_Map);
+ Append_Elmt (Subp_Formal, Formals_Map);
+
+ Next_Formal (Inher_Formal);
+ Next_Formal (Subp_Formal);
+ end loop;
+ end if;
+
+ -- Copy the original pragma while performing substitutions (if
+ -- applicable).
+
+ Check_Prag :=
+ New_Copy_Tree
+ (Source => Prag,
+ Map => Formals_Map,
+ New_Scope => Current_Scope);
+
+ -- Mark the pragma as being internally generated and reset the
+ -- Analyzed flag.
+
+ Set_Analyzed (Check_Prag, False);
+ Set_Comes_From_Source (Check_Prag, False);
+
+ -- The tree of the original pragma may contain references to the
+ -- formal parameters of the related subprogram. At the same time
+ -- the corresponding body may mark the formals as unreferenced:
+
+ -- procedure Proc (Formal : ...)
+ -- with Pre => Formal ...;
+
+ -- procedure Proc (Formal : ...) is
+ -- pragma Unreferenced (Formal);
+ -- ...
+
+ -- This creates problems because all pragma Check equivalents are
+ -- analyzed at the end of the body declarations. Since all source
+ -- references have already been accounted for, reset any references
+ -- to such formals in the generated pragma Check equivalent.
+
+ Suppress_References (Check_Prag);
+
+ if Present (Corresponding_Aspect (Prag)) then
+ Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
+ else
+ Nam := Prag_Nam;
+ end if;
+
+ -- Convert the copy into pragma Check by correcting the name and
+ -- adding a check_kind argument.
+
+ Set_Pragma_Identifier
+ (Check_Prag, Make_Identifier (Loc, Name_Check));
+
+ Prepend_To (Pragma_Argument_Associations (Check_Prag),
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Nam)));
+
+ -- Update the error message when the pragma is inherited
+
+ if Present (Inher_Id) then
+ Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
+
+ if Chars (Msg_Arg) = Name_Message then
+ String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
+
+ -- Insert "inherited" to improve the error message
+
+ if Name_Buffer (1 .. 8) = "failed p" then
+ Insert_Str_In_Name_Buffer ("inherited ", 8);
+ Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
+ end if;
+ end if;
+ end if;
+
+ return Check_Prag;
+ end Build_Pragma_Check_Equivalent;
+
+ ----------------------------
+ -- 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;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end Process_Contract_Cases_For;
+
+ -- Start of processing for Process_Contract_Cases
+
+ begin
+ Process_Contract_Cases_For (Body_Id);
+
+ if Present (Spec_Id) then
+ Process_Contract_Cases_For (Spec_Id);
+ end if;
+ end Process_Contract_Cases;
+
+ ----------------------------
+ -- Process_Postconditions --
+ ----------------------------
+
+ 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_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;
+
+ begin
+ -- Process the contract
+
+ 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;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- 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.
+
+ 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) = 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;
+
+ -- Postcondition pragmas are usually grouped together. There
+ -- is no need to inspect the whole declarative list.
+
+ else
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+ end Process_Body_Postconditions;
+
+ ---------------------------------
+ -- Process_Spec_Postconditions --
+ ---------------------------------
+
+ procedure Process_Spec_Postconditions is
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
+
+ begin
+ -- Process the contract
+
+ Items := Contract (Spec_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;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide postconditions.
+
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (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;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end loop;
+ end Process_Spec_Postconditions;
+
+ -- Start of processing for Process_Postconditions
+
+ begin
+ -- The processing of postconditions is done in reverse order (body
+ -- first) to ensure the following arrangement:
+
+ -- <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_Spec_Postconditions;
+ end if;
+ end Process_Postconditions;
+
+ ---------------------------
+ -- Process_Preconditions --
+ ---------------------------
+
+ procedure Process_Preconditions is
+ Class_Pre : Node_Id := Empty;
+ -- The sole [inherited] class-wide precondition pragma that applies
+ -- to the subprogram.
+
+ Insert_Node : Node_Id := Empty;
+ -- The insertion node after which all pragma Check equivalents are
+ -- inserted.
+
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
+ -- Merge two class-wide preconditions by "or else"-ing them. The
+ -- changes are accumulated in parameter Into. Update the error
+ -- message of Into.
+
+ procedure Prepend_To_Decls (Item : Node_Id);
+ -- Prepend a single item to the declarations of the subprogram body
+
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
+ -- Save a class-wide precondition into Class_Pre or prepend a normal
+ -- precondition ot the declarations of the body and analyze it.
+
+ procedure Process_Inherited_Preconditions;
+ -- Collect all inherited class-wide preconditions and merge them into
+ -- one big precondition to be evaluated as pragma Check.
+
+ procedure 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.
+
+ -------------------------
+ -- Merge_Preconditions --
+ -------------------------
+
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
+ function Expression_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the boolean expression argument of a precondition while
+ -- updating its parenteses count for the subsequent merge.
+
+ function Message_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the message argument of a precondition
+
+ --------------------
+ -- Expression_Arg --
+ --------------------
+
+ function Expression_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
+
+ begin
+ if Paren_Count (Arg) = 0 then
+ Set_Paren_Count (Arg, 1);
+ end if;
+
+ return Arg;
+ end Expression_Arg;
+
+ -----------------
+ -- Message_Arg --
+ -----------------
+
+ function Message_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ begin
+ return Get_Pragma_Arg (Last (Args));
+ end Message_Arg;
+
+ -- Local variables
+
+ From_Expr : constant Node_Id := Expression_Arg (From);
+ From_Msg : constant Node_Id := Message_Arg (From);
+ Into_Expr : constant Node_Id := Expression_Arg (Into);
+ Into_Msg : constant Node_Id := Message_Arg (Into);
+ Loc : constant Source_Ptr := Sloc (Into);
+
+ -- Start of processing for Merge_Preconditions
+
+ begin
+ -- Merge the two preconditions by "or else"-ing them
+
+ Rewrite (Into_Expr,
+ Make_Or_Else (Loc,
+ Right_Opnd => Relocate_Node (Into_Expr),
+ Left_Opnd => From_Expr));
+
+ -- Merge the two error messages to produce a single message of the
+ -- form:
+
+ -- failed precondition from ...
+ -- also failed inherited precondition from ...
+
+ if not Exception_Locations_Suppressed then
+ Start_String (Strval (Into_Msg));
+ Store_String_Char (ASCII.LF);
+ Store_String_Chars (" also ");
+ Store_String_Chars (Strval (From_Msg));
+
+ Set_Strval (Into_Msg, End_String);
+ end if;
+ end Merge_Preconditions;
+
+ ----------------------
+ -- Prepend_To_Decls --
+ ----------------------
+
+ procedure Prepend_To_Decls (Item : Node_Id) is
+ Decls : List_Id := Declarations (Body_Decl);
+
+ begin
+ -- Ensure that the body has a declarative list
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (Body_Decl, Decls);
+ end if;
+
+ Prepend_To (Decls, Item);
+ end Prepend_To_Decls;
+
+ ------------------------------
+ -- Prepend_To_Decls_Or_Save --
+ ------------------------------
+
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
+ Check_Prag : Node_Id;
+
+ begin
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+
+ -- Save the sole class-wide precondition (if any) for the next
+ -- step where it will be merged with inherited preconditions.
+
+ if Class_Present (Prag) then
+ pragma Assert (No (Class_Pre));
+ Class_Pre := Check_Prag;
+
+ -- Accumulate the corresponding Check pragmas at the top of the
+ -- declarations. Prepending the items ensures that they will be
+ -- evaluated in their original order.
+
+ else
+ if Present (Insert_Node) then
+ Insert_After (Insert_Node, Check_Prag);
+ else
+ Prepend_To_Decls (Check_Prag);
+ end if;
+
+ Analyze (Check_Prag);
+ end if;
+ end Prepend_To_Decls_Or_Save;
+
+ -------------------------------------
+ -- Process_Inherited_Preconditions --
+ -------------------------------------
+
+ 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;
+
+ begin
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide preconditions.
+
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (Subp_Id);
+
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition
+ and then Class_Present (Prag)
+ then
+ Check_Prag :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id);
+
+ -- The spec or 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 (Check_Prag, Class_Pre);
+ else
+ Class_Pre := Check_Prag;
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end loop;
+
+ -- Add the merged class-wide preconditions
+
+ if Present (Class_Pre) then
+ Prepend_To_Decls (Class_Pre);
+ Analyze (Class_Pre);
+ end if;
+ end Process_Inherited_Preconditions;
+
+ -------------------------------
+ -- Process_Preconditions_For --
+ -------------------------------
+
+ 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;
+
+ 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);
+ 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
+
+ Decl := Next (Subp_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);
+ 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.
+
+ else
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+ end Process_Preconditions_For;
+
+ -- Local variables
+
+ Decls : constant List_Id := Declarations (Body_Decl);
+ Decl : Node_Id;
+
+ -- Start of processing for Process_Preconditions
+
+ begin
+ -- Find the last internally generate declaration starting from the
+ -- top of the body declarations. This ensures that discriminals and
+ -- subtypes are properly visible to the pragma Check equivalents.
+
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ exit when Comes_From_Source (Decl);
+ Insert_Node := Decl;
+ Next (Decl);
+ end loop;
+ end if;
+
+ -- The processing of preconditions is done in reverse order (body
+ -- first) because each pragma Check equivalent is inserted at the
+ -- top of the declarations. This ensures that the final order is
+ -- consistent with following diagram:
+
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+
+ Process_Preconditions_For (Body_Id);
+
+ if Present (Spec_Id) then
+ Process_Preconditions_For (Spec_Id);
+ Process_Inherited_Preconditions;
+ 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.
+
+ 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
+ return;
+
+ -- Otherwise mark the subprogram
+
+ else
+ Set_Has_Expanded_Contract (Subp_Id);
+ end if;
+
+ -- Ensure that the formal parameters are visible when expanding all
+ -- contract items.
+
+ if not In_Open_Scopes (Subp_Id) then
+ Restore_Scope := True;
+ Push_Scope (Subp_Id);
+
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
+ end if;
+
+ -- 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:
+
+ -- 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;
+
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+ -- <contract case conditions>
+
+ -- <source declarations>
+ -- begin
+ -- <source statements>
+
+ -- _Preconditions (Result);
+ -- return Result;
+ -- end Example;
+
+ -- Routine _Postconditions holds all contract assertions that must be
+ -- verified on exit from the related subprogram.
+
+ -- 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.
+
+ 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.
+
+ Process_Postconditions (Stmts);
+
+ -- Step 3: Handle pragma Contract_Cases. This action must come before
+ -- the processing of invariants and predicates because those append
+ -- items to list Smts.
+
+ Process_Contract_Cases (Stmts);
+
+ -- Step 4: Apply invariant and predicate checks on a function result and
+ -- all formals. The resulting checks are accumulated in list Stmts.
+
+ Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
+
+ -- Step 5: Construct procedure _Postconditions
+
+ Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
+
+ if Restore_Scope then
+ End_Scope;
+ end if;
+ end Expand_Subprogram_Contract;
+
+ ---------------------------------
+ -- Inherit_Subprogram_Contract --
+ ---------------------------------
+
+ 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.
+
+ --------------------
+ -- Inherit_Pragma --
+ --------------------
+
+ procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
+ Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
+ New_Prag : Node_Id;
+
+ 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 is inherited for distrinction purposes.
+
+ if Present (Prag) then
+ New_Prag := New_Copy_Tree (Prag);
+ Set_Is_Inherited (New_Prag);
+
+ Add_Contract_Item (New_Prag, Subp);
+ end if;
+ end Inherit_Pragma;
+
+ -- Start of processing for Inherit_Subprogram_Contract
+
+ begin
+ -- Inheritance is carried out only when both entities are subprograms
+ -- with contracts.
+
+ 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;
+
+ -------------------------------------
+ -- Instantiate_Subprogram_Contract --
+ -------------------------------------
+
+ 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.
+
+ -------------------------
+ -- Instantiate_Pragmas --
+ -------------------------
+
+ procedure Instantiate_Pragmas (First_Prag : Node_Id) is
+ Inst_Prag : Node_Id;
+ Prag : Node_Id;
+
+ 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_Analyzed (Inst_Prag, False);
+ Append_To (L, Inst_Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Instantiate_Pragmas;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+ -- Start of processing for Instantiate_Subprogram_Contract
+
+ 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;
+
+ ----------------------------------------
+ -- Save_Global_References_In_Contract --
+ ----------------------------------------
+
+ 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.
+
+ ------------------------------------
+ -- Save_Global_References_In_List --
+ ------------------------------------
+
+ procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+ Prag : Node_Id;
+
+ begin
+ 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
+
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+ -- Start of processing for Save_Global_References_In_Contract
+
+ begin
+ -- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- C O N T R A C T S --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2015, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+-- This package contains routines that perform analysis and expansion of
+-- various contracts.
+
+with Types; use Types;
+
+package Contracts is
+
+ procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
+ -- Add pragma Prag to the contract of a constant, entry, package [body],
+ -- subprogram [body] or variable denoted by Id. The following are valid
+ -- pragmas:
+ -- Abstract_State
+ -- Async_Readers
+ -- Async_Writers
+ -- Constant_After_Elaboration
+ -- Contract_Cases
+ -- Depends
+ -- Effective_Reads
+ -- Effective_Writes
+ -- Extensions_Visible
+ -- Global
+ -- Initial_Condition
+ -- Initializes
+ -- Part_Of
+ -- Postcondition
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Refined_States
+ -- Test_Case
+ -- Volatile_Function
+
+ procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id);
+ -- Analyze the contract of the nearest package body (if any) which encloses
+ -- package or subprogram body Body_Decl.
+
+ procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
+ -- if they appeared at the end of the declarative region. The pragmas to be
+ -- considered are:
+ -- Async_Readers
+ -- Async_Writers
+ -- Effective_Reads
+ -- Effective_Writes
+ -- Part_Of
+
+ procedure Analyze_Package_Body_Contract
+ (Body_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Analyze all delayed aspects chained on the contract of package body
+ -- Body_Id as if they appeared at the end of a declarative region. The
+ -- aspects that are considered are:
+ -- Refined_State
+ --
+ -- Freeze_Id is the entity of a [generic] package body or a [generic]
+ -- subprogram body which "feezes" the contract of Body_Id.
+
+ procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of package Pack_Id
+ -- as if they appeared at the end of a declarative region. The aspects
+ -- that are considered are:
+ -- Initial_Condition
+ -- Initializes
+ -- Part_Of
+
+ procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of subprogram body
+ -- Body_Id as if they appeared at the end of a declarative region. Aspects
+ -- in question are:
+ -- Contract_Cases (stand alone body)
+ -- Depends (stand alone body)
+ -- Global (stand alone body)
+ -- Postcondition (stand alone body)
+ -- Precondition (stand alone body)
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case (stand alone body)
+
+ procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of subprogram
+ -- Subp_Id as if they appeared at the end of a declarative region. The
+ -- aspects in question are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
+
+ procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of a subprogram body
+ -- stub Stub_Id as if they appeared at the end of a declarative region. The
+ -- aspects in question are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case
+
+ procedure Create_Generic_Contract (Unit : Node_Id);
+ -- Create a contract node for a generic package, generic subprogram or a
+ -- generic body denoted by Unit by collecting all source contract-related
+ -- pragmas in the contract of the unit.
+
+ procedure Inherit_Subprogram_Contract
+ (Subp : Entity_Id;
+ From_Subp : Entity_Id);
+ -- Inherit relevant contract items from source subprogram From_Subp. Subp
+ -- denotes the destination subprogram. The inherited items are:
+ -- Extensions_Visible
+ -- ??? it would be nice if this routine handles Pre'Class and Post'Class
+
+ procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id);
+ -- Instantiate all source pragmas found in the contract of the generic
+ -- subprogram declaration template denoted by Templ. The instantiated
+ -- pragmas are added to list L.
+
+ procedure Save_Global_References_In_Contract
+ (Templ : Node_Id;
+ Gen_Id : Entity_Id);
+ -- Save all global references found within the aspect specifications and
+ -- the contract-related source pragmas assocated with generic template
+ -- Templ. Gen_Id denotes the entity of the analyzed generic copy.
+
+end Contracts;
-- --
------------------------------------------------------------------------------
-with Atree; use Atree;
-with Checks; use Checks;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Errout; use Errout;
-with Elists; use Elists;
-with Exp_Aggr; use Exp_Aggr;
-with Exp_Atag; use Exp_Atag;
-with Exp_Ch2; use Exp_Ch2;
-with Exp_Ch3; use Exp_Ch3;
-with Exp_Ch7; use Exp_Ch7;
-with Exp_Ch9; use Exp_Ch9;
-with Exp_Dbug; use Exp_Dbug;
-with Exp_Disp; use Exp_Disp;
-with Exp_Dist; use Exp_Dist;
-with Exp_Intr; use Exp_Intr;
-with Exp_Pakd; use Exp_Pakd;
-with Exp_Prag; use Exp_Prag;
-with Exp_Tss; use Exp_Tss;
-with Exp_Unst; use Exp_Unst;
-with Exp_Util; use Exp_Util;
-with Freeze; use Freeze;
-with Ghost; use Ghost;
-with Inline; use Inline;
-with Lib; use Lib;
-with Namet; use Namet;
-with Nlists; use Nlists;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Dim; use Sem_Dim;
-with Sem_Disp; use Sem_Disp;
-with Sem_Dist; use Sem_Dist;
-with Sem_Eval; use Sem_Eval;
-with Sem_Mech; use Sem_Mech;
-with Sem_Res; use Sem_Res;
-with Sem_SCIL; use Sem_SCIL;
-with Sem_Util; use Sem_Util;
-with Sinfo; use Sinfo;
-with Snames; use Snames;
-with Stand; use Stand;
-with Stringt; use Stringt;
+with Atree; use Atree;
+with Checks; use Checks;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Errout; use Errout;
+with Elists; use Elists;
+with Exp_Aggr; use Exp_Aggr;
+with Exp_Atag; use Exp_Atag;
+with Exp_Ch2; use Exp_Ch2;
+with Exp_Ch3; use Exp_Ch3;
+with Exp_Ch7; use Exp_Ch7;
+with Exp_Ch9; use Exp_Ch9;
+with Exp_Dbug; use Exp_Dbug;
+with Exp_Disp; use Exp_Disp;
+with Exp_Dist; use Exp_Dist;
+with Exp_Intr; use Exp_Intr;
+with Exp_Pakd; use Exp_Pakd;
+with Exp_Tss; use Exp_Tss;
+with Exp_Unst; use Exp_Unst;
+with Exp_Util; use Exp_Util;
+with Freeze; use Freeze;
+with Ghost; use Ghost;
+with Inline; use Inline;
+with Lib; use Lib;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Dim; use Sem_Dim;
+with Sem_Disp; use Sem_Disp;
+with Sem_Dist; use Sem_Dist;
+with Sem_Eval; use Sem_Eval;
+with Sem_Mech; use Sem_Mech;
+with Sem_Res; use Sem_Res;
+with Sem_SCIL; use Sem_SCIL;
+with Sem_Util; use Sem_Util;
+with Sinfo; use Sinfo;
+with Snames; use Snames;
+with Stand; use Stand;
with Table;
-with Targparm; use Targparm;
-with Tbuild; use Tbuild;
-with Uintp; use Uintp;
-with Validsw; use Validsw;
+with Targparm; use Targparm;
+with Tbuild; use Tbuild;
+with Uintp; use Uintp;
+with Validsw; use Validsw;
package body Exp_Ch6 is
end if;
end Expand_Simple_Function_Return;
- --------------------------------
- -- Expand_Subprogram_Contract --
- --------------------------------
-
- procedure Expand_Subprogram_Contract (N : Node_Id) is
- Body_Id : constant Entity_Id := Defining_Entity (N);
- Spec_Id : constant Entity_Id := Corresponding_Spec (N);
-
- 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.
-
- 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.
-
- function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id;
- -- Transform a [refined] pre- or postcondition denoted by Prag into an
- -- equivalent pragma Check. When the pre- or postcondition is inherited,
- -- the routine corrects the references of all formals of Inher_Id to
- -- point to the formals of Subp_Id.
-
- 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.
-
- procedure Process_Postconditions (Stmts : in out List_Id);
- -- Collect all [inherited] spec and body postconditions and accumulate
- -- their pragma Check equivalents in list Stmts.
-
- procedure Process_Preconditions;
- -- Collect all [inherited] spec and body preconditions and prepend their
- -- pragma Check equivalents to the declarations of the body.
-
- ----------------------------------------
- -- Add_Invariant_And_Predicate_Checks --
- ----------------------------------------
-
- 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.
-
- ---------------------------------
- -- Add_Invariant_Access_Checks --
- ---------------------------------
-
- procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Ref : Node_Id;
- Typ : Entity_Id;
-
- begin
- Typ := Etype (Id);
-
- if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
- Typ := Designated_Type (Typ);
-
- 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;
-
- -------------------------
- -- Invariant_Checks_OK --
- -------------------------
-
- 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 --
- -----------------------------------------
-
- function Has_Public_Visibility_Of_Subprogram return Boolean is
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
-
- begin
- -- An Initialization procedure must be considered visible even
- -- though it is internally generated.
-
- if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
- return True;
-
- elsif Ekind (Scope (Typ)) /= E_Package then
- return False;
-
- -- 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.
-
- 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;
-
- -- Determine whether the subprogram is declared in the visible
- -- declarations of the package containing the type.
-
- else
- return List_Containing (Subp_Decl) =
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Scope (Typ))));
- end if;
- end Has_Public_Visibility_Of_Subprogram;
-
- -- Start of processing for Invariant_Checks_OK
-
- 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;
-
- -- Local variables
-
- Loc : constant Source_Ptr := Sloc (N);
- -- Source location of subprogram contract
-
- Formal : Entity_Id;
- Typ : Entity_Id;
-
- -- Start of processing for Add_Invariant_And_Predicate_Checks
-
- begin
- Result := Empty;
-
- -- Process the result of a function
-
- if Ekind (Subp_Id) = E_Function then
- Typ := Etype (Subp_Id);
-
- -- Generate _Result which is used in procedure _Postconditions to
- -- verify the return value.
-
- Result := Make_Defining_Identifier (Loc, Name_uResult);
- Set_Etype (Result, Typ);
-
- -- Add an invariant check when the return type has invariants and
- -- the related function is visible to the outside.
-
- if Invariant_Checks_OK (Typ) then
- Append_Enabled_Item
- (Item =>
- Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
- List => Stmts);
- end if;
-
- -- Add an invariant check when the return type is an access to a
- -- type with invariants.
-
- Add_Invariant_Access_Checks (Result);
- 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;
-
- Add_Invariant_Access_Checks (Formal);
-
- -- 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.
-
- end if;
-
- Next_Formal (Formal);
- end loop;
- end Add_Invariant_And_Predicate_Checks;
-
- -------------------------
- -- Append_Enabled_Item --
- -------------------------
-
- 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;
-
- -- Otherwise, add the item
-
- else
- if No (List) then
- List := New_List;
- end if;
-
- -- If the pragma is a conjunct in a composite postcondition, it
- -- has been processed in reverse order. In the postcondition body
- -- if must appear before the others.
-
- 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;
-
- ------------------------------------
- -- Build_Postconditions_Procedure --
- ------------------------------------
-
- 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 (N);
- Decl : Node_Id;
-
- begin
- -- Inspect the declarations of the related subprogram body looking
- -- for the first source declaration.
-
- if Present (Decls) then
- Decl := First (Decls);
- while Present (Decl) loop
- if Comes_From_Source (Decl) then
- Insert_Before (Decl, Stmt);
- return;
- end if;
-
- Next (Decl);
- end loop;
-
- -- If we get there, then the subprogram body lacks any source
- -- declarations. The body of _Postconditions now acts as the
- -- last declaration.
-
- Append (Stmt, Decls);
-
- -- Ensure that the body has a declaration list
-
- else
- Set_Declarations (N, New_List (Stmt));
- end if;
- end Insert_Before_First_Source_Declaration;
-
- -- Local variables
-
- Loc : constant Source_Ptr := Sloc (N);
- Params : List_Id := No_List;
- Proc_Bod : Node_Id;
- Proc_Id : Entity_Id;
-
- -- Start of processing for Build_Postconditions_Procedure
-
- begin
- -- Nothing to do if there are no actions to check on exit
-
- if No (Stmts) then
- return;
- end if;
-
- Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
- Set_Debug_Info_Needed (Proc_Id);
- Set_Postconditions_Proc (Subp_Id, Proc_Id);
-
- -- The related subprogram is a function, create the specification of
- -- parameter _Result.
-
- if Present (Result) then
- Params := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Result,
- Parameter_Type =>
- New_Occurrence_Of (Etype (Result), Loc)));
- end if;
-
- -- 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:
-
- -- 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.
-
- -- Set an explicit End_Lavel 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 into to be
- -- produced, interfering with coverage analysis tools.
-
- Proc_Bod :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Proc_Id,
- Parameter_Specifications => Params),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts,
- End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
-
- Insert_Before_First_Source_Declaration (Proc_Bod);
- Analyze (Proc_Bod);
- end Build_Postconditions_Procedure;
-
- -----------------------------------
- -- Build_Pragma_Check_Equivalent --
- -----------------------------------
-
- function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id
- is
- function Suppress_Reference (N : Node_Id) return Traverse_Result;
- -- Detect whether node N references a formal parameter subject to
- -- pragma Unreferenced. If this is the case, set Comes_From_Source
- -- to False to suppress the generation of a reference when analyzing
- -- N later on.
-
- ------------------------
- -- Suppress_Reference --
- ------------------------
-
- function Suppress_Reference (N : Node_Id) return Traverse_Result is
- Formal : Entity_Id;
-
- begin
- if Is_Entity_Name (N) and then Present (Entity (N)) then
- Formal := Entity (N);
-
- -- The formal parameter is subject to pragma Unreferenced.
- -- Prevent the generation of a reference by resetting the
- -- Comes_From_Source flag.
-
- if Is_Formal (Formal)
- and then Has_Pragma_Unreferenced (Formal)
- then
- Set_Comes_From_Source (N, False);
- end if;
- end if;
-
- return OK;
- end Suppress_Reference;
-
- procedure Suppress_References is
- new Traverse_Proc (Suppress_Reference);
-
- -- Local variables
-
- Loc : constant Source_Ptr := Sloc (Prag);
- Prag_Nam : constant Name_Id := Pragma_Name (Prag);
- Check_Prag : Node_Id;
- Formals_Map : Elist_Id;
- Inher_Formal : Entity_Id;
- Msg_Arg : Node_Id;
- Nam : Name_Id;
- Subp_Formal : Entity_Id;
-
- -- Start of processing for Build_Pragma_Check_Equivalent
-
- begin
- Formals_Map := No_Elist;
-
- -- When the pre- or postcondition is inherited, map the formals of
- -- the inherited subprogram to those of the current subprogram.
-
- if Present (Inher_Id) then
- pragma Assert (Present (Subp_Id));
-
- Formals_Map := New_Elmt_List;
-
- -- Create a relation <inherited formal> => <subprogram formal>
-
- Inher_Formal := First_Formal (Inher_Id);
- Subp_Formal := First_Formal (Subp_Id);
- while Present (Inher_Formal) and then Present (Subp_Formal) loop
- Append_Elmt (Inher_Formal, Formals_Map);
- Append_Elmt (Subp_Formal, Formals_Map);
-
- Next_Formal (Inher_Formal);
- Next_Formal (Subp_Formal);
- end loop;
- end if;
-
- -- Copy the original pragma while performing substitutions (if
- -- applicable).
-
- Check_Prag :=
- New_Copy_Tree
- (Source => Prag,
- Map => Formals_Map,
- New_Scope => Current_Scope);
-
- -- Mark the pragma as being internally generated and reset the
- -- Analyzed flag.
-
- Set_Analyzed (Check_Prag, False);
- Set_Comes_From_Source (Check_Prag, False);
-
- -- The tree of the original pragma may contain references to the
- -- formal parameters of the related subprogram. At the same time
- -- the corresponding body may mark the formals as unreferenced:
-
- -- procedure Proc (Formal : ...)
- -- with Pre => Formal ...;
-
- -- procedure Proc (Formal : ...) is
- -- pragma Unreferenced (Formal);
- -- ...
-
- -- This creates problems because all pragma Check equivalents are
- -- analyzed at the end of the body declarations. Since all source
- -- references have already been accounted for, reset any references
- -- to such formals in the generated pragma Check equivalent.
-
- Suppress_References (Check_Prag);
-
- if Present (Corresponding_Aspect (Prag)) then
- Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
- else
- Nam := Prag_Nam;
- end if;
-
- -- Convert the copy into pragma Check by correcting the name and
- -- adding a check_kind argument.
-
- Set_Pragma_Identifier
- (Check_Prag, Make_Identifier (Loc, Name_Check));
-
- Prepend_To (Pragma_Argument_Associations (Check_Prag),
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Nam)));
-
- -- Update the error message when the pragma is inherited
-
- if Present (Inher_Id) then
- Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
-
- if Chars (Msg_Arg) = Name_Message then
- String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
-
- -- Insert "inherited" to improve the error message
-
- if Name_Buffer (1 .. 8) = "failed p" then
- Insert_Str_In_Name_Buffer ("inherited ", 8);
- Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
- end if;
- end if;
- end if;
-
- return Check_Prag;
- end Build_Pragma_Check_Equivalent;
-
- ----------------------------
- -- 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 (N),
- Stmts => Stmts);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end Process_Contract_Cases_For;
-
- -- Start of processing for Process_Contract_Cases
-
- begin
- Process_Contract_Cases_For (Body_Id);
-
- if Present (Spec_Id) then
- Process_Contract_Cases_For (Spec_Id);
- end if;
- end Process_Contract_Cases;
-
- ----------------------------
- -- Process_Postconditions --
- ----------------------------
-
- 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_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 (N);
- Decl : Node_Id;
- Prag : Node_Id;
-
- begin
- -- Process the contract
-
- 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;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
-
- -- 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.
-
- 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) = 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;
-
- -- Postcondition pragmas are usually grouped together. There
- -- is no need to inspect the whole declarative list.
-
- else
- exit;
- end if;
-
- Next (Decl);
- end loop;
- end if;
- end Process_Body_Postconditions;
-
- ---------------------------------
- -- Process_Spec_Postconditions --
- ---------------------------------
-
- procedure Process_Spec_Postconditions is
- Subps : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- Items : Node_Id;
- Prag : Node_Id;
- Subp_Id : Entity_Id;
-
- begin
- -- Process the contract
-
- Items := Contract (Spec_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;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
-
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide postconditions.
-
- for Index in Subps'Range loop
- Subp_Id := Subps (Index);
- Items := Contract (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;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end loop;
- end Process_Spec_Postconditions;
-
- -- Start of processing for Process_Postconditions
-
- begin
- -- The processing of postconditions is done in reverse order (body
- -- first) to ensure the following arrangement:
-
- -- <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_Spec_Postconditions;
- end if;
- end Process_Postconditions;
-
- ---------------------------
- -- Process_Preconditions --
- ---------------------------
-
- procedure Process_Preconditions is
- Class_Pre : Node_Id := Empty;
- -- The sole [inherited] class-wide precondition pragma that applies
- -- to the subprogram.
-
- Insert_Node : Node_Id := Empty;
- -- The insertion node after which all pragma Check equivalents are
- -- inserted.
-
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
- -- Merge two class-wide preconditions by "or else"-ing them. The
- -- changes are accumulated in parameter Into. Update the error
- -- message of Into.
-
- procedure Prepend_To_Decls (Item : Node_Id);
- -- Prepend a single item to the declarations of the subprogram body
-
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
- -- Save a class-wide precondition into Class_Pre or prepend a normal
- -- precondition ot the declarations of the body and analyze it.
-
- procedure Process_Inherited_Preconditions;
- -- Collect all inherited class-wide preconditions and merge them into
- -- one big precondition to be evaluated as pragma Check.
-
- procedure 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.
-
- -------------------------
- -- Merge_Preconditions --
- -------------------------
-
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
- function Expression_Arg (Prag : Node_Id) return Node_Id;
- -- Return the boolean expression argument of a precondition while
- -- updating its parenteses count for the subsequent merge.
-
- function Message_Arg (Prag : Node_Id) return Node_Id;
- -- Return the message argument of a precondition
-
- --------------------
- -- Expression_Arg --
- --------------------
-
- function Expression_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
-
- begin
- if Paren_Count (Arg) = 0 then
- Set_Paren_Count (Arg, 1);
- end if;
-
- return Arg;
- end Expression_Arg;
-
- -----------------
- -- Message_Arg --
- -----------------
-
- function Message_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- begin
- return Get_Pragma_Arg (Last (Args));
- end Message_Arg;
-
- -- Local variables
-
- From_Expr : constant Node_Id := Expression_Arg (From);
- From_Msg : constant Node_Id := Message_Arg (From);
- Into_Expr : constant Node_Id := Expression_Arg (Into);
- Into_Msg : constant Node_Id := Message_Arg (Into);
- Loc : constant Source_Ptr := Sloc (Into);
-
- -- Start of processing for Merge_Preconditions
-
- begin
- -- Merge the two preconditions by "or else"-ing them
-
- Rewrite (Into_Expr,
- Make_Or_Else (Loc,
- Right_Opnd => Relocate_Node (Into_Expr),
- Left_Opnd => From_Expr));
-
- -- Merge the two error messages to produce a single message of the
- -- form:
-
- -- failed precondition from ...
- -- also failed inherited precondition from ...
-
- if not Exception_Locations_Suppressed then
- Start_String (Strval (Into_Msg));
- Store_String_Char (ASCII.LF);
- Store_String_Chars (" also ");
- Store_String_Chars (Strval (From_Msg));
-
- Set_Strval (Into_Msg, End_String);
- end if;
- end Merge_Preconditions;
-
- ----------------------
- -- Prepend_To_Decls --
- ----------------------
-
- procedure Prepend_To_Decls (Item : Node_Id) is
- Decls : List_Id := Declarations (N);
-
- begin
- -- Ensure that the body has a declarative list
-
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (N, Decls);
- end if;
-
- Prepend_To (Decls, Item);
- end Prepend_To_Decls;
-
- ------------------------------
- -- Prepend_To_Decls_Or_Save --
- ------------------------------
-
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
- Check_Prag : Node_Id;
-
- begin
- Check_Prag := Build_Pragma_Check_Equivalent (Prag);
-
- -- Save the sole class-wide precondition (if any) for the next
- -- step where it will be merged with inherited preconditions.
-
- if Class_Present (Prag) then
- pragma Assert (No (Class_Pre));
- Class_Pre := Check_Prag;
-
- -- Accumulate the corresponding Check pragmas at the top of the
- -- declarations. Prepending the items ensures that they will be
- -- evaluated in their original order.
-
- else
- if Present (Insert_Node) then
- Insert_After (Insert_Node, Check_Prag);
- else
- Prepend_To_Decls (Check_Prag);
- end if;
-
- Analyze (Check_Prag);
- end if;
- end Prepend_To_Decls_Or_Save;
-
- -------------------------------------
- -- Process_Inherited_Preconditions --
- -------------------------------------
-
- 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;
-
- begin
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide preconditions.
-
- for Index in Subps'Range loop
- Subp_Id := Subps (Index);
- Items := Contract (Subp_Id);
-
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Check_Prag :=
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Spec_Id,
- Inher_Id => Subp_Id);
-
- -- The spec or 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 (Check_Prag, Class_Pre);
- else
- Class_Pre := Check_Prag;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end loop;
-
- -- Add the merged class-wide preconditions
-
- if Present (Class_Pre) then
- Prepend_To_Decls (Class_Pre);
- Analyze (Class_Pre);
- end if;
- end Process_Inherited_Preconditions;
-
- -------------------------------
- -- Process_Preconditions_For --
- -------------------------------
-
- 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;
-
- 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);
- 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
-
- Decl := Next (Subp_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);
- 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.
-
- else
- exit;
- end if;
-
- Next (Decl);
- end loop;
- end if;
- end Process_Preconditions_For;
-
- -- Local variables
-
- Decls : constant List_Id := Declarations (N);
- Decl : Node_Id;
-
- -- Start of processing for Process_Preconditions
-
- begin
- -- Find the last internally generate declaration starting from the
- -- top of the body declarations. This ensures that discriminals and
- -- subtypes are properly visible to the pragma Check equivalents.
-
- if Present (Decls) then
- Decl := First (Decls);
- while Present (Decl) loop
- exit when Comes_From_Source (Decl);
- Insert_Node := Decl;
- Next (Decl);
- end loop;
- end if;
-
- -- The processing of preconditions is done in reverse order (body
- -- first) because each pragma Check equivalent is inserted at the
- -- top of the declarations. This ensures that the final order is
- -- consistent with following diagram:
-
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
-
- Process_Preconditions_For (Body_Id);
-
- if Present (Spec_Id) then
- Process_Preconditions_For (Spec_Id);
- Process_Inherited_Preconditions;
- 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.
-
- 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
- return;
-
- -- Otherwise mark the subprogram
-
- else
- Set_Has_Expanded_Contract (Subp_Id);
- end if;
-
- -- Ensure that the formal parameters are visible when expanding all
- -- contract items.
-
- if not In_Open_Scopes (Subp_Id) then
- Restore_Scope := True;
- Push_Scope (Subp_Id);
-
- if Is_Generic_Subprogram (Subp_Id) then
- Install_Generic_Formals (Subp_Id);
- else
- Install_Formals (Subp_Id);
- end if;
- end if;
-
- -- 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:
-
- -- 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;
-
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
- -- <contract case conditions>
-
- -- <source declarations>
- -- begin
- -- <source statements>
-
- -- _Preconditions (Result);
- -- return Result;
- -- end Example;
-
- -- Routine _Postconditions holds all contract assertions that must be
- -- verified on exit from the related subprogram.
-
- -- 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.
-
- 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.
-
- Process_Postconditions (Stmts);
-
- -- Step 3: Handle pragma Contract_Cases. This action must come before
- -- the processing of invariants and predicates because those append
- -- items to list Smts.
-
- Process_Contract_Cases (Stmts);
-
- -- Step 4: Apply invariant and predicate checks on a function result and
- -- all formals. The resulting checks are accumulated in list Stmts.
-
- Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
-
- -- Step 5: Construct procedure _Postconditions
-
- Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
-
- if Restore_Scope then
- End_Scope;
- end if;
- end Expand_Subprogram_Contract;
-
--------------------------------------------
-- Has_Unconstrained_Access_Discriminants --
--------------------------------------------
-- This procedure contains common processing for Expand_N_Function_Call,
-- Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
- procedure Expand_Subprogram_Contract (N : Node_Id);
- -- Expand the contracts of a subprogram body and its correspoding spec (if
- -- any). This routine processes all [refined] pre- and postconditions as
- -- well as Contract_Cases, invariants and predicates. N denotes the body of
- -- the subprogram.
-
procedure Freeze_Subprogram (N : Node_Id);
-- generate the appropriate expansions related to Subprogram freeze
-- nodes (e.g. the filling of the corresponding Dispatch Table for
ada/casing.o \
ada/checks.o \
ada/comperr.o \
+ ada/contracts.o \
ada/csets.o \
ada/cstand.o \
ada/debug.o \
int __gl_num_interrupt_states = 0;
int __gl_unreserve_all_interrupts = 0;
int __gl_exception_tracebacks = 0;
+int __gl_exception_tracebacks_symbolic = 0;
int __gl_detect_blocking = 0;
int __gl_default_stack_size = -1;
int __gl_leap_seconds_support = 0;
Exception_Tracebacks : Boolean := False;
-- GNATBIND
- -- Set to True to store tracebacks in exception occurrences (-E)
+ -- Set to True to store tracebacks in exception occurrences (-Ea or -E)
+
+ Exception_Tracebacks_Symbolic : Boolean := False;
+ -- GNATBIND
+ -- Set to True to store tracebacks in exception occurrences and enable
+ -- symbolic tracebacks (-Es).
Extensions_Allowed : Boolean := False;
-- GNAT
-- may return any string output in association with a provided call chain.
-- The decorator replaces the default backtrace mentioned above.
+-- On systems that use DWARF debugging output, then if the "-g" compiler
+-- switch and the "-Es" binder switch are used, the decorator is automatically
+-- set to Symbolic_Traceback.
+
with System.Traceback_Entries;
package System.Exception_Traces is
-- output for a call chain provided by way of a tracebacks array.
procedure Set_Trace_Decorator (Decorator : Traceback_Decorator);
- -- Set the decorator to be used for future automatic outputs. Restore
- -- the default behavior (output of raw addresses) if the provided
- -- access value is null.
+ -- Set the decorator to be used for future automatic outputs. Restore the
+ -- default behavior if the provided access value is null.
--
-- Note: System.Traceback.Symbolic.Symbolic_Traceback may be used as the
-- Decorator, to get a symbolic traceback. This will cause a significant
- -- cpu and memory overhead.
+ -- cpu and memory overhead on some platforms.
+ --
+ -- Note: The Decorator is called when constructing the
+ -- Exception_Information; that needs to be taken into account
+ -- if the Decorator has any side effects.
end System.Exception_Traces;
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Errout; use Errout;
-with Exp_Util; use Exp_Util;
-with Elists; use Elists;
-with Fname; use Fname;
-with Fname.UF; use Fname.UF;
-with Freeze; use Freeze;
-with Impunit; use Impunit;
-with Inline; use Inline;
-with Lib; use Lib;
-with Lib.Load; use Lib.Load;
-with Lib.Xref; use Lib.Xref;
-with Namet; use Namet;
-with Nlists; use Nlists;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Output; use Output;
-with Par_SCO; use Par_SCO;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch7; use Sem_Ch7;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Dist; use Sem_Dist;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinfo.CN; use Sinfo.CN;
-with Sinput; use Sinput;
-with Snames; use Snames;
-with Style; use Style;
-with Stylesw; use Stylesw;
-with Tbuild; use Tbuild;
-with Uname; use Uname;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Errout; use Errout;
+with Exp_Util; use Exp_Util;
+with Elists; use Elists;
+with Fname; use Fname;
+with Fname.UF; use Fname.UF;
+with Freeze; use Freeze;
+with Impunit; use Impunit;
+with Inline; use Inline;
+with Lib; use Lib;
+with Lib.Load; use Lib.Load;
+with Lib.Xref; use Lib.Xref;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Output; use Output;
+with Par_SCO; use Par_SCO;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch7; use Sem_Ch7;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Dist; use Sem_Dist;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinfo.CN; use Sinfo.CN;
+with Sinput; use Sinput;
+with Snames; use Snames;
+with Style; use Style;
+with Stylesw; use Stylesw;
+with Tbuild; use Tbuild;
+with Uname; use Uname;
package body Sem_Ch10 is
N_Subprogram_Declaration)
then
Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
-
- -- Capture all global references in a generic subprogram that acts as
- -- a compilation unit now that the contract has been analyzed.
-
- if Is_Generic_Declaration_Or_Body (Unit_Node) then
- Save_Global_References_In_Contract
- (Templ => Original_Node (Unit_Node),
- Gen_Id => Defining_Entity (Unit_Node));
- end if;
end if;
-- Generate distribution stubs if requested and no error
Restore_Opt_Config_Switches (Opts);
end Analyze_Subprogram_Body_Stub;
- -------------------------------------------
- -- Analyze_Subprogram_Body_Stub_Contract --
- -------------------------------------------
-
- procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
- Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
-
- begin
- -- A subprogram body stub may act as its own spec or as the completion
- -- of a previous declaration. Depending on the context, the contract of
- -- the stub may contain two sets of pragmas.
-
- -- The stub is a completion, the applicable pragmas are:
- -- Refined_Depends
- -- Refined_Global
-
- if Present (Spec_Id) then
- Analyze_Subprogram_Body_Contract (Stub_Id);
-
- -- The stub acts as its own spec, the applicable pragmas are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
-
- else
- Analyze_Subprogram_Contract (Stub_Id);
- end if;
- end Analyze_Subprogram_Body_Stub_Contract;
-
---------------------
-- Analyze_Subunit --
---------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, 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 Types; use Types;
+
package Sem_Ch10 is
procedure Analyze_Compilation_Unit (N : Node_Id);
procedure Analyze_With_Clause (N : Node_Id);
procedure Analyze_Protected_Body_Stub (N : Node_Id);
procedure Analyze_Subunit (N : Node_Id);
- procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of a subprogram body
- -- stub Stub_Id as if they appeared at the end of a declarative region. The
- -- aspects in question are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Refined_Depends
- -- Refined_Global
- -- Test_Case
-
procedure Install_Context (N : Node_Id);
-- Installs the entities from the context clause of the given compilation
-- unit into the visibility chains. This is done before analyzing a unit.
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Einfo; use Einfo;
-with Elists; use Elists;
-with Errout; use Errout;
-with Expander; use Expander;
-with Exp_Disp; use Exp_Disp;
-with Fname; use Fname;
-with Fname.UF; use Fname.UF;
-with Freeze; use Freeze;
-with Ghost; use Ghost;
-with Itypes; use Itypes;
-with Lib; use Lib;
-with Lib.Load; use Lib.Load;
-with Lib.Xref; use Lib.Xref;
-with Nlists; use Nlists;
-with Namet; use Namet;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Rident; use Rident;
-with Restrict; use Restrict;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Cat; use Sem_Cat;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch7; use Sem_Ch7;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Dim; use Sem_Dim;
-with Sem_Disp; use Sem_Disp;
-with Sem_Elab; use Sem_Elab;
-with Sem_Elim; use Sem_Elim;
-with Sem_Eval; use Sem_Eval;
-with Sem_Prag; use Sem_Prag;
-with Sem_Res; use Sem_Res;
-with Sem_Type; use Sem_Type;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinfo.CN; use Sinfo.CN;
-with Sinput; use Sinput;
-with Sinput.L; use Sinput.L;
-with Snames; use Snames;
-with Stringt; use Stringt;
-with Uname; use Uname;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Contracts; use Contracts;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Expander; use Expander;
+with Exp_Disp; use Exp_Disp;
+with Fname; use Fname;
+with Fname.UF; use Fname.UF;
+with Freeze; use Freeze;
+with Ghost; use Ghost;
+with Itypes; use Itypes;
+with Lib; use Lib;
+with Lib.Load; use Lib.Load;
+with Lib.Xref; use Lib.Xref;
+with Nlists; use Nlists;
+with Namet; use Namet;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Rident; use Rident;
+with Restrict; use Restrict;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Cat; use Sem_Cat;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch7; use Sem_Ch7;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Dim; use Sem_Dim;
+with Sem_Disp; use Sem_Disp;
+with Sem_Elab; use Sem_Elab;
+with Sem_Elim; use Sem_Elim;
+with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
+with Sem_Res; use Sem_Res;
+with Sem_Type; use Sem_Type;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinfo.CN; use Sinfo.CN;
+with Sinput; use Sinput;
+with Sinput.L; use Sinput.L;
+with Snames; use Snames;
+with Stringt; use Stringt;
+with Uname; use Uname;
with Table;
-with Tbuild; use Tbuild;
-with Uintp; use Uintp;
-with Urealp; use Urealp;
-with Warnsw; use Warnsw;
+with Tbuild; use Tbuild;
+with Uintp; use Uintp;
+with Urealp; use Urealp;
+with Warnsw; use Warnsw;
with GNAT.HTable;
-- Restore suffix 'P' to primitives of Prims_List and leave Prims_List
-- set to No_Elist.
- procedure Save_Global_References_In_Aspects (N : Node_Id);
- -- Save all global references found within the expressions of all aspects
- -- that appear on node N.
-
procedure Set_Instance_Env
(Gen_Unit : Entity_Id;
Act_Unit : Entity_Id);
-- aspects that appear in the generic. This renaming declaration is
-- inserted after the instance declaration which it renames.
- procedure Instantiate_Subprogram_Contract (Templ : Node_Id);
- -- Instantiate all source pragmas found in the contract of the generic
- -- subprogram declaration template denoted by Templ. The instantiated
- -- pragmas are added to list Renaming_List.
-
------------------------------------
-- Analyze_Instance_And_Renamings --
------------------------------------
end if;
end Build_Subprogram_Renaming;
- -------------------------------------
- -- Instantiate_Subprogram_Contract --
- -------------------------------------
-
- procedure Instantiate_Subprogram_Contract (Templ : Node_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 Renaming_List.
-
- -------------------------
- -- Instantiate_Pragmas --
- -------------------------
-
- procedure Instantiate_Pragmas (First_Prag : Node_Id) is
- Inst_Prag : Node_Id;
- Prag : Node_Id;
-
- 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_Analyzed (Inst_Prag, False);
- Append_To (Renaming_List, Inst_Prag);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end Instantiate_Pragmas;
-
- -- Local variables
-
- Items : constant Node_Id := Contract (Defining_Entity (Templ));
-
- -- Start of processing for Instantiate_Subprogram_Contract
-
- 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;
-
-- Local variables
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- must be instantiated explicitly because they are not part of the
-- subprogram template.
- Instantiate_Subprogram_Contract (Original_Node (Gen_Decl));
- Build_Subprogram_Renaming;
+ Instantiate_Subprogram_Contract
+ (Original_Node (Gen_Decl), Renaming_List);
+ Build_Subprogram_Renaming;
Analyze_Instance_And_Renamings;
-- If the generic is marked Import (Intrinsic), then so is the
Copy_Generic_Node
(Original_Node (Gen_Body), Empty, Instantiating => True);
- -- Build new name (possibly qualified) for body declaration
+ -- Create proper (possibly qualified) defining name for the body, to
+ -- correspond to the one in the spec.
- Act_Body_Id := New_Copy (Act_Decl_Id);
+ Act_Body_Id :=
+ Make_Defining_Identifier (Sloc (Act_Decl_Id), Chars (Act_Decl_Id));
+ Set_Comes_From_Source (Act_Body_Id, Comes_From_Source (Act_Decl_Id));
-- Some attributes of spec entity are not inherited by body entity
then
Act_Body_Name :=
Make_Defining_Program_Unit_Name (Loc,
- Name => New_Copy_Tree (Name (Defining_Unit_Name (Act_Spec))),
+ Name =>
+ New_Copy_Tree (Name (Defining_Unit_Name (Act_Spec))),
Defining_Identifier => Act_Body_Id);
else
Act_Body_Name := Act_Body_Id;
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Anon_Id : constant Entity_Id :=
+ Act_Decl_Id : constant Entity_Id :=
Defining_Unit_Name (Specification (Act_Decl));
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
Saved_Warnings : constant Warning_Record := Save_Warnings;
Act_Body : Node_Id;
+ Act_Body_Id : Entity_Id;
Gen_Body : Node_Id;
Gen_Body_Id : Node_Id;
Pack_Body : Node_Id;
-- the spec entity appropriately.
if Is_Imported (Gen_Unit) then
- Set_Is_Imported (Anon_Id);
- Set_First_Rep_Item (Anon_Id, First_Rep_Item (Gen_Unit));
- Set_Interface_Name (Anon_Id, Interface_Name (Gen_Unit));
- Set_Convention (Anon_Id, Convention (Gen_Unit));
- Set_Has_Completion (Anon_Id);
+ Set_Is_Imported (Act_Decl_Id);
+ Set_First_Rep_Item (Act_Decl_Id, First_Rep_Item (Gen_Unit));
+ Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit));
+ Set_Convention (Act_Decl_Id, Convention (Gen_Unit));
+ Set_Has_Completion (Act_Decl_Id);
return;
-- For other cases, compile the body
("missing proper body for instantiation", Gen_Body);
end if;
- Set_Has_Completion (Anon_Id);
+ Set_Has_Completion (Act_Decl_Id);
return;
end if;
- Save_Env (Gen_Unit, Anon_Id);
+ Save_Env (Gen_Unit, Act_Decl_Id);
Style_Check := False;
-- If the context of the instance is subject to SPARK_Mode "off" or
Copy_Generic_Node
(Original_Node (Gen_Body), Empty, Instantiating => True);
- -- Create proper defining name for the body, to correspond to
- -- the one in the spec.
+ -- Create proper defining name for the body, to correspond to the one
+ -- in the spec.
+
+ Act_Body_Id :=
+ Make_Defining_Identifier (Sloc (Act_Decl_Id), Chars (Act_Decl_Id));
- Set_Defining_Unit_Name (Specification (Act_Body),
- Make_Defining_Identifier
- (Sloc (Defining_Entity (Inst_Node)), Chars (Anon_Id)));
- Set_Corresponding_Spec (Act_Body, Anon_Id);
- Set_Has_Completion (Anon_Id);
+ Set_Comes_From_Source (Act_Body_Id, Comes_From_Source (Act_Decl_Id));
+ Set_Defining_Unit_Name (Specification (Act_Body), Act_Body_Id);
+
+ Set_Corresponding_Spec (Act_Body, Act_Decl_Id);
+ Set_Has_Completion (Act_Decl_Id);
Check_Generic_Actuals (Pack_Id, False);
-- Generate a reference to link the visible subprogram instance to
if Body_Optional then
return;
- elsif Ekind (Anon_Id) = E_Procedure then
+ elsif Ekind (Act_Decl_Id) = E_Procedure then
Act_Body :=
Make_Subprogram_Body (Loc,
Specification =>
Make_Procedure_Specification (Loc,
Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Anon_Id)),
+ Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
Parameter_Specifications =>
New_Copy_List
- (Parameter_Specifications (Parent (Anon_Id)))),
+ (Parameter_Specifications (Parent (Act_Decl_Id)))),
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Raise_Program_Error (Loc,
Reason => PE_Access_Before_Elaboration);
- Set_Etype (Ret_Expr, (Etype (Anon_Id)));
+ Set_Etype (Ret_Expr, (Etype (Act_Decl_Id)));
Set_Analyzed (Ret_Expr);
Act_Body :=
Specification =>
Make_Function_Specification (Loc,
Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Anon_Id)),
+ Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
Parameter_Specifications =>
New_Copy_List
- (Parameter_Specifications (Parent (Anon_Id))),
+ (Parameter_Specifications (Parent (Act_Decl_Id))),
Result_Definition =>
- New_Occurrence_Of (Etype (Anon_Id), Loc)),
+ New_Occurrence_Of (Etype (Act_Decl_Id), Loc)),
Declarations => Empty_List,
Handled_Statement_Sequence =>
end loop;
end Save_Global_References_In_Aspects;
- ----------------------------------------
- -- Save_Global_References_In_Contract --
- ----------------------------------------
-
- 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.
-
- ------------------------------------
- -- Save_Global_References_In_List --
- ------------------------------------
-
- procedure Save_Global_References_In_List (First_Prag : Node_Id) is
- Prag : Node_Id;
-
- begin
- 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
-
- Items : constant Node_Id := Contract (Defining_Entity (Templ));
-
- -- Start of processing for Save_Global_References_In_Contract
-
- begin
- -- 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;
-
--------------------------------------
-- Set_Copied_Sloc_For_Inlined_Body --
--------------------------------------
-- restored in stack-like fashion. Front-end inlining also uses these
-- structures for the management of private/full views.
- procedure Save_Global_References_In_Contract
- (Templ : Node_Id;
- Gen_Id : Entity_Id);
- -- Save all global references found within the aspect specifications and
- -- the contract-related source pragmas assocated with generic template
- -- Templ. Gen_Id denotes the entity of the analyzed generic copy.
+ procedure Save_Global_References_In_Aspects (N : Node_Id);
+ -- Save all global references found within the expressions of all aspects
+ -- that appear on node N.
procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id);
-- This procedure is used when a subprogram body is inlined. This process
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Checks; use Checks;
-with Debug; use Debug;
-with Elists; use Elists;
-with Einfo; use Einfo;
-with Errout; use Errout;
-with Eval_Fat; use Eval_Fat;
-with Exp_Ch3; use Exp_Ch3;
-with Exp_Ch9; use Exp_Ch9;
-with Exp_Disp; use Exp_Disp;
-with Exp_Dist; use Exp_Dist;
-with Exp_Tss; use Exp_Tss;
-with Exp_Util; use Exp_Util;
-with Fname; use Fname;
-with Freeze; use Freeze;
-with Ghost; use Ghost;
-with Itypes; use Itypes;
-with Layout; use Layout;
-with Lib; use Lib;
-with Lib.Xref; use Lib.Xref;
-with Namet; use Namet;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Case; use Sem_Case;
-with Sem_Cat; use Sem_Cat;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch7; use Sem_Ch7;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Dim; use Sem_Dim;
-with Sem_Disp; use Sem_Disp;
-with Sem_Dist; use Sem_Dist;
-with Sem_Elim; use Sem_Elim;
-with Sem_Eval; use Sem_Eval;
-with Sem_Mech; use Sem_Mech;
-with Sem_Prag; use Sem_Prag;
-with Sem_Res; use Sem_Res;
-with Sem_Smem; use Sem_Smem;
-with Sem_Type; use Sem_Type;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinput; use Sinput;
-with Snames; use Snames;
-with Targparm; use Targparm;
-with Tbuild; use Tbuild;
-with Ttypes; use Ttypes;
-with Uintp; use Uintp;
-with Urealp; use Urealp;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Checks; use Checks;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Elists; use Elists;
+with Einfo; use Einfo;
+with Errout; use Errout;
+with Eval_Fat; use Eval_Fat;
+with Exp_Ch3; use Exp_Ch3;
+with Exp_Ch9; use Exp_Ch9;
+with Exp_Disp; use Exp_Disp;
+with Exp_Dist; use Exp_Dist;
+with Exp_Tss; use Exp_Tss;
+with Exp_Util; use Exp_Util;
+with Fname; use Fname;
+with Freeze; use Freeze;
+with Ghost; use Ghost;
+with Itypes; use Itypes;
+with Layout; use Layout;
+with Lib; use Lib;
+with Lib.Xref; use Lib.Xref;
+with Namet; use Namet;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Case; use Sem_Case;
+with Sem_Cat; use Sem_Cat;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch7; use Sem_Ch7;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Dim; use Sem_Dim;
+with Sem_Disp; use Sem_Disp;
+with Sem_Dist; use Sem_Dist;
+with Sem_Elim; use Sem_Elim;
+with Sem_Eval; use Sem_Eval;
+with Sem_Mech; use Sem_Mech;
+with Sem_Res; use Sem_Res;
+with Sem_Smem; use Sem_Smem;
+with Sem_Type; use Sem_Type;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinput; use Sinput;
+with Snames; use Snames;
+with Targparm; use Targparm;
+with Tbuild; use Tbuild;
+with Ttypes; use Ttypes;
+with Uintp; use Uintp;
+with Urealp; use Urealp;
package body Sem_Ch3 is
-- abstract interface types implemented by a record type or a derived
-- record type.
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
- -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
- -- if they appeared at the end of the declarative region. The pragmas to be
- -- considered are:
- -- Async_Readers
- -- Async_Writers
- -- Effective_Reads
- -- Effective_Writes
- -- Part_Of
-
procedure Build_Derived_Type
(N : Node_Id;
Parent_Type : Entity_Id;
Context : Node_Id := Empty;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
- Pack_Decl : Node_Id := Empty;
Body_Seen : Boolean := False;
-- Flag set when the first body [stub] is encountered
Context := Parent (L);
if Nkind (Context) = N_Package_Specification then
- Pack_Decl := Parent (Context);
-- When a package has private declarations, its contract must be
-- analyzed at the end of the said declarations. This way both the
end if;
elsif Nkind (Context) = N_Package_Body then
- Pack_Decl := Context;
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
-- Analyze the contracts of all subprogram declarations, subprogram
- -- bodies and variables now due to the delayed visibility needs of
- -- of their aspects and pragmas. Capture global references in generic
- -- subprograms or bodies.
+ -- bodies and variables due to the delayed visibility needs of their
+ -- aspects and pragmas.
Decl := First (L);
while Present (Decl) loop
Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
end if;
- -- Capture all global references in a generic subprogram or a body
- -- [stub] now that the contract has been analyzed.
-
- if Nkind_In (Decl, N_Generic_Subprogram_Declaration,
- N_Subprogram_Body,
- N_Subprogram_Body_Stub)
- and then Is_Generic_Declaration_Or_Body (Decl)
- then
- Save_Global_References_In_Contract
- (Templ => Original_Node (Decl),
- Gen_Id => Corresponding_Spec_Of (Decl));
- end if;
-
Next (Decl);
end loop;
- -- The owner of the declarations is a package [body]
+ if Nkind (Context) = N_Package_Body then
- if Present (Pack_Decl) then
+ -- Ensure that all abstract states and objects declared in the
+ -- state space of a package body are utilized as constituents.
- -- Capture all global references in a generic package or a body
- -- after all nested generic subprograms and bodies were subjected
- -- to the same processing.
-
- if Is_Generic_Declaration_Or_Body (Pack_Decl) then
- Save_Global_References_In_Contract
- (Templ => Original_Node (Pack_Decl),
- Gen_Id => Corresponding_Spec_Of (Pack_Decl));
- end if;
+ Check_Unused_Body_States (Defining_Entity (Context));
-- State refinements are visible upto the end the of the package
-- body declarations. Hide the state refinements from visibility
-- to restore the original state conditions.
- if Nkind (Pack_Decl) = N_Package_Body then
- Remove_Visible_Refinements (Corresponding_Spec (Pack_Decl));
- end if;
+ Remove_Visible_Refinements (Corresponding_Spec (Context));
end if;
end if;
end Analyze_Declarations;
end if;
end Analyze_Number_Declaration;
- -----------------------------
- -- Analyze_Object_Contract --
- -----------------------------
-
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
- Obj_Typ : constant Entity_Id := Etype (Obj_Id);
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Prag : Node_Id;
- Seen : Boolean := False;
-
- begin
- -- The loop parameter in an element iterator over a formal container
- -- is declared with an object declaration but no contracts apply.
-
- if Ekind (Obj_Id) = E_Loop_Parameter then
- return;
- end if;
-
- -- Constant related checks
-
- if Ekind (Obj_Id) = E_Constant then
-
- -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
- -- This check is relevant only when SPARK_Mode is on as it is not a
- -- standard Ada legality rule. Internally-generated constants that
- -- map generic formals to actuals in instantiations are allowed to
- -- be volatile.
-
- if SPARK_Mode = On
- and then Comes_From_Source (Obj_Id)
- and then Is_Effectively_Volatile (Obj_Id)
- and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
- then
- Error_Msg_N ("constant cannot be volatile", Obj_Id);
- end if;
-
- -- Variable related checks
-
- else pragma Assert (Ekind (Obj_Id) = E_Variable);
-
- -- The following checks are relevant only when SPARK_Mode is on as
- -- they are not standard Ada legality rules. Internally generated
- -- temporaries are ignored.
-
- if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
- if Is_Effectively_Volatile (Obj_Id) then
-
- -- The declaration of an effectively volatile object must
- -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
-
- if not Is_Library_Level_Entity (Obj_Id) then
- Error_Msg_N
- ("volatile variable & must be declared at library level",
- Obj_Id);
-
- -- An object of a discriminated type cannot be effectively
- -- volatile except for protected objects (SPARK RM 7.1.3(5)).
-
- elsif Has_Discriminants (Obj_Typ)
- and then not Is_Protected_Type (Obj_Typ)
- 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
-
- else
- -- A non-effectively volatile object cannot have effectively
- -- volatile components (SPARK RM 7.1.3(6)).
-
- if not Is_Effectively_Volatile (Obj_Id)
- and then Has_Volatile_Component (Obj_Typ)
- then
- Error_Msg_N
- ("non-volatile object & cannot have volatile components",
- Obj_Id);
- end if;
- end if;
- end if;
-
- if Is_Ghost_Entity (Obj_Id) then
-
- -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
-
- if Is_Effectively_Volatile (Obj_Id) then
- Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
-
- -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
-
- elsif Is_Imported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
-
- elsif Is_Exported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
- end if;
- end if;
-
- -- Analyze all external properties
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
- Seen := True;
- end if;
-
- -- Verify the mutual interaction of the various external properties
-
- if Seen then
- Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
- end if;
- end if;
-
- -- Check whether the lack of indicator Part_Of agrees with the placement
- -- of the object with respect to the state space.
-
- Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-
- if No (Prag) then
- Check_Missing_Part_Of (Obj_Id);
- end if;
-
- -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
- -- exception to this is the object that represents the dispatch table of
- -- a Ghost tagged type as the symbol needs to be exported.
-
- if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
- if Is_Exported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
-
- elsif Is_Imported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
- end if;
- end if;
- end Analyze_Object_Contract;
-
--------------------------------
-- Analyze_Object_Declaration --
--------------------------------
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Checks; use Checks;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Elists; use Elists;
-with Errout; use Errout;
-with Expander; use Expander;
-with Exp_Ch6; use Exp_Ch6;
-with Exp_Ch7; use Exp_Ch7;
-with Exp_Ch9; use Exp_Ch9;
-with Exp_Dbug; use Exp_Dbug;
-with Exp_Disp; use Exp_Disp;
-with Exp_Tss; use Exp_Tss;
-with Exp_Util; use Exp_Util;
-with Fname; use Fname;
-with Freeze; use Freeze;
-with Ghost; use Ghost;
-with Inline; use Inline;
-with Itypes; use Itypes;
-with Lib.Xref; use Lib.Xref;
-with Layout; use Layout;
-with Namet; use Namet;
-with Lib; use Lib;
-with Nlists; use Nlists;
-with Nmake; use Nmake;
-with Opt; use Opt;
-with Output; use Output;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Cat; use Sem_Cat;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch4; use Sem_Ch4;
-with Sem_Ch5; use Sem_Ch5;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Dim; use Sem_Dim;
-with Sem_Disp; use Sem_Disp;
-with Sem_Dist; use Sem_Dist;
-with Sem_Elim; use Sem_Elim;
-with Sem_Eval; use Sem_Eval;
-with Sem_Mech; use Sem_Mech;
-with Sem_Prag; use Sem_Prag;
-with Sem_Res; use Sem_Res;
-with Sem_Util; use Sem_Util;
-with Sem_Type; use Sem_Type;
-with Sem_Warn; use Sem_Warn;
-with Sinput; use Sinput;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinfo.CN; use Sinfo.CN;
-with Snames; use Snames;
-with Stringt; use Stringt;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Checks; use Checks;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Expander; use Expander;
+with Exp_Ch6; use Exp_Ch6;
+with Exp_Ch7; use Exp_Ch7;
+with Exp_Ch9; use Exp_Ch9;
+with Exp_Dbug; use Exp_Dbug;
+with Exp_Disp; use Exp_Disp;
+with Exp_Tss; use Exp_Tss;
+with Exp_Util; use Exp_Util;
+with Fname; use Fname;
+with Freeze; use Freeze;
+with Ghost; use Ghost;
+with Inline; use Inline;
+with Itypes; use Itypes;
+with Lib.Xref; use Lib.Xref;
+with Layout; use Layout;
+with Namet; use Namet;
+with Lib; use Lib;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Opt; use Opt;
+with Output; use Output;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Cat; use Sem_Cat;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch4; use Sem_Ch4;
+with Sem_Ch5; use Sem_Ch5;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Dim; use Sem_Dim;
+with Sem_Disp; use Sem_Disp;
+with Sem_Dist; use Sem_Dist;
+with Sem_Elim; use Sem_Elim;
+with Sem_Eval; use Sem_Eval;
+with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
+with Sem_Res; use Sem_Res;
+with Sem_Util; use Sem_Util;
+with Sem_Type; use Sem_Type;
+with Sem_Warn; use Sem_Warn;
+with Sinput; use Sinput;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinfo.CN; use Sinfo.CN;
+with Snames; use Snames;
+with Stringt; use Stringt;
with Style;
-with Stylesw; use Stylesw;
-with Tbuild; use Tbuild;
-with Uintp; use Uintp;
-with Urealp; use Urealp;
-with Validsw; use Validsw;
+with Stylesw; use Stylesw;
+with Tbuild; use Tbuild;
+with Uintp; use Uintp;
+with Urealp; use Urealp;
+with Validsw; use Validsw;
package body Sem_Ch6 is
Analyze_Declarations (Declarations (N));
Check_Completion;
- -- When a generic subprogram body appears inside a package, its
- -- contract is analyzed at the end of the package body declarations.
- -- This is due to the delay with respect of the package contract upon
- -- which the body contract may depend. When the generic subprogram
- -- body is a compilation unit, this delay is not necessary.
+ -- Process the contract of the subprogram body after all declarations
+ -- have been analyzed. This ensures that any contract-related pragmas
+ -- are available through the N_Contract node of the body.
- if Nkind (Parent (N)) = N_Compilation_Unit then
- Analyze_Subprogram_Body_Contract (Body_Id);
-
- -- Capture all global references in a generic subprogram body
- -- that acts as a compilation unit now that the contract has
- -- been analyzed.
-
- Save_Global_References_In_Contract
- (Templ => Original_Node (N),
- Gen_Id => Gen_Id);
- end if;
+ Analyze_Subprogram_Body_Contract (Body_Id);
Analyze (Handled_Statement_Sequence (N));
Save_Global_References (Original_Node (N));
end if;
end Analyze_Subprogram_Body;
- --------------------------------------
- -- Analyze_Subprogram_Body_Contract --
- --------------------------------------
-
- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Body_Id);
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
- Ref_Depends : Node_Id := Empty;
- Ref_Global : Node_Id := Empty;
-
- begin
- -- When a subprogram body declaration is illegal, its defining entity is
- -- left unanalyzed. There is nothing left to do in this case because the
- -- body lacks a contract, or even a proper Ekind.
-
- if Ekind (Body_Id) = E_Void then
- return;
- 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 subprogram body.
-
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
-
- -- All subprograms carry a contract, but for some it is not significant
- -- and should not be processed.
-
- if not Has_Significant_Contract (Body_Id) then
- null;
-
- -- The subprogram body is a completion, analyze all delayed pragmas that
- -- apply. Note that when the body is stand alone, the pragmas are always
- -- analyzed on the spot.
-
- elsif Present (Items) then
-
- -- Locate and store pragmas Refined_Depends and Refined_Global since
- -- their order of analysis matters.
-
- Prag := Classifications (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Refined_Depends then
- Ref_Depends := Prag;
-
- elsif Prag_Nam = Name_Refined_Global then
- Ref_Global := Prag;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze Refined_Global first as Refined_Depends may mention items
- -- classified in the global refinement.
-
- if Present (Ref_Global) then
- Analyze_Refined_Global_In_Decl_Part (Ref_Global);
- end if;
-
- -- Refined_Depends must be analyzed after Refined_Global in order to
- -- see the modes of all global refinements.
-
- if Present (Ref_Depends) then
- Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
- end if;
- end if;
-
- -- Ensure that the contract cases or postconditions mention 'Result or
- -- define a post-state.
-
- Check_Result_And_Post_State (Body_Id);
-
- -- A stand alone non-volatile function body cannot have an effectively
- -- 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.
-
- if SPARK_Mode = On
- and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
- and then not Is_Volatile_Function (Body_Id)
- then
- Check_Nonvolatile_Function_Profile (Body_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
- end Analyze_Subprogram_Body_Contract;
-
------------------------------------
-- Analyze_Subprogram_Body_Helper --
------------------------------------
-- Start of processing for Analyze_Subprogram_Body_Helper
begin
+ -- A [generic] subprogram body "freezes" the contract of the nearest
+ -- enclosing package body:
+
+ -- package body Nearest_Enclosing_Package
+ -- with Refined_State => (State => Constit)
+ -- is
+ -- Constit : ...;
+
+ -- procedure Freezes_Enclosing_Package_Body
+ -- with Refined_Depends => (Input => Constit) ...
+
+ -- This ensures that any annotations referenced by the contract of the
+ -- [generic] subprogram body are available. This form of "freezing" is
+ -- decoupled from the usual Freeze_xxx mechanism because it must also
+ -- work in the context of generics where normal freezing is disabled.
+
+ Analyze_Enclosing_Package_Body_Contract (N);
+
-- Generic subprograms are handled separately. They always have a
-- generic specification. Determine whether current scope has a
-- previous declaration.
end if;
end if;
- -- When a subprogram body appears inside a package, its contract is
- -- analyzed at the end of the package body declarations. This is due
- -- to the delay with respect of the package contract upon which the
- -- body contract may depend. When the subprogram body is stand alone
- -- and acts as a compilation unit, this delay is not necessary.
+ -- A subprogram body "freezes" its own contract. Analyze the contract
+ -- after the declarations of the body have been processed as pragmas
+ -- are now chained on the contract of the subprogram body.
- if Nkind (Parent (N)) = N_Compilation_Unit then
- Analyze_Subprogram_Body_Contract (Body_Id);
- end if;
-
- -- Deal with preconditions, [refined] postconditions, Contract_Cases,
- -- invariants and predicates associated with body and its spec. Since
- -- there is no routine Expand_Declarations which would otherwise deal
- -- with the contract expansion, generate all necessary mechanisms to
- -- verify the contract assertions now.
-
- Expand_Subprogram_Contract (N);
+ Analyze_Subprogram_Body_Contract (Body_Id);
-- If SPARK_Mode for body is not On, disable frontend inlining for this
-- subprogram in GNATprove mode, as its body should not be analyzed.
Ghost_Mode := Save_Ghost_Mode;
end Analyze_Subprogram_Body_Helper;
- ---------------------------------
- -- Analyze_Subprogram_Contract --
- ---------------------------------
-
- procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Subp_Id);
- Depends : Node_Id := Empty;
- Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
-
- begin
- -- 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 subprogram body.
-
- Save_SPARK_Mode_And_Set (Subp_Id, Mode);
-
- -- All subprograms carry a contract, but for some it is not significant
- -- and should not be processed.
-
- if not Has_Significant_Contract (Subp_Id) then
- null;
-
- elsif Present (Items) then
-
- -- Analyze pre- and postconditions
-
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze contract-cases and test-cases
-
- Prag := Contract_Test_Cases (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Contract_Cases then
- Analyze_Contract_Cases_In_Decl_Part (Prag);
- else
- pragma Assert (Prag_Nam = Name_Test_Case);
- Analyze_Test_Case_In_Decl_Part (Prag);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze classification pragmas
-
- Prag := Classifications (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Depends then
- Depends := Prag;
-
- elsif Prag_Nam = Name_Global then
- Global := Prag;
-
- -- Note that pragma Extensions_Visible has already been analyzed
-
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze Global first as Depends may mention items classified in
- -- the global categorization.
-
- if Present (Global) then
- Analyze_Global_In_Decl_Part (Global);
- end if;
-
- -- Depends must be analyzed after Global in order to see the modes of
- -- all global items.
-
- if Present (Depends) then
- Analyze_Depends_In_Decl_Part (Depends);
- end if;
-
- -- Ensure that the contract cases or postconditions mention 'Result
- -- or define a post-state.
-
- Check_Result_And_Post_State (Subp_Id);
- end if;
-
- -- A non-volatile function cannot have an effectively 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 pragma Volatile_Function is processed
- -- after the analysis of the related subprogram declaration.
-
- if SPARK_Mode = On
- and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
- and then not Is_Volatile_Function (Subp_Id)
- then
- Check_Nonvolatile_Function_Profile (Subp_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
- end Analyze_Subprogram_Contract;
-
------------------------------------
-- Analyze_Subprogram_Declaration --
------------------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id);
procedure Analyze_Subprogram_Body (N : Node_Id);
- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of subprogram body
- -- Body_Id as if they appeared at the end of a declarative region. Aspects
- -- in question are:
- -- Contract_Cases (stand alone body)
- -- Depends (stand alone body)
- -- Global (stand alone body)
- -- Postcondition (stand alone body)
- -- Precondition (stand alone body)
- -- Refined_Depends
- -- Refined_Global
- -- Refined_Post
- -- Test_Case (stand alone body)
-
- procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of subprogram
- -- Subp_Id as if they appeared at the end of a declarative region. The
- -- aspects in question are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
-
function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id;
-- Analyze subprogram specification in both subprogram declarations
-- and body declarations. Returns the defining entity for the
-- handling of private and full declarations, and the construction of dispatch
-- tables for tagged types.
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Elists; use Elists;
-with Errout; use Errout;
-with Exp_Disp; use Exp_Disp;
-with Exp_Dist; use Exp_Dist;
-with Exp_Dbug; use Exp_Dbug;
-with Ghost; use Ghost;
-with Lib; use Lib;
-with Lib.Xref; use Lib.Xref;
-with Namet; use Namet;
-with Nmake; use Nmake;
-with Nlists; use Nlists;
-with Opt; use Opt;
-with Output; use Output;
-with Restrict; use Restrict;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Cat; use Sem_Cat;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Disp; use Sem_Disp;
-with Sem_Eval; use Sem_Eval;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Snames; use Snames;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinput; use Sinput;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Contracts; use Contracts;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Exp_Disp; use Exp_Disp;
+with Exp_Dist; use Exp_Dist;
+with Exp_Dbug; use Exp_Dbug;
+with Ghost; use Ghost;
+with Lib; use Lib;
+with Lib.Xref; use Lib.Xref;
+with Namet; use Namet;
+with Nmake; use Nmake;
+with Nlists; use Nlists;
+with Opt; use Opt;
+with Output; use Output;
+with Restrict; use Restrict;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Cat; use Sem_Cat;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Disp; use Sem_Disp;
+with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Snames; use Snames;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinput; use Sinput;
with Style;
-with Uintp; use Uintp;
+with Uintp; use Uintp;
package body Sem_Ch7 is
end if;
end Analyze_Package_Body;
- -----------------------------------
- -- Analyze_Package_Body_Contract --
- -----------------------------------
-
- procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
- Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
- Mode : SPARK_Mode_Type;
- Ref_State : Node_Id;
-
- begin
- -- 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 body.
-
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
-
- Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
-
- -- The analysis of pragma Refined_State detects whether the spec has
- -- abstract states available for refinement.
-
- if Present (Ref_State) then
- Analyze_Refined_State_In_Decl_Part (Ref_State);
-
- -- State refinement is required when the package declaration defines at
- -- least one abstract state. Null states are not considered. Refinement
- -- is not envorced 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);
- end Analyze_Package_Body_Contract;
-
---------------------------------
-- Analyze_Package_Body_Helper --
---------------------------------
-- Start of processing for Analyze_Package_Body_Helper
begin
+ -- A [generic] package body "freezes" the contract of the nearest
+ -- enclosing package body:
+
+ -- package body Nearest_Enclosing_Package
+ -- with Refined_State => (State => Constit)
+ -- is
+ -- Constit : ...;
+
+ -- package body Freezes_Enclosing_Package_Body
+ -- with Refined_State => (State_2 => Constit_2)
+ -- is
+ -- Constit_2 : ...;
+
+ -- procedure Proc
+ -- with Refined_Depends => (Input => (Constit, Constit_2)) ...
+
+ -- This ensures that any annotations referenced by the contract of a
+ -- [generic] subprogram body declared within the current package body
+ -- are available. This form of "freezing" is decoupled from the usual
+ -- Freeze_xxx mechanism because it must also work in the context of
+ -- generics where normal freezing is disabled.
+
+ Analyze_Enclosing_Package_Body_Contract (N);
+
-- Find corresponding package specification, and establish the current
-- scope. The visible defining entity for the package is the defining
-- occurrence in the spec. On exit from the package body, all body
Ghost_Mode := Save_Ghost_Mode;
end Analyze_Package_Body_Helper;
- ------------------------------
- -- Analyze_Package_Contract --
- ------------------------------
-
- procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Pack_Id);
- Init : Node_Id := Empty;
- Init_Cond : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
-
- begin
- -- 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.
-
- Save_SPARK_Mode_And_Set (Pack_Id, Mode);
-
- if Present (Items) then
-
- -- Locate and store pragmas Initial_Condition and Initializes since
- -- their order of analysis matters.
-
- Prag := Classifications (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Initial_Condition then
- Init_Cond := Prag;
-
- elsif Prag_Nam = Name_Initializes then
- Init := Prag;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze the initialization related pragmas. Initializes must come
- -- before Initial_Condition due to item dependencies.
-
- if Present (Init) then
- Analyze_Initializes_In_Decl_Part (Init);
- end if;
-
- if Present (Init_Cond) then
- Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
- 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);
- end Analyze_Package_Contract;
-
---------------------------------
-- Analyze_Package_Declaration --
---------------------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, 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- --
procedure Analyze_Package_Specification (N : Node_Id);
procedure Analyze_Private_Type_Declaration (N : Node_Id);
- procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of package body
- -- Body_Id as if they appeared at the end of a declarative region. The
- -- aspects that are considered are:
- -- Refined_State
-
- procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of package Pack_Id
- -- as if they appeared at the end of a declarative region. The aspects
- -- that are considered are:
- -- Initial_Condition
- -- Initializes
- -- Part_Of
-
procedure End_Package_Scope (P : Entity_Id);
-- Calls Uninstall_Declarations, and then pops the scope stack
-- to complete the syntax checks. Certain pragmas are handled partially or
-- completely by the parser (see Par.Prag for further details).
-with Aspects; use Aspects;
-with Atree; use Atree;
-with Casing; use Casing;
-with Checks; use Checks;
-with Csets; use Csets;
-with Debug; use Debug;
-with Einfo; use Einfo;
-with Elists; use Elists;
-with Errout; use Errout;
-with Exp_Dist; use Exp_Dist;
-with Exp_Util; use Exp_Util;
-with Freeze; use Freeze;
-with Ghost; use Ghost;
-with Lib; use Lib;
-with Lib.Writ; use Lib.Writ;
-with Lib.Xref; use Lib.Xref;
-with Namet.Sp; use Namet.Sp;
-with Nlists; use Nlists;
-with Nmake; use Nmake;
-with Output; use Output;
-with Par_SCO; use Par_SCO;
-with Restrict; use Restrict;
-with Rident; use Rident;
-with Rtsfind; use Rtsfind;
-with Sem; use Sem;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch3; use Sem_Ch3;
-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_Dist; use Sem_Dist;
-with Sem_Elim; use Sem_Elim;
-with Sem_Eval; use Sem_Eval;
-with Sem_Intr; use Sem_Intr;
-with Sem_Mech; use Sem_Mech;
-with Sem_Res; use Sem_Res;
-with Sem_Type; use Sem_Type;
-with Sem_Util; use Sem_Util;
-with Sem_Warn; use Sem_Warn;
-with Stand; use Stand;
-with Sinfo; use Sinfo;
-with Sinfo.CN; use Sinfo.CN;
-with Sinput; use Sinput;
-with Stringt; use Stringt;
-with Stylesw; use Stylesw;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Casing; use Casing;
+with Checks; use Checks;
+with Contracts; use Contracts;
+with Csets; use Csets;
+with Debug; use Debug;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Exp_Dist; use Exp_Dist;
+with Exp_Util; use Exp_Util;
+with Freeze; use Freeze;
+with Ghost; use Ghost;
+with Lib; use Lib;
+with Lib.Writ; use Lib.Writ;
+with Lib.Xref; use Lib.Xref;
+with Namet.Sp; use Namet.Sp;
+with Nlists; use Nlists;
+with Nmake; use Nmake;
+with Output; use Output;
+with Par_SCO; use Par_SCO;
+with Restrict; use Restrict;
+with Rident; use Rident;
+with Rtsfind; use Rtsfind;
+with Sem; use Sem;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch3; use Sem_Ch3;
+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_Dist; use Sem_Dist;
+with Sem_Elim; use Sem_Elim;
+with Sem_Eval; use Sem_Eval;
+with Sem_Intr; use Sem_Intr;
+with Sem_Mech; use Sem_Mech;
+with Sem_Res; use Sem_Res;
+with Sem_Type; use Sem_Type;
+with Sem_Util; use Sem_Util;
+with Sem_Warn; use Sem_Warn;
+with Stand; use Stand;
+with Sinfo; use Sinfo;
+with Sinfo.CN; use Sinfo.CN;
+with Sinput; use Sinput;
+with Stringt; use Stringt;
+with Stylesw; use Stylesw;
with Table;
-with Targparm; use Targparm;
-with Tbuild; use Tbuild;
+with Targparm; use Targparm;
+with Tbuild; use Tbuild;
with Ttypes;
-with Uintp; use Uintp;
-with Uname; use Uname;
-with Urealp; use Urealp;
-with Validsw; use Validsw;
-with Warnsw; use Warnsw;
+with Uintp; use Uintp;
+with Uname; use Uname;
+with Urealp; use Urealp;
+with Validsw; use Validsw;
+with Warnsw; use Warnsw;
package body Sem_Prag is
-- Local Subprograms and Variables --
-------------------------------------
- procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id);
- -- Subsidiary routine to the analysis of pragmas Depends, Global and
- -- Refined_State. Append an entity to a list. If the list is empty, create
- -- a new list.
-
function Adjust_External_Name_Case (N : Node_Id) return Node_Id;
-- This routine is used for possible casing adjustment of an explicit
-- external name supplied as a string literal (the node N), according to
-- pragma in the source program, a breakpoint on rv catches this place in
-- the source, allowing convenient stepping to the point of interest.
- --------------
- -- Add_Item --
- --------------
-
- procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id) is
- begin
- Append_New_Elmt (Item, To => To_List);
- end Add_Item;
-
-------------------------------
-- Adjust_External_Name_Case --
-------------------------------
SPARK_Msg_NE
("duplicate use of item &", Item, Item_Id);
else
- Add_Item (Item_Id, Seen);
+ Append_New_Elmt (Item_Id, Seen);
end if;
-- Detect illegal use of an input related to a null
-- of all processed inputs.
if Is_Input or else Self_Ref then
- Add_Item (Item_Id, All_Inputs_Seen);
+ Append_New_Elmt (Item_Id, All_Inputs_Seen);
end if;
-- State related checks (SPARK RM 6.1.5(3))
-- processed items.
if Ekind (Item_Id) = E_Abstract_State then
- Add_Item (Item_Id, States_Seen);
+ Append_New_Elmt (Item_Id, States_Seen);
end if;
if Ekind_In (Item_Id, E_Abstract_State,
E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
- Add_Item (Item_Id, Constits_Seen);
+ Append_New_Elmt (Item_Id, Constits_Seen);
end if;
-- All other input/output items are illegal
-- items.
else
- Add_Item (Item_Id, Seen);
+ Append_New_Elmt (Item_Id, Seen);
if Ekind (Item_Id) = E_Abstract_State then
- Add_Item (Item_Id, States_Seen);
+ Append_New_Elmt (Item_Id, States_Seen);
end if;
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
- Add_Item (Item_Id, Constits_Seen);
+ Append_New_Elmt (Item_Id, Constits_Seen);
end if;
end if;
end Analyze_Global_Item;
-- and variables.
else
- Add_Item (Item_Id, Items_Seen);
+ Append_New_Elmt (Item_Id, Items_Seen);
if Ekind (Item_Id) = E_Abstract_State then
- Add_Item (Item_Id, States_Seen);
+ Append_New_Elmt (Item_Id, States_Seen);
end if;
if Present (Encapsulating_State (Item_Id)) then
- Add_Item (Item_Id, Constits_Seen);
+ Append_New_Elmt (Item_Id, Constits_Seen);
end if;
end if;
-- Input is legal, add it to the list of processed inputs
else
- Add_Item (Input_Id, Inputs_Seen);
+ Append_New_Elmt (Input_Id, Inputs_Seen);
if Ekind (Input_Id) = E_Abstract_State then
- Add_Item (Input_Id, States_Seen);
+ Append_New_Elmt (Input_Id, States_Seen);
end if;
if Ekind_In (Input_Id, E_Abstract_State,
E_Variable)
and then Present (Encapsulating_State (Input_Id))
then
- Add_Item (Input_Id, Constits_Seen);
+ Append_New_Elmt (Input_Id, Constits_Seen);
end if;
end if;
if Comes_From_Source (Decl)
and then Nkind (Decl) = N_Object_Declaration
then
- Add_Item (Defining_Entity (Decl), States_And_Objs);
+ Append_New_Elmt (Defining_Entity (Decl), States_And_Objs);
end if;
Next (Decl);
if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then
SPARK_Msg_NE
- ("indicator Part_Of must denote an abstract state of& "
- & "or public descendant (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote an abstract state or "
+ & "public descendant of & (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
elsif Scope (State_Id) = Parent_Unit
else
SPARK_Msg_NE
- ("indicator Part_Of must denote an abstract state of& "
- & "or public descendant (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote an abstract state or "
+ & "public descendant of & (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
end if;
procedure Record_Item (Item_Id : Entity_Id) is
begin
if not Contains (Matched_Items, Item_Id) then
- Add_Item (Item_Id, Matched_Items);
+ Append_New_Elmt (Item_Id, Matched_Items);
end if;
end Record_Item;
and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
- Add_Item (Item_Id, In_Constits);
+ Append_New_Elmt (Item_Id, In_Constits);
elsif Global_Mode = Name_In_Out then
- Add_Item (Item_Id, In_Out_Constits);
+ Append_New_Elmt (Item_Id, In_Out_Constits);
elsif Global_Mode = Name_Output then
- Add_Item (Item_Id, Out_Constits);
+ Append_New_Elmt (Item_Id, Out_Constits);
elsif Global_Mode = Name_Proof_In then
- Add_Item (Item_Id, Proof_In_Constits);
+ Append_New_Elmt (Item_Id, Proof_In_Constits);
end if;
-- When not a constituent, ensure that both occurrences of the
-- Add the item to the proper list
if Item_Mode = Name_Input then
- Add_Item (Item_Id, In_Items);
+ Append_New_Elmt (Item_Id, In_Items);
elsif Item_Mode = Name_In_Out then
- Add_Item (Item_Id, In_Out_Items);
+ Append_New_Elmt (Item_Id, In_Out_Items);
elsif Item_Mode = Name_Output then
- Add_Item (Item_Id, Out_Items);
+ Append_New_Elmt (Item_Id, Out_Items);
elsif Item_Mode = Name_Proof_In then
- Add_Item (Item_Id, Proof_In_Items);
+ Append_New_Elmt (Item_Id, Proof_In_Items);
end if;
end Collect_Global_Item;
-- Analyze_Refined_State_In_Decl_Part --
----------------------------------------
- procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Refined_State_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
Body_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
-- A list that contains all constituents processed so far. The list is
-- used to detect multiple uses of the same constituent.
+ Freeze_Posted : Boolean := False;
+ -- A flag that controls the output of a freezing-related error (see use
+ -- below).
+
Refined_States_Seen : Elist_Id := No_Elist;
-- A list that contains all refined states processed so far. The list is
-- used to detect duplicate refinements.
procedure Analyze_Refinement_Clause (Clause : Node_Id);
-- Perform full analysis of a single refinement clause
- function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id;
- -- Gather the entities of all abstract states and objects declared in
- -- the body state space of package Pack_Id.
-
procedure Report_Unrefined_States (States : Elist_Id);
-- Emit errors for all unrefined abstract states found in list States
- procedure Report_Unused_States (States : Elist_Id);
- -- Emit errors for all unused states found in list States
-
-------------------------------
-- Analyze_Refinement_Clause --
-------------------------------
procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
-- Determine whether constituent Constit denoted by its entity
- -- Constit_Id appears in Hidden_States. Emit an error when the
+ -- Constit_Id appears in Body_States. Emit an error when the
-- constituent is not a valid hidden state of the related package
-- or when it is used more than once. Otherwise remove the
- -- constituent from Hidden_States.
+ -- constituent from Body_States.
--------------------------------
-- Check_Matching_Constituent --
-- Add the constituent to the list of processed items to aid
-- with the detection of duplicates.
- Add_Item (Constit_Id, Constituents_Seen);
+ Append_New_Elmt (Constit_Id, Constituents_Seen);
-- Collect the constituent in the list of refinement items
-- and establish a relation between the refined state and
if Is_Entity_Name (Constit) then
Constit_Id := Entity_Of (Constit);
- if Ekind_In (Constit_Id, E_Abstract_State,
- E_Constant,
- E_Variable)
+ -- When a constituent is declared after a subprogram body
+ -- that caused "freezing" of the related contract where
+ -- pragma Refined_State resides, the constituent appears
+ -- undefined and carries Any_Id as its entity.
+
+ -- package body Pack
+ -- with Refined_State => (State => Constit)
+ -- is
+ -- procedure Proc
+ -- with Refined_Global => (Input => Constit)
+ -- is
+ -- ...
+ -- end Proc;
+
+ -- Constit : ...;
+ -- end Pack;
+
+ if Constit_Id = Any_Id then
+ SPARK_Msg_NE ("& is undefined", Constit, Constit_Id);
+
+ -- Emit a specialized info message when the contract of
+ -- the related package body was "frozen" by another body.
+ -- Note that it is not possible to precisely identify why
+ -- the constituent is undefined because it is not visible
+ -- when pragma Refined_State is analyzed. This message is
+ -- a reasonable approximation.
+
+ if Present (Freeze_Id) and then not Freeze_Posted then
+ Freeze_Posted := True;
+
+ Error_Msg_Name_1 := Chars (Body_Id);
+ Error_Msg_Sloc := Sloc (Freeze_Id);
+ SPARK_Msg_NE
+ ("body & declared # freezes the contract of %",
+ N, Freeze_Id);
+ SPARK_Msg_N
+ ("\all constituents must be declared before body #",
+ N);
+ end if;
+
+ -- The constituent is a valid state or object
+
+ elsif Ekind_In (Constit_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
then
Check_Matching_Constituent (Constit_Id);
+ -- Otherwise the constituent is illegal
+
else
SPARK_Msg_NE
("constituent & must denote object or state",
-- been refined.
if Node (State_Elmt) = State_Id then
- Add_Item (State_Id, Refined_States_Seen);
+ Append_New_Elmt (State_Id, Refined_States_Seen);
Remove_Elmt (Available_States, State_Elmt);
return;
end if;
Report_Unused_Constituents (Part_Of_Constits);
end Analyze_Refinement_Clause;
- -------------------------
- -- Collect_Body_States --
- -------------------------
-
- function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id is
- Result : Elist_Id := No_Elist;
- -- A list containing all body states of Pack_Id
-
- procedure Collect_Visible_States (Pack_Id : Entity_Id);
- -- Gather the entities of all abstract states and objects declared in
- -- the visible state space of package Pack_Id.
-
- ----------------------------
- -- Collect_Visible_States --
- ----------------------------
-
- procedure Collect_Visible_States (Pack_Id : Entity_Id) is
- Item_Id : Entity_Id;
-
- begin
- -- Traverse the entity chain of the package and inspect all
- -- visible items.
-
- Item_Id := First_Entity (Pack_Id);
- while Present (Item_Id) and then not In_Private_Part (Item_Id) loop
-
- -- Do not consider internally generated items as those cannot
- -- be named and participate in refinement.
-
- if not Comes_From_Source (Item_Id) then
- null;
-
- elsif Ekind (Item_Id) = E_Abstract_State then
- Add_Item (Item_Id, Result);
-
- -- Do not consider constants or variables that map generic
- -- formals to their actuals, as the formals cannot be named
- -- from the outside and participate in refinement.
-
- elsif Ekind_In (Item_Id, E_Constant, E_Variable)
- and then No (Corresponding_Generic_Association
- (Declaration_Node (Item_Id)))
- then
- Add_Item (Item_Id, Result);
-
- -- Recursively gather the visible states of a nested package
-
- elsif Ekind (Item_Id) = E_Package then
- Collect_Visible_States (Item_Id);
- end if;
-
- Next_Entity (Item_Id);
- end loop;
- end Collect_Visible_States;
-
- -- Local variables
-
- Pack_Body : constant Node_Id :=
- Declaration_Node (Body_Entity (Pack_Id));
- Decl : Node_Id;
- Item_Id : Entity_Id;
-
- -- Start of processing for Collect_Body_States
-
- begin
- -- Inspect the declarations of the body looking for source objects,
- -- packages and package instantiations.
-
- Decl := First (Declarations (Pack_Body));
- while Present (Decl) loop
-
- -- Capture source objects as internally generated temporaries
- -- cannot be named and participate in refinement.
-
- if Nkind (Decl) = N_Object_Declaration then
- Item_Id := Defining_Entity (Decl);
-
- if Comes_From_Source (Item_Id) then
- Add_Item (Item_Id, Result);
- end if;
-
- -- Capture the visible abstract states and objects of a source
- -- package [instantiation].
-
- elsif Nkind (Decl) = N_Package_Declaration then
- Item_Id := Defining_Entity (Decl);
-
- if Comes_From_Source (Item_Id) then
- Collect_Visible_States (Item_Id);
- end if;
- end if;
-
- Next (Decl);
- end loop;
-
- return Result;
- end Collect_Body_States;
-
-----------------------------
-- Report_Unrefined_States --
-----------------------------
end if;
end Report_Unrefined_States;
- --------------------------
- -- Report_Unused_States --
- --------------------------
-
- procedure Report_Unused_States (States : Elist_Id) is
- Posted : Boolean := False;
- State_Elmt : Elmt_Id;
- State_Id : Entity_Id;
-
- begin
- if Present (States) then
- State_Elmt := First_Elmt (States);
- while Present (State_Elmt) loop
- State_Id := Node (State_Elmt);
-
- -- Constants are part of the hidden state of a package, but the
- -- compiler cannot determine whether they have variable input
- -- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
- -- hidden state. Do not emit an error when a constant does not
- -- participate in a state refinement, even though it acts as a
- -- hidden state.
-
- if Ekind (State_Id) = E_Constant then
- null;
-
- -- Generate an error message of the form:
-
- -- body of package ... has unused hidden states
- -- abstract state ... defined at ...
- -- variable ... defined at ...
-
- else
- if not Posted then
- Posted := True;
- SPARK_Msg_N
- ("body of package & has unused hidden states", Body_Id);
- end if;
-
- Error_Msg_Sloc := Sloc (State_Id);
-
- if Ekind (State_Id) = E_Abstract_State then
- SPARK_Msg_NE
- ("\abstract state & defined #", Body_Id, State_Id);
-
- else
- pragma Assert (Ekind (State_Id) = E_Variable);
- SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
- end if;
- end if;
-
- Next_Elmt (State_Elmt);
- end loop;
- end if;
- end Report_Unused_States;
-
-- Local declarations
Clauses : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
-- state space of the package body. These items must be utilized as
-- constituents in a state refinement.
- Body_States := Collect_Body_States (Spec_Id);
+ Body_States := Collect_Body_States (Body_Id);
-- Multiple non-null state refinements appear as an aggregate
-- Ensure that all abstract states and objects declared in the body
-- state space of the related package are utilized as constituents.
- Report_Unused_States (Body_States);
+ Report_Unused_Body_States (Body_Id, Body_States);
end Analyze_Refined_State_In_Decl_Part;
------------------------------------
else
if Is_Input then
- Add_Item (Item, Subp_Inputs);
+ Append_New_Elmt (Item, Subp_Inputs);
else
- Add_Item (Item, Subp_Outputs);
+ Append_New_Elmt (Item, Subp_Outputs);
end if;
end if;
end Collect_Dependency_Item;
procedure Collect_Global_Item (Item : Node_Id; Mode : Name_Id) is
begin
if Nam_In (Mode, Name_In_Out, Name_Input) then
- Add_Item (Item, Subp_Inputs);
+ Append_New_Elmt (Item, Subp_Inputs);
end if;
if Nam_In (Mode, Name_In_Out, Name_Output) then
- Add_Item (Item, Subp_Outputs);
+ Append_New_Elmt (Item, Subp_Outputs);
end if;
end Collect_Global_Item;
E_In_Out_Parameter,
E_In_Parameter)
then
- Add_Item (Formal, Subp_Inputs);
+ Append_New_Elmt (Formal, Subp_Inputs);
end if;
if Ekind_In (Formal, E_Generic_In_Out_Parameter,
E_In_Out_Parameter,
E_Out_Parameter)
then
- Add_Item (Formal, Subp_Outputs);
+ Append_New_Elmt (Formal, Subp_Outputs);
-- Out parameters can act as inputs when the related type is
-- tagged, unconstrained array, unconstrained record or record
if Ekind (Formal) = E_Out_Parameter
and then Is_Unconstrained_Or_Tagged_Item (Formal)
then
- Add_Item (Formal, Subp_Inputs);
+ Append_New_Elmt (Formal, Subp_Inputs);
end if;
end if;
-- uses Analyze_Global_In_Decl_Part as a starting point, then performs
-- various consistency checks between Global and Refined_Global.
- procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of delayed pragma Refined_State
+ procedure Analyze_Refined_State_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Refined_State. Freeze_Id denotes
+ -- the entity of [generic] package body or [generic] subprogram body which
+ -- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case
with Sem_Attr; use Sem_Attr;
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_Eval; use Sem_Eval;
end if;
end Add_Block_Identifier;
- -----------------------
- -- Add_Contract_Item --
- -----------------------
-
- procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
- Items : Node_Id := Contract (Id);
-
- procedure Add_Classification;
- -- Prepend Prag to the list of classifications
-
- procedure Add_Contract_Test_Case;
- -- Prepend Prag to the list of contract and test cases
-
- procedure Add_Pre_Post_Condition;
- -- Prepend Prag to the list of pre- and postconditions
-
- ------------------------
- -- Add_Classification --
- ------------------------
-
- procedure Add_Classification is
- begin
- Set_Next_Pragma (Prag, Classifications (Items));
- Set_Classifications (Items, Prag);
- end Add_Classification;
-
- ----------------------------
- -- Add_Contract_Test_Case --
- ----------------------------
-
- procedure Add_Contract_Test_Case is
- begin
- Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
- Set_Contract_Test_Cases (Items, Prag);
- end Add_Contract_Test_Case;
-
- ----------------------------
- -- Add_Pre_Post_Condition --
- ----------------------------
-
- procedure Add_Pre_Post_Condition is
- begin
- Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
- Set_Pre_Post_Conditions (Items, Prag);
- end Add_Pre_Post_Condition;
-
- -- 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);
-
- -- Create a new contract when adding the first item
-
- if No (Items) then
- Items := Make_Contract (Sloc (Id));
- Set_Contract (Id, Items);
- end if;
-
- -- Contract items related to constants. Applicable pragmas are:
- -- Part_Of
-
- if Ekind (Id) = E_Constant then
- if Prag_Nam = Name_Part_Of then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
- -- Contract items related to [generic] packages or instantiations. The
- -- applicable pragmas are:
- -- Abstract_States
- -- Initial_Condition
- -- Initializes
- -- Part_Of (instantiation only)
-
- elsif Ekind_In (Id, E_Generic_Package, E_Package) then
- if Nam_In (Prag_Nam, Name_Abstract_State,
- Name_Initial_Condition,
- Name_Initializes)
- then
- Add_Classification;
-
- -- Indicator Part_Of must be associated with a package instantiation
-
- elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
- -- Contract items related to package bodies. The applicable pragmas are:
- -- Refined_States
-
- elsif Ekind (Id) = E_Package_Body then
- if Prag_Nam = Name_Refined_State then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
- -- Contract items related to subprogram or entry declarations. The
- -- applicable pragmas are:
- -- Contract_Cases
- -- Depends
- -- Extensions_Visible
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
- -- Volatile_Function
-
- elsif Ekind_In (Id, E_Entry, E_Entry_Family)
- or else Is_Generic_Subprogram (Id)
- or else Is_Subprogram (Id)
- then
- if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
- Add_Pre_Post_Condition;
-
- elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
- Add_Contract_Test_Case;
-
- elsif Nam_In (Prag_Nam, Name_Depends,
- Name_Extensions_Visible,
- Name_Global)
- then
- Add_Classification;
-
- elsif Prag_Nam = Name_Volatile_Function
- and then Ekind_In (Id, E_Function, E_Generic_Function)
- then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
- -- Contract items related to subprogram bodies. Applicable pragmas are:
- -- Postcondition
- -- Precondition
- -- Refined_Depends
- -- Refined_Global
- -- Refined_Post
-
- elsif Ekind (Id) = E_Subprogram_Body then
- if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
- Add_Classification;
-
- elsif Nam_In (Prag_Nam, Name_Postcondition,
- Name_Precondition,
- Name_Refined_Post)
- then
- Add_Pre_Post_Condition;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
- -- Contract items related to variables. Applicable pragmas are:
- -- Async_Readers
- -- Async_Writers
- -- Constant_After_Elaboration
- -- Effective_Reads
- -- Effective_Writes
- -- Part_Of
-
- elsif Ekind (Id) = E_Variable then
- if Nam_In (Prag_Nam, Name_Async_Readers,
- Name_Async_Writers,
- Name_Constant_After_Elaboration,
- Name_Effective_Reads,
- Name_Effective_Writes,
- Name_Part_Of)
- then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
- end if;
- end Add_Contract_Item;
-
----------------------------
-- Add_Global_Declaration --
----------------------------
end if;
end Check_Unprotected_Access;
+ ------------------------------
+ -- Check_Unused_Body_States --
+ ------------------------------
+
+ procedure Check_Unused_Body_States (Body_Id : Entity_Id) is
+ Legal_Constits : Boolean := True;
+ -- This flag designates whether all constituents of pragma Refined_State
+ -- are legal. The flag is used to suppress the generation of potentially
+ -- misleading error messages due to a malformed pragma.
+
+ procedure Process_Refinement_Clause
+ (Clause : Node_Id;
+ States : Elist_Id);
+ -- Inspect all constituents of refinement clause Clause and remove any
+ -- matches from body state list States.
+
+ -------------------------------
+ -- Process_Refinement_Clause --
+ -------------------------------
+
+ procedure Process_Refinement_Clause
+ (Clause : Node_Id;
+ States : Elist_Id)
+ is
+ procedure Process_Constituent (Constit : Node_Id);
+ -- Remove constituent Constit from body state list States
+
+ -------------------------
+ -- Process_Constituent --
+ -------------------------
+
+ procedure Process_Constituent (Constit : Node_Id) is
+ Constit_Id : Entity_Id;
+
+ begin
+ if Error_Posted (Constit) then
+ Legal_Constits := False;
+ end if;
+
+ -- Guard against illegal constituents. Only abstract states and
+ -- objects can appear on the right hand side of a refinement.
+
+ if Is_Entity_Name (Constit) then
+ Constit_Id := Entity_Of (Constit);
+
+ if Present (Constit_Id)
+ and then Ekind_In (Constit_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
+ then
+ Remove (States, Constit_Id);
+ end if;
+ end if;
+ end Process_Constituent;
+
+ -- Local variables
+
+ Constit : Node_Id;
+
+ -- Start of processing for Process_Refinement_Clause
+
+ begin
+ if Nkind (Clause) = N_Component_Association then
+ Constit := Expression (Clause);
+
+ -- Multiple constituents appear as an aggregate
+
+ if Nkind (Constit) = N_Aggregate then
+ Constit := First (Expressions (Constit));
+ while Present (Constit) loop
+ Process_Constituent (Constit);
+ Next (Constit);
+ end loop;
+
+ -- Various forms of a single constituent
+
+ else
+ Process_Constituent (Constit);
+ end if;
+ end if;
+ end Process_Refinement_Clause;
+
+ -- Local variables
+
+ Prag : constant Node_Id :=
+ Get_Pragma (Body_Id, Pragma_Refined_State);
+ Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
+ Clause : Node_Id;
+ States : Elist_Id;
+
+ -- Start of processing for Check_Unused_Body_States
+
+ begin
+ -- Inspect the clauses of pragma Refined_State and determine whether all
+ -- visible states declared within the body of the package participate in
+ -- the refinement.
+
+ if Present (Prag) then
+ Clause := Expression (Get_Argument (Prag, Spec_Id));
+ States := Collect_Body_States (Body_Id);
+
+ -- Multiple non-null state refinements appear as an aggregate
+
+ if Nkind (Clause) = N_Aggregate then
+ Clause := First (Component_Associations (Clause));
+ while Present (Clause) loop
+ Process_Refinement_Clause (Clause, States);
+ Next (Clause);
+ end loop;
+
+ -- Various forms of a single state refinement
+
+ else
+ Process_Refinement_Clause (Clause, States);
+ end if;
+
+ -- Ensure that all abstract states and objects declared in the body
+ -- state space of the related package are utilized as constituents.
+
+ if Legal_Constits then
+ Report_Unused_Body_States (Body_Id, States);
+ end if;
+ end if;
+ end Check_Unused_Body_States;
+
+ -------------------------
+ -- Collect_Body_States --
+ -------------------------
+
+ function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id is
+ procedure Collect_Visible_States
+ (Pack_Id : Entity_Id;
+ States : in out Elist_Id);
+ -- Gather the entities of all abstract states and objects declared in
+ -- the visible state space of package Pack_Id.
+
+ ----------------------------
+ -- Collect_Visible_States --
+ ----------------------------
+
+ procedure Collect_Visible_States
+ (Pack_Id : Entity_Id;
+ States : in out Elist_Id)
+ is
+ Item_Id : Entity_Id;
+
+ begin
+ -- Traverse the entity chain of the package and inspect all visible
+ -- items.
+
+ Item_Id := First_Entity (Pack_Id);
+ while Present (Item_Id) and then not In_Private_Part (Item_Id) loop
+
+ -- Do not consider internally generated items as those cannot be
+ -- named and participate in refinement.
+
+ if not Comes_From_Source (Item_Id) then
+ null;
+
+ elsif Ekind (Item_Id) = E_Abstract_State then
+ Append_New_Elmt (Item_Id, States);
+
+ -- Do not consider objects that map generic formals to their
+ -- actuals, as the formals cannot be named from the outside and
+ -- participate in refinement.
+
+ elsif Ekind_In (Item_Id, E_Constant, E_Variable)
+ and then No (Corresponding_Generic_Association
+ (Declaration_Node (Item_Id)))
+ then
+ Append_New_Elmt (Item_Id, States);
+
+ -- Recursively gather the visible states of a nested package
+
+ elsif Ekind (Item_Id) = E_Package then
+ Collect_Visible_States (Item_Id, States);
+ end if;
+
+ Next_Entity (Item_Id);
+ end loop;
+ end Collect_Visible_States;
+
+ -- Local variables
+
+ Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
+ Decl : Node_Id;
+ Item_Id : Entity_Id;
+ States : Elist_Id := No_Elist;
+
+ -- Start of processing for Collect_Body_States
+
+ begin
+ -- Inspect the declarations of the body looking for source objects,
+ -- packages and package instantiations.
+
+ Decl := First (Declarations (Body_Decl));
+ while Present (Decl) loop
+
+ -- Capture source objects as internally generated temporaries cannot
+ -- be named and participate in refinement.
+
+ if Nkind (Decl) = N_Object_Declaration then
+ Item_Id := Defining_Entity (Decl);
+
+ if Comes_From_Source (Item_Id) then
+ Append_New_Elmt (Item_Id, States);
+ end if;
+
+ -- Capture the visible abstract states and objects of a source
+ -- package [instantiation].
+
+ elsif Nkind (Decl) = N_Package_Declaration then
+ Item_Id := Defining_Entity (Decl);
+
+ if Comes_From_Source (Item_Id) then
+ Collect_Visible_States (Item_Id, States);
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ return States;
+ end Collect_Body_States;
+
------------------------
-- Collect_Interfaces --
------------------------
end if;
end Corresponding_Spec_Of;
- -----------------------------
- -- Create_Generic_Contract --
- -----------------------------
-
- procedure Create_Generic_Contract (Unit : Node_Id) is
- Templ : constant Node_Id := Original_Node (Unit);
- Templ_Id : constant Entity_Id := Defining_Entity (Templ);
-
- procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
- -- Add a single contract-related source pragma Prag to the contract of
- -- generic template Templ_Id.
-
- ---------------------------------
- -- Add_Generic_Contract_Pragma --
- ---------------------------------
-
- procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
- Prag_Templ : Node_Id;
-
- begin
- -- Mark the pragma to prevent the premature capture of global
- -- references when capturing global references of the context
- -- (see Save_References_In_Pragma).
-
- Set_Is_Generic_Contract_Pragma (Prag);
-
- -- Pragmas that apply to a generic subprogram declaration are not
- -- part of the semantic structure of the generic template:
-
- -- generic
- -- procedure Example (Formal : Integer);
- -- pragma Precondition (Formal > 0);
-
- -- Create a generic template for such pragmas and link the template
- -- of the pragma with the generic template.
-
- if Nkind (Templ) = N_Generic_Subprogram_Declaration then
- Rewrite
- (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
- Prag_Templ := Original_Node (Prag);
-
- Set_Is_Generic_Contract_Pragma (Prag_Templ);
- Add_Contract_Item (Prag_Templ, Templ_Id);
-
- -- Otherwise link the pragma with the generic template
-
- else
- Add_Contract_Item (Prag, Templ_Id);
- end if;
- end Add_Generic_Contract_Pragma;
-
- -- Local variables
-
- Context : constant Node_Id := Parent (Unit);
- Decl : Node_Id := Empty;
-
- -- Start of processing for Create_Generic_Contract
-
- begin
- -- A generic package declaration carries contract-related source pragmas
- -- in its visible declarations.
-
- if Nkind (Templ) = N_Generic_Package_Declaration then
- Set_Ekind (Templ_Id, E_Generic_Package);
-
- if Present (Visible_Declarations (Specification (Templ))) then
- Decl := First (Visible_Declarations (Specification (Templ)));
- end if;
-
- -- A generic package body carries contract-related source pragmas in its
- -- declarations.
-
- elsif Nkind (Templ) = N_Package_Body then
- Set_Ekind (Templ_Id, E_Package_Body);
-
- if Present (Declarations (Templ)) then
- Decl := First (Declarations (Templ));
- end if;
-
- -- Generic subprogram declaration
-
- 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;
-
- -- When the generic subprogram acts as a compilation unit, inspect
- -- the Pragmas_After list for contract-related source pragmas.
-
- 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;
-
- -- Otherwise inspect the successive declarations for contract-related
- -- source pragmas.
-
- else
- Decl := Next (Unit);
- end if;
-
- -- A generic subprogram body carries contract-related source pragmas in
- -- its declarations.
-
- elsif Nkind (Templ) = N_Subprogram_Body then
- Set_Ekind (Templ_Id, E_Subprogram_Body);
-
- if Present (Declarations (Templ)) then
- Decl := First (Declarations (Templ));
- end if;
- end if;
-
- -- Inspect the relevant declarations looking for contract-related source
- -- pragmas and add them to the contract of the generic unit.
-
- while Present (Decl) loop
- if Comes_From_Source (Decl) then
- if Nkind (Decl) = N_Pragma then
-
- -- The source pragma is a contract annotation
-
- if Is_Contract_Annotation (Decl) then
- Add_Generic_Contract_Pragma (Decl);
- end if;
-
- -- The region where a contract-related source pragma may appear
- -- ends with the first source non-pragma declaration or statement.
-
- else
- exit;
- end if;
- end if;
-
- Next (Decl);
- end loop;
- end Create_Generic_Contract;
-
--------------------
-- Current_Entity --
--------------------
end if;
end Inherit_Rep_Item_Chain;
- ---------------------------------
- -- Inherit_Subprogram_Contract --
- ---------------------------------
-
- 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.
-
- --------------------
- -- Inherit_Pragma --
- --------------------
-
- procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
- Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
- New_Prag : Node_Id;
-
- 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 is inherited for distrinction purposes.
-
- if Present (Prag) then
- New_Prag := New_Copy_Tree (Prag);
- Set_Is_Inherited (New_Prag);
-
- Add_Contract_Item (New_Prag, Subp);
- end if;
- end Inherit_Pragma;
-
- -- Start of processing for Inherit_Subprogram_Contract
-
- begin
- -- Inheritance is carried out only when both entities are subprograms
- -- with contracts.
-
- 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;
-
---------------------------------
-- Insert_Explicit_Dereference --
---------------------------------
(Boolean_Literals (not Range_Checks_Suppressed (E)), Loc);
end Rep_To_Pos_Flag;
+ -------------------------------
+ -- Report_Unused_Body_States --
+ -------------------------------
+
+ procedure Report_Unused_Body_States
+ (Body_Id : Entity_Id;
+ States : Elist_Id)
+ is
+ Posted : Boolean := False;
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (States) then
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ -- Constants are part of the hidden state of a package, but the
+ -- compiler cannot determine whether they have variable input
+ -- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
+ -- hidden state. Do not emit an error when a constant does not
+ -- participate in a state refinement, even though it acts as a
+ -- hidden state.
+
+ if Ekind (State_Id) = E_Constant then
+ null;
+
+ -- Generate an error message of the form:
+
+ -- body of package ... has unused hidden states
+ -- abstract state ... defined at ...
+ -- variable ... defined at ...
+
+ else
+ if not Posted then
+ Posted := True;
+ SPARK_Msg_N
+ ("body of package & has unused hidden states", Body_Id);
+ end if;
+
+ Error_Msg_Sloc := Sloc (State_Id);
+
+ if Ekind (State_Id) = E_Abstract_State then
+ SPARK_Msg_NE
+ ("\abstract state & defined #", Body_Id, State_Id);
+
+ else
+ SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
+ end if;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unused_Body_States;
+
--------------------
-- Require_Entity --
--------------------
-- it the identifier of the block. Id denotes the generated entity. If the
-- block already has an identifier, Id returns the entity of its label.
- procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
- -- Add pragma Prag to the contract of a constant, entry, package [body],
- -- subprogram [body] or variable denoted by Id. The following are valid
- -- pragmas:
- -- Abstract_State
- -- Async_Readers
- -- Async_Writers
- -- Constant_After_Elaboration
- -- Contract_Cases
- -- Depends
- -- Effective_Reads
- -- Effective_Writes
- -- Extensions_Visible
- -- Global
- -- Initial_Condition
- -- Initializes
- -- Part_Of
- -- Postcondition
- -- Precondition
- -- Refined_Depends
- -- Refined_Global
- -- Refined_Post
- -- Refined_States
- -- Test_Case
- -- Volatile_Function
-
procedure Add_Global_Declaration (N : Node_Id);
-- These procedures adds a declaration N at the library level, to be
-- elaborated before any other code in the unit. It is used for example
-- error message on node N. Used in object declarations, type conversions
-- and qualified expressions.
+ procedure Check_Function_With_Address_Parameter (Subp_Id : Entity_Id);
+ -- A subprogram that has an Address parameter and is declared in a Pure
+ -- package is not considered Pure, because the parameter may be used as a
+ -- pointer and the referenced data may change even if the address value
+ -- itself does not.
+ -- If the programmer gave an explicit Pure_Function pragma, then we respect
+ -- the pragma and leave the subprogram Pure.
+
procedure Check_Function_Writable_Actuals (N : Node_Id);
-- (Ada 2012): If the construct N has two or more direct constituents that
-- are names or expressions whose evaluation may occur in an arbitrary
-- N is one of the statement forms that is a potentially blocking
-- operation. If it appears within a protected action, emit warning.
- procedure Check_Function_With_Address_Parameter (Subp_Id : Entity_Id);
- -- A subprogram that has an Address parameter and is declared in a Pure
- -- package is not considered Pure, because the parameter may be used as a
- -- pointer and the referenced data may change even if the address value
- -- itself does not.
- -- If the programmer gave an explicit Pure_Function pragma, then we respect
- -- the pragma and leave the subprogram Pure.
-
procedure Check_Result_And_Post_State (Subp_Id : Entity_Id);
-- Determine whether the contract of subprogram Subp_Id mentions attribute
-- 'Result and it contains an expression that evaluates differently in pre-
-- and post-state.
+ procedure Check_Unused_Body_States (Body_Id : Entity_Id);
+ -- Verify that all abstract states and object declared in the state space
+ -- of a package body denoted by entity Body_Id are used as constituents.
+ -- Emit an error if this is not the case.
+
+ function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
+ -- Gather the entities of all abstract states and objects declared in the
+ -- body state space of package body Body_Id.
+
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
-- Return the corresponding spec of Decl when it denotes a package or a
-- subprogram [stub], or the defining entity of Decl.
- procedure Create_Generic_Contract (Unit : Node_Id);
- -- Create a contract node for a generic package, generic subprogram or a
- -- generic body denoted by Unit by collecting all source contract-related
- -- pragmas in the contract of the unit.
-
function Current_Entity (N : Node_Id) return Entity_Id;
pragma Inline (Current_Entity);
-- Find the currently visible definition for a given identifier, that is to
-- Inherit the rep item chain of type From_Typ without clobbering any
-- existing rep items on Typ's chain. Typ is the destination type.
- procedure Inherit_Subprogram_Contract
- (Subp : Entity_Id;
- From_Subp : Entity_Id);
- -- Inherit relevant contract items from source subprogram From_Subp. Subp
- -- denotes the destination subprogram. The inherited items are:
- -- Extensions_Visible
- -- ??? it would be nice if this routine handles Pre'Class and Post'Class
-
procedure Insert_Explicit_Dereference (N : Node_Id);
-- In a context that requires a composite or subprogram type and where a
-- prefix is an access type, rewrite the access type node N (which is the
-- more there is at least one case in the generated code (the code for
-- array assignment in a loop) that depends on this suppression.
+ procedure Report_Unused_Body_States
+ (Body_Id : Entity_Id;
+ States : Elist_Id);
+ -- Emit errors for each abstract state or object found in list States that
+ -- is declared in package body Body_Id, but is not used as constituent in a
+ -- state refinement.
+
procedure Require_Entity (N : Node_Id);
-- N is a node which should have an entity value if it is an entity name.
-- If not, then check if there were previous errors. If so, just fill
return Flag11 (N);
end Is_Expanded_Build_In_Place_Call;
+ function Is_Expanded_Contract
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ return Flag1 (N);
+ end Is_Expanded_Contract;
+
function Is_Finalization_Wrapper
(N : Node_Id) return Boolean is
begin
Set_Flag11 (N, Val);
end Set_Is_Expanded_Build_In_Place_Call;
+ procedure Set_Is_Expanded_Contract
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Contract);
+ Set_Flag1 (N, Val);
+ end Set_Is_Expanded_Contract;
+
procedure Set_Is_Finalization_Wrapper
(N : Node_Id; Val : Boolean := True) is
begin
-- is called in a dispatching context. Used to prevent a formal/actual
-- mismatch when the call is rewritten as a dispatching call.
+ -- Is_Expanded_Contract (Flag1-Sem)
+ -- Present in N_Contract nodes. Set if the contract has already undergone
+ -- expansion activities.
+
-- Is_Asynchronous_Call_Block (Flag7-Sem)
-- A flag set in a Block_Statement node to indicate that it is the
-- expansion of an asynchronous entry call. Such a block needs cleanup
-- Pre_Post_Conditions (Node1-Sem) (set to Empty if none)
-- Contract_Test_Cases (Node2-Sem) (set to Empty if none)
-- Classifications (Node3-Sem) (set to Empty if none)
+ -- Is_Expanded_Contract (Flag1-Sem)
-- Pre_Post_Conditions contains a collection of pragmas that correspond
-- to pre- and postconditions associated with an entry or a subprogram
-- Abstract_States
-- Async_Readers
-- Async_Writers
+ -- Constant_After_Elaboration
-- Depends
-- Effective_Reads
-- Effective_Writes
+ -- Extensions_Visible
-- Global
-- Initial_Condition
-- Initializes
-- Refined_Depends
-- Refined_Global
-- Refined_States
+ -- Volatile_Function
-- The ordering is in LIFO fashion.
-------------------
function Is_Expanded_Build_In_Place_Call
(N : Node_Id) return Boolean; -- Flag11
+ function Is_Expanded_Contract
+ (N : Node_Id) return Boolean; -- Flag1
+
function Is_Finalization_Wrapper
(N : Node_Id) return Boolean; -- Flag9
procedure Set_Is_Expanded_Build_In_Place_Call
(N : Node_Id; Val : Boolean := True); -- Flag11
+ procedure Set_Is_Expanded_Contract
+ (N : Node_Id; Val : Boolean := True); -- Flag1
+
procedure Set_Is_Finalization_Wrapper
(N : Node_Id; Val : Boolean := True); -- Flag9
pragma Inline (Is_Elsif);
pragma Inline (Is_Entry_Barrier_Function);
pragma Inline (Is_Expanded_Build_In_Place_Call);
+ pragma Inline (Is_Expanded_Contract);
pragma Inline (Is_Finalization_Wrapper);
pragma Inline (Is_Folded_In_Parser);
pragma Inline (Is_Generic_Contract_Pragma);
pragma Inline (Set_Is_Elsif);
pragma Inline (Set_Is_Entry_Barrier_Function);
pragma Inline (Set_Is_Expanded_Build_In_Place_Call);
+ pragma Inline (Set_Is_Expanded_Contract);
pragma Inline (Set_Is_Finalization_Wrapper);
pragma Inline (Set_Is_Folded_In_Parser);
pragma Inline (Set_Is_Generic_Contract_Pragma);
-- A little check, "gnat" at the start of a switch is not allowed except
-- for the compiler
- if Switch_Chars'Last >= Ptr + 3
+ if Max >= Ptr + 3
and then Switch_Chars (Ptr .. Ptr + 3) = "gnat"
then
Osint.Fail ("invalid switch: """ & Switch_Chars & """"
-- Processing for E switch
when 'E' =>
- Ptr := Ptr + 1;
+
+ -- -E is equivalent to -Ea (see below)
+
Exception_Tracebacks := True;
+ Ptr := Ptr + 1;
+
+ if Ptr <= Max then
+ case Switch_Chars (Ptr) is
+
+ -- -Ea sets Exception_Tracebacks
+
+ when 'a' => null;
+
+ -- -Es sets both Exception_Tracebacks and
+ -- Exception_Tracebacks_Symbolic.
+
+ when 's' => Exception_Tracebacks_Symbolic := True;
+ when others => Bad_Switch (Switch_Chars);
+ end case;
+
+ Ptr := Ptr + 1;
+ end if;
-- Processing for F switch
declare
Src_Path_Name : constant String_Ptr :=
Get_RTS_Search_Dir
- (Switch_Chars
- (Ptr + 1 .. Switch_Chars'Last),
+ (Switch_Chars (Ptr + 1 .. Max),
Include);
Lib_Path_Name : constant String_Ptr :=
Get_RTS_Search_Dir
- (Switch_Chars
- (Ptr + 1 .. Switch_Chars'Last),
+ (Switch_Chars (Ptr + 1 .. Max),
Objects);
begin
-- --
-- S p e c --
-- --
--- Copyright (C) 2001-2007, Free Software Foundation, Inc. --
+-- Copyright (C) 2001-2015, 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- --
package Switch.B is
procedure Scan_Binder_Switches (Switch_Chars : String);
- -- Procedures to scan out binder switches stored in the given string.
+ -- Procedure to scan out binder switches stored in the given string.
-- The first character is known to be a valid switch character, and there
-- are no blanks or other switch terminator characters in the string, so
-- the entire string should consist of valid switch characters, except that
projects / thirdparty / gcc.git / commitdiff
