diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 82 | ||||
| -rw-r--r-- | gcc/ada/contracts.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 38 | ||||
| -rw-r--r-- | gcc/ada/exp_pakd.adb | 83 | ||||
| -rw-r--r-- | gcc/ada/g-traceb.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/lib-writ.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/s-soflin.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch10.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 85 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.ads | 15 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 320 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 232 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 25 |
16 files changed, 629 insertions, 323 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 73c31eeabe6..27476846f1b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,85 @@ +2016-04-21 Jerome Lambourg <lambourg@adacore.com> + + * s-soflin.adb: Initialize the Stack_Limit global variable. + +2016-04-21 Hristian Kirtchev <kirtchev@adacore.com> + + * lib-writ.adb: Minor reformatting. + +2016-04-21 Ed Schonberg <schonberg@adacore.com> + + * exp_pakd.adb (Compute_Number_Components): New function to + build an expression that computes the number of a components of + an array that may be multidimensional. + (Expan_Packed_Eq): Use it. + +2016-04-21 Arnaud Charlet <charlet@adacore.com> + + * g-traceb.ads: Update list of supported platforms. + +2016-04-21 Ed Schonberg <schonberg@adacore.com> + + * sem_ch13.adb (Add_Predicates): if the type is declared in + an inner package it may be frozen outside of the package, and + the generated pragma has not been analyzed yet, the expression + for the predicate must be captured and added to the predicate + function at this point. + +2016-04-21 Hristian Kirtchev <kirtchev@adacore.com> + + * contracts.adb (Analyze_Package_Body_Contract): Do not check + for a missing package refinement because 1) packages do not have + "refinement" and 2) the check for proper state refinement is + performed in a different place. + * einfo.adb (Has_Non_Null_Visible_Refinement): Reimplemented. + (Has_Null_Visible_Refinement): Reimplemented. + * sem_ch3.adb (Analyze_Declarations): Determine whether all + abstract states have received a refinement and if not, emit + errors. + * sem_ch7.adb (Analyze_Package_Declaration): Code + cleanup. Determine whether all abstract states of the + package and any nested packages have received a refinement + and if not, emit errors. + (Requires_Completion_In_Body): Add new formal parameter + Do_Abstract_States. Update the comment on usage. Propagate the + Do_Abstract_States flag to all Unit_Requires_Body calls. + (Unit_Requires_Body): Remove formal + parameter Ignore_Abstract_States. Add new formal paramter + Do_Abstract_States. Propagate the Do_Abstract_States flag to + all Requires_Completion_In calls. + * sem_ch7.ads (Unit_Requires_Body): Remove formal + parameter Ignore_Abstract_States. Add new formal paramter + Do_Abstract_States. Update the comment on usage. + * sem_ch9.adb (Analyze_Single_Protected_Declaration): Do + not initialize the constituent list as this is now done on a + need-to-add-element basis. + (Analyze_Single_Task_Declaration): + Do not initialize the constituent list as this is now done on + a need-to-add-element basis. + * sem_ch10.adb (Decorate_State): Do not initialize the constituent + lists as this is now done on a need-to-add-element basis. + * sem_prag.adb (Analyze_Constituent): Set the + refinement constituents when adding a new element. + (Analyze_Part_Of_In_Decl_Part): Set the Part_Of constituents when + adding a new element. + (Analyze_Part_Of_Option): Set the Part_Of + constituents when adding a new element. + (Analyze_Pragma): Set the Part_Of constituents when adding a new + element. + (Check_Constituent_Usage (all versions)): Reimplemented. + (Collect_Constituent): Set the refinement constituents when adding + a new element. + (Create_Abstract_State): Do not initialize the + constituent lists as this is now done on a need-to-add-element basis. + (Propagate_Part_Of): Set the Part_Of constituents when + adding a new element. + * sem_util.adb (Check_State_Refinements): New routine. + (Has_Non_Null_Refinement): Reimplemented. + (Has_Null_Refinement): Reimplemented. + (Requires_State_Refinement): Removed. + * sem_util.ads (Check_State_Refinements): New routine. + (Requires_State_Refinement): Removed. + 2016-04-21 Hristian Kirtchev <kirtchev@adacore.com> * lib-writ.adb, sem_ch6.adb: Minor reformatting and code cleanup. diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 8aa8502dc2e..f6d236ffe0a 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2015-2016, 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- -- @@ -949,15 +949,6 @@ package body Contracts is if Present (Ref_State) then Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id); - - -- State refinement is required when the package declaration defines at - -- least one abstract state. Null states are not considered. Refinement - -- is not enforced when SPARK checks are turned off. - - elsif SPARK_Mode /= Off - and then Requires_State_Refinement (Spec_Id, Body_Id) - then - Error_Msg_N ("package & requires state refinement", Spec_Id); end if; -- Restore the SPARK_Mode of the enclosing context after all delayed diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index f52702f03fd..7172a2ac518 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -7351,22 +7351,21 @@ package body Einfo is ------------------------------------- function Has_Non_Null_Visible_Refinement (Id : E) return B is + Constits : Elist_Id; + begin -- "Refinement" is a concept applicable only to abstract states pragma Assert (Ekind (Id) = E_Abstract_State); + Constits := Refinement_Constituents (Id); - if Has_Visible_Refinement (Id) then - pragma Assert (Present (Refinement_Constituents (Id))); - - -- For a refinement to be non-null, the first constituent must be - -- anything other than null. + -- For a refinement to be non-null, the first constituent must be + -- anything other than null. - return - Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null; - end if; - - return False; + return + Has_Visible_Refinement (Id) + and then Present (Constits) + and then Nkind (Node (First_Elmt (Constits))) /= N_Null; end Has_Non_Null_Visible_Refinement; ----------------------------- @@ -7387,22 +7386,21 @@ package body Einfo is --------------------------------- function Has_Null_Visible_Refinement (Id : E) return B is + Constits : Elist_Id; + begin -- "Refinement" is a concept applicable only to abstract states pragma Assert (Ekind (Id) = E_Abstract_State); + Constits := Refinement_Constituents (Id); - if Has_Visible_Refinement (Id) then - pragma Assert (Present (Refinement_Constituents (Id))); - - -- For a refinement to be null, the state's sole constituent must be - -- a null. + -- For a refinement to be null, the state's sole constituent must be a + -- null. - return - Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null; - end if; - - return False; + return + Has_Visible_Refinement (Id) + and then Present (Constits) + and then Nkind (Node (First_Elmt (Constits))) = N_Null; end Has_Null_Visible_Refinement; -------------------- diff --git a/gcc/ada/exp_pakd.adb b/gcc/ada/exp_pakd.adb index d4968a325a0..0668369afa0 100644 --- a/gcc/ada/exp_pakd.adb +++ b/gcc/ada/exp_pakd.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -81,6 +81,12 @@ package body Exp_Pakd is -- Local Subprograms -- ----------------------- + function Compute_Number_Components + (N : Node_Id; + Typ : Entity_Id) return Node_Id; + -- Build an expression that multiplies the length of the dimensions of the + -- array, used to control array equality checks. + procedure Compute_Linear_Subscript (Atyp : Entity_Id; N : Node_Id; @@ -260,6 +266,38 @@ package body Exp_Pakd is return Adjusted; end Revert_Storage_Order; + ------------------------------- + -- Compute_Number_Components -- + ------------------------------- + + function Compute_Number_Components + (N : Node_Id; + Typ : Entity_Id) return Node_Id + is + Loc : constant Source_Ptr := Sloc (N); + Len_Expr : Node_Id; + + begin + Len_Expr := + Make_Attribute_Reference (Loc, + Attribute_Name => Name_Length, + Prefix => New_Occurrence_Of (Typ, Loc), + Expressions => New_List (Make_Integer_Literal (Loc, 1))); + + for J in 2 .. Number_Dimensions (Typ) loop + Len_Expr := + Make_Op_Multiply (Loc, + Left_Opnd => Len_Expr, + Right_Opnd => + Make_Attribute_Reference (Loc, + Attribute_Name => Name_Length, + Prefix => New_Occurrence_Of (Typ, Loc), + Expressions => New_List (Make_Integer_Literal (Loc, J)))); + end loop; + + return Len_Expr; + end Compute_Number_Components; + ------------------------------ -- Compute_Linear_Subscript -- ------------------------------ @@ -451,7 +489,6 @@ package body Exp_Pakd is PASize : Uint; Decl : Node_Id; PAT : Entity_Id; - Len_Dim : Node_Id; Len_Expr : Node_Id; Len_Bits : Uint; Bits_U1 : Node_Id; @@ -811,34 +848,7 @@ package body Exp_Pakd is -- Build an expression for the length of the array in bits. -- This is the product of the length of each of the dimensions - declare - J : Nat := 1; - - begin - Len_Expr := Empty; -- suppress junk warning - - loop - Len_Dim := - Make_Attribute_Reference (Loc, - Attribute_Name => Name_Length, - Prefix => New_Occurrence_Of (Typ, Loc), - Expressions => New_List ( - Make_Integer_Literal (Loc, J))); - - if J = 1 then - Len_Expr := Len_Dim; - - else - Len_Expr := - Make_Op_Multiply (Loc, - Left_Opnd => Len_Expr, - Right_Opnd => Len_Dim); - end if; - - J := J + 1; - exit when J > Number_Dimensions (Typ); - end loop; - end; + Len_Expr := Compute_Number_Components (Typ, Typ); -- Temporarily attach the length expression to the tree and analyze -- and resolve it, so that we can test its value. We assume that the @@ -1872,19 +1882,12 @@ package body Exp_Pakd is LLexpr := Make_Op_Multiply (Loc, - Left_Opnd => - Make_Attribute_Reference (Loc, - Prefix => New_Occurrence_Of (Ltyp, Loc), - Attribute_Name => Name_Length), - Right_Opnd => - Make_Integer_Literal (Loc, Component_Size (Ltyp))); + Left_Opnd => Compute_Number_Components (N, Ltyp), + Right_Opnd => Make_Integer_Literal (Loc, Component_Size (Ltyp))); RLexpr := Make_Op_Multiply (Loc, - Left_Opnd => - Make_Attribute_Reference (Loc, - Prefix => New_Occurrence_Of (Rtyp, Loc), - Attribute_Name => Name_Length), + Left_Opnd => Compute_Number_Components (N, Rtyp), Right_Opnd => Make_Integer_Literal (Loc, Component_Size (Rtyp))); diff --git a/gcc/ada/g-traceb.ads b/gcc/ada/g-traceb.ads index 98d11a8ef99..13f5d734799 100644 --- a/gcc/ada/g-traceb.ads +++ b/gcc/ada/g-traceb.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1999-2014, AdaCore -- +-- Copyright (C) 1999-2016, AdaCore -- -- -- -- 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- -- @@ -58,14 +58,15 @@ -- This capability is currently supported on the following targets: -- AiX PowerPC --- HP-UX -- GNU/Linux x86 +-- GNU/Linux PowerPC -- LynxOS x86 +-- LynxOS 178 xcoff PowerPC -- Solaris x86 -- Solaris sparc -- VxWorks PowerPC -- VxWorks x86 --- Windows NT/XP +-- Windows XP -- Note: see also GNAT.Traceback.Symbolic, a child unit in file g-trasym.ads -- providing symbolic trace back capability for a subset of the above targets. diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index 37f574b0442..c5f9d01c932 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -1436,10 +1436,9 @@ package body Lib.Writ is -- The dependency table also contains units that appear in the -- context of a unit loaded through a limited_with clause. These -- units are never analyzed, and thus the main unit does not - -- really have a dependency on them. - -- Subunits are always compiled in the context of the parent, - -- and their file table entries are not properly decorated, they - -- are recognized syntactically. + -- really have a dependency on them. Subunits are always compiled + -- in the context of the parent, and their file table entries are + -- not properly decorated, they are recognized syntactically. if Present (Cunit_Entity (Unum)) and then Ekind (Cunit_Entity (Unum)) = E_Void diff --git a/gcc/ada/s-soflin.adb b/gcc/ada/s-soflin.adb index 2d98f309e56..d1c10a0c67e 100644 --- a/gcc/ada/s-soflin.adb +++ b/gcc/ada/s-soflin.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -51,7 +51,7 @@ package body System.Soft_Links is -- Needed for Vx6Cert (Vx653mc) GOS cert and ravenscar-cert runtimes, -- VxMILS cert, ravenscar-cert and full runtimes, Vx 5 default runtime - Stack_Limit : aliased System.Address; + Stack_Limit : aliased System.Address := System.Null_Address; pragma Export (C, Stack_Limit, "__gnat_stack_limit"); diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index aee7fd3d2a4..da5aba8c1b9 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -5613,12 +5613,10 @@ package body Sem_Ch10 is procedure Decorate_State (Ent : Entity_Id; Scop : Entity_Id) is begin - Set_Ekind (Ent, E_Abstract_State); - Set_Etype (Ent, Standard_Void_Type); - Set_Scope (Ent, Scop); - Set_Encapsulating_State (Ent, Empty); - Set_Refinement_Constituents (Ent, New_Elmt_List); - Set_Part_Of_Constituents (Ent, New_Elmt_List); + Set_Ekind (Ent, E_Abstract_State); + Set_Etype (Ent, Standard_Void_Type); + Set_Scope (Ent, Scop); + Set_Encapsulating_State (Ent, Empty); end Decorate_State; ------------------- diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 29a4996d38c..894d7b564b3 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -8639,6 +8639,26 @@ package body Sem_Ch13 is and then Pragma_Name (Ritem) = Name_Predicate then Add_Predicate (Ritem); + + -- If the type is declared in an inner package it may be frozen + -- outside of the package, and the generated pragma has not been + -- analyzed yet, so capture the expression for the predicate + -- function at this point. + + elsif Nkind (Ritem) = N_Aspect_Specification + and then Present (Aspect_Rep_Item (Ritem)) + and then Scope (Typ) /= Current_Scope + then + declare + Prag : constant Node_Id := Aspect_Rep_Item (Ritem); + + begin + if Nkind (Prag) = N_Pragma + and then Pragma_Name (Prag) = Name_Predicate + then + Add_Predicate (Prag); + end if; + end; end if; Next_Rep_Item (Ritem); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 096ba39bcdd..cd5fd8f8e9f 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2513,6 +2513,13 @@ package body Sem_Ch3 is Remove_Visible_Refinements (Corresponding_Spec (Context)); end if; + + -- Verify that all abstract states found in any package declared in + -- the input declarative list have proper refinements. The check is + -- performed only when the context denotes a block, entry, package, + -- protected, subprogram, or task body (SPARK RM 7.2.2(3)). + + Check_State_Refinements (Context); end if; end Analyze_Declarations; diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 04ad209b32c..dc742dedc62 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -140,11 +140,13 @@ package body Sem_Ch7 is -- tightened further??? function Requires_Completion_In_Body - (Id : Entity_Id; - Pack_Id : Entity_Id) return Boolean; + (Id : Entity_Id; + Pack_Id : Entity_Id; + Do_Abstract_States : Boolean := False) return Boolean; -- Subsidiary to routines Unit_Requires_Body and Unit_Requires_Body_Info. -- Determine whether entity Id declared in package spec Pack_Id requires - -- completion in a package body. + -- completion in a package body. Flag Do_Abstract_Stats should be set when + -- abstract states are to be considered in the completion test. procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id); -- Outputs info messages showing why package Pack_Id requires a body. The @@ -940,15 +942,12 @@ package body Sem_Ch7 is Id : constant Node_Id := Defining_Entity (N); Par : constant Node_Id := Parent_Spec (N); + Is_Comp_Unit : constant Boolean := + Nkind (Parent (N)) = N_Compilation_Unit; + Body_Required : Boolean; -- True when this package declaration requires a corresponding body - Comp_Unit : Boolean; - -- True when this package declaration is not a nested declaration - - PF : Boolean; - -- True when in the context of a declared pure library unit - begin if Debug_Flag_C then Write_Str ("==> package spec "); @@ -990,9 +989,9 @@ package body Sem_Ch7 is Analyze_Aspect_Specifications (N, Id); end if; - -- Ada 2005 (AI-217): Check if the package has been illegally named - -- in a limited-with clause of its own context. In this case the error - -- has been previously notified by Analyze_Context. + -- Ada 2005 (AI-217): Check if the package has been illegally named in + -- a limited-with clause of its own context. In this case the error has + -- been previously notified by Analyze_Context. -- limited with Pkg; -- ERROR -- package Pkg is ... @@ -1003,30 +1002,45 @@ package body Sem_Ch7 is Push_Scope (Id); - PF := Is_Pure (Enclosing_Lib_Unit_Entity); - Set_Is_Pure (Id, PF); - + Set_Is_Pure (Id, Is_Pure (Enclosing_Lib_Unit_Entity)); Set_Categorization_From_Pragmas (N); Analyze (Specification (N)); Validate_Categorization_Dependency (N, Id); - Body_Required := Unit_Requires_Body (Id); + -- Determine whether the package requires a body. Abstract states are + -- intentionally ignored because they do require refinement which can + -- only come in a body, but at the same time they do not force the need + -- for a body on their own (SPARK RM 7.1.4(4) and 7.2.2(3)). - -- When this spec does not require an explicit body, we know that there - -- are no entities requiring completion in the language sense; we call - -- Check_Completion here only to ensure that any nested package - -- declaration that requires an implicit body gets one. (In the case - -- where a body is required, Check_Completion is called at the end of - -- the body's declarative part.) + Body_Required := Unit_Requires_Body (Id); if not Body_Required then + + -- If the package spec does not require an explicit body, then there + -- are not entities requiring completion in the language sense. Call + -- Check_Completion now to ensure that nested package declarations + -- that require an implicit body get one. (In the case where a body + -- is required, Check_Completion is called at the end of the body's + -- declarative part.) + Check_Completion; - end if; - Comp_Unit := Nkind (Parent (N)) = N_Compilation_Unit; + -- If the package spec does not require an explicit body, then all + -- abstract states declared in nested packages cannot possibly get + -- a proper refinement (SPARK RM 7.2.2(3)). This check is performed + -- only when the compilation unit is the main unit to allow for + -- modular SPARK analysis where packages do not necessarily have + -- bodies. + + if Is_Comp_Unit then + Check_State_Refinements + (Context => N, + Is_Main_Unit => Parent (N) = Cunit (Main_Unit)); + end if; + end if; - if Comp_Unit then + if Is_Comp_Unit then -- Set Body_Required indication on the compilation unit node, and -- determine whether elaboration warnings may be meaningful on it. @@ -1046,7 +1060,7 @@ package body Sem_Ch7 is -- visibility tests that rely on the fact that we have exited the scope -- of Id. - if Comp_Unit then + if Is_Comp_Unit then Validate_RT_RAT_Component (N); end if; @@ -2439,8 +2453,9 @@ package body Sem_Ch7 is --------------------------------- function Requires_Completion_In_Body - (Id : Entity_Id; - Pack_Id : Entity_Id) return Boolean + (Id : Entity_Id; + Pack_Id : Entity_Id; + Do_Abstract_States : Boolean := False) return Boolean is begin -- Always ignore child units. Child units get added to the entity list @@ -2473,7 +2488,7 @@ package body Sem_Ch7 is (Ekind (Id) = E_Package and then Id /= Pack_Id and then not Has_Completion (Id) - and then Unit_Requires_Body (Id)) + and then Unit_Requires_Body (Id, Do_Abstract_States)) or else (Ekind (Id) = E_Incomplete_Type @@ -2488,7 +2503,7 @@ package body Sem_Ch7 is (Ekind (Id) = E_Generic_Package and then Id /= Pack_Id and then not Has_Completion (Id) - and then Unit_Requires_Body (Id)) + and then Unit_Requires_Body (Id, Do_Abstract_States)) or else (Is_Generic_Subprogram (Id) @@ -2955,8 +2970,8 @@ package body Sem_Ch7 is ------------------------ function Unit_Requires_Body - (Pack_Id : Entity_Id; - Ignore_Abstract_State : Boolean := False) return Boolean + (Pack_Id : Entity_Id; + Do_Abstract_States : Boolean := False) return Boolean is E : Entity_Id; @@ -3012,7 +3027,9 @@ package body Sem_Ch7 is if Ekind (E) = E_Abstract_State then null; - elsif Requires_Completion_In_Body (E, Pack_Id) then + elsif Requires_Completion_In_Body + (E, Pack_Id, Do_Abstract_States) + then Requires_Body := True; exit; end if; @@ -3025,7 +3042,7 @@ package body Sem_Ch7 is -- a completion in a body (SPARK RM 7.1.4(4) and (6)). This check is not -- performed if the caller requests this behavior. - if not Ignore_Abstract_State + if Do_Abstract_States and then Ekind_In (Pack_Id, E_Generic_Package, E_Package) and then Has_Non_Null_Abstract_State (Pack_Id) and then Requires_Body diff --git a/gcc/ada/sem_ch7.ads b/gcc/ada/sem_ch7.ads index 59f27b086bb..2963aed984c 100644 --- a/gcc/ada/sem_ch7.ads +++ b/gcc/ada/sem_ch7.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -53,17 +53,14 @@ package Sem_Ch7 is -- child for public child packages. function Unit_Requires_Body - (Pack_Id : Entity_Id; - Ignore_Abstract_State : Boolean := False) return Boolean; + (Pack_Id : Entity_Id; + Do_Abstract_States : Boolean := False) return Boolean; -- Determine whether package Pack_Id requires a body. A specification needs -- a body if it contains declarations that require completion in the body. -- A non-Ghost [generic] package does not require a body when it declares - -- Ghost entities exclusively. If flag Ignore_Abstract_State is True, then - -- the test for a non-null abstract state (which normally requires a body) - -- is not carried out. The flag is not currently used, but may be useful - -- in the future if we implement a compatibility mode which warns about - -- possible incompatibilities if a SPARK 2014 program is compiled with a - -- SPARK-unaware compiler. + -- Ghost entities exclusively. When flag Do_Abstract_States is set to True, + -- non-null abstract states are considered in determining the need for a + -- body. procedure May_Need_Implicit_Body (E : Entity_Id); -- If a package declaration contains tasks or RACWs and does not require diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 03c584bba71..442a71d9f08 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -2685,7 +2685,6 @@ package body Sem_Ch9 is Enter_Name (Obj_Id); Set_Ekind (Obj_Id, E_Variable); Set_Etype (Obj_Id, Typ); - Set_Part_Of_Constituents (Obj_Id, New_Elmt_List); Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Obj_Id); @@ -2772,7 +2771,6 @@ package body Sem_Ch9 is Enter_Name (Obj_Id); Set_Ekind (Obj_Id, E_Variable); Set_Etype (Obj_Id, Typ); - Set_Part_Of_Constituents (Obj_Id, New_Elmt_List); Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Obj_Id); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 4d1b2b1b526..0d75d220261 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3342,6 +3342,7 @@ package body Sem_Prag is Errors : constant Nat := Serious_Errors_Detected; Var_Decl : constant Node_Id := Find_Related_Context (N); Var_Id : constant Entity_Id := Defining_Entity (Var_Decl); + Constits : Elist_Id; Encap_Id : Entity_Id; Legal : Boolean; @@ -3362,8 +3363,14 @@ package body Sem_Prag is if Legal then pragma Assert (Present (Encap_Id)); + Constits := Part_Of_Constituents (Encap_Id); + + if No (Constits) then + Constits := New_Elmt_List; + Set_Part_Of_Constituents (Encap_Id, Constits); + end if; - Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id)); + Append_Elmt (Var_Id, Constits); Set_Encapsulating_State (Var_Id, Encap_Id); end if; @@ -10568,6 +10575,7 @@ package body Sem_Prag is procedure Analyze_Part_Of_Option (Opt : Node_Id) is Encap : constant Node_Id := Expression (Opt); + Constits : Elist_Id; Encap_Id : Entity_Id; Legal : Boolean; @@ -10587,8 +10595,14 @@ package body Sem_Prag is if Legal then pragma Assert (Present (Encap_Id)); + Constits := Part_Of_Constituents (Encap_Id); - Append_Elmt (State_Id, Part_Of_Constituents (Encap_Id)); + if No (Constits) then + Constits := New_Elmt_List; + Set_Part_Of_Constituents (Encap_Id, Constits); + end if; + + Append_Elmt (State_Id, Constits); Set_Encapsulating_State (State_Id, Encap_Id); end if; end Analyze_Part_Of_Option; @@ -10670,13 +10684,11 @@ package body Sem_Prag is -- Null states never come from source - Set_Comes_From_Source (State_Id, not Is_Null); - Set_Parent (State_Id, State); - Set_Ekind (State_Id, E_Abstract_State); - Set_Etype (State_Id, Standard_Void_Type); - Set_Encapsulating_State (State_Id, Empty); - Set_Refinement_Constituents (State_Id, New_Elmt_List); - Set_Part_Of_Constituents (State_Id, New_Elmt_List); + Set_Comes_From_Source (State_Id, not Is_Null); + Set_Parent (State_Id, State); + Set_Ekind (State_Id, E_Abstract_State); + Set_Etype (State_Id, Standard_Void_Type); + Set_Encapsulating_State (State_Id, Empty); -- An abstract state declared within a Ghost region becomes -- Ghost (SPARK RM 6.9(2)). @@ -18193,7 +18205,8 @@ package body Sem_Prag is ----------------------- procedure Propagate_Part_Of (Pack_Id : Entity_Id) is - Item_Id : Entity_Id; + Constits : Elist_Id; + Item_Id : Entity_Id; begin -- Traverse the entity chain of the package and set relevant @@ -18217,8 +18230,14 @@ package body Sem_Prag is E_Variable) then Has_Item := True; + Constits := Part_Of_Constituents (State_Id); + + if No (Constits) then + Constits := New_Elmt_List; + Set_Part_Of_Constituents (State_Id, Constits); + end if; - Append_Elmt (Item_Id, Part_Of_Constituents (State_Id)); + Append_Elmt (Item_Id, Constits); Set_Encapsulating_State (Item_Id, State_Id); -- Recursively handle nested packages and instantiations @@ -18248,6 +18267,7 @@ package body Sem_Prag is -- Local variables + Constits : Elist_Id; Encap : Node_Id; Encap_Id : Entity_Id; Item_Id : Entity_Id; @@ -18334,7 +18354,14 @@ package body Sem_Prag is pragma Assert (Present (Encap_Id)); if Ekind (Item_Id) = E_Constant then - Append_Elmt (Item_Id, Part_Of_Constituents (Encap_Id)); + Constits := Part_Of_Constituents (Encap_Id); + + if No (Constits) then + Constits := New_Elmt_List; + Set_Part_Of_Constituents (Encap_Id, Constits); + end if; + + Append_Elmt (Item_Id, Constits); Set_Encapsulating_State (Item_Id, Encap_Id); -- Propagate the Part_Of indicator to the visible state @@ -23657,7 +23684,7 @@ package body Sem_Prag is -- the pool of candidates. The seach continues because a single -- dependence clause may have multiple matching refinements. - if Inputs_Match and then Outputs_Match then + if Inputs_Match and Outputs_Match then Clause_Matched := True; Remove (Ref_Clause); end if; @@ -23769,45 +23796,49 @@ package body Sem_Prag is ----------------------------- procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constits : constant Elist_Id := + Refinement_Constituents (State_Id); Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; Posted : Boolean := False; begin - Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); - -- The constituent acts as an input (SPARK RM 7.2.5(3)) + -- The constituent acts as an input (SPARK RM 7.2.5(3)) - if Present (Body_Inputs) - and then Appears_In (Body_Inputs, Constit_Id) - then - Error_Msg_Name_1 := Chars (State_Id); - SPARK_Msg_NE - ("constituent & of state % must act as output in " - & "dependence refinement", N, Constit_Id); + if Present (Body_Inputs) + and then Appears_In (Body_Inputs, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + SPARK_Msg_NE + ("constituent & of state % must act as output in " + & "dependence refinement", N, Constit_Id); - -- The constituent is altogether missing (SPARK RM 7.2.5(3)) + -- The constituent is altogether missing (SPARK RM 7.2.5(3)) + + elsif No (Body_Outputs) + or else not Appears_In (Body_Outputs, Constit_Id) + then + if not Posted then + Posted := True; + SPARK_Msg_NE + ("output state & must be replaced by all its " + & "constituents in dependence refinement", + N, State_Id); + end if; - elsif No (Body_Outputs) - or else not Appears_In (Body_Outputs, Constit_Id) - then - if not Posted then - Posted := True; SPARK_Msg_NE - ("output state & must be replaced by all its " - & "constituents in dependence refinement", - N, State_Id); + ("\constituent & is missing in output list", + N, Constit_Id); end if; - SPARK_Msg_NE - ("\constituent & is missing in output list", - N, Constit_Id); - end if; - - Next_Elmt (Constit_Elmt); - end loop; + Next_Elmt (Constit_Elmt); + end loop; + end if; end Check_Constituent_Usage; -- Local variables @@ -24328,6 +24359,8 @@ package body Sem_Prag is ----------------------------- procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constits : constant Elist_Id := + Refinement_Constituents (State_Id); Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; Has_Missing : Boolean := False; @@ -24340,28 +24373,31 @@ package body Sem_Prag is -- Process all the constituents of the state and note their modes -- within the global refinement. - Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); - if Present_Then_Remove (In_Constits, Constit_Id) then - Input_Seen := True; + if Present_Then_Remove (In_Constits, Constit_Id) then + Input_Seen := True; - elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then - In_Out_Seen := True; + elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then + In_Out_Seen := True; - elsif Present_Then_Remove (Out_Constits, Constit_Id) then - Output_Seen := True; + elsif Present_Then_Remove (Out_Constits, Constit_Id) then + Output_Seen := True; - elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then - Proof_In_Seen := True; + elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) + then + Proof_In_Seen := True; - else - Has_Missing := True; - end if; + else + Has_Missing := True; + end if; - Next_Elmt (Constit_Elmt); - end loop; + Next_Elmt (Constit_Elmt); + end loop; + end if; -- An In_Out constituent is a valid completion @@ -24462,40 +24498,45 @@ package body Sem_Prag is ----------------------------- procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constits : constant Elist_Id := + Refinement_Constituents (State_Id); Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; In_Seen : Boolean := False; begin - Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); - -- At least one of the constituents appears as an Input + -- At least one of the constituents appears as an Input - if Present_Then_Remove (In_Constits, Constit_Id) then - In_Seen := True; + if Present_Then_Remove (In_Constits, Constit_Id) then + In_Seen := True; - -- A Proof_In constituent can refine an Input state as long as - -- there is at least one Input constituent present. + -- A Proof_In constituent can refine an Input state as long + -- as there is at least one Input constituent present. - elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then - null; + elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) + then + null; - -- The constituent appears in the global refinement, but has - -- mode In_Out or Output (SPARK RM 7.2.4(5)). + -- The constituent appears in the global refinement, but has + -- mode In_Out or Output (SPARK RM 7.2.4(5)). - elsif Present_Then_Remove (In_Out_Constits, Constit_Id) - or else Present_Then_Remove (Out_Constits, Constit_Id) - then - Error_Msg_Name_1 := Chars (State_Id); - SPARK_Msg_NE - ("constituent & of state % must have mode `Input` in " - & "global refinement", N, Constit_Id); - end if; + elsif Present_Then_Remove (In_Out_Constits, Constit_Id) + or else Present_Then_Remove (Out_Constits, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + SPARK_Msg_NE + ("constituent & of state % must have mode `Input` in " + & "global refinement", N, Constit_Id); + end if; - Next_Elmt (Constit_Elmt); - end loop; + Next_Elmt (Constit_Elmt); + end loop; + end if; -- Not one of the constituents appeared as Input @@ -24557,47 +24598,51 @@ package body Sem_Prag is ----------------------------- procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constits : constant Elist_Id := + Refinement_Constituents (State_Id); Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; Posted : Boolean := False; begin - Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); - if Present_Then_Remove (Out_Constits, Constit_Id) then - null; + if Present_Then_Remove (Out_Constits, Constit_Id) then + null; - -- The constituent appears in the global refinement, but has - -- mode Input, In_Out or Proof_In (SPARK RM 7.2.4(5)). + -- The constituent appears in the global refinement, but has + -- mode Input, In_Out or Proof_In (SPARK RM 7.2.4(5)). - elsif Present_Then_Remove (In_Constits, Constit_Id) - or else Present_Then_Remove (In_Out_Constits, Constit_Id) - or else Present_Then_Remove (Proof_In_Constits, Constit_Id) - then - Error_Msg_Name_1 := Chars (State_Id); - SPARK_Msg_NE - ("constituent & of state % must have mode `Output` in " - & "global refinement", N, Constit_Id); + elsif Present_Then_Remove (In_Constits, Constit_Id) + or else Present_Then_Remove (In_Out_Constits, Constit_Id) + or else Present_Then_Remove (Proof_In_Constits, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + SPARK_Msg_NE + ("constituent & of state % must have mode `Output` in " + & "global refinement", N, Constit_Id); - -- The constituent is altogether missing (SPARK RM 7.2.5(3)) + -- The constituent is altogether missing (SPARK RM 7.2.5(3)) + + else + if not Posted then + Posted := True; + SPARK_Msg_NE + ("`Output` state & must be replaced by all its " + & "constituents in global refinement", N, State_Id); + end if; - else - if not Posted then - Posted := True; SPARK_Msg_NE - ("`Output` state & must be replaced by all its " - & "constituents in global refinement", N, State_Id); + ("\constituent & is missing in output list", + N, Constit_Id); end if; - SPARK_Msg_NE - ("\constituent & is missing in output list", - N, Constit_Id); - end if; - - Next_Elmt (Constit_Elmt); - end loop; + Next_Elmt (Constit_Elmt); + end loop; + end if; end Check_Constituent_Usage; -- Local variables @@ -24652,35 +24697,39 @@ package body Sem_Prag is ----------------------------- procedure Check_Constituent_Usage (State_Id : Entity_Id) is + Constits : constant Elist_Id := + Refinement_Constituents (State_Id); Constit_Elmt : Elmt_Id; Constit_Id : Entity_Id; Proof_In_Seen : Boolean := False; begin - Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id)); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); - -- At least one of the constituents appears as Proof_In + -- At least one of the constituents appears as Proof_In - if Present_Then_Remove (Proof_In_Constits, Constit_Id) then - Proof_In_Seen := True; + if Present_Then_Remove (Proof_In_Constits, Constit_Id) then + Proof_In_Seen := True; - -- The constituent appears in the global refinement, but has - -- mode Input, In_Out or Output (SPARK RM 7.2.4(5)). + -- The constituent appears in the global refinement, but has + -- mode Input, In_Out or Output (SPARK RM 7.2.4(5)). - elsif Present_Then_Remove (In_Constits, Constit_Id) - or else Present_Then_Remove (In_Out_Constits, Constit_Id) - or else Present_Then_Remove (Out_Constits, Constit_Id) - then - Error_Msg_Name_1 := Chars (State_Id); - SPARK_Msg_NE - ("constituent & of state % must have mode `Proof_In` in " - & "global refinement", N, Constit_Id); - end if; + elsif Present_Then_Remove (In_Constits, Constit_Id) + or else Present_Then_Remove (In_Out_Constits, Constit_Id) + or else Present_Then_Remove (Out_Constits, Constit_Id) + then + Error_Msg_Name_1 := Chars (State_Id); + SPARK_Msg_NE + ("constituent & of state % must have mode `Proof_In` " + & "in global refinement", N, Constit_Id); + end if; - Next_Elmt (Constit_Elmt); - end loop; + Next_Elmt (Constit_Elmt); + end loop; + end if; -- Not one of the constituents appeared as Proof_In @@ -25340,6 +25389,8 @@ package body Sem_Prag is ------------------------- procedure Collect_Constituent is + Constits : Elist_Id; + begin -- The Ghost policy in effect at the point of abstract state -- declaration and constituent must match (SPARK RM 6.9(15)) @@ -25368,7 +25419,14 @@ package body Sem_Prag is -- and establish a relation between the refined state and -- the item. - Append_Elmt (Constit_Id, Refinement_Constituents (State_Id)); + Constits := Refinement_Constituents (State_Id); + + if No (Constits) then + Constits := New_Elmt_List; + Set_Refinement_Constituents (State_Id, Constits); + end if; + + Append_Elmt (Constit_Id, Constits); Set_Encapsulating_State (Constit_Id, State_Id); -- The state has at least one legal constituent, mark the @@ -25482,6 +25540,7 @@ package body Sem_Prag is -- Local variables Constit_Id : Entity_Id; + Constits : Elist_Id; -- Start of processing for Analyze_Constituent @@ -25503,7 +25562,14 @@ package body Sem_Prag is -- Collect the constituent in the list of refinement items - Append_Elmt (Constit, Refinement_Constituents (State_Id)); + Constits := Refinement_Constituents (State_Id); + + if No (Constits) then + Constits := New_Elmt_List; + Set_Refinement_Constituents (State_Id, Constits); + end if; + + Append_Elmt (Constit, Constits); -- The state has at least one legal constituent, mark the -- start of the refinement region. The region ends when the diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index a47002645bd..21157ec9086 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3621,6 +3621,172 @@ package body Sem_Util is end if; end Check_Result_And_Post_State; + ----------------------------- + -- Check_State_Refinements -- + ----------------------------- + + procedure Check_State_Refinements + (Context : Node_Id; + Is_Main_Unit : Boolean := False) + is + procedure Check_Package (Pack : Node_Id); + -- Verify that all abstract states of a [generic] package denoted by its + -- declarative node Pack have proper refinement. Recursively verify the + -- visible and private declarations of the [generic] package for other + -- nested packages. + + procedure Check_Packages_In (Decls : List_Id); + -- Seek out [generic] package declarations within declarative list Decls + -- and verify the status of their abstract state refinement. + + function SPARK_Mode_Is_Off (N : Node_Id) return Boolean; + -- Determine whether construct N is subject to pragma SPARK_Mode Off + + ------------------- + -- Check_Package -- + ------------------- + + procedure Check_Package (Pack : Node_Id) is + Body_Id : constant Entity_Id := Corresponding_Body (Pack); + Spec : constant Node_Id := Specification (Pack); + States : constant Elist_Id := + Abstract_States (Defining_Entity (Pack)); + + State_Elmt : Elmt_Id; + State_Id : Entity_Id; + + begin + -- Do not verify proper state refinement when the package is subject + -- to pragma SPARK_Mode Off because this disables the requirement for + -- state refinement. + + if SPARK_Mode_Is_Off (Pack) then + null; + + -- State refinement can only occur in a completing packge body. Do + -- not verify proper state refinement when the body is subject to + -- pragma SPARK_Mode Off because this disables the requirement for + -- state refinement. + + elsif Present (Body_Id) + and then SPARK_Mode_Is_Off (Unit_Declaration_Node (Body_Id)) + then + null; + + -- Do not verify proper state refinement when the package is an + -- instance as this check was already performed in the generic. + + elsif Present (Generic_Parent (Spec)) then + null; + + -- Otherwise examine the contents of the package + + else + if Present (States) then + State_Elmt := First_Elmt (States); + while Present (State_Elmt) loop + State_Id := Node (State_Elmt); + + -- Emit an error when a non-null state lacks any form of + -- refinement. + + if not Is_Null_State (State_Id) + and then not Has_Null_Refinement (State_Id) + and then not Has_Non_Null_Refinement (State_Id) + then + Error_Msg_N ("state & requires refinement", State_Id); + end if; + + Next_Elmt (State_Elmt); + end loop; + end if; + + Check_Packages_In (Visible_Declarations (Spec)); + Check_Packages_In (Private_Declarations (Spec)); + end if; + end Check_Package; + + ----------------------- + -- Check_Packages_In -- + ----------------------- + + procedure Check_Packages_In (Decls : List_Id) is + Decl : Node_Id; + + begin + if Present (Decls) then + Decl := First (Decls); + while Present (Decl) loop + if Nkind_In (Decl, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Check_Package (Decl); + end if; + + Next (Decl); + end loop; + end if; + end Check_Packages_In; + + ----------------------- + -- SPARK_Mode_Is_Off -- + ----------------------- + + function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is + Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N)); + + begin + return + Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off; + end SPARK_Mode_Is_Off; + + -- Start of processing for Check_State_Refinements + + begin + -- A block may declare a nested package + + if Nkind (Context) = N_Block_Statement then + Check_Packages_In (Declarations (Context)); + + -- An entry, protected, subprogram, or task body may declare a nested + -- package. + + elsif Nkind_In (Context, N_Entry_Body, + N_Protected_Body, + N_Subprogram_Body, + N_Task_Body) + then + -- Do not verify proper state refinement when the body is subject to + -- pragma SPARK_Mode Off because this disables the requirement for + -- state refinement. + + if not SPARK_Mode_Is_Off (Context) then + Check_Packages_In (Declarations (Context)); + end if; + + -- A package body may declare a nested package + + elsif Nkind (Context) = N_Package_Body then + Check_Package (Unit_Declaration_Node (Corresponding_Spec (Context))); + + -- Do not verify proper state refinement when the body is subject to + -- pragma SPARK_Mode Off because this disables the requirement for + -- state refinement. + + if not SPARK_Mode_Is_Off (Context) then + Check_Packages_In (Declarations (Context)); + end if; + + -- A library level [generic] package may declare a nested package + + elsif Nkind_In (Context, N_Generic_Package_Declaration, + N_Package_Declaration) + and then Is_Main_Unit + then + Check_Package (Context); + end if; + end Check_State_Refinements; + ------------------------------ -- Check_Unprotected_Access -- ------------------------------ @@ -6294,9 +6460,9 @@ package body Sem_Util is or else Is_Internal (E) then declare + Decl : constant Node_Id := Parent (E); Prev : Entity_Id; Prev_Vis : Entity_Id; - Decl : constant Node_Id := Parent (E); begin -- If E is an implicit declaration, it cannot be the first @@ -9329,18 +9495,18 @@ package body Sem_Util is ----------------------------- function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean is + Constits : Elist_Id; + begin pragma Assert (Ekind (Id) = E_Abstract_State); + Constits := Refinement_Constituents (Id); -- For a refinement to be non-null, the first constituent must be -- anything other than null. - if Present (Refinement_Constituents (Id)) then - return - Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null; - end if; - - return False; + return + Present (Constits) + and then Nkind (Node (First_Elmt (Constits))) /= N_Null; end Has_Non_Null_Refinement; ------------------------ @@ -9438,18 +9604,18 @@ package body Sem_Util is ------------------------- function Has_Null_Refinement (Id : Entity_Id) return Boolean is + Constits : Elist_Id; + begin pragma Assert (Ekind (Id) = E_Abstract_State); + Constits := Refinement_Constituents (Id); -- For a refinement to be null, the state's sole constituent must be a -- null. - if Present (Refinement_Constituents (Id)) then - return - Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null; - end if; - - return False; + return + Present (Constits) + and then Nkind (Node (First_Elmt (Constits))) = N_Null; end Has_Null_Refinement; ------------------------------- @@ -18259,46 +18425,6 @@ package body Sem_Util is end if; end Require_Entity; - ------------------------------- - -- Requires_State_Refinement -- - ------------------------------- - - function Requires_State_Refinement - (Spec_Id : Entity_Id; - Body_Id : Entity_Id) return Boolean - is - Prag : constant Node_Id := SPARK_Pragma (Body_Id); - - begin - -- A package that does not define at least one abstract state cannot - -- possibly require refinement. - - if No (Abstract_States (Spec_Id)) then - return False; - - -- The package instroduces a single null state which does not merit - -- refinement. - - elsif Has_Null_Abstract_State (Spec_Id) then - return False; - - -- Check whether the package body is subject to pragma SPARK_Mode. If - -- it is and the mode is Off, the package body is considered to be in - -- regular Ada and does not require refinement. - - elsif Present (Prag) - and then Get_SPARK_Mode_From_Annotation (Prag) = Off - then - return False; - - -- The spec defines at least one abstract state and the body has no way - -- of circumventing the refinement. - - else - return True; - end if; - end Requires_State_Refinement; - ------------------------------ -- Requires_Transient_Scope -- ------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 93fadaacab4..5286ec6426e 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, 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- -- @@ -257,10 +257,6 @@ package Sem_Util is -- not necessarily mean that CE could be raised, but a response of True -- means that for sure CE cannot be raised. - procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id); - -- Verify the legality of reference Ref to variable Var_Id when the - -- variable is a constituent of a single protected/task type. - procedure Check_Dynamically_Tagged_Expression (Expr : Node_Id; Typ : Entity_Id; @@ -322,6 +318,10 @@ package Sem_Util is -- Verify that the profile of nonvolatile function Func_Id does not contain -- effectively volatile parameters or return type. + procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id); + -- Verify the legality of reference Ref to variable Var_Id when the + -- variable is a constituent of a single protected/task type. + procedure Check_Potentially_Blocking_Operation (N : Node_Id); -- N is one of the statement forms that is a potentially blocking -- operation. If it appears within a protected action, emit warning. @@ -331,6 +331,15 @@ package Sem_Util is -- 'Result and it contains an expression that evaluates differently in pre- -- and post-state. + procedure Check_State_Refinements + (Context : Node_Id; + Is_Main_Unit : Boolean := False); + -- Verify that all abstract states declared in a block statement, entry + -- body, package body, protected body, subprogram body, task body, or a + -- package declaration denoted by Context have proper refinement. Emit an + -- error if this is not the case. Flag Is_Main_Unit should be set when + -- Context denotes the main compilation unit. + procedure Check_Unused_Body_States (Body_Id : Entity_Id); -- Verify that all abstract states and objects declared in the state space -- of package body Body_Id are used as constituents. Emit an error if this @@ -2007,12 +2016,6 @@ package Sem_Util is -- This is used as a defense mechanism against ill-formed trees caused by -- previous errors (particularly in -gnatq mode). - function Requires_State_Refinement - (Spec_Id : Entity_Id; - Body_Id : Entity_Id) return Boolean; - -- Determine whether a package denoted by its spec and body entities - -- requires refinement of abstract states. - function Requires_Transient_Scope (Id : Entity_Id) return Boolean; -- Id is a type entity. The result is True when temporaries of this type -- need to be wrapped in a transient scope to be reclaimed properly when a |