procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[multiple changes]

Browse source 
2015-10-23  Bob Duff  <duff@adacore.com>

	* exp_strm.adb (Build_Record_Or_Elementary_Input_Function): Use
	Underlying_Type for B_Typ, in case the Typ is a subtype of a type with
	unknown discriminants.
	* g-awk.ads: Minor style fix in comment

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* debug.adb: Document the use of debug switch -gnatd.5.
	* einfo.adb: Code reformatting.	(Is_Ghost_Entity): Moved from ghost.adb.
	* einfo.ads New synthesized attribute Is_Ghost_Enity along
	with usage in nodes and pragma Inline.
	(Is_Ghost_Entity: Moved from ghost.ads.
	* exp_ch3.adb Code reformatting.
	(Expand_Freeze_Array_Type): Capture, set and restore the Ghost mode.
	(Expand_Freeze_Class_Wide_Type): Capture, set and restore the
	Ghost mode.
	(Expand_Freeze_Enumeration_Type): Capture, set and
	restore the Ghost mode.
	(Expand_Freeze_Record_Type): Capture, set and restore the Ghost mode.
	* exp_ch6.adb (Expand_Subprogram_Contract): Do not expand the
	contract of an ignored Ghost subprogram.
	* exp_ch13.adb Add with and use clauses for Ghost.
	(Expand_N_Freeze_Entity): Capture, set and restore the Ghost mode.
	* exp_dbug.adb (Get_External_Name): Code reformatting. Add a
	special prefix for ignored Ghost entities or when requested by
	-gnatd.5 for any Ghost entity.
	* exp_dbug.ads Document the use of prefix "_ghost_" for ignored
	Ghost entities.
	* exp_prag.adb (Expand_Pragma_Check): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Loop_Variant): Use In_Assertion_Expr
	to signal the original context.
	* ghost.adb (Check_Ghost_Overriding): Code cleanup.
	(Is_Ghost_Entity): Moved to einfo.adb.	(Is_OK_Declaration):
	Move the assertion expression check to the outer level.
	(Is_OK_Ghost_Context): An assertion expression is a valid Ghost
	context.
	* ghost.ads (Is_Ghost_Entity): Moved to einfo.ads.
	* sem_ch3.adb (Analyze_Object_Contract): A source Ghost object
	cannot be imported or exported. Mark internally generated objects
	as Ghost when applicable.
	(Make_Class_Wide_Type): Inherit the ghostness of the root tagged type.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Mark
	a stand alone subprogram body as Ghost when applicable.
	(Analyze_Subprogram_Declaration): Mark internally generated
	subprograms as Ghost when applicable.
	* sem_ch7.adb: Code cleanup.
	* sem_ch13.adb (Add_Invariants): Add various formal
	parameters to break dependency on global variables.
	(Build_Invariant_Procedure): Code cleanup. Capture, set and
	restore the Ghost mode.
	* sem_res.adb (Resolve_Actuals): The actual parameter of a source
	Ghost subprogram whose formal is of mode IN OUT or OUT must be
	a Ghost variable.

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch8.adb Code cleanup.
	(Find_Expanded_Name): Replace
	the call to In_Pragmas_Depends_Or_Global with a call to
	In_Abstract_View_Pragma.
	(In_Abstract_View_Pragma): New routine.
	(In_Pragmas_Depends_Or_Global): Removed.
	* sem_prag.adb (Analyze_Part_Of): Catch a case where indicator
	Part_Of denotes the abstract view of a variable.

From-SVN: r229224
This commit is contained in:
Arnaud Charlet 2015-10-23 12:29:50 +02:00
parent 2e88509395
commit 95fef24ff9
21 changed files with 1614 additions and 1393 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
gcc/ada/ChangeLog
View file

