[Ada] Support for Ghost type extensions, major Ghost entity clean up
Arnaud Charlet
charlet@adacore.com
Fri Jan 13 09:35:00 GMT 2017
This patch reimplements the handling of Ghost entities and Ghost statements by
reevaluating the management of Ghost regions. Ghost regions are now installed
and removed by key processing routines such as Analyze and Expand. Management
code no longer permiates context-specific routines with a few exceptions.
The patch also completes support for Ghost type extensions and allows for
proper handling of mixed Ghost and non-Ghost parent and derived types.
-------------
-- Sources --
-------------
-- semantics.ads
package Semantics is
----------------------
-- Basic extensions --
----------------------
package No_Primitives_1 is
type Living_Parent is tagged null record;
type Ghost_Child is
new Living_Parent with null record with Ghost; -- OK
end No_Primitives_1;
package No_Primitives_2 is
type Living_Parent is tagged private;
type Ghost_Child is tagged private with Ghost;
private
type Living_Parent is tagged null record;
type Ghost_Child is new Living_Parent with null record; -- OK
end No_Primitives_2;
package No_Primitives_3 is
type Ghost_Parent is tagged null record with Ghost;
type Ghost_Child is
new Ghost_Parent with null record with Ghost; -- OK
end No_Primitives_3;
package No_Primitives_4 is
type Ghost_Parent is tagged private with Ghost;
type Ghost_Child is tagged private with Ghost;
private
type Ghost_Parent is tagged null record;
type Ghost_Child is new Ghost_Parent with null record; -- OK
end No_Primitives_4;
package No_Primitives_5 is
type Living_Iface is interface;
type Living_Parent is tagged null record;
type Ghost_Child is
new Living_Parent
and Living_Iface with null record with Ghost; -- OK
end No_Primitives_5;
package No_Primitives_6 is
type Living_Iface is interface;
type Living_Parent is tagged private;
type Ghost_Child is new Living_Iface with private with Ghost; -- OK
private
type Living_Parent is tagged null record;
type Ghost_Child is
new Living_Parent and Living_Iface with null record; -- OK
end No_Primitives_6;
package No_Primitives_7 is
type Ghost_Iface is interface with Ghost;
type Ghost_Parent is tagged null record with Ghost;
type Ghost_Child is
new Ghost_Parent and Ghost_Iface with null record with Ghost;-- OK
end No_Primitives_7;
package No_Primitives_8 is
type Ghost_Iface is interface with Ghost;
type Ghost_Parent is tagged private with Ghost;
type Ghost_Child is new Ghost_Iface with private with Ghost; -- OK
private
type Ghost_Parent is tagged null record;
type Ghost_Child is
new Ghost_Parent and Ghost_Iface with null record; -- OK
end No_Primitives_8;
-----------------
-- Inheritance --
-----------------
package Inheritance_1 is
type Living_Parent is tagged null record;
procedure Proc (Obj : Living_Parent);
type Ghost_Child is new Living_Parent with null record with Ghost;
-- inherits Proc
end Inheritance_1;
package Inheritance_2 is
type Living_Parent is tagged private;
procedure Proc (Obj : Living_Parent);
type Ghost_Child is tagged private;
private
type Living_Parent is tagged null record;
type Ghost_Child is new Living_Parent with null record;
-- inherits Proc
end Inheritance_2;
package Inheritance_3 is
type Ghost_Parent is tagged null record;
procedure Proc (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is
new Ghost_Parent with null record with Ghost;
-- inherits Proc
end Inheritance_3;
package Inheritance_4 is
type Ghost_Parent is tagged private with Ghost;
procedure Proc (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is tagged private with Ghost;
private
type Ghost_Parent is tagged null record;
type Ghost_Child is new Ghost_Parent with null record;
-- inherits Proc
end Inheritance_4;
----------------
-- Overriding --
----------------
package Overriding_1 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Ghost_Child is
new Living_Parent and Living_Iface with null record with Ghost;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_1;
package Overriding_2 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Ghost_Child is new Living_Iface with private with Ghost;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
private
type Ghost_Child is new Living_Parent and Living_Iface with null record;
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_2;
package Overriding_3 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Living_Child is new Living_Parent and Living_Iface with null record;
overriding procedure Proc_1 (Obj : Living_Child) with Ghost; -- ERROR
overriding procedure Proc_2 (Obj : Living_Child) with Ghost; -- ERROR
end Overriding_3;
package Overriding_4 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Living_Child is tagged private;
private
type Living_Child is new Living_Parent with null record;
overriding procedure Proc_1 (Obj : Living_Child) with Ghost; -- ERROR
overriding procedure Proc_2 (Obj : Living_Child) with Ghost; -- ERROR
end Overriding_4;
package Overriding_5 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent) with Ghost;
type Living_Child is new Living_Parent with null record;
overriding procedure Proc_1 (Obj : Living_Child); -- ERROR
overriding procedure Proc_2 (Obj : Living_Child); -- ERROR
end Overriding_5;
package Overriding_6 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent) with Ghost;
type Living_Child is tagged private;
private
type Living_Child is new Living_Parent with null record;
overriding procedure Proc_1 (Obj : Living_Child); -- ERROR
overriding procedure Proc_2 (Obj : Living_Child); -- ERROR
end Overriding_6;
package Overriding_7 is
type Ghost_Iface is interface with Ghost;
procedure Proc_1 (Obj : Ghost_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Ghost_Child is
new Living_Parent and Ghost_Iface with null record with Ghost;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_7;
package Overriding_8 is
type Ghost_Iface is interface with Ghost;
procedure Proc_1 (Obj : Ghost_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc_2 (Obj : Living_Parent);
type Ghost_Child is new Ghost_Iface with private with Ghost;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
private
type Ghost_Child is new Living_Parent and Ghost_Iface with null record;
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_8;
package Overriding_9 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Ghost_Parent is tagged null record with Ghost;
procedure Proc_2 (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is
new Ghost_Parent and Living_Iface with null record with Ghost;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_9;
package Overriding_10 is
type Living_Iface is interface;
procedure Proc_1 (Obj : Living_Iface) is abstract;
type Ghost_Parent is tagged null record with Ghost;
procedure Proc_2 (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is new Living_Iface with private with Ghost;
private
type Ghost_Child is new Ghost_Parent and Living_Iface with null record;
overriding procedure Proc_1 (Obj : Ghost_Child) with Ghost; -- OK
overriding procedure Proc_2 (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_10;
package Overriding_11 is
type Ghost_Iface is interface with Ghost;
procedure Proc (Obj : Ghost_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc (Obj : Living_Parent);
type Ghost_Child is
new Living_Parent and Ghost_Iface with null record with Ghost;
overriding procedure Proc (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_11;
package Overriding_12 is
type Ghost_Iface is interface with Ghost;
procedure Proc (Obj : Ghost_Iface) is abstract with Ghost;
type Living_Parent is tagged null record;
procedure Proc (Obj : Living_Parent);
type Ghost_Child is new Ghost_Iface with private with Ghost;
private
type Ghost_Child is new Living_Parent and Ghost_Iface with null record;
overriding procedure Proc (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_12;
package Overriding_13 is
type Living_Iface is interface;
procedure Proc (Obj : Living_Iface) is abstract;
type Ghost_Parent is tagged null record with Ghost;
procedure Proc (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is
new Ghost_Parent and Living_Iface with null record with Ghost;
overriding procedure Proc (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_13;
package Overriding_14 is
type Living_Iface is interface;
procedure Proc (Obj : Living_Iface) is abstract;
type Ghost_Parent is tagged null record with Ghost;
procedure Proc (Obj : Ghost_Parent) with Ghost;
type Ghost_Child is new Living_Iface with private with Ghost;
private
type Ghost_Child is new Ghost_Parent and Living_Iface with null record;
overriding procedure Proc (Obj : Ghost_Child) with Ghost; -- OK
end Overriding_14;
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c semantics.ads
emantics.ads:148:28: incompatible ghost policies in effect
semantics.ads:148:28: "Proc_1" declared at line 142 as non-ghost subprogram
semantics.ads:148:28: overridden at line 148 with ghost policy "Ignore"
semantics.ads:149:28: incompatible overriding in effect
semantics.ads:149:28: "Proc_2" declared at line 145 as non-ghost subprogram
semantics.ads:149:28: overridden at line 149 with ghost subprogram
semantics.ads:162:18: subprogram "Proc_1" is not overriding
semantics.ads:163:28: incompatible overriding in effect
semantics.ads:163:28: "Proc_2" declared at line 157 as non-ghost subprogram
semantics.ads:163:28: overridden at line 163 with ghost subprogram
semantics.ads:174:18: subprogram "Proc_1" is not overriding
semantics.ads:175:28: incompatible overriding in effect
semantics.ads:175:28: "Proc_2" declared at line 171 as ghost subprogram
semantics.ads:175:28: overridden at line 175 with non-ghost subprogram
semantics.ads:188:18: subprogram "Proc_1" is not overriding
semantics.ads:189:28: incompatible overriding in effect
semantics.ads:189:28: "Proc_2" declared at line 183 as ghost subprogram
semantics.ads:189:28: overridden at line 189 with non-ghost subprogram
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>
* atree.adb (Allocate_Initialize_Node): A newly created node is
no longer marked as Ghost at this level.
(Mark_New_Ghost_Node): New routine.
(New_Copy): Mark the copy as Ghost.
(New_Entity): Mark the entity as Ghost.
(New_Node): Mark the node as Ghost.
* einfo.adb (Is_Checked_Ghost_Entity): This attribute can now
apply to unanalyzed entities.
(Is_Ignored_Ghost_Entity): This attribute can now apply to unanalyzed
entities.
(Set_Is_Checked_Ghost_Entity): This attribute now
applies to all entities as well as unanalyzed entities.
(Set_Is_Ignored_Ghost_Entity): This attribute now applies to
all entities as well as unanalyzed entities.
* expander.adb Add with and use clauses for Ghost.
(Expand): Install and revert the Ghost region associated with the node
being expanded.
* exp_ch3.adb (Expand_Freeze_Array_Type): Remove all Ghost-related code.
(Expand_Freeze_Class_Wide_Type): Remoe all Ghost-related code.
(Expand_Freeze_Enumeration_Type): Remove all Ghost-related code.
(Expand_Freeze_Record_Type): Remove all Ghost-related code.
(Freeze_Type): Install and revert the Ghost region associated
with the type being frozen.
* exp_ch5.adb Remove with and use clauses for Ghost.
(Expand_N_Assignment_Statement): Remove all Ghost-related code.
* exp_ch6.adb Remove with and use clauses for Ghost.
(Expand_N_Procedure_Call_Statement): Remove all Ghost-relatd code.
(Expand_N_Subprogram_Body): Remove all Ghost-related code.
* exp_ch7.adb (Build_Invariant_Procedure_Body): Install and revert the
Ghost region of the working type.
(Build_Invariant_Procedure_Declaration): Install and revert
the Ghost region of the working type.
(Expand_N_Package_Body): Remove all Ghost-related code.
* exp_ch8.adb Remove with and use clauses for Ghost.
(Expand_N_Exception_Renaming_Declaration): Remove all Ghost-related
code.
(Expand_N_Object_Renaming_Declaration): Remove all Ghost-related code.
(Expand_N_Package_Renaming_Declaration): Remove all Ghost-related code.
(Expand_N_Subprogram_Renaming_Declaration): Remove all Ghost-related
code.
* exp_ch13.adb Remove with and use clauses for Ghost.
(Expand_N_Freeze_Entity): Remove all Ghost-related code.
* exp_disp.adb (Make_DT): Install and revert the Ghost region of
the tagged type. Move the generation of various entities within
the Ghost region of the type.
* exp_prag.adb Remove with and use clauses for Ghost.
(Expand_Pragma_Check): Remove all Ghost-related code.
(Expand_Pragma_Contract_Cases): Remove all Ghost-related code.
(Expand_Pragma_Initial_Condition): Remove all Ghost-related code.
(Expand_Pragma_Loop_Variant): Remove all Ghost-related code.
* exp_util.adb (Build_DIC_Procedure_Body): Install
and revert the Ghost region of the working types.
(Build_DIC_Procedure_Declaration): Install and revert the
Ghost region of the working type.
(Make_Invariant_Call): Install and revert the Ghost region of the
associated type.
(Make_Predicate_Call): Reimplemented. Install and revert the
Ghost region of the associated type.
* freeze.adb (Freeze_Entity): Install and revert the Ghost region
of the entity being frozen.
(New_Freeze_Node): Removed.
* ghost.adb Remove with and use clauses for Opt.
(Check_Ghost_Completion): Update the parameter profile
and all references to formal parameters.
(Ghost_Entity): Update the comment on usage.
(Install_Ghost_Mode): New routines.
(Is_Ghost_Assignment): New routine.
(Is_Ghost_Declaration): New routine.
(Is_Ghost_Pragma): New routine.
(Is_Ghost_Procedure_Call): New routine.
(Is_Ghost_Renaming): Removed.
(Is_OK_Declaration): Reimplemented.
(Is_OK_Pragma): Reimplemented.
(Is_OK_Statement): Reimplemented.
(Is_Subject_To_Ghost): Update the comment on usage.
(Mark_And_Set_Ghost_Assignment): New routine.
(Mark_And_Set_Ghost_Body): New routine.
(Mark_And_Set_Ghost_Completion): New routine.
(Mark_And_Set_Ghost_Declaration): New routine.
(Mark_And_Set_Ghost_Instantiation): New routine.
(Mark_And_Set_Ghost_Procedure_Call): New routine.
(Mark_Full_View_As_Ghost): Removed.
(Mark_Ghost_Declaration_Or_Body): New routine.
(Mark_Ghost_Pragma): New routine.
(Mark_Ghost_Renaming): New routine.
(Mark_Pragma_As_Ghost): Removed.
(Mark_Renaming_As_Ghost): Removed.
(Propagate_Ignored_Ghost_Code): Update the comment on usage.
(Prune_Node): Freeze nodes no longer need special pruning, they
are processed by the general ignored Ghost code mechanism.
(Restore_Ghost_Mode): New routine.
(Set_Ghost_Mode): Reimplemented.
(Set_Ghost_Mode_From_Entity): Removed.
* ghost.ads Add with and use clauses for Ghost.
(Check_Ghost_Completion): Update the parameter profile
along with the comment on usage.
(Install_Ghost_Mode): New routine.
(Is_Ghost_Assignment): New routine.
(Is_Ghost_Declaration): New routine.
(Is_Ghost_Pragma): New routine.
(Is_Ghost_Procedure_Call): New routine.
(Mark_And_Set_Ghost_Assignment): New routine.
(Mark_And_Set_Ghost_Body): New routine.
(Mark_And_Set_Ghost_Completion): New routine.
(Mark_And_Set_Ghost_Declaration): New routine.
(Mark_And_Set_Ghost_Instantiation): New routine.
(Mark_And_Set_Ghost_Procedure_Call): New routine.
(Mark_Full_View_As_Ghost): Removed.
(Mark_Ghost_Pragma): New routine.
(Mark_Ghost_Renaming): New routine.
(Mark_Pragma_As_Ghost): Removed.
(Mark_Renaming_As_Ghost): Removed.
(Restore_Ghost_Mode): New routine.
(Set_Ghost_Mode): Redefined.
(Set_Ghost_Mode_From_Entity): Removed.
* sem.adb (Analyze): Install and revert the Ghost region of the
node being analyzed.
(Do_Analyze): Change the way a clean Ghost
region is installed and reverted.
* sem_ch3.adb (Analyze_Full_Type_Declaration): Remove
all Ghost-related code.
(Analyze_Incomplete_Type_Decl): Remove all Ghost-related code.
(Analyze_Number_Declaration): Remove all Ghost-related code.
(Analyze_Object_Declaration): Install and revert the Ghost region of
a deferred object declaration's completion.
(Array_Type_Declaration): Remove all Ghost-related code.
(Build_Derived_Type): Update the comment on
the propagation of Ghost attributes from a parent to a derived type.
(Derive_Subprogram): Remove all Ghost-related code.
(Make_Class_Wide_Type): Remove all Ghost-related code.
(Make_Implicit_Base): Remove all Ghost-related code.
(Process_Full_View): Install and revert the Ghost region of
the partial view. There is no longer need to check the Ghost
completion here.
* sem_ch5.adb (Analyze_Assignment): Install and revert the Ghost
region of the left hand side.
* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Remove
all Ghost-related code.
(Analyze_Expression_Function): Remove all Ghost-related code.
(Analyze_Generic_Subprogram_Body): Remove all Ghost-related code.
(Analyze_Procedure_Call): Install and revert the Ghost region of
the procedure being called.
(Analyze_Subprogram_Body_Helper): Install and revert the Ghost
region of the spec or body.
(Analyze_Subprogram_Declaration): Remove all Ghost-related code.
(Build_Subprogram_Declaration): Remove all Ghost-related code.
(Find_Corresponding_Spec): Remove all Ghost-related code.
(Process_Formals): Remove all Ghost-related code.
* sem_ch7.adb (Analyze_Package_Body_Helper): Install and revert
the Ghost region of the spec.
(Analyze_Package_Declaration): Remove all Ghost-related code.
* sem_ch8.adb (Analyze_Exception_Renaming): Mark a renaming as
Ghost when it aliases a Ghost entity.
(Analyze_Generic_Renaming): Mark a renaming as Ghost when it aliases
a Ghost entity.
(Analyze_Object_Renaming): Mark a renaming as Ghost when
it aliases a Ghost entity.
(Analyze_Package_Renaming): Mark a renaming as Ghost when it aliases
a Ghost entity.
(Analyze_Subprogram_Renaming): Mark a renaming as Ghost when it
aliases a Ghost entity.
* sem_ch11.adb Remove with and use clauses for Ghost.
(Analyze_Exception_Declaration): Remove all Ghost-related code.
* sem_ch12.adb (Analyze_Generic_Package_Declaration): Remove all
Ghost-related code.
(Analyze_Generic_Subprogram_Declaration): Remove all Ghost-related
code.
(Analyze_Package_Instantiation): Install and revert the Ghost region
of the package instantiation.
(Analyze_Subprogram_Instantiation): Install
and revert the Ghost region of the subprogram instantiation.
(Instantiate_Package_Body): Code clean up. Install and revert the
Ghost region of the package body.
(Instantiate_Subprogram_Body): Code clean up. Install and revert the
Ghost region of the subprogram body.
* sem_ch13.adb (Build_Predicate_Functions): Install
and revert the Ghost region of the related type.
(Build_Predicate_Function_Declaration): Code clean up. Install
and rever the Ghost region of the related type.
* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
Install and revert the Ghost region of the pragma.
(Analyze_Initial_Condition_In_Decl_Part): Install and revert the
Ghost region of the pragma.
(Analyze_Pragma): Install and revert the Ghost region of various
pragmas. Mark a pragma as Ghost when it is related to a Ghost entity
or encloses a Ghost entity.
(Analyze_Pre_Post_Condition): Install and revert the Ghost
region of the pragma.
(Analyze_Pre_Post_Condition_In_Decl_Part): Install and revert the
Ghost region of the pragma.
* sem_res.adb (Resolve): Remove all Ghost-related code.
* sem_util.adb (Is_Declaration): Reimplemented.
(Is_Declaration_Other_Than_Renaming): New routine.
* sem_util.ads (Is_Declaration_Other_Than_Renaming): New routine.
* sinfo.adb (Is_Checked_Ghost_Pragma): New routine.
(Is_Ghost_Pragma): Removed.
(Is_Ignored_Ghost_Pragma): New routine.
(Set_Is_Checked_Ghost_Pragma): New routine.
(Set_Is_Ghost_Pragma): Removed.
(Set_Is_Ignored_Ghost_Pragma): New routine.
* sinfo.ads: Update the documentation on Ghost mode and
Ghost regions. New attributes Is_Checked_Ghost_Pragma
and Is_Ignored_Ghost_Pragma along with usages in nodes.
Remove attribute Is_Ghost_Pragma along with usages in nodes.
(Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
(Is_Ghost_Pragma): Removed along with pragma Inline.
(Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.
(Set_Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
(Set_Is_Ghost_Pragma): Removed along with pragma Inline.
(Set_Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.
-------------- next part --------------
Index: exp_ch5.adb
===================================================================
--- exp_ch5.adb (revision 244365)
+++ exp_ch5.adb (working copy)
@@ -38,7 +38,6 @@
with Exp_Pakd; use Exp_Pakd;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
@@ -1613,15 +1612,7 @@
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The assignment statement is Ghost when the left hand side is Ghost.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
-- Special case to check right away, if the Componentwise_Assignment
-- flag is set, this is a reanalysis from the expansion of the primitive
-- assignment procedure for a tagged type, and all we need to do is to
@@ -1631,7 +1622,6 @@
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -1723,7 +1713,6 @@
Rewrite (N, Call);
Analyze (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end;
@@ -1812,8 +1801,8 @@
loop
Set_Analyzed (Exp, False);
- if Nkind_In
- (Exp, N_Selected_Component, N_Indexed_Component)
+ if Nkind_In (Exp, N_Indexed_Component,
+ N_Selected_Component)
then
Exp := Prefix (Exp);
else
@@ -1874,7 +1863,6 @@
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2099,7 +2087,6 @@
if not Crep then
Expand_Bit_Packed_Element_Set (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Change of representation case
@@ -2198,7 +2185,6 @@
-- expansion, since they would be missed in -gnatc mode ???
Error_Msg_N ("assignment not available on limited type", N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2401,7 +2387,6 @@
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
- Ghost_Mode := Save_Ghost_Mode;
return;
end Tagged_Case;
@@ -2419,7 +2404,6 @@
end loop;
Expand_Assign_Array (N, Actual_Rhs);
- Ghost_Mode := Save_Ghost_Mode;
return;
end;
@@ -2427,7 +2411,6 @@
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Scalar types. This is where we perform the processing related to the
@@ -2540,11 +2523,8 @@
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
-
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_N_Assignment_Statement;
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 244352)
+++ exp_prag.adb (working copy)
@@ -32,7 +32,6 @@
with Exp_Ch11; use Exp_Ch11;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
-with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
@@ -317,8 +316,6 @@
-- 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
@@ -326,16 +323,9 @@
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.
+ -- Since this check is active, rewrite the pragma into a corresponding
+ -- if statement, and then analyze the statement.
- Set_Ghost_Mode (N);
-
- -- Since this check is active, we rewrite the pragma into a
- -- corresponding if statement, and then analyze the statement.
-
-- The normal case expansion transforms:
-- pragma Check (name, condition [,message]);
@@ -492,12 +482,9 @@
elsif Nam = Name_Assert then
Error_Msg_N ("?A?assertion will fail at run time", N);
else
-
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Check;
---------------------------------
@@ -997,8 +984,6 @@
Aggr : constant Node_Id :=
Expression (First (Pragma_Argument_Associations (CCs)));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Case_Guard : Node_Id;
CG_Checks : Node_Id;
CG_Stmts : List_Id;
@@ -1032,12 +1017,6 @@
return;
end if;
- -- The contract cases is Ghost when it applies to a Ghost entity. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly flagged as Ghost.
-
- Set_Ghost_Mode (CCs);
-
-- The expansion of contract cases is quite distributed as it produces
-- various statements to evaluate the case guards and consequences. To
-- preserve the original context, set the Is_Assertion_Expr flag. This
@@ -1272,7 +1251,6 @@
Append_To (Stmts, Conseq_Checks);
In_Assertion_Expr := In_Assertion_Expr - 1;
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Contract_Cases;
---------------------------------------
@@ -1372,15 +1350,14 @@
-------------------------------------
procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
- Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
+ Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
+
Check : Node_Id;
Expr : Node_Id;
Init_Cond : Node_Id;
List : List_Id;
Pack_Id : Entity_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
Pack_Id := Corresponding_Spec (Spec_Or_Body);
@@ -1419,12 +1396,6 @@
Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
- -- The initial condition is Ghost when it applies to a Ghost entity. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly flagged as Ghost.
-
- Set_Ghost_Mode (Init_Cond);
-
-- The caller should check whether the package is subject to pragma
-- Initial_Condition.
@@ -1437,7 +1408,6 @@
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -1455,8 +1425,6 @@
Append_To (List, Check);
Analyze (Check);
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Initial_Condition;
------------------------------------
@@ -1632,8 +1600,8 @@
-- Local variables
- Expr : constant Node_Id := Expression (Variant);
- Expr_Typ : constant Entity_Id := Etype (Expr);
+ Expr : constant Node_Id := Expression (Variant);
+ Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
Loop_Loc : constant Source_Ptr := Sloc (Loop_Stmt);
Curr_Id : Entity_Id;
@@ -1804,10 +1772,6 @@
end if;
end Process_Variant;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_Pragma_Loop_Variant
begin
@@ -1820,12 +1784,6 @@
return;
end if;
- -- The loop variant is Ghost when it applies 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);
-
-- 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
@@ -1896,7 +1854,6 @@
-- 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;
--------------------------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 244369)
+++ sem_ch3.adb (working copy)
@@ -2824,13 +2824,6 @@
if not Analyzed (T) then
Set_Analyzed (T);
- -- A type declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (T);
- end if;
-
case Nkind (Def) is
when N_Access_To_Subprogram_Definition =>
Access_Subprogram_Declaration (T, Def);
@@ -3072,13 +3065,6 @@
Set_Is_First_Subtype (T, True);
Set_Etype (T, T);
- -- An incomplete type declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (T);
- end if;
-
-- Ada 2005 (AI-326): Minimum decoration to give support to tagged
-- incomplete types.
@@ -3186,13 +3172,6 @@
Generate_Definition (Id);
Enter_Name (Id);
- -- A number declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- This is an optimization of a common case of an integer literal
if Nkind (E) = N_Integer_Literal then
@@ -3435,8 +3414,9 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
- Related_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
+ Related_Id : Entity_Id;
-- Start of processing for Analyze_Object_Declaration
@@ -3501,14 +3481,14 @@
end if;
end if;
- -- The object declaration is Ghost when it is subject to pragma Ghost or
- -- completes a deferred Ghost constant. Set the mode now to ensure that
- -- any nodes generated during analysis and expansion are properly marked
- -- as Ghost.
+ if Present (Prev_Entity) then
- Set_Ghost_Mode (N, Prev_Entity);
+ -- The object declaration is Ghost when it completes a deferred Ghost
+ -- constant.
- if Present (Prev_Entity) then
+ Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode);
+ Mode_Set := True;
+
Constant_Redeclaration (Id, N, T);
Generate_Reference (Prev_Entity, Id, 'c');
@@ -3802,8 +3782,7 @@
and then Analyzed (N)
and then No (Expression (N))
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- If E is null and has been replaced by an N_Raise_Constraint_Error
@@ -4061,23 +4040,6 @@
Set_Ekind (Id, E_Variable);
end if;
- -- An object declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
-
- -- The Ghost policy in effect at the point of declaration
- -- and at the point of completion must match
- -- (SPARK RM 6.9(14)).
-
- if Present (Prev_Entity)
- and then Is_Ghost_Entity (Prev_Entity)
- then
- Check_Ghost_Completion (Prev_Entity, Id);
- end if;
- end if;
-
Rewrite (N,
Make_Object_Renaming_Declaration (Loc,
Defining_Identifier => Id,
@@ -4087,10 +4049,8 @@
Set_Renamed_Object (Id, E);
Freeze_Before (N, T);
Set_Is_Frozen (Id);
+ goto Leave;
- Ghost_Mode := Save_Ghost_Mode;
- return;
-
else
-- Ensure that the generated subtype has a unique external name
-- when the related object is public. This guarantees that the
@@ -4263,22 +4223,6 @@
Init_Esize (Id);
Set_Optimize_Alignment_Flags (Id);
- -- An object declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None
- or else (Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity))
- then
- Set_Is_Ghost_Entity (Id);
-
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
-
- if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
- Check_Ghost_Completion (Prev_Entity, Id);
- end if;
- end if;
-
-- Deal with aliased case
if Aliased_Present (N) then
@@ -4481,7 +4425,9 @@
Check_No_Hidden_State (Id);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze_Object_Declaration;
---------------------------
@@ -5501,13 +5447,13 @@
procedure Array_Type_Declaration (T : in out Entity_Id; Def : Node_Id) is
Component_Def : constant Node_Id := Component_Definition (Def);
Component_Typ : constant Node_Id := Subtype_Indication (Component_Def);
+ P : constant Node_Id := Parent (Def);
Element_Type : Entity_Id;
Implicit_Base : Entity_Id;
Index : Node_Id;
- Related_Id : Entity_Id := Empty;
Nb_Index : Nat;
- P : constant Node_Id := Parent (Def);
Priv : Entity_Id;
+ Related_Id : Entity_Id := Empty;
begin
if Nkind (Def) = N_Constrained_Array_Definition then
@@ -5563,8 +5509,8 @@
then
declare
Loc : constant Source_Ptr := Sloc (Def);
- New_E : Entity_Id;
Decl : Entity_Id;
+ New_E : Entity_Id;
begin
New_E := Make_Temporary (Loc, 'T');
@@ -5705,12 +5651,6 @@
Propagate_Concurrent_Flags (Implicit_Base, Element_Type);
- -- Inherit the "ghostness" from the constrained array type
-
- if Ghost_Mode > None or else Is_Ghost_Entity (T) then
- Set_Is_Ghost_Entity (Implicit_Base);
- end if;
-
-- Unconstrained array case
else
@@ -6188,12 +6128,6 @@
Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base);
Set_Has_Delayed_Freeze (Implicit_Base, True);
-
- -- Inherit the "ghostness" from the parent base type
-
- if Ghost_Mode > None or else Is_Ghost_Entity (Parent_Base) then
- Set_Is_Ghost_Entity (Implicit_Base);
- end if;
end Make_Implicit_Base;
-- Start of processing for Build_Derived_Array_Type
@@ -9132,7 +9066,7 @@
-- (anonymous) base type.
if Has_Predicates (Parent_Type)
- or else Has_Predicates (First_Subtype (Parent_Type))
+ or else Has_Predicates (First_Subtype (Parent_Type))
then
Set_Has_Predicates (Derived_Type);
end if;
@@ -9148,8 +9082,9 @@
Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type);
end if;
- -- Propagate the attributes related to pragma Ghost from the parent type
- -- to the derived type or type extension (SPARK RM 6.9(9)).
+ -- A derived type becomes Ghost when its parent type is also Ghost
+ -- (SPARK RM 6.9(9)). Note that the Ghost-related attributes are not
+ -- directly inherited because the Ghost policy in effect may differ.
if Is_Ghost_Entity (Parent_Type) then
Set_Is_Ghost_Entity (Derived_Type);
@@ -14936,12 +14871,6 @@
Set_Alias (New_Subp, Actual_Subp);
end if;
- -- Inherit the "ghostness" from the parent subprogram
-
- if Is_Ghost_Entity (Alias (New_Subp)) then
- Set_Is_Ghost_Entity (New_Subp);
- end if;
-
-- Derived subprograms of a tagged type must inherit the convention
-- of the parent subprogram (a requirement of AI-117). Derived
-- subprograms of untagged types simply get convention Ada by default.
@@ -18346,12 +18275,6 @@
-- 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;
----------------
@@ -19584,11 +19507,14 @@
Full_Indic : Node_Id;
Full_Parent : Entity_Id;
+ Mode : Ghost_Mode_Type;
Priv_Parent : Entity_Id;
-- Start of processing for Process_Full_View
begin
+ Mark_And_Set_Ghost_Completion (N, Priv_T, Mode);
+
-- First some sanity checks that must be done after semantic
-- decoration of the full view and thus cannot be placed with other
-- similar checks in Find_Type_Name
@@ -19701,7 +19627,7 @@
-- error situation [7.3(8)].
if Priv_Parent = Any_Type or else Full_Parent = Any_Type then
- return;
+ goto Leave;
-- Ada 2005 (AI-251): Interfaces in the full type can be given in
-- any order. Therefore we don't have to check that its parent must
@@ -20053,7 +19979,7 @@
Next_Elmt (Prim_Elmt);
end loop;
- return;
+ goto Leave;
end;
-- For non-concurrent types, transfer explicit primitives, but
@@ -20190,19 +20116,6 @@
Set_Has_Specified_Stream_Output (Full_T);
end if;
- if Is_Ghost_Entity (Priv_T) then
-
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Priv_T, Full_T);
-
- -- Propagate the attributes related to pragma Ghost from the private
- -- to the full view.
-
- Mark_Full_View_As_Ghost (Priv_T, Full_T);
- end if;
-
-- Propagate Default_Initial_Condition-related attributes from the
-- partial view to the full view and its base type.
@@ -20251,6 +20164,9 @@
Set_Predicate_Function (Full_T, Predicate_Function (Priv_T));
end if;
end if;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Process_Full_View;
-----------------------------------
Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb (revision 244366)
+++ exp_ch7.adb (working copy)
@@ -4353,9 +4353,8 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Dummy : Entity_Id;
+ Mode : Ghost_Mode_Type;
Priv_Item : Node_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
@@ -4406,6 +4405,11 @@
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working 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 (Work_Typ, Mode);
+
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent types or interfaces, or be an array or record
-- type whose components have invariants.
@@ -4416,7 +4420,7 @@
-- inherited by implementing types.
if Is_Interface (Work_Typ) then
- return;
+ goto Leave;
end if;
-- Obtain both views of the type
@@ -4445,7 +4449,7 @@
-- Nothing to do because the processing of the underlying full
-- view already checked the invariants of the partial view.
- return;
+ goto Leave;
end if;
-- Create a declaration for the "partial" invariant procedure if it
@@ -4482,14 +4486,9 @@
-- Nothing to do if the invariant procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
- return;
+ goto Leave;
end if;
- -- The working 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 (Work_Typ);
-
-- Emulate the environment of the invariant procedure by installing
-- its scope and formal parameters. Note that this is not needed, but
-- having the scope of the invariant procedure installed helps with
@@ -4667,7 +4666,8 @@
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_Invariant_Procedure_Body;
-------------------------------------------
@@ -4680,8 +4680,7 @@
is
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
+ Mode : Ghost_Mode_Type;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Nam : Name_Id;
@@ -4725,6 +4724,11 @@
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working 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 (Work_Typ, Mode);
+
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent or interface types, or be an array or record
-- type whose components have invariants.
@@ -4735,26 +4739,21 @@
-- inherited by implementing types.
if Is_Interface (Work_Typ) then
- return;
+ goto Leave;
-- Nothing to do if the type already has a "partial" invariant procedure
elsif Partial_Invariant then
if Present (Partial_Invariant_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
-- Nothing to do if the type already has a "full" invariant procedure
elsif Present (Invariant_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
- -- The working 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 (Work_Typ);
-
-- The caller requests the declaration of the "partial" invariant
-- procedure.
@@ -4791,13 +4790,6 @@
Set_Needs_Debug_Info (Proc_Id);
end if;
- -- Mark the invariant procedure explicitly as Ghost because it does not
- -- come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Proc_Id);
- end if;
-
-- Obtain all views of the input type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
@@ -4868,7 +4860,8 @@
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_Invariant_Procedure_Declaration;
---------------------
@@ -5835,15 +5828,7 @@
Spec_Id : constant Entity_Id := Corresponding_Spec (N);
Fin_Id : Entity_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The package body is Ghost when the corresponding spec is Ghost. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N, Spec_Id);
-
-- This is done only for non-generic packages
if Ekind (Spec_Id) = E_Package then
@@ -5899,8 +5884,6 @@
end;
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Body;
----------------------------------
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 244350)
+++ sem_ch5.adb (working copy)
@@ -270,7 +270,7 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Analyze_Assignment
@@ -287,7 +287,7 @@
-- Ghost entity. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Assignment (N, Mode);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
@@ -356,8 +356,8 @@
if PIt = No_Interp then
Error_Msg_N
- ("ambiguous left-hand side"
- & " in assignment", Lhs);
+ ("ambiguous left-hand side in "
+ & "assignment", Lhs);
exit;
else
Resolve (Prefix (Lhs), PIt.Typ);
@@ -392,8 +392,7 @@
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
@@ -464,21 +463,20 @@
-- effect (AARM D.5.2 (5/2)).
if Locking_Policy /= 'C' then
- Error_Msg_N ("assignment to the attribute PRIORITY has " &
- "no effect??", Lhs);
- Error_Msg_N ("\since no Locking_Policy has been " &
- "specified??", Lhs);
+ Error_Msg_N
+ ("assignment to the attribute PRIORITY has no effect??",
+ Lhs);
+ Error_Msg_N
+ ("\since no Locking_Policy has been specified??", Lhs);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- Error of assigning to limited type. We do however allow this in
-- certain cases where the front end generates the assignments.
@@ -497,17 +495,14 @@
Explain_Limited_Type (T1, Lhs);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- A class-wide type may be a limited view. This illegal case is not
-- caught by previous checks.
- elsif Ekind (T1) = E_Class_Wide_Type
- and then From_Limited_With (T1)
- then
+ elsif Ekind (T1) = E_Class_Wide_Type and then From_Limited_With (T1) then
Error_Msg_NE ("invalid use of limited view of&", Lhs, T1);
- return;
+ goto Leave;
-- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be
-- abstract. This is only checked when the assignment Comes_From_Source,
@@ -545,8 +540,7 @@
then
Error_Msg_N ("invalid use of incomplete type", Lhs);
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Now we can complete the resolution of the right hand side
@@ -563,8 +557,7 @@
if Rhs = Error then
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
T2 := Etype (Rhs);
@@ -572,8 +565,7 @@
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Ada 2005 (AI-326): In case of explicit dereference of incomplete
@@ -600,8 +592,7 @@
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- If the rhs is class-wide or dynamically tagged, then require the lhs
@@ -693,8 +684,7 @@
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- If we know the right hand side is non-null, then we convert to the
-- target type, since we don't need a run time check in that case.
@@ -914,7 +904,9 @@
end;
Analyze_Dimension (N);
- Ghost_Mode := Save_Ghost_Mode;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Analyze_Assignment;
-----------------------------
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 244365)
+++ exp_util.adb (working copy)
@@ -1712,12 +1712,11 @@
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
+ Mode : Ghost_Mode_Type;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
@@ -1749,6 +1748,11 @@
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the DIC procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The working type must be either define a DIC pragma of its own or
-- inherit one from a parent type.
@@ -1767,7 +1771,7 @@
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
- return;
+ goto Leave;
end if;
-- The working type may lack a DIC procedure declaration. This may be
@@ -1799,14 +1803,9 @@
-- Nothing to do if the DIC procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the DIC procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
-- Emulate the environment of the DIC procedure by installing its scope
-- and formal parameters.
@@ -1917,7 +1916,8 @@
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_DIC_Procedure_Body;
-------------------------------------
@@ -1927,10 +1927,9 @@
procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
+ Mode : Ghost_Mode_Type;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Typ_Decl : Node_Id;
@@ -1973,6 +1972,11 @@
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the DIC procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The type must be either subject to a DIC pragma or inherit one from a
-- parent type.
@@ -1991,19 +1995,14 @@
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
- return;
+ goto Leave;
-- Nothing to do if the type already has a DIC procedure
elsif Present (DIC_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the DIC procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
Proc_Id :=
Make_Defining_Identifier (Loc,
Chars =>
@@ -2025,13 +2024,6 @@
Set_Needs_Debug_Info (Proc_Id);
end if;
- -- Mark the DIC procedure explicitly as Ghost because it does not come
- -- from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Proc_Id);
- end if;
-
-- Obtain all views of the input type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
@@ -2106,7 +2098,8 @@
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_DIC_Procedure_Declaration;
--------------------------
@@ -7816,8 +7809,9 @@
-------------------------
function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
- Loc : constant Source_Ptr := Sloc (Expr);
- Typ : constant Entity_Id := Base_Type (Etype (Expr));
+ Loc : constant Source_Ptr := Sloc (Expr);
+ Typ : constant Entity_Id := Base_Type (Etype (Expr));
+
Proc_Id : Entity_Id;
begin
@@ -7910,11 +7904,11 @@
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Expr);
- Call : Node_Id;
- PFM : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (Expr);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Call : Node_Id;
+ Func_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
begin
pragma Assert (Present (Predicate_Function (Typ)));
@@ -7922,33 +7916,24 @@
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the call is properly marked as Ghost.
- Set_Ghost_Mode_From_Entity (Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Call special membership version if requested and available
- if Mem then
- PFM := Predicate_Function_M (Typ);
-
- if Present (PFM) then
- Call :=
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (PFM, Loc),
- Parameter_Associations => New_List (Relocate_Node (Expr)));
-
- Ghost_Mode := Save_Ghost_Mode;
- return Call;
- end if;
+ if Mem and then Present (Predicate_Function_M (Typ)) then
+ Func_Id := Predicate_Function_M (Typ);
+ else
+ Func_Id := Predicate_Function (Typ);
end if;
-- Case of calling normal predicate function
Call :=
Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Predicate_Function (Typ), Loc),
+ Name => New_Occurrence_Of (Func_Id, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return Call;
end Make_Predicate_Call;
Index: sinfo.adb
===================================================================
--- sinfo.adb (revision 244352)
+++ sinfo.adb (working copy)
@@ -1809,6 +1809,14 @@
return Flag11 (N);
end Is_Checked;
+ function Is_Checked_Ghost_Pragma
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ return Flag3 (N);
+ end Is_Checked_Ghost_Pragma;
+
function Is_Component_Left_Opnd
(N : Node_Id) return Boolean is
begin
@@ -1917,22 +1925,22 @@
return Flag2 (N);
end Is_Generic_Contract_Pragma;
- function Is_Ghost_Pragma
+ function Is_Ignored
(N : Node_Id) return Boolean is
begin
pragma Assert (False
+ or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- return Flag3 (N);
- end Is_Ghost_Pragma;
+ return Flag9 (N);
+ end Is_Ignored;
- function Is_Ignored
+ function Is_Ignored_Ghost_Pragma
(N : Node_Id) return Boolean is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- return Flag9 (N);
- end Is_Ignored;
+ return Flag8 (N);
+ end Is_Ignored_Ghost_Pragma;
function Is_In_Discriminant_Check
(N : Node_Id) return Boolean is
@@ -5088,6 +5096,14 @@
Set_Flag11 (N, Val);
end Set_Is_Checked;
+ procedure Set_Is_Checked_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ Set_Flag3 (N, Val);
+ end Set_Is_Checked_Ghost_Pragma;
+
procedure Set_Is_Component_Left_Opnd
(N : Node_Id; Val : Boolean := True) is
begin
@@ -5196,22 +5212,22 @@
Set_Flag2 (N, Val);
end Set_Is_Generic_Contract_Pragma;
- procedure Set_Is_Ghost_Pragma
+ procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
+ or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- Set_Flag3 (N, Val);
- end Set_Is_Ghost_Pragma;
+ Set_Flag9 (N, Val);
+ end Set_Is_Ignored;
- procedure Set_Is_Ignored
+ procedure Set_Is_Ignored_Ghost_Pragma
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- Set_Flag9 (N, Val);
- end Set_Is_Ignored;
+ Set_Flag8 (N, Val);
+ end Set_Is_Ignored_Ghost_Pragma;
procedure Set_Is_In_Discriminant_Check
(N : Node_Id; Val : Boolean := True) is
Index: sinfo.ads
===================================================================
--- sinfo.ads (revision 244353)
+++ sinfo.ads (working copy)
@@ -528,26 +528,81 @@
-- Ghost Mode --
----------------
- -- When a declaration is subject to pragma Ghost, it establishes a Ghost
- -- region depending on the Ghost assertion policy in effect at the point
- -- of declaration. This region is temporal and starts right before the
- -- analysis of the Ghost declaration and ends after its expansion. The
- -- values of global variable Opt.Ghost_Mode are as follows:
+ -- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and
+ -- Ghost statements. The intent of the feature is to treat Ghost constructs
+ -- as non-existent when Ghost assertion policy Ignore is in effect.
+ -- The corresponding nodes which map to Ghost constructs are:
+
+ -- Ghost entities
+ -- Declaration nodes
+ -- N_Package_Body
+ -- N_Subprogram_Body
+
+ -- Ghost statements
+ -- N_Assignment_Statement
+ -- N_Procedure_Call_Statement
+ -- N_Pragma
+
+ -- In addition, the compiler treats instantiations as Ghost entities
+
+ -- To achieve the removal of ignored Ghost constructs, the compiler relies
+ -- on global variable Ghost_Mode and a mechanism called "Ghost regions".
+ -- The values of the global variable are as follows:
+
-- 1. Check - All static semantics as defined in SPARK RM 6.9 are in
- -- effect.
+ -- effect. The Ghost region has mode Check.
-- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI
- -- files, object files as well as the final executable.
+ -- files, object files, and the final executable. The Ghost region
+ -- has mode Ignore.
- -- To achieve the runtime semantics of "Ignore", the compiler marks each
- -- node created during an ignored Ghost region and signals all enclosing
- -- scopes that such a node resides within. The compilation unit where the
- -- node resides is also added to an auxiliary table for post processing.
+ -- 3. None - No Ghost region is in effect
+ -- A Ghost region is a compiler operating mode, similar to Check_Syntax,
+ -- however a region is much more finely grained and depends on the policy
+ -- in effect. The region starts prior to the analysis of a Ghost construct
+ -- and ends immediately after its expansion. The region is established as
+ -- follows:
+
+ -- 1. Declarations - Prior to analysis, if the declaration is subject to
+ -- pragma Ghost.
+
+ -- 2. Renaming declarations - Same as 1) or when the renamed entity is
+ -- Ghost.
+
+ -- 3. Completing declarations - Same as 1) or when the declaration is
+ -- partially analyzed and the declaration completes a Ghost entity.
+
+ -- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is
+ -- partially analyzed and completes a Ghost entity.
+
+ -- 5. N_Assignment_Statement - After the left hand side is analyzed and
+ -- references a Ghost entity.
+
+ -- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes
+ -- a Ghost procedure.
+
+ -- 7. N_Pragma - During analysis, when the related entity is Ghost or the
+ -- pragma encloses a Ghost entity.
+
+ -- 8. Instantiations - Save as 1) or when the instantiation is partially
+ -- analyzed and the generic template is Ghost.
+
+ -- Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine
+ -- Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled
+ -- similar to scopes for decoupled expansion such as the generation of
+ -- dispatch tables or the creation of a predicate function.
+
+ -- If the mode of a Ghost region is Ignore, any newly created nodes as well
+ -- as source entities are marked as ignored Ghost. In additon, the marking
+ -- process signals all enclosing scopes that an ignored Ghost node resides
+ -- within. The compilation unit where the node resides is also added to an
+ -- auxiliary table for post processing.
+
-- After the analysis and expansion of all compilation units takes place
-- as well as the instantiation of all inlined [generic] bodies, the GNAT
- -- driver initiates a separate pass which removes all ignored Ghost code
+ -- driver initiates a separate pass which removes all ignored Ghost nodes
-- from all units stored in the auxiliary table.
--------------------
@@ -1581,6 +1636,11 @@
-- be further modified (in some cases these flags are copied when a
-- pragma is rewritten).
+ -- Is_Checked_Ghost_Pragma (Flag3-Sem)
+ -- This flag is present in N_Pragma nodes. It is set when the pragma is
+ -- related to a checked Ghost entity or encloses a checked Ghost entity.
+ -- This flag has no relation to Is_Checked.
+
-- Is_Component_Left_Opnd (Flag13-Sem)
-- Is_Component_Right_Opnd (Flag14-Sem)
-- Present in concatenation nodes, to indicate that the corresponding
@@ -1651,11 +1711,6 @@
-- Refined_State
-- Test_Case
- -- Is_Ghost_Pragma (Flag3-Sem)
- -- This flag is present in N_Pragma nodes. It is set when the pragma is
- -- either declared within a Ghost construct or it applies to a Ghost
- -- construct.
-
-- Is_Ignored (Flag9-Sem)
-- A flag set in an N_Aspect_Specification or N_Pragma node if there was
-- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
@@ -1670,6 +1725,11 @@
-- aspect/pragma is fully analyzed and checked for other syntactic
-- and semantic errors, but it does not have any semantic effect.
+ -- Is_Ignored_Ghost_Pragma (Flag8-Sem)
+ -- This flag is present in N_Pragma nodes. It is set when the pragma is
+ -- related to an ignored Ghost entity or encloses ignored Ghost entity.
+ -- This flag has no relation to Is_Ignored.
+
-- Is_In_Discriminant_Check (Flag11-Sem)
-- This flag is present in a selected component, and is used to indicate
-- that the reference occurs within a discriminant check. The
@@ -2519,11 +2579,12 @@
-- Import_Interface_Present (Flag16-Sem)
-- Is_Analyzed_Pragma (Flag5-Sem)
-- Is_Checked (Flag11-Sem)
+ -- Is_Checked_Ghost_Pragma (Flag3-Sem)
-- Is_Delayed_Aspect (Flag14-Sem)
-- Is_Disabled (Flag15-Sem)
-- Is_Generic_Contract_Pragma (Flag2-Sem)
- -- Is_Ghost_Pragma (Flag3-Sem)
-- Is_Ignored (Flag9-Sem)
+ -- Is_Ignored_Ghost_Pragma (Flag8-Sem)
-- Is_Inherited_Pragma (Flag4-Sem)
-- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
-- Uneval_Old_Accept (Flag7-Sem)
@@ -9364,6 +9425,9 @@
function Is_Checked
(N : Node_Id) return Boolean; -- Flag11
+ function Is_Checked_Ghost_Pragma
+ (N : Node_Id) return Boolean; -- Flag3
+
function Is_Component_Left_Opnd
(N : Node_Id) return Boolean; -- Flag13
@@ -9403,12 +9467,12 @@
function Is_Generic_Contract_Pragma
(N : Node_Id) return Boolean; -- Flag2
- function Is_Ghost_Pragma
- (N : Node_Id) return Boolean; -- Flag3
-
function Is_Ignored
(N : Node_Id) return Boolean; -- Flag9
+ function Is_Ignored_Ghost_Pragma
+ (N : Node_Id) return Boolean; -- Flag8
+
function Is_In_Discriminant_Check
(N : Node_Id) return Boolean; -- Flag11
@@ -10414,6 +10478,9 @@
procedure Set_Is_Checked
(N : Node_Id; Val : Boolean := True); -- Flag11
+ procedure Set_Is_Checked_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True); -- Flag3
+
procedure Set_Is_Component_Left_Opnd
(N : Node_Id; Val : Boolean := True); -- Flag13
@@ -10453,12 +10520,12 @@
procedure Set_Is_Generic_Contract_Pragma
(N : Node_Id; Val : Boolean := True); -- Flag2
- procedure Set_Is_Ghost_Pragma
- (N : Node_Id; Val : Boolean := True); -- Flag3
-
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True); -- Flag9
+ procedure Set_Is_Ignored_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True); -- Flag8
+
procedure Set_Is_In_Discriminant_Check
(N : Node_Id; Val : Boolean := True); -- Flag11
@@ -12865,6 +12932,7 @@
pragma Inline (Is_Asynchronous_Call_Block);
pragma Inline (Is_Boolean_Aspect);
pragma Inline (Is_Checked);
+ pragma Inline (Is_Checked_Ghost_Pragma);
pragma Inline (Is_Component_Left_Opnd);
pragma Inline (Is_Component_Right_Opnd);
pragma Inline (Is_Controlling_Actual);
@@ -12878,8 +12946,8 @@
pragma Inline (Is_Finalization_Wrapper);
pragma Inline (Is_Folded_In_Parser);
pragma Inline (Is_Generic_Contract_Pragma);
- pragma Inline (Is_Ghost_Pragma);
pragma Inline (Is_Ignored);
+ pragma Inline (Is_Ignored_Ghost_Pragma);
pragma Inline (Is_In_Discriminant_Check);
pragma Inline (Is_Inherited_Pragma);
pragma Inline (Is_Machine_Number);
@@ -13210,6 +13278,7 @@
pragma Inline (Set_Is_Asynchronous_Call_Block);
pragma Inline (Set_Is_Boolean_Aspect);
pragma Inline (Set_Is_Checked);
+ pragma Inline (Set_Is_Checked_Ghost_Pragma);
pragma Inline (Set_Is_Component_Left_Opnd);
pragma Inline (Set_Is_Component_Right_Opnd);
pragma Inline (Set_Is_Controlling_Actual);
@@ -13223,8 +13292,8 @@
pragma Inline (Set_Is_Finalization_Wrapper);
pragma Inline (Set_Is_Folded_In_Parser);
pragma Inline (Set_Is_Generic_Contract_Pragma);
- pragma Inline (Set_Is_Ghost_Pragma);
pragma Inline (Set_Is_Ignored);
+ pragma Inline (Set_Is_Ignored_Ghost_Pragma);
pragma Inline (Set_Is_In_Discriminant_Check);
pragma Inline (Set_Is_Inherited_Pragma);
pragma Inline (Set_Is_Machine_Number);
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 244350)
+++ sem_ch7.adb (working copy)
@@ -537,10 +537,10 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
+ Mode : Ghost_Mode_Type;
New_N : Node_Id;
Pack_Decl : Node_Id;
Spec_Id : Entity_Id;
@@ -643,7 +643,7 @@
-- the mode now to ensure that any nodes generated during analysis and
-- expansion are properly flagged as ignored Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Style.Check_Identifier (Body_Id, Spec_Id);
@@ -738,19 +738,6 @@
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
end if;
- -- 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 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
- -- point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Spec_Id, Body_Id);
- end if;
-
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
@@ -942,7 +929,7 @@
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Analyze_Package_Body_Helper;
---------------------------------
@@ -951,7 +938,6 @@
procedure Analyze_Package_Declaration (N : Node_Id) 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;
@@ -983,16 +969,6 @@
Set_SPARK_Aux_Pragma_Inherited (Id);
end if;
- -- A package declared within a Ghost refion is automatically Ghost. A
- -- child package is Ghost when its parent is Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None
- or else (Present (Par)
- and then Is_Ghost_Entity (Defining_Entity (Unit (Par))))
- then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
@@ -1793,13 +1769,6 @@
New_Private_Type (N, Id, N);
Set_Depends_On_Private (Id);
- -- A type declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
Index: einfo.adb
===================================================================
--- einfo.adb (revision 244352)
+++ einfo.adb (working copy)
@@ -2093,7 +2093,10 @@
function Is_Checked_Ghost_Entity (Id : E) return B is
begin
- pragma Assert (Nkind (Id) in N_Entity);
+ -- Allow this attribute to appear on non-analyzed entities
+
+ pragma Assert (Nkind (Id) in N_Entity
+ or else Ekind (Id) = E_Void);
return Flag277 (Id);
end Is_Checked_Ghost_Entity;
@@ -2280,7 +2283,10 @@
function Is_Ignored_Ghost_Entity (Id : E) return B is
begin
- pragma Assert (Nkind (Id) in N_Entity);
+ -- Allow this attribute to appear on non-analyzed entities
+
+ pragma Assert (Nkind (Id) in N_Entity
+ or else Ekind (Id) = E_Void);
return Flag278 (Id);
end Is_Ignored_Ghost_Entity;
@@ -5161,20 +5167,9 @@
procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is
begin
- pragma Assert (Is_Formal (Id)
- or else Is_Object (Id)
- or else Is_Package_Or_Generic_Package (Id)
- or else Is_Subprogram_Or_Generic_Subprogram (Id)
- or else Is_Type (Id)
- or else Ekind (Id) = E_Abstract_State
- or else Ekind (Id) = E_Component
- or else Ekind (Id) = E_Discriminant
- or else Ekind (Id) = E_Exception
- or else Ekind (Id) = E_Package_Body
- or else Ekind (Id) = E_Subprogram_Body
+ -- Allow this attribute to appear on non-analyzed entities
- -- Allow this attribute to appear on non-analyzed entities
-
+ pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
Set_Flag277 (Id, V);
end Set_Is_Checked_Ghost_Entity;
@@ -5377,20 +5372,9 @@
procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is
begin
- pragma Assert (Is_Formal (Id)
- or else Is_Object (Id)
- or else Is_Package_Or_Generic_Package (Id)
- or else Is_Subprogram_Or_Generic_Subprogram (Id)
- or else Is_Type (Id)
- or else Ekind (Id) = E_Abstract_State
- or else Ekind (Id) = E_Component
- or else Ekind (Id) = E_Discriminant
- or else Ekind (Id) = E_Exception
- or else Ekind (Id) = E_Package_Body
- or else Ekind (Id) = E_Subprogram_Body
+ -- Allow this attribute to appear on non-analyzed entities
- -- Allow this attribute to appear on non-analyzed entities
-
+ pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
Set_Flag278 (Id, V);
end Set_Is_Ignored_Ghost_Entity;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 244365)
+++ sem_prag.adb (working copy)
@@ -459,9 +459,8 @@
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
CCase : Node_Id;
+ Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
@@ -478,7 +477,7 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
@@ -524,8 +523,8 @@
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
Set_Is_Analyzed_Pragma (N);
+ Restore_Ghost_Mode (Mode);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
@@ -2656,7 +2655,7 @@
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
begin
-- Do not analyze the pragma multiple times
@@ -2670,16 +2669,16 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- The expression is preanalyzed because it has not been moved to its
-- final place yet. A direct analysis may generate side effects and this
-- is not desired at this point.
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
- Ghost_Mode := Save_Ghost_Mode;
-
Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
@@ -4133,7 +4132,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
end Analyze_Depends_Global;
@@ -4316,16 +4315,16 @@
Subp_Id := Defining_Entity (Subp_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Subp_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Pre_Post_Condition_In_Decl_Part.
Add_Contract_Item (N, Defining_Entity (Subp_Decl));
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Subp_Id);
-
-- Fully analyze the pragma when it appears inside an entry or
-- subprogram body because it cannot benefit from forward references.
@@ -4446,7 +4445,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
if Nam_In (Pname, Name_Refined_Depends, Name_Refined_Global) then
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
@@ -4510,7 +4509,7 @@
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost variable being
-- processed for error detection purposes.
@@ -4684,7 +4683,7 @@
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost name being
-- processed for error detection purposes.
@@ -6793,13 +6792,12 @@
return;
end if;
- E := Entity (E_Arg);
- Decl := Declaration_Node (E);
+ E := Entity (E_Arg);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Check duplicate before we chain ourselves
@@ -6856,6 +6854,8 @@
-- Now check appropriateness of the entity
+ Decl := Declaration_Node (E);
+
if Is_Type (E) then
if Rep_Item_Too_Early (E, N)
or else
@@ -8358,7 +8358,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Def_Id);
+ Mark_Ghost_Pragma (N, Def_Id);
Kill_Size_Check_Code (Def_Id);
Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False);
end if;
@@ -9006,7 +9006,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Subp);
+ Mark_Ghost_Pragma (N, Subp);
-- Capture the entity of the first Ghost subprogram being
-- processed for error detection purposes.
@@ -9266,7 +9266,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Handler);
+ Mark_Ghost_Pragma (N, Handler);
Set_Is_Interrupt_Handler (Handler);
pragma Assert (Ekind (Prot_Typ) = E_Protected_Type);
@@ -9759,7 +9759,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Enforce RM 11.5(7) which requires that for a pragma that
-- appears within a package spec, the named entity must be
@@ -11216,6 +11216,12 @@
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Pack_Id);
@@ -11231,13 +11237,6 @@
-- Analyze all these pragmas in the order outlined above
Analyze_If_Present (Pragma_SPARK_Mode);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
- Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-
States := Expression (Get_Argument (N, Pack_Id));
-- Multiple non-null abstract states appear as an aggregate
@@ -11484,7 +11483,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Lib_Entity);
+ Mark_Ghost_Pragma (N, Lib_Entity);
-- This pragma should only apply to a RCI unit (RM E.2.3(23))
@@ -11560,7 +11559,7 @@
if Is_Entity_Name (Get_Pragma_Arg (Nam_Arg))
and then Present (Entity (Get_Pragma_Arg (Nam_Arg)))
then
- Mark_Pragma_As_Ghost (N, Entity (Get_Pragma_Arg (Nam_Arg)));
+ Mark_Ghost_Pragma (N, Entity (Get_Pragma_Arg (Nam_Arg)));
end if;
-- Not allowed in compiler units (bootstrap issues)
@@ -12111,17 +12110,17 @@
if Ekind (Obj_Id) = E_Variable then
- -- Chain the pragma on the contract for further processing by
- -- Analyze_External_Property_In_Decl_Part.
-
- Add_Contract_Item (N, Obj_Id);
-
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Id);
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_External_Property_In_Decl_Part.
+
+ Add_Contract_Item (N, Obj_Id);
+
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
@@ -12202,7 +12201,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Nm);
+ Mark_Ghost_Pragma (N, Nm);
if not Is_Remote_Call_Interface (C_Ent)
and then not Is_Remote_Types (C_Ent)
@@ -12322,7 +12321,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
Check_Duplicate_Pragma (E);
if Rep_Item_Too_Early (E, N)
@@ -12471,16 +12470,15 @@
Cname : Name_Id;
Eloc : Source_Ptr;
Expr : Node_Id;
+ Mode : Ghost_Mode_Type;
Str : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
-- Pragma Check is Ghost when it applies to a Ghost entity. Set
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are marked as Ghost.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
@@ -12677,7 +12675,7 @@
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Check;
--------------------------
@@ -13175,15 +13173,15 @@
return;
end if;
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Obj_Id);
-
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Id);
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Obj_Id);
+
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
@@ -13287,17 +13285,17 @@
Spec_Id := Unique_Defining_Entity (Subp_Decl);
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Contract_Cases_In_Decl_Part.
-
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
-
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Contract_Cases_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
-- Fully analyze the pragma when it appears inside an entry
-- or subprogram body because it cannot benefit from forward
-- references.
@@ -13361,7 +13359,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
end Convention;
---------------------------
@@ -13832,7 +13830,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The pragma signals that the type defines its own DIC assertion
-- expression.
@@ -13961,7 +13959,7 @@
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Entity (Pool));
+ Mark_Ghost_Pragma (N, Entity (Pool));
else
Error_Pragma_Arg
@@ -14145,7 +14143,7 @@
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if (Is_First_Subtype (E)
and then
@@ -14194,7 +14192,7 @@
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- The expression must be analyzed in the special manner
-- described in "Handling of Default and Per-Object
@@ -14420,7 +14418,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if Nkind_In (Unit (Cunit_Node), N_Package_Body,
N_Subprogram_Body)
@@ -14612,7 +14610,7 @@
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Def_Id);
+ Mark_Ghost_Pragma (N, Def_Id);
if Ekind (Def_Id) /= E_Constant then
Note_Possible_Modification
@@ -15032,6 +15030,13 @@
return;
end if;
+ -- Mark the pragma as Ghost if the related subprogram is also
+ -- Ghost. This also ensures that any expansion performed further
+ -- below will produce Ghost nodes.
+
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Defining_Entity (Subp_Decl));
@@ -15042,13 +15047,6 @@
Analyze_If_Present (Pragma_SPARK_Mode);
- -- Mark the pragma as Ghost if the related subprogram is also
- -- Ghost. This also ensures that any expansion performed further
- -- below will produce Ghost nodes.
-
- Spec_Id := Unique_Defining_Entity (Subp_Decl);
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- Examine the formals of the related subprogram
Formal := First_Formal (Spec_Id);
@@ -15123,7 +15121,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
Note_Possible_Modification
(Get_Pragma_Arg (Arg2), Sure => False);
@@ -15211,7 +15209,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- If it's an access-to-subprogram type (in particular, not a
-- subtype), set the flag on that type.
@@ -16112,7 +16110,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Check duplicate before we chain ourselves
@@ -16218,6 +16216,11 @@
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Initial_Condition_In_Decl_Part.
@@ -16236,11 +16239,6 @@
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Abstract_State);
Analyze_If_Present (Pragma_Initializes);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
end Initial_Condition;
------------------------
@@ -16332,6 +16330,12 @@
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Initializes_In_Decl_Part.
@@ -16349,13 +16353,6 @@
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Abstract_State);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
- Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-
Analyze_If_Present (Pragma_Initial_Condition);
end Initializes;
@@ -16903,7 +16900,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The pragma defines a type-specific invariant, the type is said
-- to have invariants of its "own".
@@ -17253,7 +17250,7 @@
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Subprograms
@@ -17277,7 +17274,7 @@
-- Ghost for the purposes of legality checks and
-- removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Capture the entity of the first Ghost subprogram
-- being processed for error detection purposes.
@@ -17685,7 +17682,7 @@
-- Ghost. This also ensures that any expansion performed further
-- below will produce Ghost nodes.
- Mark_Pragma_As_Ghost (N, Entry_Id);
+ Mark_Ghost_Pragma (N, Entry_Id);
-- Analyze the Integer expression
@@ -17866,7 +17863,7 @@
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Capture the entity of the first Ghost procedure being
-- processed for error detection purposes.
@@ -18110,7 +18107,7 @@
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Entity name was given
@@ -18514,7 +18511,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
if not Is_Array_Type (Typ) and then not Is_Record_Type (Typ) then
Error_Pragma ("pragma% must specify array or record type");
@@ -18737,12 +18734,11 @@
end if;
Item_Id := Defining_Entity (Stmt);
- Encap := Get_Pragma_Arg (Arg1);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Item_Id);
+ Mark_Ghost_Pragma (N, Item_Id);
-- Chain the pragma on the contract for further processing by
-- Analyze_Part_Of_In_Decl_Part or for completeness.
@@ -18762,6 +18758,8 @@
-- instantiation.
else
+ Encap := Get_Pragma_Arg (Arg1);
+
-- Detect any discrepancies between the placement of the
-- constant or package instantiation with respect to state
-- space and the encapsulating state.
@@ -18888,7 +18886,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- The pragma may come from an aspect on a private declaration,
-- even if the freeze point at which this is analyzed in the
@@ -18976,13 +18974,12 @@
end if;
Ent := Entity (Get_Pragma_Arg (Arg1));
- Decl := Parent (Ent);
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Check for duplication before inserting in list of
-- representation items.
@@ -18993,6 +18990,8 @@
return;
end if;
+ Decl := Parent (Ent);
+
if Present (Expression (Decl)) then
Error_Pragma_Arg
("object for pragma% cannot have initialization", Arg1);
@@ -19197,7 +19196,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The remaining processing is simply to link the pragma on to
-- the rep item chain, for processing when the type is frozen.
@@ -19249,7 +19248,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The remaining processing is simply to link the pragma on to
-- the rep item chain, for processing when the type is frozen.
@@ -19284,7 +19283,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
Check_Duplicate_Pragma (Ent);
-- This filters out pragmas inside generic parents that show up
@@ -19919,7 +19918,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
if not Debug_Flag_U then
Set_Is_Pure (Ent);
@@ -19958,7 +19957,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Present (E) then
loop
@@ -20303,6 +20302,11 @@
Spec_Id := Corresponding_Spec (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Refined_State_In_Decl_Part.
@@ -20313,11 +20317,6 @@
Analyze_If_Present (Pragma_SPARK_Mode);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- State refinement is allowed only when the corresponding package
-- declaration has non-null pragma Abstract_State. Refinement not
-- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)).
@@ -20401,7 +20400,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Nkind (Parent (E)) = N_Formal_Type_Declaration
and then Ekind (E) = E_General_Access_Type
@@ -20446,7 +20445,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if K = N_Package_Declaration
or else K = N_Generic_Package_Declaration
@@ -20488,7 +20487,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
@@ -20688,7 +20687,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
@@ -20740,7 +20739,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- We require the pragma to apply to a type declared in a package
-- declaration, but not (immediately) within a package body.
@@ -21922,7 +21921,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Nam_Id);
+ Mark_Ghost_Pragma (N, Nam_Id);
Set_Debug_Info_Off (Nam_Id);
end Suppress_Debug_Info;
@@ -21965,7 +21964,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if not Is_Type (E) and then Ekind (E) /= E_Variable then
Error_Pragma_Arg
@@ -22366,16 +22365,16 @@
Subp_Id := Defining_Entity (Subp_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Subp_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Test_Case_In_Decl_Part.
Add_Contract_Item (N, Subp_Id);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Subp_Id);
-
-- Preanalyze the original aspect argument "Name" for ASIS or for
-- a generic subprogram to properly capture global references.
@@ -22449,7 +22448,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Rep_Item_Too_Early (E, N)
or else
@@ -22598,7 +22597,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
if Typ = Any_Type
or else Rep_Item_Too_Early (Typ, N)
@@ -22759,7 +22758,7 @@
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E_Id);
+ Mark_Ghost_Pragma (N, E_Id);
Set_Universal_Aliasing (Implementation_Base_Type (E_Id));
Record_Rep_Item (E_Id, N);
end Universal_Alias;
@@ -22835,7 +22834,7 @@
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost type being
-- processed for error detection purposes.
@@ -23069,6 +23068,11 @@
return;
end if;
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Spec_Id);
@@ -23079,11 +23083,6 @@
Analyze_If_Present (Pragma_SPARK_Mode);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- A volatile function cannot override a non-volatile function
-- (SPARK RM 7.1.2(15)). Overriding checks are usually performed
-- in New_Overloaded_Entity, however at that point the pragma has
@@ -23634,9 +23633,8 @@
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Errors : Nat;
+ Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
@@ -23653,7 +23651,7 @@
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
@@ -23722,9 +23720,9 @@
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
- Ghost_Mode := Save_Ghost_Mode;
-
Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 244352)
+++ sem_ch12.adb (working copy)
@@ -3331,13 +3331,6 @@
Set_Ekind (Id, E_Generic_Package);
Set_Etype (Id, Standard_Void_Type);
- -- A generic package declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
@@ -3548,13 +3541,6 @@
Set_Etype (Id, Standard_Void_Type);
end if;
- -- A generic subprogram declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- For a library unit, we have reconstructed the entity for the unit,
-- and must reset it in the library tables. We also make sure that
-- Body_Required is set properly in the original compilation unit node.
@@ -3676,6 +3662,8 @@
-- Local declarations
+ Mode : Ghost_Mode_Type;
+
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
@@ -3746,6 +3734,13 @@
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A package instantiation is Ghost when it is subject to pragma Ghost
+ -- or the generic template is Ghost. Set the mode now to ensure that
+ -- any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
+
-- Verify that it is the name of a generic package
-- A visibility glitch: if the instance is a child unit and the generic
@@ -4437,6 +4432,8 @@
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Restore_Ghost_Mode (Mode);
+
exception
when Instantiation_Error =>
if Parent_Installed then
@@ -4451,6 +4448,8 @@
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Package_Instantiation;
--------------------------
@@ -5084,6 +5083,8 @@
-- Local variables
+ Mode : Ghost_Mode_Type;
+
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
@@ -5126,6 +5127,13 @@
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A subprogram instantiation is Ghost when it is subject to pragma
+ -- Ghost or the generic template is Ghost. Set the mode now to ensure
+ -- that any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
+
Generate_Reference (Gen_Unit, Gen_Id);
if Nkind (Gen_Id) = N_Identifier
@@ -5137,7 +5145,7 @@
if Etype (Gen_Unit) = Any_Type then
Restore_Env;
- return;
+ goto Leave;
end if;
-- Verify that it is a generic subprogram of the right kind, and that
@@ -5322,8 +5330,8 @@
Error_Msg_NE
("access parameter& is controlling,", N, Formal);
Error_Msg_NE
- ("\corresponding parameter of & must be "
- & "explicitly null-excluding", N, Gen_Id);
+ ("\corresponding parameter of & must be explicitly "
+ & "null-excluding", N, Gen_Id);
end if;
Next_Formal (Formal);
@@ -5386,6 +5394,8 @@
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Restore_Ghost_Mode (Mode);
+
exception
when Instantiation_Error =>
if Parent_Installed then
@@ -5399,6 +5409,8 @@
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Subprogram_Instantiation;
-------------------------
@@ -10780,32 +10792,17 @@
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
+ Act_Spec : constant Node_Id := Specification (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
-
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Spec : constant Node_Id := Specification (Act_Decl);
- Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec);
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
Save_Style_Check : constant Boolean := Style_Check;
- Act_Body : Node_Id;
- Act_Body_Id : Entity_Id;
- Act_Body_Name : Node_Id;
- Gen_Body : Node_Id;
- Gen_Body_Id : Node_Id;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
-
- Parent_Installed : Boolean := False;
-
- Vis_Prims_List : Elist_Id := No_Elist;
- -- List of primitives made temporarily visible in the instantiation
- -- to match the visibility of the formal type
-
procedure Check_Initialized_Types;
-- In a generic package body, an entity of a generic private type may
-- appear uninitialized. This is suspicious, unless the actual is a
@@ -10874,6 +10871,23 @@
end loop;
end Check_Initialized_Types;
+ -- Local variables
+
+ Act_Body : Node_Id;
+ Act_Body_Id : Entity_Id;
+ Act_Body_Name : Node_Id;
+ Gen_Body : Node_Id;
+ Gen_Body_Id : Node_Id;
+ Mode : Ghost_Mode_Type;
+ Par_Ent : Entity_Id := Empty;
+ Par_Vis : Boolean := False;
+
+ Parent_Installed : Boolean := False;
+
+ Vis_Prims_List : Elist_Id := No_Elist;
+ -- List of primitives made temporarily visible in the instantiation
+ -- to match the visibility of the formal type.
+
-- Start of processing for Instantiate_Package_Body
begin
@@ -10886,6 +10900,12 @@
return;
end if;
+ -- The package being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id, Mode);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
@@ -10911,7 +10931,7 @@
if not Unit_Requires_Body (Defining_Entity (Gen_Decl))
and then Body_Optional
then
- return;
+ goto Leave;
else
Load_Parent_Of_Generic
(Inst_Node, Specification (Gen_Decl), Body_Optional);
@@ -11175,6 +11195,9 @@
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Instantiate_Package_Body;
---------------------------------
@@ -11186,13 +11209,12 @@
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Decl_Id : constant Entity_Id :=
- Defining_Unit_Name (Specification (Act_Decl));
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
@@ -11204,6 +11226,7 @@
Act_Body_Id : Entity_Id;
Gen_Body : Node_Id;
Gen_Body_Id : Node_Id;
+ Mode : Ghost_Mode_Type;
Pack_Body : Node_Id;
Par_Ent : Entity_Id := Empty;
Par_Vis : Boolean := False;
@@ -11222,6 +11245,12 @@
return;
end if;
+ -- The subprogram being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id, Mode);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
@@ -11248,7 +11277,7 @@
Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit));
Set_Convention (Act_Decl_Id, Convention (Gen_Unit));
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
-- For other cases, compile the body
@@ -11273,12 +11302,11 @@
if Expander_Active
and then Operating_Mode = Generate_Code
then
- Error_Msg_N
- ("missing proper body for instantiation", Gen_Body);
+ Error_Msg_N ("missing proper body for instantiation", Gen_Body);
end if;
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
end if;
Save_Env (Gen_Unit, Act_Decl_Id);
@@ -11410,27 +11438,25 @@
and then Nkind (Parent (Inst_Node)) /= N_Compilation_Unit
then
if Body_Optional then
- return;
+ goto Leave;
elsif Ekind (Act_Decl_Id) = E_Procedure then
Act_Body :=
Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
- New_Copy_List
- (Parameter_Specifications (Parent (Act_Decl_Id)))),
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
+ Parameter_Specifications =>
+ New_Copy_List
+ (Parameter_Specifications (Parent (Act_Decl_Id)))),
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List (
- Make_Raise_Program_Error (Loc,
- Reason =>
- PE_Access_Before_Elaboration))));
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Make_Raise_Program_Error (Loc,
+ Reason => PE_Access_Before_Elaboration))));
else
Ret_Expr :=
@@ -11444,9 +11470,9 @@
Make_Subprogram_Body (Loc,
Specification =>
Make_Function_Specification (Loc,
- Defining_Unit_Name =>
+ Defining_Unit_Name =>
Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
+ Parameter_Specifications =>
New_Copy_List
(Parameter_Specifications (Parent (Act_Decl_Id))),
Result_Definition =>
@@ -11455,9 +11481,8 @@
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List
- (Make_Simple_Return_Statement (Loc, Ret_Expr))));
+ Statements => New_List (
+ Make_Simple_Return_Statement (Loc, Ret_Expr))));
end if;
Pack_Body :=
@@ -11471,6 +11496,9 @@
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
----------------------
Index: sem.adb
===================================================================
--- sem.adb (revision 244350)
+++ sem.adb (working copy)
@@ -98,7 +98,8 @@
-------------
procedure Analyze (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
begin
Debug_A_Entry ("analyzing ", N);
@@ -115,7 +116,8 @@
-- marked as Ghost.
if Is_Declaration (N) then
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Declaration (N, Mode);
+ Mode_Set := True;
end if;
-- Otherwise processing depends on the node kind
@@ -747,7 +749,9 @@
Expand_SPARK_Potential_Renaming (N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze;
-- Version with check(s) suppressed
@@ -1351,7 +1355,7 @@
-- Set up a clean environment before analyzing
- Ghost_Mode := None;
+ Install_Ghost_Mode (None);
Outer_Generic_Scope := Empty;
Scope_Suppress := Suppress_Options;
Scope_Stack.Table
@@ -1373,7 +1377,7 @@
Pop_Scope;
Restore_Scope_Stack (List);
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Save_Ghost_Mode);
Style_Max_Line_Length := Save_Max_Line;
end Do_Analyze;
Index: freeze.adb
===================================================================
--- freeze.adb (revision 244369)
+++ freeze.adb (working copy)
@@ -2071,9 +2071,6 @@
-- Determine whether an arbitrary entity is subject to Boolean aspect
-- Import and its value is specified as True.
- function New_Freeze_Node return Node_Id;
- -- Create a new freeze node for entity E
-
procedure Wrap_Imported_Subprogram (E : Entity_Id);
-- If E is an entity for an imported subprogram with pre/post-conditions
-- then this procedure will create a wrapper to ensure that proper run-
@@ -2283,14 +2280,12 @@
if Convention (Rec_Type) = Convention_C then
Error_Msg_N
- ("?x?discriminated record has no direct " &
- "equivalent in C",
- A2);
+ ("?x?discriminated record has no direct equivalent in "
+ & "C", A2);
else
Error_Msg_N
- ("?x?discriminated record has no direct " &
- "equivalent in C++",
- A2);
+ ("?x?discriminated record has no direct equivalent in "
+ & "C++", A2);
end if;
Error_Msg_NE
@@ -4703,39 +4698,6 @@
return False;
end Has_Boolean_Aspect_Import;
- ---------------------
- -- New_Freeze_Node --
- ---------------------
-
- function New_Freeze_Node return Node_Id is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
- Result : Node_Id;
-
- begin
- -- Handle the case where an ignored Ghost subprogram freezes the type
- -- of one of its formals. The type can either be non-Ghost or checked
- -- Ghost. Since the freeze node for the type is generated in the
- -- context of the subprogram, the node will be incorrectly flagged as
- -- ignored Ghost and erroneously removed from the tree.
-
- -- type Typ is ...;
- -- procedure Ignored_Ghost_Proc (Formal : Typ) with Ghost;
-
- -- Reset the Ghost mode to "none". This preserves the freeze node.
-
- if Ghost_Mode = Ignore
- and then not Is_Ignored_Ghost_Entity (E)
- and then not Is_Ignored_Ghost_Node (E)
- then
- Ghost_Mode := None;
- end if;
-
- Result := New_Node (N_Freeze_Entity, Loc);
-
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
- end New_Freeze_Node;
-
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
@@ -4927,7 +4889,7 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Freeze_Entity
@@ -4936,7 +4898,7 @@
-- now to ensure that any nodes generated during freezing are properly
-- flagged as Ghost.
- Set_Ghost_Mode_From_Entity (E);
+ Set_Ghost_Mode (E, Mode);
-- We are going to test for various reasons why this entity need not be
-- frozen here, but in the case of an Itype that's defined within a
@@ -4953,15 +4915,13 @@
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
elsif Ekind (E) = E_Generic_Package then
Result := Freeze_Generic_Entities (E);
+ goto Leave;
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
-
-- It is improper to freeze an external entity within a generic because
-- its freeze node will appear in a non-valid context. The entity will
-- be frozen in the proper scope after the current generic is analyzed.
@@ -4974,8 +4934,8 @@
Analyze_Aspects_At_Freeze_Point (E);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
-- the instance, the same applies to the subtype renaming the actual.
@@ -4985,20 +4945,20 @@
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Do not freeze a global entity within an inner scope created during
-- expansion. A call to subprogram E within some internal procedure
@@ -5031,8 +4991,8 @@
then
exit;
else
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
end if;
@@ -5067,8 +5027,8 @@
end loop;
if No (S) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
end;
end if;
@@ -5153,8 +5113,7 @@
if not Is_Internal (E) and then Do_Freeze_Profile then
if not Freeze_Profile (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
end if;
@@ -5336,8 +5295,8 @@
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
-- Check for error of Type_Invariant'Class applied to an untagged
@@ -5607,8 +5566,7 @@
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- The equivalent type associated with a class-wide subtype needs
@@ -5749,8 +5707,7 @@
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of full view present
@@ -5841,8 +5798,7 @@
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of underlying full view present
@@ -5871,8 +5827,7 @@
Check_Debug_Info_Needed (E);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of no full view present. If entity is derived or subtype,
-- it is safe to freeze, correctness depends on the frozen status
@@ -5885,8 +5840,8 @@
else
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
-- For access subprogram, freeze types of all formals, the return
@@ -5933,8 +5888,7 @@
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- Some special processing for non-generic types to complete
@@ -6465,7 +6419,7 @@
Set_Sloc (F_Node, Loc);
else
- F_Node := New_Freeze_Node;
+ F_Node := New_Node (N_Freeze_Entity, Loc);
Set_Freeze_Node (E, F_Node);
Set_Access_Types_To_Process (F_Node, No_Elist);
Set_TSS_Elist (F_Node, No_Elist);
@@ -6547,7 +6501,8 @@
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
return Result;
end Freeze_Entity;
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 244369)
+++ sem_util.adb (working copy)
@@ -12075,32 +12075,37 @@
function Is_Declaration (N : Node_Id) return Boolean is
begin
+ return
+ Is_Declaration_Other_Than_Renaming (N)
+ or else Is_Renaming_Declaration (N);
+ end Is_Declaration;
+
+ ----------------------------------------
+ -- Is_Declaration_Other_Than_Renaming --
+ ----------------------------------------
+
+ function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is
+ begin
case Nkind (N) is
when N_Abstract_Subprogram_Declaration |
N_Exception_Declaration |
- N_Exception_Renaming_Declaration |
+ N_Expression_Function |
N_Full_Type_Declaration |
- N_Generic_Function_Renaming_Declaration |
N_Generic_Package_Declaration |
- N_Generic_Package_Renaming_Declaration |
- N_Generic_Procedure_Renaming_Declaration |
N_Generic_Subprogram_Declaration |
N_Number_Declaration |
N_Object_Declaration |
- N_Object_Renaming_Declaration |
N_Package_Declaration |
- N_Package_Renaming_Declaration |
N_Private_Extension_Declaration |
N_Private_Type_Declaration |
N_Subprogram_Declaration |
- N_Subprogram_Renaming_Declaration |
N_Subtype_Declaration =>
return True;
when others =>
return False;
end case;
- end Is_Declaration;
+ end Is_Declaration_Other_Than_Renaming;
--------------------------------
-- Is_Declared_Within_Variant --
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 244369)
+++ sem_util.ads (working copy)
@@ -1361,6 +1361,9 @@
function Is_Declaration (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a declaration
+ function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a non-renaming declaration
+
function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean;
-- Returns True iff component Comp is declared within a variant part
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 244356)
+++ sem_res.adb (working copy)
@@ -1996,10 +1996,6 @@
return;
end Resolution_Failed;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Resolve
begin
@@ -2007,14 +2003,6 @@
return;
end if;
- -- A declaration may be subject to pragma Ghost. Set the mode now to
- -- ensure that any nodes generated during analysis and expansion are
- -- marked as Ghost.
-
- if Is_Declaration (N) then
- Set_Ghost_Mode (N);
- end if;
-
-- Access attribute on remote subprogram cannot be used for a non-remote
-- access-to-subprogram type.
@@ -2130,7 +2118,6 @@
if Analyzed (N) then
Debug_A_Exit ("resolving ", N, " (done, already analyzed)");
Analyze_Dimension (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Any case of Any_Type as the Etype value means that we had a
@@ -2138,7 +2125,6 @@
elsif Etype (N) = Any_Type then
Debug_A_Exit ("resolving ", N, " (done, Etype = Any_Type)");
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2578,7 +2564,6 @@
then
Resolve (N, Full_View (Typ));
Set_Etype (N, Typ);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Check for an aggregate. Sometimes we can get bogus aggregates
@@ -2687,7 +2672,6 @@
if Address_Integer_Convert_OK (Typ, Etype (N)) then
Rewrite (N, Unchecked_Convert_To (Typ, Relocate_Node (N)));
Analyze_And_Resolve (N, Typ);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Under relaxed RM semantics silently replace occurrences of null
@@ -2725,8 +2709,8 @@
Error_Msg_Node_2 := Typ;
Error_Msg_NE
- ("no visible interpretation of& "
- & "matches expected type&", N, Subp_Name);
+ ("no visible interpretation of& matches expected type&",
+ N, Subp_Name);
end;
if All_Errors_Mode then
@@ -2758,14 +2742,12 @@
end if;
Resolution_Failed;
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Test if we have more than one interpretation for the context
elsif Ambiguous then
Resolution_Failed;
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Only one intepretation
@@ -2838,7 +2820,6 @@
and then Present (Entity (N))
and then Ekind (Entity (N)) /= E_Operator
then
-
if not Is_Predefined_Op (Entity (N)) then
Rewrite_Operator_As_Call (N, Entity (N));
@@ -2853,14 +2834,12 @@
-- Rewrite_Renamed_Operator.
if Analyzed (N) then
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
end if;
case N_Subexpr'(Nkind (N)) is
-
when N_Aggregate => Resolve_Aggregate (N, Ctx_Type);
when N_Allocator => Resolve_Allocator (N, Ctx_Type);
@@ -3003,7 +2982,6 @@
if Nkind (N) not in N_Subexpr then
Debug_A_Exit ("resolving ", N, " (done)");
Expand (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -3038,8 +3016,6 @@
Expand (N);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Resolve;
-------------
Index: expander.adb
===================================================================
--- expander.adb (revision 244350)
+++ expander.adb (working copy)
@@ -41,6 +41,7 @@
with Exp_Ch12; use Exp_Ch12;
with Exp_Ch13; use Exp_Ch13;
with Exp_Prag; use Exp_Prag;
+with Ghost; use Ghost;
with Opt; use Opt;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
@@ -77,6 +78,8 @@
------------
procedure Expand (N : Node_Id) is
+ Mode : Ghost_Mode_Type;
+
begin
-- If we were analyzing a default expression (or other spec expression)
-- the Full_Analysis flag must be off. If we are in expansion mode then
@@ -88,6 +91,11 @@
and then (Full_Analysis or else not Expander_Active)
and then not (Inside_A_Generic and then Expander_Active));
+ -- Establish the Ghost mode of the context to ensure that any generated
+ -- nodes during expansion are marked as Ghost.
+
+ Set_Ghost_Mode (N, Mode);
+
-- The GNATprove_Mode flag indicates that a light expansion for formal
-- verification should be used. This expansion is never done inside
-- generics, because otherwise, this breaks the name resolution
@@ -105,7 +113,7 @@
-- needed, and in general cannot be done correctly, in this mode, so
-- we are all done.
- return;
+ goto Leave;
-- There are three reasons for the Expander_Active flag to be false
@@ -140,7 +148,7 @@
Pop_Scope;
end if;
- return;
+ goto Leave;
else
begin
@@ -482,7 +490,7 @@
exception
when RE_Not_Available =>
- return;
+ goto Leave;
end;
-- Set result as analyzed and then do a possible transient wrap. The
@@ -510,6 +518,9 @@
Debug_A_Exit ("expanding ", N, " (done)");
end if;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Expand;
---------------------------
Index: ghost.adb
===================================================================
--- ghost.adb (revision 244352)
+++ ghost.adb (working copy)
@@ -33,7 +33,6 @@
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
-with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Disp; use Sem_Disp;
@@ -65,20 +64,30 @@
-----------------------
function Ghost_Entity (N : Node_Id) return Entity_Id;
- -- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
- -- a reference to a Ghost entity. Return Empty if there is no such entity.
+ -- Find the entity of a reference to a Ghost entity. Return Empty if there
+ -- is no such entity.
+ procedure Install_Ghost_Mode (Mode : Name_Id);
+ -- Install a specific Ghost mode denoted by Mode by setting global variable
+ -- Ghost_Mode.
+
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
- -- Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
- -- declaration or body N is subject to aspect or pragma Ghost. Use this
- -- routine in cases where [source] pragma Ghost has not been analyzed yet,
- -- but the context needs to establish the "ghostness" of N.
+ -- Determine whether declaration or body N is subject to aspect or pragma
+ -- Ghost. This routine must be used in cases where pragma Ghost has not
+ -- been analyzed yet, but the context needs to establish the "ghostness"
+ -- of N.
+ procedure Mark_Ghost_Declaration_Or_Body
+ (N : Node_Id;
+ Mode : Name_Id);
+ -- Mark the defining entity of declaration or body N as Ghost depending on
+ -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
+ -- body.
+
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
- -- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
- -- Signal all enclosing scopes that they now contain ignored Ghost code.
- -- Add the compilation unit containing N to table Ignored_Ghost_Units for
- -- post processing.
+ -- Signal all enclosing scopes that they now contain at least one ignored
+ -- Ghost node denoted by N. Add the compilation unit containing N to table
+ -- Ignored_Ghost_Units for post processing.
----------------------------
-- Add_Ignored_Ghost_Unit --
@@ -112,34 +121,37 @@
----------------------------
procedure Check_Ghost_Completion
- (Partial_View : Entity_Id;
- Full_View : Entity_Id)
+ (Prev_Id : Entity_Id;
+ Compl_Id : Entity_Id)
is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
+ -- Nothing to do if one of the views is missing
+
+ if No (Prev_Id) or else No (Compl_Id) then
+ null;
+
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(14)).
- if Is_Checked_Ghost_Entity (Partial_View)
+ elsif Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
then
- Error_Msg_Sloc := Sloc (Full_View);
+ Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
- Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
- Error_Msg_N ("\& completed # with ghost policy `Ignore`",
- Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id);
+ Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);
- elsif Is_Ignored_Ghost_Entity (Partial_View)
+ elsif Is_Ignored_Ghost_Entity (Prev_Id)
and then Policy = Name_Check
then
- Error_Msg_Sloc := Sloc (Full_View);
+ Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
- Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
- Error_Msg_N ("\& completed # with ghost policy `Check`",
- Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id);
+ Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
end if;
end Check_Ghost_Completion;
@@ -165,23 +177,31 @@
function Is_OK_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Decl must either
- -- 1) Be subject to pragma Ghost
- -- 2) Rename a Ghost entity
+ --
+ -- * Define a Ghost entity
+ --
+ -- * Be subject to pragma Ghost
function Is_OK_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether node Prag is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Prag must either
- -- 1) Be an assertion expression pragma
- -- 2) Denote pragma Global, Depends, Initializes, Refined_Global,
- -- Refined_Depends or Refined_State
- -- 3) Specify an aspect of a Ghost entity
- -- 4) Contain a reference to a Ghost entity
+ --
+ -- * Be an assertion expression pragma
+ --
+ -- * Denote pragma Global, Depends, Initializes, Refined_Global,
+ -- Refined_Depends or Refined_State.
+ --
+ -- * Specify an aspect of a Ghost entity
+ --
+ -- * Contain a reference to a Ghost entity
function Is_OK_Statement (Stmt : Node_Id) return Boolean;
-- Determine whether node Stmt is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Stmt must either
- -- 1) Denote a call to a Ghost procedure
- -- 2) Denote an assignment statement whose target is Ghost
+ --
+ -- * Denote a procedure call to a Ghost procedure
+ --
+ -- * Denote an assignment statement whose target is Ghost
-----------------------
-- Is_OK_Declaration --
@@ -192,10 +212,6 @@
-- Determine whether node N appears in the profile of a subprogram
-- body.
- function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
- -- Determine whether node Ren_Decl denotes a renaming declaration
- -- with a Ghost name.
-
--------------------------------
-- In_Subprogram_Body_Profile --
--------------------------------
@@ -216,23 +232,6 @@
and then Nkind (Parent (Spec)) = N_Subprogram_Body;
end In_Subprogram_Body_Profile;
- -----------------------
- -- Is_Ghost_Renaming --
- -----------------------
-
- function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
- Nam_Id : Entity_Id;
-
- begin
- if Is_Renaming_Declaration (Ren_Decl) then
- Nam_Id := Ghost_Entity (Name (Ren_Decl));
-
- return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
- end if;
-
- return False;
- end Is_Ghost_Renaming;
-
-- Local variables
Subp_Decl : Node_Id;
@@ -241,21 +240,9 @@
-- Start of processing for Is_OK_Declaration
begin
- if Is_Declaration (Decl) then
+ if Is_Ghost_Declaration (Decl) then
+ return True;
- -- A renaming declaration is Ghost when it renames a Ghost
- -- entity.
-
- if Is_Ghost_Renaming (Decl) then
- return True;
-
- -- The declaration may not have been analyzed yet, determine
- -- whether it is subject to pragma Ghost.
-
- elsif Is_Subject_To_Ghost (Decl) then
- return True;
- end if;
-
-- Special cases
-- A reference to a Ghost entity may appear within the profile of
@@ -303,7 +290,7 @@
-- OK as long as the initial declaration is Ghost.
if Nkind (Subp_Decl) = N_Expression_Function then
- return Is_Subject_To_Ghost (Subp_Decl);
+ return Is_Ghost_Declaration (Subp_Decl);
end if;
end if;
@@ -358,8 +345,6 @@
-- Local variables
- Arg : Node_Id;
- Arg_Id : Entity_Id;
Prag_Id : Pragma_Id;
Prag_Nam : Name_Id;
@@ -399,21 +384,6 @@
Name_Refined_State)
then
return True;
-
- -- Otherwise a normal pragma is Ghost when it encloses a Ghost
- -- name (SPARK RM 6.9(3)).
-
- else
- Arg := First (Pragma_Argument_Associations (Prag));
- while Present (Arg) loop
- Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
-
- if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
- return True;
- end if;
-
- Next (Arg);
- end loop;
end if;
end if;
@@ -425,19 +395,18 @@
---------------------
function Is_OK_Statement (Stmt : Node_Id) return Boolean is
- Nam_Id : Entity_Id;
-
begin
- -- An assignment statement or a procedure call is Ghost when the
- -- name denotes a Ghost entity.
+ -- An assignment statement is Ghost when the target is a Ghost
+ -- entity.
- if Nkind_In (Stmt, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- Nam_Id := Ghost_Entity (Name (Stmt));
+ if Nkind (Stmt) = N_Assignment_Statement then
+ return Is_Ghost_Assignment (Stmt);
- return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
+ -- A procedure call is Ghost when it calls a Ghost procedure
+ elsif Nkind (Stmt) = N_Procedure_Call_Statement then
+ return Is_Ghost_Procedure_Call (Stmt);
+
-- Special cases
-- An if statement is a suitable context for a Ghost entity if it
@@ -829,7 +798,7 @@
Ref : Node_Id;
begin
- -- When the reference extracts a subcomponent, recover the related
+ -- When the reference denotes a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
Ref := N;
@@ -881,7 +850,97 @@
Ignored_Ghost_Units.Init;
end Initialize;
+ ------------------------
+ -- Install_Ghost_Mode --
+ ------------------------
+
+ procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
+ begin
+ Ghost_Mode := Mode;
+ end Install_Ghost_Mode;
+
+ procedure Install_Ghost_Mode (Mode : Name_Id) is
+ begin
+ if Mode = Name_Check then
+ Ghost_Mode := Check;
+
+ elsif Mode = Name_Ignore then
+ Ghost_Mode := Ignore;
+
+ elsif Mode = Name_None then
+ Ghost_Mode := None;
+ end if;
+ end Install_Ghost_Mode;
+
-------------------------
+ -- Is_Ghost_Assignment --
+ -------------------------
+
+ function Is_Ghost_Assignment (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- An assignment statement is Ghost when its target denotes a Ghost
+ -- entity.
+
+ if Nkind (N) = N_Assignment_Statement then
+ Id := Ghost_Entity (Name (N));
+
+ return Present (Id) and then Is_Ghost_Entity (Id);
+ end if;
+
+ return False;
+ end Is_Ghost_Assignment;
+
+ --------------------------
+ -- Is_Ghost_Declaration --
+ --------------------------
+
+ function Is_Ghost_Declaration (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- A declaration is Ghost when it elaborates a Ghost entity or is
+ -- subject to pragma Ghost.
+
+ if Is_Declaration (N) then
+ Id := Defining_Entity (N);
+
+ return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N);
+ end if;
+
+ return False;
+ end Is_Ghost_Declaration;
+
+ ---------------------
+ -- Is_Ghost_Pragma --
+ ---------------------
+
+ function Is_Ghost_Pragma (N : Node_Id) return Boolean is
+ begin
+ return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N);
+ end Is_Ghost_Pragma;
+
+ -----------------------------
+ -- Is_Ghost_Procedure_Call --
+ -----------------------------
+
+ function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- A procedure call is Ghost when it invokes a Ghost procedure
+
+ if Nkind (N) = N_Procedure_Call_Statement then
+ Id := Ghost_Entity (Name (N));
+
+ return Present (Id) and then Is_Ghost_Entity (Id);
+ end if;
+
+ return False;
+ end Is_Ghost_Procedure_Call;
+
+ -------------------------
-- Is_Subject_To_Ghost --
-------------------------
@@ -1021,67 +1080,400 @@
Ignored_Ghost_Units.Release;
end Lock;
+ -----------------------------------
+ -- Mark_And_Set_Ghost_Assignment --
+ -----------------------------------
+
+ procedure Mark_And_Set_Ghost_Assignment
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Id : Entity_Id;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- An assignment statement becomes Ghost when its target denotes a Ghost
+ -- object. Install the Ghost mode of the target.
+
+ Id := Ghost_Entity (Name (N));
+
+ if Present (Id) then
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end if;
+ end Mark_And_Set_Ghost_Assignment;
+
-----------------------------
- -- Mark_Full_View_As_Ghost --
+ -- Mark_And_Set_Ghost_Body --
-----------------------------
- procedure Mark_Full_View_As_Ghost
- (Priv_Typ : Entity_Id;
- Full_Typ : Entity_Id)
+ procedure Mark_And_Set_Ghost_Body
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
is
- Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+ Policy : Name_Id := No_Name;
begin
- if Is_Checked_Ghost_Entity (Priv_Typ) then
- Set_Is_Checked_Ghost_Entity (Full_Typ);
+ -- Save the previous Ghost mode in effect
- elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
- Set_Is_Ignored_Ghost_Entity (Full_Typ);
- Set_Is_Ignored_Ghost_Node (Full_Decl);
- Propagate_Ignored_Ghost_Code (Full_Decl);
+ Mode := Ghost_Mode;
+
+ -- A body becomes Ghost when it is subject to aspect or pragma Ghost
+
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- A body declared within a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- Inherit the "ghostness" of the previous declaration when the body
+ -- acts as a completion.
+
+ elsif Present (Spec_Id) then
+ if Is_Checked_Ghost_Entity (Spec_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Spec_Id) then
+ Policy := Name_Ignore;
+ end if;
end if;
- end Mark_Full_View_As_Ghost;
- --------------------------
- -- Mark_Pragma_As_Ghost --
- --------------------------
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
- procedure Mark_Pragma_As_Ghost
- (Prag : Node_Id;
- Context_Id : Entity_Id)
+ Check_Ghost_Completion
+ (Prev_Id => Spec_Id,
+ Compl_Id => Body_Id);
+
+ -- Mark the body as its formals as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Body;
+
+ -----------------------------------
+ -- Mark_And_Set_Ghost_Completion --
+ -----------------------------------
+
+ procedure Mark_And_Set_Ghost_Completion
+ (N : Node_Id;
+ Prev_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
is
+ Compl_Id : constant Entity_Id := Defining_Entity (N);
+ Policy : Name_Id := No_Name;
+
begin
- if Is_Checked_Ghost_Entity (Context_Id) then
- Set_Is_Ghost_Pragma (Prag);
+ -- Save the previous Ghost mode in effect
- elsif Is_Ignored_Ghost_Entity (Context_Id) then
- Set_Is_Ghost_Pragma (Prag);
- Set_Is_Ignored_Ghost_Node (Prag);
- Propagate_Ignored_Ghost_Code (Prag);
+ Mode := Ghost_Mode;
+
+ -- A completion elaborated in a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- The completion becomes Ghost when its initial declaration is also
+ -- Ghost.
+
+ elsif Is_Checked_Ghost_Entity (Prev_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Prev_Id) then
+ Policy := Name_Ignore;
end if;
- end Mark_Pragma_As_Ghost;
- ----------------------------
- -- Mark_Renaming_As_Ghost --
- ----------------------------
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
- procedure Mark_Renaming_As_Ghost
- (Ren_Decl : Node_Id;
- Nam_Id : Entity_Id)
+ Check_Ghost_Completion
+ (Prev_Id => Prev_Id,
+ Compl_Id => Compl_Id);
+
+ -- Mark the completion as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Completion;
+
+ ------------------------------------
+ -- Mark_And_Set_Ghost_Declaration --
+ ------------------------------------
+
+ procedure Mark_And_Set_Ghost_Declaration
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
is
- Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
+ Par_Id : Entity_Id;
+ Policy : Name_Id := No_Name;
begin
- if Is_Checked_Ghost_Entity (Nam_Id) then
- Set_Is_Checked_Ghost_Entity (Ren_Id);
+ -- Save the previous Ghost mode in effect
- elsif Is_Ignored_Ghost_Entity (Nam_Id) then
- Set_Is_Ignored_Ghost_Entity (Ren_Id);
- Set_Is_Ignored_Ghost_Node (Ren_Decl);
- Propagate_Ignored_Ghost_Code (Ren_Decl);
+ Mode := Ghost_Mode;
+
+ -- A declaration becomes Ghost when it is subject to aspect or pragma
+ -- Ghost.
+
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- A declaration elaborated in a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- A child package or subprogram declaration becomes Ghost when its
+ -- parent is Ghost (SPARK RM 6.9(2)).
+
+ elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration,
+ N_Generic_Package_Declaration,
+ N_Generic_Package_Renaming_Declaration,
+ N_Generic_Procedure_Renaming_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Package_Declaration,
+ N_Package_Renaming_Declaration,
+ N_Subprogram_Declaration,
+ N_Subprogram_Renaming_Declaration)
+ and then Present (Parent_Spec (N))
+ then
+ Par_Id := Defining_Entity (Unit (Parent_Spec (N)));
+
+ if Is_Checked_Ghost_Entity (Par_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Par_Id) then
+ Policy := Name_Ignore;
+ end if;
end if;
- end Mark_Renaming_As_Ghost;
+ -- Mark the declaration and its formals as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Declaration;
+
+ --------------------------------------
+ -- Mark_And_Set_Ghost_Instantiation --
+ --------------------------------------
+
+ procedure Mark_And_Set_Ghost_Instantiation
+ (N : Node_Id;
+ Gen_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Policy : Name_Id := No_Name;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- An instantiation becomes Ghost when it is subject to pragma Ghost
+
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- An instantiation declaration within a Ghost region is automatically
+ -- Ghost (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- Inherit the "ghostness" of the generic unit
+
+ elsif Is_Checked_Ghost_Entity (Gen_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Gen_Id) then
+ Policy := Name_Ignore;
+ end if;
+
+ -- Mark the instantiation as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Instantiation;
+
+ ---------------------------------------
+ -- Mark_And_Set_Ghost_Procedure_Call --
+ ---------------------------------------
+
+ procedure Mark_And_Set_Ghost_Procedure_Call
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Id : Entity_Id;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- A procedure call becomes Ghost when the procedure being invoked is
+ -- Ghost. Install the Ghost mode of the procedure.
+
+ Id := Ghost_Entity (Name (N));
+
+ if Present (Id) then
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end if;
+ end Mark_And_Set_Ghost_Procedure_Call;
+
+ ------------------------------------
+ -- Mark_Ghost_Declaration_Or_Body --
+ ------------------------------------
+
+ procedure Mark_Ghost_Declaration_Or_Body
+ (N : Node_Id;
+ Mode : Name_Id)
+ is
+ Id : constant Entity_Id := Defining_Entity (N);
+
+ Mark_Formals : Boolean := False;
+ Param : Node_Id;
+ Param_Id : Entity_Id;
+
+ begin
+ -- Mark the related node and its entity
+
+ if Mode = Name_Check then
+ Mark_Formals := True;
+ Set_Is_Checked_Ghost_Entity (Id);
+
+ elsif Mode = Name_Ignore then
+ Mark_Formals := True;
+ Set_Is_Ignored_Ghost_Entity (Id);
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+
+ -- Mark all formal parameters when the related node denotes a subprogram
+ -- or a body. The traversal is performed via the specification because
+ -- the related subprogram or body may be unanalyzed.
+
+ -- ??? could extra formal parameters cause a Ghost leak?
+
+ if Mark_Formals
+ and then Nkind_In (N, N_Abstract_Subprogram_Declaration,
+ N_Formal_Abstract_Subprogram_Declaration,
+ N_Formal_Concrete_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub,
+ N_Subprogram_Declaration,
+ N_Subprogram_Renaming_Declaration)
+ then
+ Param := First (Parameter_Specifications (Specification (N)));
+ while Present (Param) loop
+ Param_Id := Defining_Entity (Param);
+
+ if Mode = Name_Check then
+ Set_Is_Checked_Ghost_Entity (Param_Id);
+
+ elsif Mode = Name_Ignore then
+ Set_Is_Ignored_Ghost_Entity (Param_Id);
+ end if;
+
+ Next (Param);
+ end loop;
+ end if;
+ end Mark_Ghost_Declaration_Or_Body;
+
+ -----------------------
+ -- Mark_Ghost_Pragma --
+ -----------------------
+
+ procedure Mark_Ghost_Pragma
+ (N : Node_Id;
+ Id : Entity_Id)
+ is
+ begin
+ -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
+ -- a Ghost entity.
+
+ if Is_Checked_Ghost_Entity (Id) then
+ Set_Is_Checked_Ghost_Pragma (N);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Set_Is_Ignored_Ghost_Pragma (N);
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end Mark_Ghost_Pragma;
+
+ -------------------------
+ -- Mark_Ghost_Renaming --
+ -------------------------
+
+ procedure Mark_Ghost_Renaming
+ (N : Node_Id;
+ Id : Entity_Id)
+ is
+ Policy : Name_Id := No_Name;
+
+ begin
+ -- A renaming becomes Ghost when it renames a Ghost entity
+
+ if Is_Checked_Ghost_Entity (Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Policy := Name_Ignore;
+ end if;
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+ end Mark_Ghost_Renaming;
+
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
@@ -1091,7 +1483,7 @@
Scop : Entity_Id;
begin
- -- Traverse the parent chain looking for blocks, packages and
+ -- Traverse the parent chain looking for blocks, packages, and
-- subprograms or their respective bodies.
Nod := Parent (N);
@@ -1187,17 +1579,6 @@
Prune (N);
return Skip;
- -- A freeze node for an ignored ghost entity must be pruned as
- -- well, to prevent meaningless references in the back end.
-
- -- ??? the freeze node itself should be ignored ghost
-
- elsif Nkind (N) = N_Freeze_Entity
- and then Is_Ignored_Ghost_Entity (Entity (N))
- then
- Prune (N);
- return Skip;
-
-- Scoping constructs such as blocks, packages, subprograms and
-- bodies offer some flexibility with respect to pruning.
@@ -1249,135 +1630,103 @@
end loop;
end Remove_Ignored_Ghost_Code;
+ ------------------------
+ -- Restore_Ghost_Mode --
+ ------------------------
+
+ procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is
+ begin
+ Ghost_Mode := Mode;
+ end Restore_Ghost_Mode;
+
--------------------
-- Set_Ghost_Mode --
--------------------
- procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
- procedure Set_From_Entity (Ent_Id : Entity_Id);
- -- Set the value of global variable Ghost_Mode depending on the mode of
- -- entity Ent_Id.
+ procedure Set_Ghost_Mode
+ (N : Node_Or_Entity_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+ -- Install the Ghost mode of entity Id
- procedure Set_From_Policy;
- -- Set the value of global variable Ghost_Mode depending on the current
- -- Ghost policy in effect.
+ --------------------------------
+ -- Set_Ghost_Mode_From_Entity --
+ --------------------------------
- ---------------------
- -- Set_From_Entity --
- ---------------------
-
- procedure Set_From_Entity (Ent_Id : Entity_Id) is
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
begin
- Set_Ghost_Mode_From_Entity (Ent_Id);
-
- if Is_Ignored_Ghost_Entity (Ent_Id) then
- Set_Is_Ignored_Ghost_Node (N);
- Propagate_Ignored_Ghost_Code (N);
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+ else
+ Install_Ghost_Mode (None);
end if;
- end Set_From_Entity;
+ end Set_Ghost_Mode_From_Entity;
- ---------------------
- -- Set_From_Policy --
- ---------------------
-
- procedure Set_From_Policy is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
-
- begin
- if Policy = Name_Check then
- Ghost_Mode := Check;
-
- elsif Policy = Name_Ignore then
- Ghost_Mode := Ignore;
-
- Set_Is_Ignored_Ghost_Node (N);
- Propagate_Ignored_Ghost_Code (N);
- end if;
- end Set_From_Policy;
-
-- Local variables
- Nam_Id : Entity_Id;
+ Id : Entity_Id;
-- Start of processing for Set_Ghost_Mode
begin
- -- The input node denotes one of the many declaration kinds that may be
- -- subject to pragma Ghost.
+ -- Save the previous Ghost mode in effect
- if Is_Declaration (N) then
- if Is_Subject_To_Ghost (N) then
- Set_From_Policy;
+ Mode := Ghost_Mode;
- -- The declaration denotes the completion of a deferred constant,
- -- pragma Ghost appears on the partial declaration.
+ -- The Ghost mode of an assignment statement depends on the Ghost mode
+ -- of the target.
- elsif Nkind (N) = N_Object_Declaration
- and then Constant_Present (N)
- and then Present (Id)
- then
- Set_From_Entity (Id);
+ if Nkind (N) = N_Assignment_Statement then
+ Id := Ghost_Entity (Name (N));
- -- The declaration denotes the full view of a private type, pragma
- -- Ghost appears on the partial declaration.
-
- elsif Nkind (N) = N_Full_Type_Declaration
- and then Is_Private_Type (Defining_Entity (N))
- and then Present (Id)
- then
- Set_From_Entity (Id);
+ if Present (Id) then
+ Set_Ghost_Mode_From_Entity (Id);
end if;
- -- The input denotes an assignment or a procedure call. In this case
- -- the Ghost mode is dictated by the name of the construct.
+ -- The Ghost mode of a body or a declaration depends on the Ghost mode
+ -- of its defining entity.
- elsif Nkind_In (N, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- Nam_Id := Ghost_Entity (Name (N));
+ elsif Is_Body (N) or else Is_Declaration (N) then
+ Set_Ghost_Mode_From_Entity (Defining_Entity (N));
- if Present (Nam_Id) then
- Set_From_Entity (Nam_Id);
- end if;
+ -- The Ghost mode of an entity depends on the entity itself
- -- The input denotes a package or subprogram body
+ elsif Nkind (N) in N_Entity then
+ Set_Ghost_Mode_From_Entity (N);
- elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
- if (Present (Id) and then Is_Ghost_Entity (Id))
- or else Is_Subject_To_Ghost (N)
- then
- Set_From_Policy;
- end if;
+ -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
+ -- of the entity being frozen.
- -- The input denotes a pragma
+ elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then
+ Set_Ghost_Mode_From_Entity (Entity (N));
- elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
- if Is_Ignored_Ghost_Node (N) then
- Ghost_Mode := Ignore;
+ -- The Ghost mode of a pragma depends on the associated entity. The
+ -- property is encoded in the pragma itself.
+
+ elsif Nkind (N) = N_Pragma then
+ if Is_Checked_Ghost_Pragma (N) then
+ Install_Ghost_Mode (Check);
+ elsif Is_Ignored_Ghost_Pragma (N) then
+ Install_Ghost_Mode (Ignore);
else
- Ghost_Mode := Check;
+ Install_Ghost_Mode (None);
end if;
- -- The input denotes a freeze node
+ -- The Ghost mode of a procedure call depends on the Ghost mode of the
+ -- procedure being invoked.
- elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
- Set_From_Entity (Id);
+ elsif Nkind (N) = N_Procedure_Call_Statement then
+ Id := Ghost_Entity (Name (N));
+
+ if Present (Id) then
+ Set_Ghost_Mode_From_Entity (Id);
+ end if;
end if;
end Set_Ghost_Mode;
- --------------------------------
- -- Set_Ghost_Mode_From_Entity --
- --------------------------------
-
- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
- begin
- if Is_Checked_Ghost_Entity (Id) then
- Ghost_Mode := Check;
- elsif Is_Ignored_Ghost_Entity (Id) then
- Ghost_Mode := Ignore;
- end if;
- end Set_Ghost_Mode_From_Entity;
-
-------------------------
-- Set_Is_Ghost_Entity --
-------------------------
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 244356)
+++ exp_ch6.adb (working copy)
@@ -44,7 +44,6 @@
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
-with Ghost; use Ghost;
with Inline; use Inline;
with Lib; use Lib;
with Namet; use Namet;
@@ -5188,17 +5187,8 @@
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The procedure call is Ghost when the name is Ghost. Set the mode now
- -- to ensure that any nodes generated during expansion are properly set
- -- as Ghost.
-
- Set_Ghost_Mode (N);
-
Expand_Call (N);
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Procedure_Call_Statement;
--------------------------------------
@@ -5358,8 +5348,6 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Except_H : Node_Id;
L : List_Id;
Spec_Id : Entity_Id;
@@ -5390,13 +5378,6 @@
end if;
end if;
- -- The subprogram body is Ghost when it is stand alone and subject to
- -- pragma Ghost or the corresponding spec is Ghost. To accomodate both
- -- cases, set the mode now to ensure that any nodes generated during
- -- expansion are marked as Ghost.
-
- Set_Ghost_Mode (N, Spec_Id);
-
-- Set L to either the list of declarations if present, or to the list
-- of statements if no declarations are present. This is used to insert
-- new stuff at the start.
@@ -5518,7 +5499,6 @@
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
@@ -5543,7 +5523,7 @@
begin
if not Acts_As_Spec (N)
and then Nkind (Parent (Parent (Spec_Id))) /=
- N_Subprogram_Body_Stub
+ N_Subprogram_Body_Stub
then
null;
@@ -5631,8 +5611,6 @@
-- Set to encode entity names in package body before gigi is called
Qualify_Entity_Names (N);
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Body;
-----------------------------------
Index: ghost.ads
===================================================================
--- ghost.ads (revision 244350)
+++ ghost.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2014-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- --
@@ -26,6 +26,7 @@
-- This package contains routines that deal with the static and runtime
-- semantics of Ghost entities.
+with Opt; use Opt;
with Types; use Types;
package Ghost is
@@ -35,13 +36,15 @@
-- post processing.
procedure Check_Ghost_Completion
- (Partial_View : Entity_Id;
- Full_View : Entity_Id);
- -- Verify that the Ghost policy of a full view or a completion is the same
- -- as the Ghost policy of the partial view. Emit an error if this is not
- -- the case.
+ (Prev_Id : Entity_Id;
+ Compl_Id : Entity_Id);
+ -- Verify that the Ghost policy of initial entity Prev_Id is compatible
+ -- with the Ghost policy of completing entity Compl_Id. Emit an error if
+ -- this is not the case.
- procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
+ procedure Check_Ghost_Context
+ (Ghost_Id : Entity_Id;
+ Ghost_Ref : Node_Id);
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
@@ -71,71 +74,150 @@
procedure Initialize;
-- Initialize internal tables
+ procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
+ -- Set the value of global variable Ghost_Mode depending on the Ghost
+ -- policy denoted by Mode.
+
+ function Is_Ghost_Assignment (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes an assignment statement whose
+ -- target is a Ghost entity.
+
+ function Is_Ghost_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a declaration which defines
+ -- a Ghost entity.
+
+ function Is_Ghost_Pragma (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a pragma which encloses a
+ -- Ghost entity or is associated with a Ghost entity.
+
+ function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a procedure call invoking a
+ -- Ghost procedure.
+
procedure Lock;
-- Lock internal tables before calling backend
- procedure Mark_Full_View_As_Ghost
- (Priv_Typ : Entity_Id;
- Full_Typ : Entity_Id);
- -- Set all Ghost-related attributes of type Full_Typ depending on the Ghost
- -- mode of incomplete or private type Priv_Typ.
+ procedure Mark_And_Set_Ghost_Assignment
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark assignment statement N as Ghost when:
+ --
+ -- * The left hand side denotes a Ghost entity
+ --
+ -- Install the Ghost mode of the assignment statement. Mode is the Ghost
+ -- mode in effect prior to processing the assignment. This routine starts
+ -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
- procedure Mark_Pragma_As_Ghost
- (Prag : Node_Id;
- Context_Id : Entity_Id);
- -- Set all Ghost-related attributes of pragma Prag if its context denoted
- -- by Id is a Ghost entity.
+ procedure Mark_And_Set_Ghost_Body
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark package or subprogram body N as Ghost when:
+ --
+ -- * The body is subject to pragma Ghost
+ --
+ -- * The body completes a previous declaration whose spec denoted by
+ -- Spec_Id is a Ghost entity.
+ --
+ -- * The body appears within a Ghost region
+ --
+ -- Install the Ghost mode of the body. Mode is the Ghost mode prior to
+ -- processing the body. This routine starts a Ghost region and must be
+ -- used in conjunction with Restore_Ghost_Mode.
- procedure Mark_Renaming_As_Ghost
- (Ren_Decl : Node_Id;
- Nam_Id : Entity_Id);
- -- Set all Ghost-related attributes of renaming declaration Ren_Decl if its
- -- renamed name denoted by Nam_Id is a Ghost entity.
+ procedure Mark_And_Set_Ghost_Completion
+ (N : Node_Id;
+ Prev_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark completion N of a deferred constant or private type [extension]
+ -- Ghost when:
+ --
+ -- * The entity of the previous declaration denoted by Prev_Id is Ghost
+ --
+ -- * The completion appears within a Ghost region
+ --
+ -- Install the Ghost mode of the completion. Mode is the Ghost mode prior
+ -- to processing the completion. This routine starts a Ghost region and
+ -- must be used in conjunction with Restore_Ghost_Mode.
- procedure Remove_Ignored_Ghost_Code;
- -- Remove all code marked as ignored Ghost from the trees of all qualifying
- -- units (SPARK RM 6.9(4)).
+ procedure Mark_And_Set_Ghost_Declaration
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark declaration N as Ghost when:
--
- -- WARNING: this is a separate front end pass, care should be taken to keep
- -- it optimized.
+ -- * The declaration is subject to pragma Ghost
+ --
+ -- * The declaration denotes a child package or subprogram and the parent
+ -- is a Ghost unit.
+ --
+ -- * The declaration appears within a Ghost region
+ --
+ -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior
+ -- to processing the declaration. This routine starts a Ghost region and
+ -- must be used in conjunction with Restore_Ghost_Mode.
- procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
- -- Set the value of global variable Ghost_Mode depending on the following
- -- scenarios:
+ procedure Mark_And_Set_Ghost_Instantiation
+ (N : Node_Id;
+ Gen_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark instantiation N as Ghost when:
--
- -- If N is a declaration, determine whether N is subject to pragma Ghost.
- -- If this is the case, the Ghost_Mode is set based on the current Ghost
- -- policy in effect. Special cases:
+ -- * The instantiation is subject to pragma Ghost
--
- -- N is the completion of a deferred constant, the Ghost_Mode is set
- -- based on the mode of partial declaration entity denoted by Id.
+ -- * The generic template denoted by Gen_Id is Ghost
--
- -- N is the full view of a private type, the Ghost_Mode is set based
- -- on the mode of the partial declaration entity denoted by Id.
+ -- * The instantiation appears within a Ghost region
--
- -- If N is an assignment statement or a procedure call, the Ghost_Mode is
- -- set based on the mode of the name.
+ -- Install the Ghost mode of the instantiation. Mode is the Ghost mode
+ -- prior to processing the instantiation. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Procedure_Call
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark procedure call N as Ghost when:
--
- -- If N denotes a package or a subprogram body, the Ghost_Mode is set to
- -- the current Ghost policy in effect if the body is subject to Ghost or
- -- the corresponding spec denoted by Id is a Ghost entity.
+ -- * The procedure being invoked is a Ghost entity
--
- -- If N is a pragma, the Ghost_Mode is set based on the mode of the
- -- pragma.
+ -- Install the Ghost mode of the procedure call. Mode is the Ghost mode
+ -- prior to processing the procedure call. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_Ghost_Pragma
+ (N : Node_Id;
+ Id : Entity_Id);
+ -- Mark pragma N as Ghost when:
--
- -- If N is a freeze node, the Global_Mode is set based on the mode of
- -- entity Id.
+ -- * The pragma encloses Ghost entity Id
--
- -- WARNING: the caller must save and restore the value of Ghost_Mode in a
- -- a stack-like fasion as this routine may override the existing value.
+ -- * The pragma is associated with Ghost entity Id
- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
- -- Set the valye of global variable Ghost_Mode depending on the mode of
- -- entity Id.
+ procedure Mark_Ghost_Renaming
+ (N : Node_Id;
+ Id : Entity_Id);
+ -- Mark renaming declaration N as Ghost when:
--
- -- WARNING: the caller must save and restore the value of Ghost_Mode in a
- -- a stack-like fasion as this routine may override the existing value.
+ -- * Renamed entity Id denotes a Ghost entity
+ procedure Remove_Ignored_Ghost_Code;
+ -- Remove all code marked as ignored Ghost from the trees of all qualifying
+ -- units (SPARK RM 6.9(4)).
+ --
+ -- WARNING: this is a separate front end pass, care should be taken to keep
+ -- it optimized.
+
+ procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
+ -- Terminate a Ghost region by restoring the Ghost mode prior to the
+ -- region denoted by Mode. This routine must be used in conjunction
+ -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
+
+ procedure Set_Ghost_Mode
+ (N : Node_Or_Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior
+ -- to processing the node. This routine starts a Ghost region and must be
+ -- used in conjunction with Restore_Ghost_Mode.
+
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current
-- Ghost assertion policy in effect.
Index: exp_ch13.adb
===================================================================
--- exp_ch13.adb (revision 244350)
+++ exp_ch13.adb (working copy)
@@ -32,7 +32,6 @@
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;
@@ -345,10 +344,8 @@
Insert_Action (N,
Make_Object_Declaration (Loc,
Defining_Identifier => Temp_Id,
- Object_Definition =>
- New_Occurrence_Of (Expr_Typ, Loc),
- Expression =>
- Relocate_Node (Expr)));
+ Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
+ Expression => Relocate_Node (Expr)));
New_Expr := New_Occurrence_Of (Temp_Id, Loc);
Set_Etype (New_Expr, Expr_Typ);
@@ -371,8 +368,6 @@
procedure Expand_N_Freeze_Entity (N : Node_Id) is
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;
@@ -380,10 +375,6 @@
In_Outer_Scope : Boolean;
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),
@@ -451,14 +442,12 @@
-- 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;
@@ -470,7 +459,6 @@
if No (E_Scope) then
Check_Error_Detected;
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -688,7 +676,6 @@
-- 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;
-------------------------------------------
Index: exp_ch8.adb
===================================================================
--- exp_ch8.adb (revision 244350)
+++ exp_ch8.adb (working copy)
@@ -30,7 +30,6 @@
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
-with Ghost; use Ghost;
with Namet; use Namet;
with Nmake; use Nmake;
with Nlists; use Nlists;
@@ -50,25 +49,14 @@
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Decl : Node_Id;
begin
- -- The exception renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
@@ -161,20 +149,9 @@
end if;
end Evaluation_Required;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_N_Object_Renaming_Declaration
begin
- -- The object renaming declaration is Ghost when it is subject to pragma
- -- Ghost or renames a Ghost entity. To accomodate both cases, set the
- -- mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
-- Perform name evaluation if required
if Evaluation_Required (Nam) then
@@ -217,8 +194,6 @@
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
@@ -226,18 +201,9 @@
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Decl : Node_Id;
begin
- -- The package renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases,
- -- set the mode now to ensure that any nodes generated during expansion
- -- are properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
@@ -276,8 +242,6 @@
Insert_Action (N, Decl);
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
@@ -327,19 +291,11 @@
-- Local variables
- Nam : constant Node_Id := Name (N);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Nam : constant Node_Id := Name (N);
-- Start of processing for Expand_N_Subprogram_Renaming_Declaration
begin
- -- The subprogram renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
- -- the mode now to ensure that any nodes created during expansion are
- -- properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- When the prefix of the name is a function call, we must force the
-- call to be made by removing side effects from the call, since we
-- must only call the function once.
@@ -403,8 +359,6 @@
end if;
end;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 244369)
+++ sem_ch6.adb (working copy)
@@ -233,13 +233,6 @@
Set_Categorization_From_Scope (Subp_Id, Scop);
- -- An abstract subprogram declared within a Ghost region is rendered
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Subp_Id);
- end if;
-
if Ekind (Scope (Subp_Id)) = E_Protected_Type then
Error_Msg_N ("abstract subprogram not allowed in protected type", N);
@@ -502,15 +495,6 @@
Set_Is_Inlined (Defining_Entity (N));
- -- If the expression function is Ghost, mark its body entity as
- -- Ghost too. This avoids spurious errors on unanalyzed body entities
- -- of expression functions, which are not yet marked as ghost, yet
- -- identified as the Corresponding_Body of the ghost declaration.
-
- if Is_Ghost_Entity (Def_Id) then
- Set_Is_Ghost_Entity (Defining_Entity (New_Body));
- end if;
-
-- Establish the linkages between the spec and the body. These are
-- used when the expression function acts as the prefix of attribute
-- 'Access in order to freeze the original expression which has been
@@ -1264,19 +1248,6 @@
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Scope (Body_Id, Scope (Gen_Id));
- -- Inherit the "ghostness" of the generic spec. Note that this
- -- property is not directly inherited as the body may be subject
- -- to a different Ghost assertion policy.
-
- 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
- -- the point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Gen_Id, Body_Id);
- end if;
-
Check_Fully_Conformant (Body_Id, Gen_Id, Body_Id);
if Nkind (N) = N_Subprogram_Body_Stub then
@@ -1559,10 +1530,9 @@
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
Actual : Node_Id;
+ Mode : Ghost_Mode_Type;
New_N : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Analyze_Procedure_Call
begin
@@ -1604,7 +1574,7 @@
-- Set the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Procedure_Call (N, Mode);
-- Otherwise analyze the parameters
@@ -1628,7 +1598,7 @@
if Present (Actuals) then
Error_Msg_N
("no parameters allowed for this call", First (Actuals));
- return;
+ goto Leave;
end if;
Set_Etype (N, Standard_Void_Type);
@@ -1638,8 +1608,7 @@
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
elsif Is_Entity_Name (P)
and then Ekind (Entity (P)) /= E_Entry_Family
@@ -1775,7 +1744,8 @@
Error_Msg_N ("invalid procedure or entry call", N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Analyze_Procedure_Call;
------------------------------
@@ -1783,10 +1753,9 @@
------------------------------
procedure Analyze_Return_Statement (N : Node_Id) is
+ pragma Assert (Nkind_In (N, N_Extended_Return_Statement,
+ N_Simple_Return_Statement));
- pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
- N_Extended_Return_Statement));
-
Returns_Object : constant Boolean :=
Nkind (N) = N_Extended_Return_Statement
or else
@@ -2489,13 +2458,8 @@
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
-- Ensure that the generated corresponding spec and original body
- -- share the same Ghost and SPARK_Mode attributes.
+ -- share the same SPARK_Mode attributes.
- Set_Is_Checked_Ghost_Entity
- (Body_Id, Is_Checked_Ghost_Entity (Spec_Id));
- Set_Is_Ignored_Ghost_Entity
- (Body_Id, Is_Ignored_Ghost_Entity (Spec_Id));
-
Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
Set_SPARK_Pragma_Inherited
(Body_Id, SPARK_Pragma_Inherited (Spec_Id));
@@ -3131,7 +3095,8 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
-- Start of processing for Analyze_Subprogram_Body_Helper
@@ -3183,7 +3148,9 @@
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
+
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id));
@@ -3194,15 +3161,13 @@
Check_Missing_Return;
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
- else
- -- Previous entity conflicts with subprogram name. Attempting to
- -- enter name will post error.
+ -- Otherwise a previous entity conflicts with the subprogram name.
+ -- Attempting to enter name will post error.
+ else
Enter_Name (Body_Id);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -3213,7 +3178,6 @@
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- Ghost_Mode := Save_Ghost_Mode;
return;
else
@@ -3230,7 +3194,8 @@
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
else
Spec_Id := Find_Corresponding_Spec (N);
@@ -3240,7 +3205,8 @@
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
-- In GNATprove mode, if the body has no previous spec, create
-- one so that the inlining machinery can operate properly.
@@ -3304,8 +3270,7 @@
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- A subprogram body should cause freezing of its own declaration,
@@ -3342,7 +3307,8 @@
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
end if;
end if;
@@ -3394,7 +3360,7 @@
-- function.
Set_Is_Immediately_Visible (Corresponding_Spec (N), False);
- return;
+ goto Leave;
end if;
-- If a separate spec is present, then deal with freezing issues
@@ -3445,26 +3411,12 @@
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
else
Set_Convention (Body_Id, Convention (Spec_Id));
Set_Has_Completion (Spec_Id);
- -- 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.
-
- 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 point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Spec_Id, Body_Id);
- end if;
-
if Is_Protected_Type (Scope (Spec_Id)) then
Prot_Typ := Scope (Spec_Id);
end if;
@@ -3518,8 +3470,7 @@
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
@@ -3630,13 +3581,6 @@
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);
@@ -3759,8 +3703,7 @@
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Handle inlining
@@ -4182,7 +4125,8 @@
-- Check for variables that are never modified
declare
- E1, E2 : Entity_Id;
+ E1 : Entity_Id;
+ E2 : Entity_Id;
begin
-- If there is a separate spec, then transfer Never_Set_In_Source
@@ -4247,7 +4191,10 @@
Set_Directly_Designated_Type (Etype (Spec_Id), Desig_View);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze_Subprogram_Body_Helper;
------------------------------------
@@ -4309,13 +4256,6 @@
Set_SPARK_Pragma_Inherited (Designator);
end if;
- -- A subprogram declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Designator);
- end if;
-
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
@@ -8197,10 +8137,6 @@
Set_Convention (Designator, Convention (E));
- if Is_Ghost_Entity (E) then
- Set_Is_Ghost_Entity (Designator);
- end if;
-
-- Skip past subprogram bodies and subprogram renamings that
-- may appear to have a matching spec, but that aren't fully
-- conformant with it. That can occur in cases where an
@@ -9762,8 +9698,8 @@
Set_Is_Primitive (S);
Check_Private_Overriding (B_Typ);
- -- The Ghost policy in effect at the point of declaration of
- -- a tagged type and a primitive operation must match
+ -- The Ghost policy in effect at the point of declaration
+ -- or a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
@@ -9795,8 +9731,8 @@
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
- -- The Ghost policy in effect at the point of declaration of
- -- a tagged type and a primitive operation must match
+ -- The Ghost policy in effect at the point of declaration
+ -- of a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
@@ -11058,13 +10994,6 @@
Set_Etype (Formal, Formal_Type);
- -- A formal parameter declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Formal);
- end if;
-
-- Deal with default expression if present
Default := Expression (Param_Spec);
Index: exp_disp.adb
===================================================================
--- exp_disp.adb (revision 244350)
+++ exp_disp.adb (working copy)
@@ -4367,71 +4367,62 @@
-- Local variables
- Elab_Code : constant List_Id := New_List;
- Result : constant List_Id := New_List;
- Tname : constant Name_Id := Chars (Typ);
+ Elab_Code : constant List_Id := New_List;
+ Result : constant List_Id := New_List;
+ Tname : constant Name_Id := Chars (Typ);
+
+ -- The following name entries are used by Make_DT to generate a number
+ -- of entities related to a tagged type. These entities may be generated
+ -- in a scope other than that of the tagged type declaration, and if
+ -- the entities for two tagged types with the same name happen to be
+ -- generated in the same scope, we have to take care to use different
+ -- names. This is achieved by means of a unique serial number appended
+ -- to each generated entity name.
+
+ Name_DT : constant Name_Id :=
+ New_External_Name (Tname, 'T', Suffix_Index => -1);
+ Name_Exname : constant Name_Id :=
+ New_External_Name (Tname, 'E', Suffix_Index => -1);
+ Name_HT_Link : constant Name_Id :=
+ New_External_Name (Tname, 'H', Suffix_Index => -1);
+ Name_Predef_Prims : constant Name_Id :=
+ New_External_Name (Tname, 'R', Suffix_Index => -1);
+ Name_SSD : constant Name_Id :=
+ New_External_Name (Tname, 'S', Suffix_Index => -1);
+ Name_TSD : constant Name_Id :=
+ New_External_Name (Tname, 'B', Suffix_Index => -1);
+
AI : Elmt_Id;
AI_Tag_Elmt : Elmt_Id;
AI_Tag_Comp : Elmt_Id;
+ DT : Entity_Id;
DT_Aggr_List : List_Id;
DT_Constr_List : List_Id;
DT_Ptr : Entity_Id;
+ Exname : Entity_Id;
+ HT_Link : Entity_Id;
ITable : Node_Id;
I_Depth : Nat := 0;
Iface_Table_Node : Node_Id;
+ Mode : Ghost_Mode_Type;
Name_ITable : Name_Id;
Nb_Predef_Prims : Nat := 0;
Nb_Prim : Nat := 0;
New_Node : Node_Id;
Num_Ifaces : Nat := 0;
Parent_Typ : Entity_Id;
+ Predef_Prims : Entity_Id;
Prim : Entity_Id;
Prim_Elmt : Elmt_Id;
Prim_Ops_Aggr_List : List_Id;
+ SSD : Entity_Id;
Suffix_Index : Int;
Typ_Comps : Elist_Id;
Typ_Ifaces : Elist_Id;
+ TSD : Entity_Id;
TSD_Aggr_List : List_Id;
TSD_Tags_List : List_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
- -- The following name entries are used by Make_DT to generate a number
- -- of entities related to a tagged type. These entities may be generated
- -- in a scope other than that of the tagged type declaration, and if
- -- the entities for two tagged types with the same name happen to be
- -- generated in the same scope, we have to take care to use different
- -- names. This is achieved by means of a unique serial number appended
- -- to each generated entity name.
-
- Name_DT : constant Name_Id :=
- New_External_Name (Tname, 'T', Suffix_Index => -1);
- Name_Exname : constant Name_Id :=
- New_External_Name (Tname, 'E', Suffix_Index => -1);
- Name_HT_Link : constant Name_Id :=
- New_External_Name (Tname, 'H', Suffix_Index => -1);
- Name_Predef_Prims : constant Name_Id :=
- New_External_Name (Tname, 'R', Suffix_Index => -1);
- Name_SSD : constant Name_Id :=
- New_External_Name (Tname, 'S', Suffix_Index => -1);
- Name_TSD : constant Name_Id :=
- New_External_Name (Tname, 'B', Suffix_Index => -1);
-
- -- Entities built with above names
-
- DT : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_DT);
- Exname : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_Exname);
- HT_Link : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_HT_Link);
- Predef_Prims : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_Predef_Prims);
- SSD : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_SSD);
- TSD : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_TSD);
-
-- Start of processing for Make_DT
begin
@@ -4441,7 +4432,7 @@
-- the mode now to ensure that any nodes generated during dispatch table
-- creation are properly marked as Ghost.
- Set_Ghost_Mode (Declaration_Node (Typ), Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Handle cases in which there is no need to build the dispatch table
@@ -4449,19 +4440,17 @@
or else No (Access_Disp_Table (Typ))
or else Is_CPP_Class (Typ)
then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
elsif not RTE_Available (RE_Tag) then
Append_To (Result,
Make_Object_Declaration (Loc,
- Defining_Identifier => Node (First_Elmt
- (Access_Disp_Table (Typ))),
+ Defining_Identifier =>
+ Node (First_Elmt (Access_Disp_Table (Typ))),
Object_Definition => New_Occurrence_Of (RTE (RE_Tag), Loc),
Constant_Present => True,
Expression =>
@@ -4470,8 +4459,7 @@
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- Ensure that the value of Max_Predef_Prims defined in a-tags is
@@ -4481,18 +4469,23 @@
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
else
if Max_Predef_Prims /= 9 then
Error_Msg_N ("run-time library configuration error", Typ);
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
end if;
+ DT := Make_Defining_Identifier (Loc, Name_DT);
+ Exname := Make_Defining_Identifier (Loc, Name_Exname);
+ HT_Link := Make_Defining_Identifier (Loc, Name_HT_Link);
+ Predef_Prims := Make_Defining_Identifier (Loc, Name_Predef_Prims);
+ SSD := Make_Defining_Identifier (Loc, Name_SSD);
+ TSD := Make_Defining_Identifier (Loc, Name_TSD);
+
-- Initialize Parent_Typ handling private types
Parent_Typ := Etype (Typ);
@@ -4695,7 +4688,7 @@
Set_SCIL_Entity (New_Node, Typ);
Set_SCIL_Node (Last (Result), New_Node);
- goto Early_Exit_For_SCIL;
+ goto Leave_SCIL;
-- Gnat2scil has its own implementation of dispatch tables,
-- different than what is being implemented here. Generating
@@ -4772,7 +4765,7 @@
Set_SCIL_Entity (New_Node, Typ);
Set_SCIL_Node (Last (Result), New_Node);
- goto Early_Exit_For_SCIL;
+ goto Leave_SCIL;
-- Gnat2scil has its own implementation of dispatch tables,
-- different than what is being implemented here. Generating
@@ -6238,13 +6231,15 @@
end;
end if;
- <<Early_Exit_For_SCIL>>
+ <<Leave_SCIL>>
-- Register the tagged type in the call graph nodes table
Register_CG_Node (Typ);
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
+
return Result;
end Make_DT;
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 244369)
+++ sem_ch8.adb (working copy)
@@ -575,7 +575,7 @@
-- The exception renaming declaration may become Ghost if it renames
-- a Ghost entity.
- Mark_Renaming_As_Ghost (N, Entity (Nam));
+ Mark_Ghost_Renaming (N, Entity (Nam));
else
Error_Msg_N ("invalid exception name in renaming", Nam);
end if;
@@ -658,11 +658,9 @@
K : Entity_Kind)
is
New_P : constant Entity_Id := Defining_Entity (N);
+ Inst : Boolean := False;
Old_P : Entity_Id;
- Inst : Boolean := False;
- -- Prevent junk warning
-
begin
if Name (N) = Error then
return;
@@ -705,17 +703,17 @@
Set_Renamed_Object (New_P, Old_P);
end if;
+ -- The generic renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ Mark_Ghost_Renaming (N, Old_P);
+
Set_Is_Pure (New_P, Is_Pure (Old_P));
Set_Is_Preelaborated (New_P, Is_Preelaborated (Old_P));
Set_Etype (New_P, Etype (Old_P));
Set_Has_Completion (New_P);
- -- The generic renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Old_P);
-
if In_Open_Scopes (Old_P) then
Error_Msg_N ("within its scope, generic denotes its instance", N);
end if;
@@ -840,7 +838,15 @@
-- already-analyzed expression.
if Nkind (Nam) = N_Selected_Component and then Analyzed (Nam) then
- T := Etype (Nam);
+
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
+ T := Etype (Nam);
Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam);
if Present (Dec) then
@@ -860,6 +866,13 @@
T := Entity (Subtype_Mark (N));
Analyze (Nam);
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- Reject renamings of conversions unless the type is tagged, or
-- the conversion is implicit (which can occur for cases of anonymous
-- access types in Ada 2012).
@@ -928,12 +941,20 @@
-- Ada 2005 (AI-230/AI-254): Access renaming
else pragma Assert (Present (Access_Definition (N)));
- T := Access_Definition
- (Related_Nod => N,
- N => Access_Definition (N));
+ T :=
+ Access_Definition
+ (Related_Nod => N,
+ N => Access_Definition (N));
Analyze (Nam);
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- Ada 2005 AI05-105: if the declaration has an anonymous access
-- type, the renamed object must also have an anonymous type, and
-- this is a name resolution rule. This was implicit in the last part
@@ -1071,7 +1092,6 @@
("\suggest using an initialized constant "
& "object instead?R?", Nam);
end if;
-
end case;
end if;
@@ -1296,13 +1316,6 @@
Set_Is_True_Constant (Id, True);
end if;
- -- The object renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- if Is_Entity_Name (Nam) then
- Mark_Renaming_As_Ghost (N, Entity (Nam));
- end if;
-
-- The entity of the renaming declaration needs to reflect whether the
-- renamed object is volatile. Is_Volatile is set if the renamed object
-- is volatile in the RM legality sense.
@@ -1393,7 +1406,7 @@
else
Error_Msg_Sloc := Sloc (Old_P);
Error_Msg_NE
- ("expect package name in renaming, found& declared#",
+ ("expect package name in renaming, found& declared#",
Name (N), Old_P);
end if;
@@ -1418,19 +1431,18 @@
Set_Renamed_Object (New_P, Old_P);
end if;
+ -- The package renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ Mark_Ghost_Renaming (N, Old_P);
+
Set_Has_Completion (New_P);
-
- Set_First_Entity (New_P, First_Entity (Old_P));
- Set_Last_Entity (New_P, Last_Entity (Old_P));
+ Set_First_Entity (New_P, First_Entity (Old_P));
+ Set_Last_Entity (New_P, Last_Entity (Old_P));
Set_First_Private_Entity (New_P, First_Private_Entity (Old_P));
Check_Library_Unit_Renaming (N, Old_P);
Generate_Reference (Old_P, Name (N));
- -- The package renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Old_P);
-
-- If the renaming is in the visible part of a package, then we set
-- Renamed_In_Spec for the renamed package, to prevent giving
-- warnings about no entities referenced. Such a warning would be
@@ -2574,8 +2586,8 @@
and then Expander_Active
then
declare
+ Prefix_Type : constant Entity_Id := Entity (Prefix (Nam));
Stream_Prim : Entity_Id;
- Prefix_Type : constant Entity_Id := Entity (Prefix (Nam));
begin
-- The class-wide forms of the stream attributes are not
@@ -2610,13 +2622,13 @@
Find_Optional_Prim_Op (Prefix_Type, TSS_Stream_Write);
when others =>
Error_Msg_N
- ("attribute must be a primitive"
- & " dispatching operation", Nam);
+ ("attribute must be a primitive dispatching operation",
+ Nam);
return;
end case;
- -- If no operation was found, and the type is limited,
- -- the user should have defined one.
+ -- If no operation was found, and the type is limited, the user
+ -- should have defined one.
if No (Stream_Prim) then
if Is_Limited_Type (Prefix_Type) then
@@ -2655,8 +2667,8 @@
end if;
end if;
- -- Check whether this declaration corresponds to the instantiation
- -- of a formal subprogram.
+ -- Check whether this declaration corresponds to the instantiation of a
+ -- formal subprogram.
-- If this is an instantiation, the corresponding actual is frozen and
-- error messages can be made more precise. If this is a default
@@ -2677,8 +2689,8 @@
-- is an external axiomatization on the package.
if CW_Actual
- and then Box_Present (Inst_Node)
- and then not
+ and then Box_Present (Inst_Node)
+ and then not
(GNATprove_Mode
and then
Present (Containing_Package_With_Ext_Axioms (Formal_Spec)))
@@ -2691,11 +2703,17 @@
and then not Is_Overloaded (Nam)
then
Old_S := Entity (Nam);
+
+ -- The subprogram renaming declaration may become Ghost if it
+ -- renames a Ghost entity.
+
+ Mark_Ghost_Renaming (N, Old_S);
+
New_S := Analyze_Subprogram_Specification (Spec);
-- Operator case
- if Ekind (Entity (Nam)) = E_Operator then
+ if Ekind (Old_S) = E_Operator then
-- Box present
@@ -2729,9 +2747,9 @@
and then Hidden /= Old_S
then
Error_Msg_Sloc := Sloc (Hidden);
- Error_Msg_N ("default subprogram is resolved " &
- "in the generic declaration " &
- "(RM 12.6(17))??", N);
+ Error_Msg_N
+ ("default subprogram is resolved in the generic "
+ & "declaration (RM 12.6(17))??", N);
Error_Msg_NE ("\and will not use & #??", N, Hidden);
end if;
end;
@@ -2740,6 +2758,14 @@
else
Analyze (Nam);
+
+ -- The subprogram renaming declaration may become Ghost if it
+ -- renames a Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
New_S := Analyze_Subprogram_Specification (Spec);
end if;
@@ -2749,6 +2775,13 @@
Analyze (Nam);
+ -- The subprogram renaming declaration may become Ghost if it renames
+ -- a Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- The renaming defines a new overloaded entity, which is analyzed
-- like a subprogram declaration.
@@ -2845,8 +2878,9 @@
Error_Msg_NE
("subprogram& overrides inherited operation",
N, Rename_Spec);
- elsif
- Style_Check and then not Must_Override (Specification (N))
+
+ elsif Style_Check
+ and then not Must_Override (Specification (N))
then
Style.Missing_Overriding (N, Rename_Spec);
end if;
@@ -3025,11 +3059,6 @@
Set_Is_Pure (New_S, Is_Pure (Entity (Nam)));
Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam)));
- -- The subprogram renaming declaration may become Ghost if it renames
- -- a Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Entity (Nam));
-
-- Ada 2005 (AI-423): Check the consistency of null exclusions
-- between a subprogram and its correct renaming.
@@ -3068,8 +3097,8 @@
not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
then
Error_Msg_N
- ("renamed entity cannot be "
- & "subprogram that requires overriding (RM 8.5.4 (5.1))", N);
+ ("renamed entity cannot be subprogram that requires overriding "
+ & "(RM 8.5.4 (5.1))", N);
end if;
end if;
@@ -3124,7 +3153,7 @@
then
Error_Msg_N
("subprogram in renaming_as_body cannot be intrinsic",
- Name (N));
+ Name (N));
end if;
Set_Has_Completion (Rename_Spec);
@@ -3364,8 +3393,7 @@
then
Error_Msg_Node_2 := T1;
Error_Msg_NE
- ("default & on & is not directly visible",
- Nam, Nam);
+ ("default & on & is not directly visible", Nam, Nam);
end if;
end;
end if;
@@ -3396,8 +3424,8 @@
then
Error_Msg_N ("access parameter is controlling,", New_F);
Error_Msg_NE
- ("\corresponding parameter of& "
- & "must be explicitly null excluding", New_F, Old_S);
+ ("\corresponding parameter of& must be explicitly null "
+ & "excluding", New_F, Old_S);
end if;
Next_Formal (Old_F);
Index: atree.adb
===================================================================
--- atree.adb (revision 244350)
+++ atree.adb (working copy)
@@ -549,16 +549,20 @@
-- Local Subprograms --
-----------------------
- procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
- -- Fixup parent pointers for the syntactic children of Fix_Node after
- -- a copy, setting them to Fix_Node when they pointed to Ref_Node.
-
function Allocate_Initialize_Node
(Src : Node_Id;
With_Extension : Boolean) return Node_Id;
-- Allocate a new node or node extension. If Src is not empty, the
-- information for the newly-allocated node is copied from it.
+ procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
+ -- Fixup parent pointers for the syntactic children of Fix_Node after a
+ -- copy, setting them to Fix_Node when they pointed to Ref_Node.
+
+ procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id);
+ -- Mark arbitrary node or entity N as Ghost when it is created within a
+ -- Ghost region.
+
------------------------------
-- Allocate_Initialize_Node --
------------------------------
@@ -594,13 +598,6 @@
Node_Count := Node_Count + 1;
end if;
- -- Mark the node as ignored Ghost if it is created in an ignored Ghost
- -- region.
-
- if Ghost_Mode = Ignore then
- Set_Is_Ignored_Ghost_Node (New_Id);
- end if;
-
-- Clear Check_Actuals to False
Set_Check_Actuals (New_Id, False);
@@ -1432,7 +1429,6 @@
-----------------
procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is
-
procedure Fix_Parent (Field : Union_Id);
-- Fixup one parent pointer. Field is checked to see if it points to
-- a node, list, or element list that has a parent that points to
@@ -1590,6 +1586,28 @@
Orig_Nodes.Release;
end Lock;
+ -------------------------
+ -- Mark_New_Ghost_Node --
+ -------------------------
+
+ procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id) is
+ begin
+ -- The Ghost node is created within a Ghost region
+
+ if Ghost_Mode = Check then
+ if Nkind (N) in N_Entity then
+ Set_Is_Checked_Ghost_Entity (N);
+ end if;
+
+ elsif Ghost_Mode = Ignore then
+ if Nkind (N) in N_Entity then
+ Set_Is_Ignored_Ghost_Entity (N);
+ end if;
+
+ Set_Is_Ignored_Ghost_Node (N);
+ end if;
+ end Mark_New_Ghost_Node;
+
----------------------------
-- Mark_Rewrite_Insertion --
----------------------------
@@ -1630,6 +1648,10 @@
-- aspects if this is required for the particular situation.
Set_Has_Aspects (New_Id, False);
+
+ -- Mark the copy as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (New_Id);
end if;
return New_Id;
@@ -1662,6 +1684,10 @@
Nodes.Table (Ent).Sloc := New_Sloc;
pragma Debug (New_Node_Debugging_Output (Ent));
+ -- Mark the new entity as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (Ent);
+
return Ent;
end New_Entity;
@@ -1690,6 +1716,10 @@
Current_Error_Node := Nod;
end if;
+ -- Mark the new node as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (Nod);
+
return Nod;
end New_Node;
Index: sem_ch11.adb
===================================================================
--- sem_ch11.adb (revision 244350)
+++ sem_ch11.adb (working copy)
@@ -27,7 +27,6 @@
with Checks; use Checks;
with Einfo; use Einfo;
with Errout; use Errout;
-with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
@@ -67,13 +66,6 @@
Set_Is_Statically_Allocated (Id);
Set_Is_Pure (Id, PF);
- -- An exception declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 244369)
+++ sem_ch13.adb (working copy)
@@ -8524,7 +8524,7 @@
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Build_Predicate_Functions
@@ -8541,7 +8541,7 @@
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the predicate functions are properly marked as Ghost.
- Set_Ghost_Mode_From_Entity (Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Prepare to construct predicate expression
@@ -8647,20 +8647,12 @@
FBody : Node_Id;
begin
-
-- The predicate function is shared between views of a type
if Is_Private_Type (Typ) and then Present (Full_View (Typ)) then
Set_Predicate_Function (Full_View (Typ), SId);
end if;
- -- Mark the predicate function explicitly as Ghost because it does
- -- not come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (SId);
- end if;
-
-- Build function body
Spec :=
@@ -8743,13 +8735,6 @@
Set_Predicate_Function_M (Full_View (Typ), SId);
end if;
- -- Mark the predicate function explicitly as Ghost because it
- -- does not come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (SId);
- end if;
-
Spec :=
Make_Function_Specification (Loc,
Defining_Unit_Name => SId,
@@ -8902,7 +8887,7 @@
end;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Build_Predicate_Functions;
------------------------------------------
@@ -8914,45 +8899,45 @@
is
Loc : constant Source_Ptr := Sloc (Typ);
- Object_Entity : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_Internal_Name ('I'));
+ Func_Decl : Node_Id;
+ Func_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
+ Spec : Node_Id;
- -- The formal parameter of the function
+ begin
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the predicate functions are properly marked as Ghost.
- SId : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Typ), "Predicate"));
+ Set_Ghost_Mode (Typ, Mode);
- -- The entity for the function spec
+ Func_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Typ), "Predicate"));
- FDecl : Node_Id;
- Spec : Node_Id;
-
- begin
Spec :=
Make_Function_Specification (Loc,
- Defining_Unit_Name => SId,
+ Defining_Unit_Name => Func_Id,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
+ Defining_Identifier => Make_Temporary (Loc, 'I'),
Parameter_Type => New_Occurrence_Of (Typ, Loc))),
Result_Definition =>
New_Occurrence_Of (Standard_Boolean, Loc));
- FDecl := Make_Subprogram_Declaration (Loc, Specification => Spec);
+ Func_Decl := Make_Subprogram_Declaration (Loc, Specification => Spec);
- Set_Ekind (SId, E_Function);
- Set_Etype (SId, Standard_Boolean);
- Set_Is_Internal (SId);
- Set_Is_Predicate_Function (SId);
- Set_Predicate_Function (Typ, SId);
+ Set_Ekind (Func_Id, E_Function);
+ Set_Etype (Func_Id, Standard_Boolean);
+ Set_Is_Internal (Func_Id);
+ Set_Is_Predicate_Function (Func_Id);
+ Set_Predicate_Function (Typ, Func_Id);
- Insert_After (Parent (Typ), FDecl);
+ Insert_After (Parent (Typ), Func_Decl);
+ Analyze (Func_Decl);
- Analyze (FDecl);
+ Restore_Ghost_Mode (Mode);
- return FDecl;
+ return Func_Decl;
end Build_Predicate_Function_Declaration;
-----------------------------------------
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb (revision 244366)
+++ exp_ch3.adb (working copy)
@@ -4361,13 +4361,7 @@
Base : constant Entity_Id := Base_Type (Typ);
Comp_Typ : constant Entity_Id := Component_Type (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
if not Is_Bit_Packed_Array (Typ) then
-- If the component contains tasks, so does the array type. This may
@@ -4435,8 +4429,6 @@
then
Build_Array_Init_Proc (Base, N);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Array_Type;
-----------------------------------
@@ -4477,8 +4469,6 @@
Typ : constant Entity_Id := Entity (N);
Root : constant Entity_Id := Root_Type (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_Freeze_Class_Wide_Type
begin
@@ -4511,15 +4501,10 @@
return;
end if;
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Create the body of TSS primitive Finalize_Address. This automatically
-- sets the TSS entry for the class-wide type.
Make_Finalize_Address_Body (Typ);
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Class_Wide_Type;
------------------------------------
@@ -4530,8 +4515,6 @@
Typ : constant Entity_Id := Entity (N);
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Arr : Entity_Id;
Ent : Entity_Id;
Fent : Entity_Id;
@@ -4546,10 +4529,6 @@
pragma Warnings (Off, Func);
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Various optimizations possible if given representation is contiguous
Is_Contiguous := True;
@@ -4832,11 +4811,8 @@
Set_Debug_Info_Off (Fent);
end if;
- Ghost_Mode := Save_Ghost_Mode;
-
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_Freeze_Enumeration_Type;
@@ -4848,8 +4824,6 @@
Typ : constant Node_Id := Entity (N);
Typ_Decl : constant Node_Id := Parent (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Comp : Entity_Id;
Comp_Typ : Entity_Id;
Predef_List : List_Id;
@@ -4867,10 +4841,6 @@
-- Start of processing for Expand_Freeze_Record_Type
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Build discriminant checking functions if not a derived type (for
-- derived types that are not tagged types, always use the discriminant
-- checking functions of the parent type). However, for untagged types
@@ -5291,8 +5261,6 @@
end loop;
end;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Record_Type;
------------------------------------
@@ -7135,10 +7103,9 @@
-- Local variables
Def_Id : constant Entity_Id := Entity (N);
+ Mode : Ghost_Mode_Type;
Result : Boolean := False;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Freeze_Type
begin
@@ -7146,7 +7113,7 @@
-- now to ensure that any nodes generated during freezing are properly
-- marked as Ghost.
- Set_Ghost_Mode (N, Def_Id);
+ Set_Ghost_Mode (Def_Id, Mode);
-- Process any remote access-to-class-wide types designating the type
-- being frozen.
@@ -7474,12 +7441,12 @@
Build_Invariant_Procedure_Body (Def_Id);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return Result;
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return False;
end Freeze_Type;
More information about the Gcc-patches
mailing list