diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 102 | ||||
| -rw-r--r-- | gcc/ada/bindgen.adb | 26 | ||||
| -rw-r--r-- | gcc/ada/bindusg.adb | 5 | ||||
| -rw-r--r-- | gcc/ada/contracts.adb | 2453 | ||||
| -rw-r--r-- | gcc/ada/contracts.ads | 156 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 1362 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 1 | ||||
| -rw-r--r-- | gcc/ada/init.c | 1 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/s-exctra.ads | 15 | ||||
| -rw-r--r-- | gcc/ada/sem_ch10.adb | 130 | ||||
| -rw-r--r-- | gcc/ada/sem_ch10.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 283 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 331 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 391 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.ads | 25 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 208 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 422 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 674 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 71 | ||||
| -rw-r--r-- | gcc/ada/sinfo.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/switch-b.adb | 30 | ||||
| -rw-r--r-- | gcc/ada/switch-b.ads | 4 |
28 files changed, 3681 insertions, 3103 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 28cc00c..88a2197 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,105 @@ +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 diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb index cf4b59f..e284a0e 100644 --- a/gcc/ada/bindgen.adb +++ b/gcc/ada/bindgen.adb @@ -166,6 +166,7 @@ package body Bindgen is -- 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; @@ -235,10 +236,13 @@ package body Bindgen is -- 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 @@ -607,10 +611,16 @@ package body Bindgen is 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;"); @@ -795,8 +805,12 @@ package body Bindgen is 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 := "); diff --git a/gcc/ada/bindusg.adb b/gcc/ada/bindusg.adb index e5c0e36..f1a6177 100644 --- a/gcc/ada/bindusg.adb +++ b/gcc/ada/bindusg.adb @@ -108,7 +108,10 @@ package body Bindusg is -- 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 diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb new file mode 100644 index 0000000..ffdd510 --- /dev/null +++ b/gcc/ada/contracts.adb @@ -0,0 +1,2453 @@ +------------------------------------------------------------------------------ +-- -- +-- 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; diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads new file mode 100644 index 0000000..beeed57 --- /dev/null +++ b/gcc/ada/contracts.ads @@ -0,0 +1,156 @@ +------------------------------------------------------------------------------ +-- -- +-- 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; diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 05828b2..1e142aa 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -23,60 +23,59 @@ -- -- ------------------------------------------------------------------------------ -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 @@ -6773,1263 +6772,6 @@ 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 -- -------------------------------------------- diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads index 1cc993f..2184d58 100644 --- a/gcc/ada/exp_ch6.ads +++ b/gcc/ada/exp_ch6.ads @@ -41,12 +41,6 @@ package Exp_Ch6 is -- 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 diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 7378d6f..a8ce672 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -243,6 +243,7 @@ GNAT_ADA_OBJS = \ ada/casing.o \ ada/checks.o \ ada/comperr.o \ + ada/contracts.o \ ada/csets.o \ ada/cstand.o \ ada/debug.o \ diff --git a/gcc/ada/init.c b/gcc/ada/init.c index c649d67..243f3b8 100644 --- a/gcc/ada/init.c +++ b/gcc/ada/init.c @@ -110,6 +110,7 @@ char *__gl_interrupt_states = 0; 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; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 992658e..e99c6b7 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -595,7 +595,12 @@ package Opt is 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 diff --git a/gcc/ada/s-exctra.ads b/gcc/ada/s-exctra.ads index 25c2f72..ae6936e 100644 --- a/gcc/ada/s-exctra.ads +++ b/gcc/ada/s-exctra.ads @@ -48,6 +48,10 @@ -- 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 @@ -89,12 +93,15 @@ 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; diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index bae9762..41ceb3d 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -23,50 +23,50 @@ -- -- ------------------------------------------------------------------------------ -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 @@ -940,15 +940,6 @@ 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 @@ -2006,39 +1997,6 @@ package body Sem_Ch10 is 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 -- --------------------- diff --git a/gcc/ada/sem_ch10.ads b/gcc/ada/sem_ch10.ads index c003526..d4b28cd 100644 --- a/gcc/ada/sem_ch10.ads +++ b/gcc/ada/sem_ch10.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -24,6 +24,7 @@ ------------------------------------------------------------------------------ with Types; use Types; + package Sem_Ch10 is procedure Analyze_Compilation_Unit (N : Node_Id); procedure Analyze_With_Clause (N : Node_Id); @@ -33,19 +34,6 @@ package Sem_Ch10 is 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. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 60bd94c..6891c64 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -23,60 +23,61 @@ -- -- ------------------------------------------------------------------------------ -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; @@ -842,10 +843,6 @@ package body Sem_Ch12 is -- 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); @@ -4803,11 +4800,6 @@ package body Sem_Ch12 is -- 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 -- ------------------------------------ @@ -5009,53 +5001,6 @@ package body Sem_Ch12 is 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; @@ -5227,9 +5172,10 @@ package body Sem_Ch12 is -- 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 @@ -10888,9 +10834,12 @@ package body Sem_Ch12 is 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 @@ -10901,7 +10850,8 @@ package body Sem_Ch12 is 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; @@ -11109,7 +11059,7 @@ package body Sem_Ch12 is 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)); @@ -11119,6 +11069,7 @@ package body Sem_Ch12 is 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; @@ -11160,11 +11111,11 @@ package body Sem_Ch12 is -- 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 @@ -11194,11 +11145,11 @@ package body Sem_Ch12 is ("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 @@ -11221,14 +11172,17 @@ package body Sem_Ch12 is 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 @@ -11327,16 +11281,16 @@ package body Sem_Ch12 is 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 => @@ -11352,7 +11306,7 @@ package body Sem_Ch12 is 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 := @@ -11360,12 +11314,12 @@ package body Sem_Ch12 is 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 => @@ -14970,63 +14924,6 @@ package body Sem_Ch12 is 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 -- -------------------------------------- diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads index 53ff6c5..c54d735 100644 --- a/gcc/ada/sem_ch12.ads +++ b/gcc/ada/sem_ch12.ads @@ -152,12 +152,9 @@ package Sem_Ch12 is -- 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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 82c3dd8..4355329 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -23,64 +23,62 @@ -- -- ------------------------------------------------------------------------------ -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 @@ -93,16 +91,6 @@ 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; @@ -2306,7 +2294,6 @@ package body Sem_Ch3 is 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 @@ -2477,7 +2464,6 @@ package body Sem_Ch3 is 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 @@ -2506,14 +2492,12 @@ package body Sem_Ch3 is 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 @@ -2533,43 +2517,21 @@ package body Sem_Ch3 is 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; @@ -3288,173 +3250,6 @@ package body Sem_Ch3 is 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 -- -------------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 30be333..283b770 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -23,70 +23,71 @@ -- -- ------------------------------------------------------------------------------ -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 @@ -1377,23 +1378,11 @@ 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)); @@ -2220,102 +2209,6 @@ package body Sem_Ch6 is 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 -- ------------------------------------ @@ -3102,6 +2995,24 @@ package body Sem_Ch6 is -- 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. @@ -3842,23 +3753,11 @@ package body Sem_Ch6 is 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. @@ -4096,116 +3995,6 @@ package body Sem_Ch6 is 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 -- ------------------------------------ diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads index 427559e..ff24ed8 100644 --- a/gcc/ada/sem_ch6.ads +++ b/gcc/ada/sem_ch6.ads @@ -45,31 +45,6 @@ package Sem_Ch6 is 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 diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index a3870e8..5814bc8 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -28,44 +28,45 @@ -- 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 @@ -182,47 +183,6 @@ 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 -- --------------------------------- @@ -582,6 +542,30 @@ package body Sem_Ch7 is -- 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 @@ -944,74 +928,6 @@ package body Sem_Ch7 is 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 -- --------------------------------- diff --git a/gcc/ada/sem_ch7.ads b/gcc/ada/sem_ch7.ads index a243ac5f..59f27b0 100644 --- a/gcc/ada/sem_ch7.ads +++ b/gcc/ada/sem_ch7.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -32,20 +32,6 @@ package Sem_Ch7 is 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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b952674..d97bc86 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -29,62 +29,63 @@ -- 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 @@ -165,11 +166,6 @@ 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 @@ -277,15 +273,6 @@ package body Sem_Prag is -- 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 -- ------------------------------- @@ -826,7 +813,7 @@ package body Sem_Prag is 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 @@ -846,7 +833,7 @@ package body Sem_Prag is -- 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)) @@ -901,7 +888,7 @@ package body Sem_Prag is -- 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, @@ -909,7 +896,7 @@ package body Sem_Prag is 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 @@ -2016,16 +2003,16 @@ package body Sem_Prag is -- 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; @@ -2396,14 +2383,14 @@ package body Sem_Prag is -- 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; @@ -2504,10 +2491,10 @@ package body Sem_Prag is -- 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, @@ -2515,7 +2502,7 @@ package body Sem_Prag is 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; @@ -2610,7 +2597,7 @@ package body Sem_Prag is 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); @@ -3481,8 +3468,8 @@ package body Sem_Prag is 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 @@ -3494,8 +3481,8 @@ package body Sem_Prag is 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; @@ -22493,7 +22480,7 @@ package body Sem_Prag is 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; @@ -23664,16 +23651,16 @@ package body Sem_Prag is 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 @@ -23821,13 +23808,13 @@ package body Sem_Prag is -- 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; @@ -24091,7 +24078,10 @@ package body Sem_Prag is -- 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); @@ -24109,6 +24099,10 @@ package body Sem_Prag is -- 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. @@ -24116,16 +24110,9 @@ package body Sem_Prag is 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 -- ------------------------------- @@ -24190,10 +24177,10 @@ package body Sem_Prag is 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 -- @@ -24212,7 +24199,7 @@ package body Sem_Prag is -- 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 @@ -24436,12 +24423,56 @@ package body Sem_Prag is 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", @@ -24519,7 +24550,7 @@ package body Sem_Prag is -- 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; @@ -24754,104 +24785,6 @@ package body Sem_Prag is 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 -- ----------------------------- @@ -24871,61 +24804,6 @@ package body Sem_Prag is 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)); @@ -24945,7 +24823,7 @@ package body Sem_Prag is -- 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 @@ -24977,7 +24855,7 @@ package body Sem_Prag is -- 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; ------------------------------------ @@ -25857,9 +25735,9 @@ package body Sem_Prag is 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; @@ -25908,11 +25786,11 @@ package body Sem_Prag is 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; @@ -25988,14 +25866,14 @@ package body Sem_Prag is 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 @@ -26004,7 +25882,7 @@ package body Sem_Prag is 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; diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 862c564..45a3ebc 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -209,8 +209,12 @@ package Sem_Prag is -- 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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index a805200..634b479 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -52,7 +52,6 @@ with Sem_Aux; use Sem_Aux; 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; @@ -250,209 +249,6 @@ package body Sem_Util is 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 -- ---------------------------- @@ -3692,6 +3488,231 @@ package body Sem_Util is 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 -- ------------------------ @@ -4766,147 +4787,6 @@ package body Sem_Util is 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 -- -------------------- @@ -10250,53 +10130,6 @@ package body Sem_Util is 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 -- --------------------------------- @@ -17171,6 +17004,63 @@ package body Sem_Util is (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 -- -------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 1ed93de..81e63ed 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -49,32 +49,6 @@ package Sem_Util is -- 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 @@ -276,6 +250,14 @@ package Sem_Util is -- 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 @@ -322,19 +304,20 @@ package Sem_Util is -- 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); @@ -434,11 +417,6 @@ package Sem_Util is -- 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 @@ -1159,14 +1137,6 @@ package Sem_Util is -- 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 @@ -1877,6 +1847,13 @@ package Sem_Util is -- 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 diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 824acd5..0fc3851 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -1860,6 +1860,14 @@ package body Sinfo is 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 @@ -5073,6 +5081,14 @@ package body Sinfo is 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 diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 218f4bc..5f2f092 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1542,6 +1542,10 @@ package Sinfo is -- 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 @@ -7564,6 +7568,7 @@ package Sinfo is -- 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 @@ -7592,9 +7597,11 @@ package Sinfo is -- Abstract_States -- Async_Readers -- Async_Writers + -- Constant_After_Elaboration -- Depends -- Effective_Reads -- Effective_Writes + -- Extensions_Visible -- Global -- Initial_Condition -- Initializes @@ -7602,6 +7609,7 @@ package Sinfo is -- Refined_Depends -- Refined_Global -- Refined_States + -- Volatile_Function -- The ordering is in LIFO fashion. ------------------- @@ -9322,6 +9330,9 @@ package Sinfo is 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 @@ -10348,6 +10359,9 @@ package Sinfo is 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 @@ -12748,6 +12762,7 @@ package Sinfo is 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); @@ -13085,6 +13100,7 @@ package Sinfo is 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); diff --git a/gcc/ada/switch-b.adb b/gcc/ada/switch-b.adb index 8e3806e..b26c583 100644 --- a/gcc/ada/switch-b.adb +++ b/gcc/ada/switch-b.adb @@ -127,7 +127,7 @@ package body Switch.B is -- 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 & """" @@ -229,8 +229,28 @@ package body Switch.B is -- 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 @@ -542,13 +562,11 @@ package body Switch.B is 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 diff --git a/gcc/ada/switch-b.ads b/gcc/ada/switch-b.ads index 9ec9189..e22296a 100644 --- a/gcc/ada/switch-b.ads +++ b/gcc/ada/switch-b.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -32,7 +32,7 @@ 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 |