@ -1,3 +1,71 @@
2015-10-23 Bob Duff <duff@adacore.com>
* exp_strm.adb (Build_Record_Or_Elementary_Input_Function): Use
Underlying_Type for B_Typ, in case the Typ is a subtype of a type with
unknown discriminants.
* g-awk.ads: Minor style fix in comment
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
* debug.adb: Document the use of debug switch -gnatd.5.
* einfo.adb: Code reformatting. (Is_Ghost_Entity): Moved from ghost.adb.
* einfo.ads New synthesized attribute Is_Ghost_Enity along
with usage in nodes and pragma Inline.
(Is_Ghost_Entity: Moved from ghost.ads.
* exp_ch3.adb Code reformatting.
(Expand_Freeze_Array_Type): Capture, set and restore the Ghost mode.
(Expand_Freeze_Class_Wide_Type): Capture, set and restore the
Ghost mode.
(Expand_Freeze_Enumeration_Type): Capture, set and
restore the Ghost mode.
(Expand_Freeze_Record_Type): Capture, set and restore the Ghost mode.
* exp_ch6.adb (Expand_Subprogram_Contract): Do not expand the
contract of an ignored Ghost subprogram.
* exp_ch13.adb Add with and use clauses for Ghost.
(Expand_N_Freeze_Entity): Capture, set and restore the Ghost mode.
* exp_dbug.adb (Get_External_Name): Code reformatting. Add a
special prefix for ignored Ghost entities or when requested by
-gnatd.5 for any Ghost entity.
* exp_dbug.ads Document the use of prefix "_ghost_" for ignored
Ghost entities.
* exp_prag.adb (Expand_Pragma_Check): Capture, set and restore the
Ghost mode.
(Expand_Pragma_Loop_Variant): Use In_Assertion_Expr
to signal the original context.
* ghost.adb (Check_Ghost_Overriding): Code cleanup.
(Is_Ghost_Entity): Moved to einfo.adb. (Is_OK_Declaration):
Move the assertion expression check to the outer level.
(Is_OK_Ghost_Context): An assertion expression is a valid Ghost
context.
* ghost.ads (Is_Ghost_Entity): Moved to einfo.ads.
* sem_ch3.adb (Analyze_Object_Contract): A source Ghost object
cannot be imported or exported. Mark internally generated objects
as Ghost when applicable.
(Make_Class_Wide_Type): Inherit the ghostness of the root tagged type.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Mark
a stand alone subprogram body as Ghost when applicable.
(Analyze_Subprogram_Declaration): Mark internally generated
subprograms as Ghost when applicable.
* sem_ch7.adb: Code cleanup.
* sem_ch13.adb (Add_Invariants): Add various formal
parameters to break dependency on global variables.
(Build_Invariant_Procedure): Code cleanup. Capture, set and
restore the Ghost mode.
* sem_res.adb (Resolve_Actuals): The actual parameter of a source
Ghost subprogram whose formal is of mode IN OUT or OUT must be
a Ghost variable.
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch8.adb Code cleanup.
(Find_Expanded_Name): Replace
the call to In_Pragmas_Depends_Or_Global with a call to
In_Abstract_View_Pragma.
(In_Abstract_View_Pragma): New routine.
(In_Pragmas_Depends_Or_Global): Removed.
* sem_prag.adb (Analyze_Part_Of): Catch a case where indicator
Part_Of denotes the abstract view of a variable.
2015-10-23 Arnaud Charlet <charlet@adacore.com>
* sem_util.ads (Unique_Defining_Entity): Document the result

8
gcc/ada/debug.adb
View file

@ -159,7 +159,7 @@ package body Debug is
-- d.2 Allow statements in declarative part
-- d.3 Output debugging information from Exp_Unst
-- d.4
-- d.5
-- d.5 Generate Ghost external sumbols regardless of Ghost policy
-- d.6
-- d.7
-- d.8
@ -762,6 +762,12 @@ package body Debug is
-- d.3 Output debugging information from Exp_Unst, including the name of
-- any unreachable subprograms that get deleted.
-- d.5 Generate specialized external symbols for Ghost entities where the
-- name of the entity is prefixed by "_ghost_" regardless of whether
-- the Ghost policy is Check or Ignore. WARNING: This switch may cause
-- linking issues related to Ghost entities declared with Ghost policy
-- Check.
------------------------------------------
-- Documentation for Binder Debug Flags --
------------------------------------------

29
gcc/ada/einfo.adb
View file

@ -3399,8 +3399,7 @@ package body Einfo is
function Is_Concurrent_Body (Id : E) return B is
begin
return Ekind (Id) in
Concurrent_Body_Kind;
return Ekind (Id) in Concurrent_Body_Kind;
end Is_Concurrent_Body;
function Is_Concurrent_Record_Type (Id : E) return B is
@ -3415,8 +3414,7 @@ package body Einfo is
function Is_Decimal_Fixed_Point_Type (Id : E) return B is
begin
return Ekind (Id) in
Decimal_Fixed_Point_Kind;
return Ekind (Id) in Decimal_Fixed_Point_Kind;
end Is_Decimal_Fixed_Point_Type;
function Is_Digits_Type (Id : E) return B is
@ -3446,14 +3444,12 @@ package body Einfo is
function Is_Enumeration_Type (Id : E) return B is
begin
return Ekind (Id) in
Enumeration_Kind;
return Ekind (Id) in Enumeration_Kind;
end Is_Enumeration_Type;
function Is_Fixed_Point_Type (Id : E) return B is
begin
return Ekind (Id) in
Fixed_Point_Kind;
return Ekind (Id) in Fixed_Point_Kind;
end Is_Fixed_Point_Type;
function Is_Floating_Point_Type (Id : E) return B is
@ -3481,16 +3477,19 @@ package body Einfo is
return Ekind (Id) in Generic_Unit_Kind;
end Is_Generic_Unit;
function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
begin
return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
end Is_Ghost_Entity;
function Is_Incomplete_Or_Private_Type (Id : E) return B is
begin
return Ekind (Id) in
Incomplete_Or_Private_Kind;
return Ekind (Id) in Incomplete_Or_Private_Kind;
end Is_Incomplete_Or_Private_Type;
function Is_Incomplete_Type (Id : E) return B is
begin
return Ekind (Id) in
Incomplete_Kind;
return Ekind (Id) in Incomplete_Kind;
end Is_Incomplete_Type;
function Is_Integer_Type (Id : E) return B is
@ -3500,8 +3499,7 @@ package body Einfo is
function Is_Modular_Integer_Type (Id : E) return B is
begin
return Ekind (Id) in
Modular_Integer_Kind;
return Ekind (Id) in Modular_Integer_Kind;
end Is_Modular_Integer_Type;
function Is_Named_Number (Id : E) return B is
@ -3521,8 +3519,7 @@ package body Einfo is
function Is_Ordinary_Fixed_Point_Type (Id : E) return B is
begin
return Ekind (Id) in
Ordinary_Fixed_Point_Kind;
return Ekind (Id) in Ordinary_Fixed_Point_Kind;
end Is_Ordinary_Fixed_Point_Type;
function Is_Overloadable (Id : E) return B is

14
gcc/ada/einfo.ads
View file

@ -2502,6 +2502,13 @@ package Einfo is
-- package, generic function, generic procedure), and False for all
-- other entities.
-- Is_Ghost_Entity (synthesized)
-- Applies to all entities. Yields True for abstract states, [generic]
-- packages, [generic] subprograms, components, discriminants, formal
-- parameters, objects, package bodies, subprogram bodies, and [sub]types
-- subject to pragma Ghost or those that inherit the Ghost propery from
-- an enclosing construct.
-- Is_Hidden (Flag57)
-- Defined in all entities. Set for all entities declared in the
-- private part or body of a package. Also marks generic formals of a
@ -5384,6 +5391,7 @@ package Einfo is
-- Declaration_Node (synth)
-- Has_Foreign_Convention (synth)
-- Is_Dynamic_Scope (synth)
-- Is_Ghost_Entity (synth)
-- Is_Standard_Character_Type (synth)
-- Is_Standard_String_Type (synth)
-- Underlying_Type (synth)
@ -7158,9 +7166,10 @@ package Einfo is
function Is_Formal_Subprogram (Id : E) return B;
function Is_Generic_Actual_Subprogram (Id : E) return B;
function Is_Generic_Actual_Type (Id : E) return B;
function Is_Generic_Unit (Id : E) return B;
function Is_Generic_Type (Id : E) return B;
function Is_Generic_Subprogram (Id : E) return B;
function Is_Generic_Type (Id : E) return B;
function Is_Generic_Unit (Id : E) return B;
function Is_Ghost_Entity (Id : E) return B;
function Is_Incomplete_Or_Private_Type (Id : E) return B;
function Is_Incomplete_Type (Id : E) return B;
function Is_Integer_Type (Id : E) return B;
@ -8380,6 +8389,7 @@ package Einfo is
pragma Inline (Is_Generic_Subprogram);
pragma Inline (Is_Generic_Type);
pragma Inline (Is_Generic_Unit);
pragma Inline (Is_Ghost_Entity);
pragma Inline (Is_Hidden);
pragma Inline (Is_Hidden_Non_Overridden_Subpgm);
pragma Inline (Is_Hidden_Open_Scope);

