OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

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.

From-SVN: r235326
This commit is contained in:
Arnaud Charlet 2016-04-21 11:46:18 +02:00
parent c4dc212506
commit 22a4f9d54d
16 changed files with 633 additions and 327 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
gcc/ada/ChangeLog
View File

@ -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.

11
gcc/ada/contracts.adb
View File

@ -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

38
gcc/ada/einfo.adb
View File

@ -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;
--------------------

83
gcc/ada/exp_pakd.adb
View File

@ -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)));

7
gcc/ada/g-traceb.ads
View File

@ -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.

7
gcc/ada/lib-writ.adb
View File

@ -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

4
gcc/ada/s-soflin.adb
View File

@ -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");

12
gcc/ada/sem_ch10.adb
View File

@ -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;
-------------------

20
gcc/ada/sem_ch13.adb
View File

@ -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);

7
gcc/ada/sem_ch3.adb
View File

@ -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;

85
gcc/ada/sem_ch7.adb
View File

@ -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);
-- 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)).
Body_Required := Unit_Requires_Body (Id);
-- 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.)
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;
-- 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;
Comp_Unit := Nkind (Parent (N)) = N_Compilation_Unit;
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

15
gcc/ada/sem_ch7.ads
View File

@ -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

4
gcc/ada/sem_ch9.adb
View File

@ -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);

328
gcc/ada/sem_prag.adb
View File

@ -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);
Append_Elmt (Var_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 (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);
Append_Elmt (Item_Id, 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, 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);
-- 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;
if Present (Body_Inputs)
and then Appears_In (Body_Inputs, Constit_Id)
then
Error_Msg_Name_1 := Chars (State_Id);
SPARK_Msg_NE
("output state & must be replaced by all its "
& "constituents in dependence refinement",
N, State_Id);
("constituent & of state % must act as output in "
& "dependence refinement", N, Constit_Id);
-- 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;
SPARK_Msg_NE
("\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);
-- The constituent is altogether missing (SPARK RM 7.2.5(3))
else
if not Posted then
Posted := True;
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
("`Output` state & must be replaced by all its "
& "constituents in global refinement", N, State_Id);
("constituent & of state % must have mode `Output` in "
& "global refinement", N, Constit_Id);
-- 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;
SPARK_Msg_NE
("\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

232
gcc/ada/sem_util.adb
View File

@ -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 --
------------------------------

25
gcc/ada/sem_util.ads
View File

@ -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