diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-04-21 09:46:18 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-04-21 09:46:18 +0000 |
| commit | 0ea022247edfc7fcd05713c2226ccc632486c69e (patch) | |
| tree | df2aa9b9f66c3d60d3ad578b000ee3ac83c7f466 | |
| parent | 3e5b2144d52f039ec79d92e29ee6e7fe823b2b32 (diff) | |
| download | gcc-0ea022247edfc7fcd05713c2226ccc632486c69e.tar.gz | |
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@235326 138bc75d-0d04-0410-961f-82ee72b054a4
| -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 |