19
gcc/ada/exp_ch13.adb
View file

@ -32,6 +32,7 @@ with Exp_Imgv; use Exp_Imgv;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
@ -361,14 +362,21 @@ package body Exp_Ch13 is
----------------------------
procedure Expand_N_Freeze_Entity (N : Node_Id) is
E : constant Entity_Id := Entity (N);
E : constant Entity_Id := Entity (N);
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Decl : Node_Id;
Delete : Boolean := False;
E_Scope : Entity_Id;
In_Other_Scope : Boolean;
In_Outer_Scope : Boolean;
Decl : Node_Id;
Delete : Boolean := False;
begin
-- Ensure that all freezing activities are properly flagged as Ghost
Set_Ghost_Mode_From_Entity (E);
-- If there are delayed aspect specifications, we insert them just
-- before the freeze node. They are already analyzed so we don't need
-- to reanalyze them (they were analyzed before the type was frozen),
@ -436,13 +444,14 @@ package body Exp_Ch13 is
-- statement, insert them back into the tree now.
Explode_Initialization_Compound_Statement (E);
Ghost_Mode := Save_Ghost_Mode;
return;
-- Only other items requiring any front end action are types and
-- subprograms.
elsif not Is_Type (E) and then not Is_Subprogram (E) then
Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@ -454,6 +463,7 @@ package body Exp_Ch13 is
if No (E_Scope) then
Check_Error_Detected;
Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@ -671,6 +681,7 @@ package body Exp_Ch13 is
-- whether we are inside a (possibly nested) call to this procedure.
Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Freeze_Entity;
-------------------------------------------

2426
gcc/ada/exp_ch3.adb
View file

File diff suppressed because it is too large Load diff

6
gcc/ada/exp_ch6.adb
View file

@ -7766,6 +7766,12 @@ package body Exp_Ch6 is
elsif not Has_Significant_Contract (Subp_Id) then
return;
-- The contract of an ignored Ghost subprogram does not need expansion
-- because the subprogram and all calls to it will be removed.
elsif Is_Ignored_Ghost_Entity (Subp_Id) then
return;
end if;
-- Do not re-expand the same contract. This scenario occurs when a

43
gcc/ada/exp_dbug.adb
View file

@ -575,9 +575,7 @@ package body Exp_Dbug is
-- Couldn't we just test Original_Operating_Mode here? ???
if Operating_Mode /= Generate_Code
and then not Generating_Code
then
if Operating_Mode /= Generate_Code and then not Generating_Code then
return;
end if;
@ -641,11 +639,11 @@ package body Exp_Dbug is
Lo_Discr : constant Boolean :=
Nkind (Lo) = N_Identifier
and then Ekind (Entity (Lo)) = E_Discriminant;
and then Ekind (Entity (Lo)) = E_Discriminant;
Hi_Discr : constant Boolean :=
Nkind (Hi) = N_Identifier
and then Ekind (Entity (Hi)) = E_Discriminant;
and then Ekind (Entity (Hi)) = E_Discriminant;
Lo_Encode : constant Boolean := Lo_Con or Lo_Discr;
Hi_Encode : constant Boolean := Hi_Con or Hi_Discr;
@ -717,11 +715,8 @@ package body Exp_Dbug is
procedure Get_External_Name
(Entity : Entity_Id;
Has_Suffix : Boolean := False;
Suffix : String := "")
Suffix : String := "")
is
E : Entity_Id := Entity;
Kind : Entity_Kind;
procedure Get_Qualified_Name_And_Append (Entity : Entity_Id);
-- Appends fully qualified name of given entity to Name_Buffer
@ -752,6 +747,10 @@ package body Exp_Dbug is
end if;
end Get_Qualified_Name_And_Append;
-- Local variables
E : Entity_Id := Entity;
-- Start of processing for Get_External_Name
begin
@ -777,15 +776,25 @@ package body Exp_Dbug is
E := Defining_Identifier (Entity);
end if;
Kind := Ekind (E);
-- Add a special prefix to distinguish ignored Ghost entities. These
-- entities should not leak in the "living" space and they should be
-- removed by the compiler in a post-processing pass. The prefix is
-- also added to any kind of Ghost entity when switch -gnatd.5 is
-- enabled.
if Is_Ignored_Ghost_Entity (E)
or else (Debug_Flag_Dot_5 and Is_Ghost_Entity (E))
then
Add_Str_To_Name_Buffer ("_ghost_");
end if;
-- Case of interface name being used
if (Kind = E_Procedure or else
Kind = E_Function or else
Kind = E_Constant or else
Kind = E_Variable or else
Kind = E_Exception)
if Ekind_In (E, E_Constant,
E_Exception,
E_Function,
E_Procedure,
E_Variable)
and then Present (Interface_Name (E))
and then No (Address_Clause (E))
and then not Has_Suffix
@ -816,9 +825,7 @@ package body Exp_Dbug is
if Is_Generic_Instance (E)
and then Is_Subprogram (E)
and then not Is_Compilation_Unit (Scope (E))
and then (Ekind (Scope (E)) = E_Package
or else
Ekind (Scope (E)) = E_Package_Body)
and then Ekind_In (Scope (E), E_Package, E_Package_Body)
and then Present (Related_Instance (Scope (E)))
then
E := Related_Instance (Scope (E));

11
gcc/ada/exp_dbug.ads
View file

@ -76,6 +76,12 @@ package Exp_Dbug is
-- qualification for such entities. In particular this means that direct
-- local variables of a procedure are not qualified.
-- For ignored Ghost entities, the encoding adds a prefix "_ghost_" to aid
-- the detection of leaks in the "living" space. Ignored Ghost entities and
-- any code associated with them should be removed by the compiler in a
-- post-processing pass. As a result, object files should not contain any
-- occurrences of this prefix.
-- As an example of the local name convention, consider a procedure V.W
-- with a local variable X, and a nested block Y containing an entity Z.
-- The fully qualified names of the entities X and Z are:
@ -414,7 +420,7 @@ package Exp_Dbug is
procedure Get_External_Name
(Entity : Entity_Id;
Has_Suffix : Boolean := False;
Suffix : String := "");
Suffix : String := "");
-- Set Name_Buffer and Name_Len to the external name of the entity. The
-- external name is the Interface_Name, if specified, unless the entity
-- has an address clause or Has_Suffix is true.
@ -1185,8 +1191,7 @@ package Exp_Dbug is
function Make_Packed_Array_Impl_Type_Name
(Typ : Entity_Id;
Csize : Uint)
return Name_Id;
Csize : Uint) return Name_Id;
-- This function is used in Exp_Pakd to create the name that is encoded as
-- described above. The entity Typ provides the name ttt, and the value
-- Csize is the component size that provides the nnn value.

22
gcc/ada/exp_prag.adb
View file

@ -321,6 +321,8 @@ package body Exp_Prag is
-- Assert_Failure, so that coverage analysis tools can relate the
-- call to the failed check.
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
-- Nothing to do if pragma is ignored
@ -328,6 +330,13 @@ package body Exp_Prag is
return;
end if;
-- Pragmas Assert, Assert_And_Cut, Assume, Check and Loop_Invariant are
-- Ghost when they apply to a Ghost entity. Set the mode now to ensure
-- that any nodes generated during expansion are properly flagged as
-- Ghost.
Set_Ghost_Mode (N);
-- Since this check is active, we rewrite the pragma into a
-- corresponding if statement, and then analyze the statement.
@ -482,7 +491,7 @@ package body Exp_Prag is
if Is_Entity_Name (Original_Node (Cond))
and then Entity (Original_Node (Cond)) = Standard_False
then
return;
null;
elsif Nam = Name_Assert then
Error_Msg_N ("?A?assertion will fail at run time", N);
@ -491,6 +500,8 @@ package body Exp_Prag is
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Check;
---------------------------------
@ -1806,6 +1817,14 @@ package body Exp_Prag is
Set_Ghost_Mode (N);
-- The expansion of Loop_Variant is quite distributed as it produces
-- various statements to capture and compare the arguments. To preserve
-- the original context, set the Is_Assertion_Expr flag. This aids the
-- Ghost legality checks when verifying the placement of a reference to
-- a Ghost entity.
In_Assertion_Expr := In_Assertion_Expr + 1;
-- Locate the enclosing loop for which this assertion applies. In the
-- case of Ada 2012 array iteration, we might be dealing with nested
-- loops. Only the outermost loop has an identifier.
@ -1867,6 +1886,7 @@ package body Exp_Prag is
-- corresponding declarations and statements. We leave it in the tree
-- for documentation purposes. It will be ignored by the backend.
In_Assertion_Expr := In_Assertion_Expr - 1;
Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Loop_Variant;

4
gcc/ada/exp_strm.adb
View file

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -1121,7 +1121,7 @@ package body Exp_Strm is
Decl : out Node_Id;
Fnam : out Entity_Id)
is
B_Typ : constant Entity_Id := Base_Type (Typ);
B_Typ : constant Entity_Id := Underlying_Type (Base_Type (Typ));
Cn : Name_Id;
Constr : List_Id;
Decls : List_Id;

4
gcc/ada/g-awk.ads
View file

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2000-2011, AdaCore --
-- Copyright (C) 2000-2015, 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- --
@ -465,7 +465,7 @@ package GNAT.AWK is
Pattern : GNAT.Regpat.Pattern_Matcher;
Action : Match_Action_Callback);
-- Same as above but it pass the set of matches to the action
-- procedure. This is useful to analyse further why and where a regular
-- procedure. This is useful to analyze further why and where a regular
-- expression did match.
procedure Register

77
gcc/ada/ghost.adb
View file

@ -229,11 +229,6 @@ package body Ghost is
elsif Is_Subject_To_Ghost (Decl) then
return True;
-- The declaration appears within an assertion expression
elsif In_Assertion_Expr > 0 then
return True;
end if;
-- Special cases
@ -338,13 +333,13 @@ package body Ghost is
if Is_Ghost_Pragma (Prag) then
return True;
-- An assertion expression is a Ghost pragma when it contains a
-- An assertion expression pragma is Ghost when it contains a
-- reference to a Ghost entity (SPARK RM 6.9(11)).
elsif Assertion_Expression_Pragma (Prag_Id) then
-- Predicates are excluded from this category when they do
-- not apply to a Ghost subtype (SPARK RM 6.9(12)).
-- not apply to a Ghost subtype (SPARK RM 6.9(11)).
if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
Name_Predicate,
@ -413,27 +408,17 @@ package body Ghost is
-- Special cases
elsif Nkind (Stmt) = N_If_Statement then
-- An if statement is a suitable context for a Ghost entity if it
-- is the byproduct of assertion expression expansion. Note that
-- the assertion expression may not be related to a Ghost entity,
-- but it may still contain references to Ghost entities.
-- An if statement is a suitable context for a Ghost entity if
-- it is the byproduct of assertion expression expansion. Note
-- that the assertion expression may not be related to a Ghost
-- entity, but it may still contain references to Ghost
-- entities.
if Nkind (Original_Node (Stmt)) = N_Pragma
and then Assertion_Expression_Pragma
(Get_Pragma_Id (Original_Node (Stmt)))
then
return True;
-- The expansion of pragma Contract_Cases produces various if
-- statements to evaluate all case guards. This is a suitable
-- context as Contract_Cases is an assertion expression.
elsif In_Assertion_Expr > 0 then
return True;
end if;
elsif Nkind (Stmt) = N_If_Statement
and then Nkind (Original_Node (Stmt)) = N_Pragma
and then Assertion_Expression_Pragma
(Get_Pragma_Id (Original_Node (Stmt)))
then
return True;
end if;
return False;
@ -487,13 +472,26 @@ package body Ghost is
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
return False;
exit;
end if;
Par := Parent (Par);
end loop;
return False;
-- The expansion of assertion expression pragmas and attribute Old
-- may cause a legal Ghost entity reference to become illegal due
-- to node relocation. Check the In_Assertion_Expr counter as last
-- resort to try and infer the original legal context.
if In_Assertion_Expr > 0 then
return True;
-- Otherwise the context is not suitable for a reference to a
-- Ghost entity.
else
return False;
end if;
end if;
end Is_OK_Ghost_Context;
@ -592,32 +590,32 @@ package body Ghost is
(Subp : Entity_Id;
Overridden_Subp : Entity_Id)
is
Par_Subp : Entity_Id;
Over_Subp : Entity_Id;
begin
if Present (Subp) and then Present (Overridden_Subp) then
Par_Subp := Ultimate_Alias (Overridden_Subp);
Over_Subp := Ultimate_Alias (Overridden_Subp);
-- The Ghost policy in effect at the point of declaration of a parent
-- and an overriding subprogram must match (SPARK RM 6.9(17)).
if Is_Checked_Ghost_Entity (Par_Subp)
if Is_Checked_Ghost_Entity (Over_Subp)
and then Is_Ignored_Ghost_Entity (Subp)
then
Error_Msg_N ("incompatible ghost policies in effect", Subp);
Error_Msg_Sloc := Sloc (Par_Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N ("\& declared # with ghost policy `Check`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
elsif Is_Ignored_Ghost_Entity (Par_Subp)
elsif Is_Ignored_Ghost_Entity (Over_Subp)
and then Is_Checked_Ghost_Entity (Subp)
then
Error_Msg_N ("incompatible ghost policies in effect", Subp);
Error_Msg_Sloc := Sloc (Par_Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
Error_Msg_Sloc := Sloc (Subp);
@ -686,15 +684,6 @@ package body Ghost is
Ignored_Ghost_Units.Init;
end Initialize;
---------------------
-- Is_Ghost_Entity --
---------------------
function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
begin
return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
end Is_Ghost_Entity;
-------------------------
-- Is_Subject_To_Ghost --
-------------------------

4
gcc/ada/ghost.ads
View file

@ -62,10 +62,6 @@ package Ghost is
procedure Initialize;
-- Initialize internal tables
function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
-- Determine whether entity Id is Ghost. To qualify as such, the entity
-- must be subject to pragma Ghost.
procedure Lock;
-- Lock internal tables before calling backend

88
gcc/ada/sem_ch13.adb
View file

@ -7836,7 +7836,7 @@ package body Sem_Ch13 is
end if;
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the predicate functions are properly marked as Ghost.
-- ensure that the invariant procedure is properly marked as Ghost.
Set_Ghost_Mode_From_Entity (Typ);
@ -7889,23 +7889,11 @@ package body Sem_Ch13 is
-- end typInvariant;
procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
Priv_Decls : constant List_Id := Private_Declarations (N);
Vis_Decls : constant List_Id := Visible_Declarations (N);
Loc : constant Source_Ptr := Sloc (Typ);
Stmts : List_Id;
Spec : Node_Id;
SId : Entity_Id;
PDecl : Node_Id;
PBody : Node_Id;
Object_Entity : Node_Id;
-- The entity of the formal for the procedure
Object_Name : Name_Id;
-- Name for argument of invariant procedure
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
procedure Add_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Stmts : in out List_Id;
Inherit : Boolean);
-- Appends statements to Stmts for any invariants in the rep item chain
-- of the given type. If Inherit is False, then we only process entries
-- on the chain for the type Typ. If Inherit is True, then we ignore any
@ -7917,7 +7905,12 @@ package body Sem_Ch13 is
-- Add_Invariants --
--------------------
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
procedure Add_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Stmts : in out List_Id;
Inherit : Boolean)
is
procedure Add_Invariant (Prag : Node_Id);
-- Create a runtime check to verify the exression of invariant pragma
-- Prag. All generated code is added to list Stmts.
@ -7988,17 +7981,18 @@ package body Sem_Ch13 is
Make_Attribute_Reference (Nloc,
Prefix => New_Occurrence_Of (T, Nloc),
Attribute_Name => Name_Class),
Expression => Make_Identifier (Nloc, Object_Name)));
Expression =>
Make_Identifier (Nloc, Chars (Obj_Id))));
Set_Entity (Expression (N), Object_Entity);
Set_Entity (Expression (N), Obj_Id);
Set_Etype (Expression (N), Typ);
end if;
-- Invariant, replace with obj
else
Rewrite (N, Make_Identifier (Nloc, Object_Name));
Set_Entity (N, Object_Entity);
Rewrite (N, Make_Identifier (Nloc, Chars (Obj_Id)));
Set_Entity (N, Obj_Id);
Set_Etype (N, Typ);
end if;
@ -8190,9 +8184,31 @@ package body Sem_Ch13 is
end loop;
end Add_Invariants;
-- Local variables
Loc : constant Source_Ptr := Sloc (Typ);
Priv_Decls : constant List_Id := Private_Declarations (N);
Vis_Decls : constant List_Id := Visible_Declarations (N);
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
PBody : Node_Id;
PDecl : Node_Id;
SId : Entity_Id;
Spec : Node_Id;
Stmts : List_Id;
Obj_Id : Node_Id;
-- The entity of the formal for the procedure
-- Start of processing for Build_Invariant_Procedure
begin
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the invariant procedure is properly marked as Ghost.
Set_Ghost_Mode_From_Entity (Typ);
Stmts := No_List;
PDecl := Empty;
PBody := Empty;
@ -8219,6 +8235,7 @@ package body Sem_Ch13 is
and then Nkind (PDecl) = N_Subprogram_Declaration
and then Present (Corresponding_Body (PDecl))
then
Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@ -8229,14 +8246,17 @@ package body Sem_Ch13 is
-- Recover formal of procedure, for use in the calls to invariant
-- functions (including inherited ones).
Object_Entity :=
Obj_Id :=
Defining_Identifier
(First (Parameter_Specifications (Specification (PDecl))));
Object_Name := Chars (Object_Entity);
-- Add invariants for the current type
Add_Invariants (Typ, Inherit => False);
Add_Invariants
(T => Typ,
Obj_Id => Obj_Id,
Stmts => Stmts,
Inherit => False);
-- Add invariants for parent types
@ -8258,7 +8278,11 @@ package body Sem_Ch13 is
exit when Parent_Typ = Current_Typ;
Current_Typ := Parent_Typ;
Add_Invariants (Current_Typ, Inherit => True);
Add_Invariants
(T => Current_Typ,
Obj_Id => Obj_Id,
Stmts => Stmts,
Inherit => True);
end loop;
end;
@ -8278,7 +8302,11 @@ package body Sem_Ch13 is
Iface := Node (AI);
if not Is_Ancestor (Iface, Typ, Use_Full_View => True) then
Add_Invariants (Iface, Inherit => True);
Add_Invariants
(T => Iface,
Obj_Id => Obj_Id,
Stmts => Stmts,
Inherit => True);
end if;
Next_Elmt (AI);
@ -8289,7 +8317,7 @@ package body Sem_Ch13 is
-- Build the procedure if we generated at least one Check pragma
if Stmts /= No_List then
Spec := Copy_Separate_Tree (Specification (PDecl));
Spec := Copy_Separate_Tree (Specification (PDecl));
PBody :=
Make_Subprogram_Body (Loc,
@ -8342,6 +8370,8 @@ package body Sem_Ch13 is
Analyze (PBody);
end if;
end if;
Ghost_Mode := Save_Ghost_Mode;
end Build_Invariant_Procedure;
-------------------------------

56
gcc/ada/sem_ch3.adb
View file

@ -3441,9 +3441,11 @@ package body Sem_Ch3 is
Check_Missing_Part_Of (Obj_Id);
end if;
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8))
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
-- exception to this is the object that represents the dispatch table of
-- a Ghost tagged type as the symbol needs to be exported.
if Is_Ghost_Entity (Obj_Id) then
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
@ -4166,7 +4168,7 @@ package body Sem_Ch3 is
-- An object declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
if Comes_From_Source (Id) and then Ghost_Mode > None then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
-- The Ghost policy in effect at the point of declaration
@ -4347,10 +4349,8 @@ package body Sem_Ch3 is
-- An object declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (Id)
and then (Ghost_Mode > None
or else (Present (Prev_Entity)
and then Is_Ghost_Entity (Prev_Entity)))
if Ghost_Mode > None
or else (Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity))
then
Set_Is_Ghost_Entity (Id);
@ -5730,7 +5730,7 @@ package body Sem_Ch3 is
-- Inherit the "ghostness" from the constrained array type
if Is_Ghost_Entity (T) or else Ghost_Mode > None then
if Ghost_Mode > None or else Is_Ghost_Entity (T) then
Set_Is_Ghost_Entity (Implicit_Base);
end if;
@ -6214,7 +6214,7 @@ package body Sem_Ch3 is
-- Inherit the "ghostness" from the parent base type
if Is_Ghost_Entity (Parent_Base) or else Ghost_Mode > None then
if Ghost_Mode > None or else Is_Ghost_Entity (Parent_Base) then
Set_Is_Ghost_Entity (Implicit_Base);
end if;
end Make_Implicit_Base;
@ -15815,25 +15815,23 @@ package body Sem_Ch3 is
elsif Protected_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared"
& " as a protected interface",
N, Parent_Type);
("descendant of & must be declared as a protected "
& "interface", N, Parent_Type);
elsif Synchronized_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared"
& " as a synchronized interface",
N, Parent_Type);
("descendant of & must be declared as a synchronized "
& "interface", N, Parent_Type);
elsif Task_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared as a task interface",
("descendant of & must be declared as a task interface",
N, Parent_Type);
else
Error_Msg_N
("(Ada 2005) limited interface cannot "
& "inherit from non-limited interface", Indic);
("(Ada 2005) limited interface cannot inherit from "
& "non-limited interface", Indic);
end if;
-- Ada 2005 (AI-345): Non-limited interfaces can only inherit
@ -15848,19 +15846,17 @@ package body Sem_Ch3 is
elsif Protected_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared"
& " as a protected interface",
N, Parent_Type);
("descendant of & must be declared as a protected "
& "interface", N, Parent_Type);
elsif Synchronized_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared"
& " as a synchronized interface",
N, Parent_Type);
("descendant of & must be declared as a synchronized "
& "interface", N, Parent_Type);
elsif Task_Present (Iface_Def) then
Error_Msg_NE
("descendant of& must be declared as a task interface",
("descendant of & must be declared as a task interface",
N, Parent_Type);
else
null;
@ -15874,8 +15870,8 @@ package body Sem_Ch3 is
and then not Is_Interface (Parent_Type)
then
Error_Msg_N
("parent type of a record extension cannot be "
& "a synchronized tagged type (RM 3.9.1 (3/1))", N);
("parent type of a record extension cannot be a synchronized "
& "tagged type (RM 3.9.1 (3/1))", N);
Set_Etype (T, Any_Type);
return;
end if;
@ -18240,6 +18236,12 @@ package body Sem_Ch3 is
-- The class-wide type of a class-wide type is itself (RM 3.9(14))
Set_Class_Wide_Type (CW_Type, CW_Type);
-- Inherit the "ghostness" from the root tagged type
if Ghost_Mode > None or else Is_Ghost_Entity (T) then
Set_Is_Ghost_Entity (CW_Type);
end if;
end Make_Class_Wide_Type;
----------------

13
gcc/ada/sem_ch6.adb
View file

@ -1267,7 +1267,7 @@ package body Sem_Ch6 is
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
if Is_Ghost_Entity (Gen_Id) or else Ghost_Mode > None then
if Ghost_Mode > None or else Is_Ghost_Entity (Gen_Id) then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at
@ -3286,7 +3286,7 @@ package body Sem_Ch6 is
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and
@ -3457,6 +3457,13 @@ package body Sem_Ch6 is
New_Overloaded_Entity (Body_Id);
-- A subprogram body declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
end if;
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Acts_As_Spec (N);
Generate_Definition (Body_Id);
@ -4184,7 +4191,7 @@ package body Sem_Ch6 is
-- A subprogram declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (Designator) and then Ghost_Mode > None then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
end if;

8
gcc/ada/sem_ch7.adb
View file

@ -742,11 +742,11 @@ package body Sem_Ch7 is
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
end if;
-- Inherit the "ghostness" of the subprogram spec. Note that this
-- property is not directly inherited as the body may be subject to a
-- different Ghost assertion policy.
-- Inherit the "ghostness" of the package spec. Note that this property
-- is not directly inherited as the body may be subject to a different
-- Ghost assertion policy.
if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at the

89
gcc/ada/sem_ch8.adb
View file

@ -5644,41 +5644,61 @@ package body Sem_Ch8 is
-- the scope of its declaration.
procedure Find_Expanded_Name (N : Node_Id) is
function In_Pragmas_Depends_Or_Global (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node N appears in pragmas [Refined_]
-- Depends or [Refined_]Global.
function In_Abstract_View_Pragma (Nod : Node_Id) return Boolean;
-- Determine whether expanded name Nod appears within a pragma which is
-- a suitable context for an abstract view of a state or variable. The
-- following pragmas fall in this category:
-- Depends
-- Global
-- Initializes
-- Refined_Depends
-- Refined_Global
--
-- In addition, pragma Abstract_State is also considered suitable even
-- though it is an illegal context for an abstract view as this allows
-- for proper resolution of abstract views of variables. This illegal
-- context is later flagged in the analysis of indicator Part_Of.
----------------------------------
-- In_Pragmas_Depends_Or_Global --
----------------------------------
-----------------------------
-- In_Abstract_View_Pragma --
-----------------------------
function In_Pragmas_Depends_Or_Global (N : Node_Id) return Boolean is
function In_Abstract_View_Pragma (Nod : Node_Id) return Boolean is
Par : Node_Id;
begin
-- Climb the parent chain looking for a pragma
Par := N;
Par := Nod;
while Present (Par) loop
if Nkind (Par) = N_Pragma
and then Nam_In (Pragma_Name (Par), Name_Depends,
Name_Global,
Name_Refined_Depends,
Name_Refined_Global)
then
return True;
if Nkind (Par) = N_Pragma then
if Nam_In (Pragma_Name (Par), Name_Abstract_State,
Name_Depends,
Name_Global,
Name_Initializes,
Name_Refined_Depends,
Name_Refined_Global)
then
return True;
-- Otherwise the pragma is not a legal context for an abstract
-- view.
else
exit;
end if;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
return False;
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Pragmas_Depends_Or_Global;
end In_Abstract_View_Pragma;
-- Local variables
@ -5724,18 +5744,19 @@ package body Sem_Ch8 is
Is_New_Candidate := True;
-- Handle abstract views of states and variables. These are
-- acceptable only when the reference to the view appears in
-- pragmas [Refined_]Depends and [Refined_]Global.
-- acceptable candidates only when the reference to the view
-- appears in certain pragmas.
if Ekind (Id) = E_Abstract_State
and then From_Limited_With (Id)
and then Present (Non_Limited_View (Id))
then
if In_Pragmas_Depends_Or_Global (N) then
if In_Abstract_View_Pragma (N) then
Candidate := Non_Limited_View (Id);
Is_New_Candidate := True;
-- Hide candidate because it is not used in a proper context
-- Hide the candidate because it is not used in a proper
-- context.
else
Candidate := Empty;
@ -5827,22 +5848,22 @@ package body Sem_Ch8 is
Find_Expanded_Name (N);
return;
-- There is an implicit instance of the predefined operator in
-- the given scope. The operator entity is defined in Standard.
-- Has_Implicit_Operator makes the node into an Expanded_Name.
elsif Nkind (Selector) = N_Operator_Symbol
and then Has_Implicit_Operator (N)
then
-- There is an implicit instance of the predefined operator in
-- the given scope. The operator entity is defined in Standard.
-- Has_Implicit_Operator makes the node into an Expanded_Name.
return;
-- If there is no literal defined in the scope denoted by the
-- prefix, the literal may belong to (a type derived from)
-- Standard_Character, for which we have no explicit literals.
elsif Nkind (Selector) = N_Character_Literal
and then Has_Implicit_Character_Literal (N)
then
-- If there is no literal defined in the scope denoted by the
-- prefix, the literal may belong to (a type derived from)
-- Standard_Character, for which we have no explicit literals.
return;
else
@ -5879,8 +5900,8 @@ package body Sem_Ch8 is
and then not In_Private_Part (Current_Scope)
and then not Is_Private_Descendant (Current_Scope)
then
Error_Msg_N ("private child unit& is not visible here",
Selector);
Error_Msg_N
("private child unit& is not visible here", Selector);
-- Normal case where we have a missing with for a child unit
@ -5929,8 +5950,9 @@ package body Sem_Ch8 is
E_Package,
E_Procedure)
then
P := Generic_Parent (Specification
(Unit_Declaration_Node (S)));
P :=
Generic_Parent (Specification
(Unit_Declaration_Node (S)));
-- Check that P is a generic child of the generic
-- parent of the prefix.
@ -5968,7 +5990,6 @@ package body Sem_Ch8 is
-- Here we have the case of an undefined component
else
-- The prefix may hide a homonym in the context that
-- declares the desired entity. This error can use a
-- specialized message.

15
gcc/ada/sem_prag.adb
View file

@ -3413,6 +3413,19 @@ package body Sem_Prag is
return;
end if;
-- Catch a case where indicator Part_Of denotes the abstract view of
-- a variable which appears as an abstract state (SPARK RM 10.1.2 2).
if From_Limited_With (State_Id)
and then Present (Non_Limited_View (State_Id))
and then Ekind (Non_Limited_View (State_Id)) = E_Variable
then
SPARK_Msg_N
("indicator Part_Of must denote an abstract state", State);
SPARK_Msg_N ("\& denotes abstract view of object", State);
return;
end if;
-- Determine where the state, object or the package instantiation
-- lives with respect to the enclosing packages or package bodies (if
-- any). This placement dictates the legality of the encapsulating
@ -11693,7 +11706,7 @@ package body Sem_Prag is
Scope_Suppress.Overflow_Mode_Assertions := Eliminated;
end;
-- Not that special case!
-- Not that special case
else
Analyze (N);

3
gcc/ada/sem_res.adb
View file

@ -4528,7 +4528,8 @@ package body Sem_Res is
-- The actual parameter of a Ghost subprogram whose formal is of
-- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(13)).
if Is_Ghost_Entity (Nam)
if Comes_From_Source (Nam)
and then Is_Ghost_Entity (Nam)
and then Ekind_In (F, E_In_Out_Parameter, E_Out_Parameter)
and then Is_Entity_Name (A)
and then Present (Entity (A))