+2015-10-16 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch3.adb (Expand_N_Full_Type_Declaration): Do not capture,
+ set and restore the Ghost mode.
+ (Expand_N_Object_Declaration): Do not capture, set and restore the
+ Ghost mode.
+ (Freeze_Type): Redo the capture and restore of the Ghost mode.
+ (Restore_Globals): Removed.
+ * exp_ch5.adb (Expand_N_Assignment_Statement): Redo the capture
+ and restore of the Ghost mode.
+ (Restore_Globals): Removed.
+ * exp_ch6.adb (Expand_N_Procedure_Call_Statement):
+ Redo the capture and restore of the Ghost mode.
+ (Expand_N_Subprogram_Body): Redo the capture, set and restore
+ of the Ghost mode.
+ (Expand_N_Subprogram_Declaration): Do not
+ capture, set and restore the Ghost mode.
+ (Restore_Globals): Removed.
+ * exp_ch7.adb (Expand_N_Package_Body): Redo the capture, set
+ and restore of the Ghost mode.
+ (Expand_N_Package_Declaration): Do not capture, set and restore the
+ Ghost mode.
+ * exp_ch8.adb (Expand_N_Exception_Renaming_Declaration):
+ Redo the capture and restore of the Ghost mode.
+ (Expand_N_Object_Renaming_Declaration): Redo
+ the capture and restore of the Ghost mode.
+ (Expand_N_Package_Renaming_Declaration):
+ Redo the capture and restore of the Ghost mode.
+ (Expand_N_Subprogram_Renaming_Declaration): Redo the capture
+ and restore of the Ghost mode.
+ * exp_ch11.adb Remove with and use clauses for Ghost.
+ (Expand_N_Exception_Declaration): Do not capture, set and restore
+ the Ghost mode.
+ * exp_disp.adb (Make_DT): Redo the capture and restore of the
+ Ghost mode.
+ (Restore_Globals): Removed.
+ * exp_prag.adb (Expand_Pragma_Check): Do not capture, set
+ and restore the Ghost mode.
+ (Expand_Pragma_Contract_Cases):
+ Redo the capture and restore of the Ghost mode. Preserve the
+ original context of contract cases by setting / resetting the
+ In_Assertion_Expr counter.
+ (Expand_Pragma_Initial_Condition):
+ Redo the capture and restore of the Ghost mode.
+ (Expand_Pragma_Loop_Variant): Redo the capture and restore of
+ the Ghost mode.
+ (Restore_Globals): Removed.
+ * exp_util.adb (Make_Predicate_Call): Redo the capture and
+ restore of the Ghost mode.
+ (Restore_Globals): Removed.
+ * freeze.adb (Freeze_Entity): Redo the capture and restore of
+ the Ghost mode.
+ (Restore_Globals): Removed.
+ * ghost.adb (Check_Ghost_Context): Remove the RM reference from
+ the error message.
+ (Is_OK_Statement): Account for statements
+ that appear in assertion expressions.
+ (Is_Subject_To_Ghost):
+ Moved from spec.
+ * ghost.ads (Is_Subject_To_Ghost): Moved to body.
+ * rtsfind.ads (Load_RTU): Redo the capture and restore of the
+ Ghost mode.
+ * sem.adb Add with and use clauses for Ghost.
+ (Analyze): Redo
+ the capture and restore of the Ghost mode. Set the Ghost mode
+ when analyzing a declaration.
+ (Do_Analyze): Redo the capture
+ and restore of the Ghost mode.
+ * sem_ch3.adb (Analyze_Full_Type_Declaration): Do not capture, set
+ and restore the Ghost mode.
+ (Analyze_Incomplete_Type_Decl):
+ Do not capture, set and restore the Ghost mode.
+ (Analyze_Number_Declaration): Do not capture, set and restore the
+ Ghost mode.
+ (Analyze_Object_Declaration): Do not capture, set and
+ restore the Ghost mode.
+ (Analyze_Private_Extension_Declaration):
+ Do not capture, set and restore the Ghost mode.
+ (Analyze_Subtype_Declaration): Do not capture, set and restore
+ the Ghost mode.
+ (Restore_Globals): Removed.
+ * sem_ch5.adb (Analyze_Assignment): Redo the capture and restore
+ of the Ghost mode.
+ (Restore_Globals): Removed.
+ * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
+ Do not capture, set and restore the Ghost mode.
+ (Analyze_Procedure_Call): Redo the capture and restore of the
+ Ghost mode.
+ (Analyze_Subprogram_Body_Helper): Redo the capture
+ and restore of the Ghost mode. (Analyze_Subprogram_Declaration):
+ Do not capture, set and restore the Ghost mode.
+ (Restore_Globals): Removed.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Redo the capture and
+ restore of the Ghost mode.
+ (Analyze_Package_Declaration):
+ Do not capture, set and restore the Ghost mode.
+ (Analyze_Private_Type_Declaration): Do not capture, set and
+ restore the Ghost mode.
+ (Restore_Globals): Removed.
+ * sem_ch8.adb (Analyze_Exception_Renaming): Do not capture,
+ set and restore the Ghost mode.
+ (Analyze_Generic_Renaming): Do not capture, set and restore the Ghost
+ mode.
+ (Analyze_Object_Renaming): Do not capture, set and restore the
+ Ghost mode.
+ (Analyze_Package_Renaming): Do not capture, set and restore the Ghost
+ mode.
+ (Analyze_Subprogram_Renaming): Do not capture, set and restore the
+ Ghost mode.
+ (Restore_Globals): Removed.
+ * sem_ch11.adb (Analyze_Exception_Declaration): Do not capture,
+ set and restore the Ghost mode.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration):
+ Do not capture, set and restore the Ghost mode.
+ (Analyze_Generic_Subprogram_Declaration): Do not capture, set
+ and restore the Ghost mode.
+ * sem_ch13.adb (Build_Invariant_Procedure_Declaration): Redo
+ the capture and restore of the Ghost mode.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
+ Redo the capture and restore of the Ghost mode.
+ (Analyze_External_Property_In_Decl_Part):
+ Redo the capture and restore of the Ghost mode.
+ (Analyze_Initial_Condition_In_Decl_Part): Redo the
+ capture and restore of the Ghost mode. (Analyze_Pragma):
+ Do not capture, set and restore the Ghost mode for Assert.
+ Redo the capture and restore of the Ghost mode for Check. Do
+ not capture and restore the Ghost mode for Invariant.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Redo the capture and
+ restore of the Ghost mode.
+ * sem_res.adb (Resolve): Capture, set and restore the Ghost mode
+ when resolving a declaration.
+ * sem_util.adb (Build_Default_Init_Cond_Procedure_Body):
+ Redo the capture and restore of the Ghost mode.
+ (Build_Default_Init_Cond_Procedure_Declaration): Redo the capture
+ and restore of the Ghost mode.
+
2015-10-16 Bob Duff <duff@adacore.com>
* debug.adb: Document -gnatdQ switch.
with Exp_Ch7; use Exp_Ch7;
with Exp_Intr; use Exp_Intr;
with Exp_Util; use Exp_Util;
-with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
-- end if;
procedure Expand_N_Exception_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
- Loc : constant Source_Ptr := Sloc (N);
+ Id : constant Entity_Id := Defining_Identifier (N);
+ Loc : constant Source_Ptr := Sloc (N);
Ex_Id : Entity_Id;
Flag_Id : Entity_Id;
L : List_Id;
return;
end if;
- -- The exception declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- Definition of the external name: nam : constant String := "A.B.NAME";
Ex_Id :=
Insert_List_After_And_Analyze (N, L);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Exception_Declaration;
---------------------------------------------
-- Local declarations
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- B_Id : constant Entity_Id := Base_Type (Def_Id);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
+ B_Id : constant Entity_Id := Base_Type (Def_Id);
FN : Node_Id;
Par_Id : Entity_Id;
-- Start of processing for Expand_N_Full_Type_Declaration
begin
- -- The type declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
if Is_Access_Type (Def_Id) then
Build_Master (Def_Id);
end if;
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Full_Type_Declaration;
---------------------------------
---------------------------------
procedure Expand_N_Object_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- Expr : constant Node_Id := Expression (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Obj_Def : constant Node_Id := Object_Definition (N);
- Typ : constant Entity_Id := Etype (Def_Id);
- Base_Typ : constant Entity_Id := Base_Type (Typ);
+ Loc : constant Source_Ptr := Sloc (N);
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
+ Expr : constant Node_Id := Expression (N);
+ Obj_Def : constant Node_Id := Object_Definition (N);
+ Typ : constant Entity_Id := Etype (Def_Id);
+ Base_Typ : constant Entity_Id := Base_Type (Typ);
Expr_Q : Node_Id;
function Build_Equivalent_Aggregate return Boolean;
-- Generate all default initialization actions for object Def_Id. Any
-- new code is inserted after node After.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
function Rewrite_As_Renaming return Boolean;
-- Indicate whether to rewrite a declaration with initialization into an
-- object renaming declaration (see below).
end if;
end Default_Initialize_Object;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-------------------------
-- Rewrite_As_Renaming --
-------------------------
return;
end if;
- -- The object declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- First we do special processing for objects of a tagged type where
-- this is the point at which the type is frozen. The creation of the
-- dispatch table and the initialization procedure have to be deferred
and then Is_Build_In_Place_Function_Call (Expr_Q)
then
Make_Build_In_Place_Call_In_Object_Declaration (N, Expr_Q);
- Restore_Globals;
-- The previous call expands the expression initializing the
-- built-in-place object into further code that will be analyzed
end;
end if;
- Restore_Globals;
return;
-- Common case of explicit object initialization
-- to avoid its management in the backend
Set_Expression (N, Empty);
- Restore_Globals;
return;
-- Handle initialization of limited tagged types
end;
end if;
- Restore_Globals;
-
-- Exception on library entity not available
exception
when RE_Not_Available =>
- Restore_Globals;
return;
end Expand_N_Object_Declaration;
-- node using Append_Freeze_Actions.
function Freeze_Type (N : Node_Id) return Boolean is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect in case the type being frozen
- -- sets a different mode.
-
procedure Process_RACW_Types (Typ : Entity_Id);
-- Validate and generate stubs for all RACW types associated with type
-- Typ.
-- Associate type Typ's Finalize_Address primitive with the finalization
-- masters of pending access-to-Typ types.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------
-- Process_RACW_Types --
------------------------
end if;
end Process_Pending_Access_Types;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Local variables
Def_Id : constant Entity_Id := Entity (N);
Result : Boolean := False;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Freeze_Type
begin
- -- The type being frozen may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- freezing are properly flagged as ignored Ghost.
+ -- The type being frozen may be subject to pragma Ghost. Set the mode
+ -- now to ensure that any nodes generated during freezing are properly
+ -- marked as Ghost.
Set_Ghost_Mode (N, Def_Id);
Process_Pending_Access_Types (Def_Id);
Freeze_Stream_Operations (N, Def_Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
exception
when RE_Not_Available =>
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return False;
end Freeze_Type;
-- cannot just be passed on to the back end in untransformed state.
procedure Expand_N_Assignment_Statement (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Crep : constant Boolean := Change_Of_Representation (N);
Lhs : constant Node_Id := Name (N);
Loc : constant Source_Ptr := Sloc (N);
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
- -- Start of processing for Expand_N_Assignment_Statement
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
- -- The assignment statement may be Ghost if the left hand side is Ghost.
+ -- 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 flagged as ignored Ghost.
+ -- are properly marked as Ghost.
Set_Ghost_Mode (N);
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Rewrite (N, Call);
Analyze (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end;
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if not Crep then
Expand_Bit_Packed_Element_Set (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Change of representation case
-- Nothing to do for valuetypes
-- ??? Set_Scope_Is_Transient (False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
elsif Is_Tagged_Type (Typ)
-- expansion, since they would be missed in -gnatc mode ???
Error_Msg_N ("assignment not available on limited type", N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end Tagged_Case;
end loop;
Expand_Assign_Array (N, Actual_Rhs);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end;
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Scalar types. This is where we perform the processing related to the
end if;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
exception
when RE_Not_Available =>
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_N_Assignment_Statement;
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
- -- The procedure call may be Ghost if the name is Ghost. Set the mode
- -- now to ensure that any nodes generated during expansion are properly
- -- flagged as ignored Ghost.
+ -- 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);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
- Ghost_Mode := GM;
+ Expand_Call (N);
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Procedure_Call_Statement;
--------------------------------------
-- Wrap thread body
procedure Expand_N_Subprogram_Body (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Loc : constant Source_Ptr := Sloc (N);
- HSS : constant Node_Id := Handled_Statement_Sequence (N);
- Body_Id : Entity_Id;
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+ HSS : constant Node_Id := Handled_Statement_Sequence (N);
+ Loc : constant Source_Ptr := Sloc (N);
Except_H : Node_Id;
L : List_Id;
Spec_Id : Entity_Id;
-- the latter test is not critical, it does not matter if we add a few
-- extra returns, since they get eliminated anyway later on.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
----------------
-- Add_Return --
----------------
end if;
end Add_Return;
- ---------------------
- -- Restore_Globals --
- ---------------------
+ -- Local varaibles
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Subprogram_Body
begin
- -- The subprogram body may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are flagged as ignored Ghost.
+ if Present (Corresponding_Spec (N)) then
+ Spec_Id := Corresponding_Spec (N);
+ else
+ Spec_Id := Body_Id;
+ end if;
- Set_Ghost_Mode (N);
+ -- 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
end;
end if;
- -- Find entity for subprogram
-
- Body_Id := Defining_Entity (N);
-
- if Present (Corresponding_Spec (N)) then
- Spec_Id := Corresponding_Spec (N);
- else
- Spec_Id := Body_Id;
- end if;
-
-- Need poll on entry to subprogram if polling enabled. We only do this
-- for non-empty subprograms, since it does not seem necessary to poll
-- for a dummy null subprogram.
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
Unest_Bodies.Append ((Spec_Id, N));
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Body;
-----------------------------------
-- If the declaration is for a null procedure, emit null body
procedure Expand_N_Subprogram_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Subp : constant Entity_Id := Defining_Entity (N);
- Scop : constant Entity_Id := Scope (Subp);
+ Loc : constant Source_Ptr := Sloc (N);
+ Subp : constant Entity_Id := Defining_Entity (N);
+ Scop : constant Entity_Id := Scope (Subp);
Prot_Bod : Node_Id;
Prot_Decl : Node_Id;
Prot_Id : Entity_Id;
begin
- -- The subprogram declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- In SPARK, subprogram declarations are only allowed in package
-- specifications.
Set_Is_Inlined (Subp, False);
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Subprogram_Declaration;
--------------------------------
-- Encode entity names in package body
procedure Expand_N_Package_Body (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Spec_Ent : constant Entity_Id := Corresponding_Spec (N);
- Fin_Id : Entity_Id;
+ 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 may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- 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);
+ Set_Ghost_Mode (N, Spec_Id);
-- This is done only for non-generic packages
- if Ekind (Spec_Ent) = E_Package then
+ if Ekind (Spec_Id) = E_Package then
Push_Scope (Corresponding_Spec (N));
-- Build dispatch tables of library level tagged types
if Tagged_Type_Expansion
- and then Is_Library_Level_Entity (Spec_Ent)
+ and then Is_Library_Level_Entity (Spec_Id)
then
Build_Static_Dispatch_Tables (N);
end if;
-- assertion expression must be verified at the end of the body
-- statements.
- if Present (Get_Pragma (Spec_Ent, Pragma_Initial_Condition)) then
+ if Present (Get_Pragma (Spec_Id, Pragma_Initial_Condition)) then
Expand_Pragma_Initial_Condition (N);
end if;
end if;
Set_Elaboration_Flag (N, Corresponding_Spec (N));
- Set_In_Package_Body (Spec_Ent, False);
+ Set_In_Package_Body (Spec_Id, False);
-- Set to encode entity names in package body before gigi is called
Qualify_Entity_Names (N);
- if Ekind (Spec_Ent) /= E_Generic_Package then
+ if Ekind (Spec_Id) /= E_Generic_Package then
Build_Finalizer
(N => N,
Clean_Stmts => No_List,
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Body;
----------------------------------
-- appear.
procedure Expand_N_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Entity (N);
Spec : constant Node_Id := Specification (N);
Decls : List_Id;
return;
end if;
- -- The package declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- For a package declaration that implies no associated body, generate
-- task activation call and RACW supporting bodies now (since we won't
-- have a specific separate compilation unit for that).
Set_Finalizer (Id, Fin_Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Package_Declaration;
-----------------------------
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Decl : Node_Id;
begin
- -- The exception renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during expansion are properly flagged as ignored Ghost.
+ -- 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);
Insert_Action (N, Decl);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Object_Renaming_Declaration
begin
- -- The object renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during expansion are properly flagged as ignored Ghost.
+ -- 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);
Insert_Action (N, Decl);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Decl : Node_Id;
begin
- -- The package renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during expansion are properly flagged as ignored Ghost.
+ -- 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);
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Nam : constant Node_Id := Name (N);
+ Nam : constant Node_Id := Name (N);
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Subprogram_Renaming_Declaration
begin
- -- The subprogram renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes created
- -- during expansion are properly flagged as ignored Ghost.
+ -- 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);
end;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;
-- end;
function Make_DT (Typ : Entity_Id; N : Node_Id := Empty) return List_Id is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect in case the tagged type sets a
- -- different mode.
-
Loc : constant Source_Ptr := Sloc (Typ);
Max_Predef_Prims : constant Int :=
-- this secondary dispatch table by Make_Tags when its unique external
-- name was generated.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------------
-- Check_Premature_Freezing --
------------------------------
Append_Elmt (Iface_DT, DT_Decl);
end Make_Secondary_DT;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Local variables
Elab_Code : constant List_Id := New_List;
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
begin
pragma Assert (Is_Frozen (Typ));
- -- The tagged type being processed may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during dispatch table creation are properly flagged as ignored Ghost.
+ -- The tagged type being processed may be subject to pragma Ghost. Set
+ -- 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);
or else Convention (Typ) = Convention_CIL
or else Convention (Typ) = Convention_Java
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
elsif not RTE_Available (RE_Tag) then
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
else
if Max_Predef_Prims /= 9 then
Error_Msg_N ("run-time library configuration error", Typ);
Error_Msg_CRT ("tagged types", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
end if;
Register_CG_Node (Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end Make_DT;
--------------------------
procedure Expand_Pragma_Check (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Cond : constant Node_Id := Arg2 (N);
- Nam : constant Name_Id := Chars (Arg1 (N));
+ Cond : constant Node_Id := Arg2 (N);
+ Nam : constant Name_Id := Chars (Arg1 (N));
Msg : Node_Id;
Loc : constant Source_Ptr := Sloc (First_Node (Cond));
return;
end if;
- -- Set the Ghost mode in effect from the pragma. In general both the
- -- assertion policy and the Ghost policy of pragma Check must agree,
- -- but there are cases where this can be circumvented. For instance,
- -- a living subtype with an ignored predicate may be declared in one
- -- packade, an ignored Ghost object in another and the compilation may
- -- use -gnata to enable assertions.
- -- ??? Ghost predicates are under redesign
-
- Set_Ghost_Mode (N);
-
-- Since this check is active, we rewrite the pragma into a
-- corresponding if statement, and then analyze the statement.
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_Pragma_Check;
---------------------------------
Aggr : constant Node_Id :=
Expression (First (Pragma_Argument_Associations (CCs)));
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Case_Guard : Node_Id;
CG_Checks : Node_Id;
return;
end if;
- -- The contract cases may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- 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
+ -- aids the Ghost legality checks when verifying the placement of a
+ -- reference to a Ghost entity.
+
+ In_Assertion_Expr := In_Assertion_Expr + 1;
+
Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-- Create the counter which tracks the number of case guards that
Append_To (Stmts, Conseq_Checks);
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ In_Assertion_Expr := In_Assertion_Expr - 1;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Contract_Cases;
---------------------------------------
-------------------------------------
procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
Check : Node_Id;
Expr : Node_Id;
List : List_Id;
Pack_Id : Entity_Id;
- -- Start of processing for Expand_Pragma_Initial_Condition
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
- -- The initial condition be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- 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);
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Append_To (List, Check);
Analyze (Check);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Initial_Condition;
------------------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_Pragma_Loop_Variant
return;
end if;
- -- The loop variant may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- 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);
-- corresponding declarations and statements. We leave it in the tree
-- for documentation purposes. It will be ignored by the backend.
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Loop_Variant;
--------------------------------
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (Expr);
Call : Node_Id;
PFM : Entity_Id;
- -- Start of processing for Make_Predicate_Call
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
pragma Assert (Present (Predicate_Function (Typ)));
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the call is properly flagged as
- -- ignored Ghost.
+ -- 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);
Name => New_Occurrence_Of (PFM, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Call;
end if;
end if;
New_Occurrence_Of (Predicate_Function (Typ), Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Call;
end Make_Predicate_Call;
-------------------
function Freeze_Entity (E : Entity_Id; N : Node_Id) return List_Id is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect in case the entity being frozen
- -- sets a different mode.
-
Loc : constant Source_Ptr := Sloc (N);
Atype : Entity_Id;
Comp : Entity_Id;
-- call, but rather must go in the package holding the function, so that
-- the backend can process it in the proper context.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
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-
Append_List (Result, Decls);
end Late_Freeze_Subprogram;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
end if;
end Wrap_Imported_Subprogram;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Freeze_Entity
begin
- -- The entity being frozen may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- freezing are properly flagged as ignored Ghost.
+ -- The entity being frozen may be subject to pragma Ghost. Set the mode
+ -- now to ensure that any nodes generated during freezing are properly
+ -- flagged as Ghost.
Set_Ghost_Mode_From_Entity (E);
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- It is improper to freeze an external entity within a generic because
Analyze_Aspects_At_Freeze_Point (E);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Do not freeze a global entity within an inner scope created during
then
exit;
else
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
end if;
end loop;
if No (S) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
end;
elsif Ekind (E) = E_Generic_Package then
Result := Freeze_Generic_Entities (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
if not Is_Internal (E) then
if not Freeze_Profile (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
end if;
if Late_Freezing then
Late_Freeze_Subprogram (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of full view present
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of underlying full view present
Check_Debug_Info_Needed (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of no full view present. If entity is derived or subtype,
else
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
end if;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end Freeze_Entity;
-- 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.
+ 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.
+
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.
-- Special cases
- -- An if statement is a suitable context for a Ghost entity if it
- -- is the byproduct of assertion expression expansion.
+ elsif Nkind (Stmt) = N_If_Statement then
- elsif Nkind (Stmt) = N_If_Statement
- and then Nkind (Original_Node (Stmt)) = N_Pragma
- and then Assertion_Expression_Pragma
- (Get_Pragma_Id (Original_Node (Stmt)))
- then
- return True;
+ -- An if statement is a suitable context for a Ghost entity if
+ -- it is the byproduct of assertion expression expansion. Note
+ -- that the assertion expression may not be related to a Ghost
+ -- entity, but it may still contain references to Ghost
+ -- entities.
+
+ if Nkind (Original_Node (Stmt)) = N_Pragma
+ and then Assertion_Expression_Pragma
+ (Get_Pragma_Id (Original_Node (Stmt)))
+ then
+ return True;
+
+ -- The expansion of pragma Contract_Cases produces various if
+ -- statements to evaluate all case guards. This is a suitable
+ -- context as Contract_Cases is an assertion expression.
+
+ elsif In_Assertion_Expr > 0 then
+ return True;
+ end if;
end if;
return False;
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-- Otherwise the Ghost entity appears in a non-Ghost context and affects
- -- its behavior or value.
+ -- its behavior or value (SPARK RM 6.9(11,12)).
else
- Error_Msg_N
- ("ghost entity cannot appear in this context (SPARK RM 6.9(11))",
- Ghost_Ref);
+ Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
end if;
end Check_Ghost_Context;
Expr := Get_Pragma_Arg (Expr);
end if;
- -- Determine whether the expression of the aspect is static and
- -- denotes True.
+ -- Determine whether the expression of the aspect or pragma is static
+ -- and denotes True.
if Present (Expr) then
Preanalyze_And_Resolve (Expr);
-- Determine whether entity Id is Ghost. To qualify as such, the entity
-- must be subject to pragma Ghost.
- function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
- -- Determine whether declarative node 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.
-
procedure Lock;
-- Lock internal tables before calling backend
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect to ensure a clean environment
- -- when analyzing the unit.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Load_RTU
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
- -- Restore the original Ghost mode now that analysis has taken place
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Load_RTU;
--------------------
with Elists; use Elists;
with Expander; use Expander;
with Fname; use Fname;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Nlists; use Nlists;
-------------
procedure Analyze (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect in case the construct sets a
- -- different mode.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
Debug_A_Entry ("analyzing ", N);
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;
+
-- Otherwise processing depends on the node kind
case Nkind (N) is
Expand (N);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze;
-- Version with check(s) suppressed
----------------
procedure Do_Analyze is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the current Ghost mode in effect in case the compilation unit
- -- is withed from a unit with a different Ghost mode.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
List : Elist_Id;
Pop_Scope;
Restore_Scope_Stack (List);
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Do_Analyze;
-- Local variables
-----------------------------------
procedure Analyze_Exception_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
- PF : constant Boolean := Is_Pure (Current_Scope);
+ Id : constant Entity_Id := Defining_Identifier (N);
+ PF : constant Boolean := Is_Pure (Current_Scope);
begin
- -- The exception declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Exception);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Exception_Declaration;
--------------------------------
------------------------------------------
procedure Analyze_Generic_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Decls : constant List_Id :=
Visible_Declarations (Specification (N));
Save_Parent : Node_Id;
begin
- -- The generic package declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- We introduce a renaming of the enclosing package, to have a usable
end if;
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Package_Declaration;
--------------------------------------------
--------------------------------------------
procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Formals : List_Id;
Id : Entity_Id;
New_N : Node_Id;
Typ : Entity_Id;
begin
- -- The generic subprogram declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- Create copy of generic unit, and save for instantiation. If the unit
Generate_Reference_To_Formals (Id);
List_Inherited_Pre_Post_Aspects (Id);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Subprogram_Declaration;
-----------------------------------
function Build_Invariant_Procedure_Declaration
(Typ : Entity_Id) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Typ);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Loc : constant Source_Ptr := Sloc (Typ);
Decl : Node_Id;
Obj_Id : Entity_Id;
SId : Entity_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
-- Check for duplicate definitions
return Empty;
end if;
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the predicate functions are properly
- -- flagged as ignored Ghost.
+ -- 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);
Defining_Identifier => Obj_Id,
Parameter_Type => New_Occurrence_Of (Typ, Loc)))));
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
return Decl;
end Build_Invariant_Procedure_Declaration;
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Build_Predicate_Functions
return;
end if;
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the predicate functions are properly
- -- flagged as ignored Ghost.
+ -- 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);
end;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Predicate_Functions;
-----------------------------------------
-----------------------------------
procedure Analyze_Full_Type_Declaration (N : Node_Id) is
- Def : constant Node_Id := Type_Definition (N);
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Def : constant Node_Id := Type_Definition (N);
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
T : Entity_Id;
Prev : Entity_Id;
-- list later in Sem_Disp.Check_Operation_From_Incomplete_Type (which
-- is called from Process_Incomplete_Dependents).
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------------------
-- Check_Ops_From_Incomplete_Type --
------------------------------------
end if;
end Check_Ops_From_Incomplete_Type;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Start of processing for Analyze_Full_Type_Declaration
begin
Prev := Find_Type_Name (N);
- -- The type declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N, Prev);
-
-- The full view, if present, now points to the current type. If there
-- is an incomplete partial view, set a link to it, to simplify the
-- retrieval of primitive operations of the type.
end if;
if Etype (T) = Any_Type then
- Restore_Globals;
return;
end if;
Analyze_Aspect_Specifications (N, Def_Id);
end if;
end if;
-
- Restore_Globals;
end Analyze_Full_Type_Declaration;
----------------------------------
----------------------------------
procedure Analyze_Incomplete_Type_Decl (N : Node_Id) is
- F : constant Boolean := Is_Pure (Current_Scope);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- T : Entity_Id;
+ F : constant Boolean := Is_Pure (Current_Scope);
+ T : Entity_Id;
begin
Check_SPARK_05_Restriction ("incomplete type is not allowed", N);
- -- The incomplete type declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
Generate_Definition (Defining_Identifier (N));
-- Process an incomplete declaration. The identifier must not have been
Set_Private_Dependents (T, New_Elmt_List);
Set_Is_Pure (T, F);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Incomplete_Type_Decl;
-----------------------------------
--------------------------------
procedure Analyze_Number_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
E : constant Node_Id := Expression (N);
Id : constant Entity_Id := Defining_Identifier (N);
Index : Interp_Index;
It : Interp;
T : Entity_Id;
- -- Start of processing for Analyze_Number_Declaration
-
begin
- -- The number declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
Generate_Definition (Id);
Enter_Name (Id);
Set_Etype (Id, Universal_Integer);
Set_Ekind (Id, E_Named_Integer);
Set_Is_Frozen (Id, True);
-
- Restore_Globals;
return;
end if;
Set_Ekind (Id, E_Constant);
Set_Never_Set_In_Source (Id, True);
Set_Is_True_Constant (Id, True);
-
- Restore_Globals;
return;
end if;
Rewrite (E, Make_Integer_Literal (Sloc (N), 1));
Set_Etype (E, Any_Type);
end if;
-
- Restore_Globals;
end Analyze_Number_Declaration;
-----------------------------
--------------------------------
procedure Analyze_Object_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ Id : constant Entity_Id := Defining_Identifier (N);
Act_T : Entity_Id;
T : Entity_Id;
-- Any other relevant delayed aspects on object declarations ???
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
-----------------
-- Count_Tasks --
-----------------
return False;
end Delayed_Aspect_Present;
- ---------------------
- -- Restore_Globals --
- ---------------------
+ -- Local variables
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Analyze_Object_Declaration
end if;
end if;
- -- The object declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
+ -- 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.
Set_Ghost_Mode (N, Prev_Entity);
and then Analyzed (N)
and then No (Expression (N))
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Freeze_Before (N, T);
Set_Is_Frozen (Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
Check_No_Hidden_State (Id);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Object_Declaration;
---------------------------
-------------------------------------------
procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Indic : constant Node_Id := Subtype_Indication (N);
- T : constant Entity_Id := Defining_Identifier (N);
+ Indic : constant Node_Id := Subtype_Indication (N);
+ T : constant Entity_Id := Defining_Identifier (N);
Parent_Base : Entity_Id;
Parent_Type : Entity_Id;
begin
- -- The private extension declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- Ada 2005 (AI-251): Decorate all names in list of ancestor interfaces
if Is_Non_Empty_List (Interface_List (N)) then
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, T);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Private_Extension_Declaration;
---------------------------------
(N : Node_Id;
Skip : Boolean := False)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
R_Checks : Check_Result;
T : Entity_Id;
begin
- -- The subtype declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
Generate_Definition (Id);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Init_Size_Align (Id);
end if;
Analyze_Dimension (N);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Subtype_Declaration;
--------------------------------
------------------------
procedure Analyze_Assignment (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Lhs : constant Node_Id := Name (N);
- Rhs : constant Node_Id := Expression (N);
+ Lhs : constant Node_Id := Name (N);
+ Rhs : constant Node_Id := Expression (N);
T1 : Entity_Id;
T2 : Entity_Id;
Decl : Node_Id;
-- the assignment, and at the end of processing before setting any new
-- current values in place.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
procedure Set_Assignment_Type
(Opnd : Node_Id;
Opnd_Type : in out Entity_Id);
end if;
end Kill_Lhs;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-------------------------
-- Set_Assignment_Type --
-------------------------
end if;
end Set_Assignment_Type;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Assignment
begin
Analyze (Lhs);
- -- The left hand side of an assignment may reference an entity subject
- -- to pragma Ghost with policy Ignore. Set the mode now to ensure that
- -- any nodes generated during analysis and expansion are properly
- -- flagged as ignored Ghost.
+ -- An assignment statement is Ghost when the left hand side denotes a
+ -- 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);
Analyze (Rhs);
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
"specified??", Lhs);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Error of assigning to limited type. We do however allow this in
Explain_Limited_Type (T1, Lhs);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be
then
Error_Msg_N ("invalid use of incomplete type", Lhs);
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if Rhs = Error then
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- If we know the right hand side is non-null, then we convert to the
end;
Analyze_Dimension (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Assignment;
-----------------------------
---------------------------------------------
procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Scop : constant Entity_Id := Current_Scope;
- Subp_Id : constant Entity_Id :=
+ Scop : constant Entity_Id := Current_Scope;
+ Subp_Id : constant Entity_Id :=
Analyze_Subprogram_Specification (Specification (N));
begin
- -- The abstract subprogram declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Subp_Id);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Subp_Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Abstract_Subprogram_Declaration;
---------------------------------
----------------------------
procedure Analyze_Procedure_Call (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
procedure Analyze_Call_And_Resolve;
-- Do Analyze and Resolve calls for procedure call
-- At end, check illegal order dependence.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------------
-- Analyze_Call_And_Resolve --
------------------------------
end if;
end Analyze_Call_And_Resolve;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Local variables
Actuals : constant List_Id := Parameter_Associations (N);
Actual : Node_Id;
New_N : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Procedure_Call
begin
return;
end if;
- -- The name of the procedure call may reference an entity subject to
- -- pragma Ghost with policy Ignore. Set the mode now to ensure that any
- -- nodes generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
+ -- A procedure call is Ghost when its name denotes a Ghost procedure.
+ -- Set the mode now to ensure that any nodes generated during analysis
+ -- and expansion are properly marked as Ghost.
Set_Ghost_Mode (N);
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
elsif Is_Entity_Name (P)
Error_Msg_N ("invalid procedure or entry call", N);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Procedure_Call;
------------------------------
-- the subprogram, or to perform conformance checks.
procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Body_Spec : Node_Id := Specification (N);
Body_Id : Entity_Id := Defining_Entity (Body_Spec);
-- Determine whether subprogram Subp_Id is a primitive of a concurrent
-- type that implements an interface and has a private view.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
procedure Set_Trivial_Subprogram (N : Node_Id);
-- Sets the Is_Trivial_Subprogram flag in both spec and body of the
-- subprogram whose body is being analyzed. N is the statement node
return False;
end Is_Private_Concurrent_Primitive;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
----------------------------
-- Set_Trivial_Subprogram --
----------------------------
end if;
end Verify_Overriding_Indicator;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Subprogram_Body_Helper
begin
if Is_Generic_Subprogram (Prev_Id) then
Spec_Id := Prev_Id;
- -- The corresponding spec may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged
- -- as ignored Ghost.
+ -- A subprogram body is Ghost when it is stand alone and subject
+ -- to pragma Ghost or when the corresponding spec is 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);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Check_Missing_Return;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
-- enter name will post error.
Enter_Name (Body_Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
if Is_Private_Concurrent_Primitive (Body_Id) then
Spec_Id := Disambiguate_Spec;
- -- The corresponding spec may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged
- -- as ignored Ghost.
+ -- A subprogram body is Ghost when it is stand alone and
+ -- subject to pragma Ghost or when the corresponding spec is
+ -- 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);
else
Spec_Id := Find_Corresponding_Spec (N);
- -- The corresponding spec may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged
- -- as ignored Ghost.
+ -- A subprogram body is Ghost when it is stand alone and
+ -- subject to pragma Ghost or when the corresponding spec is
+ -- 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);
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
else
Spec_Id := Corresponding_Spec (N);
- -- The corresponding spec may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged
- -- as ignored Ghost.
+ -- A subprogram body is Ghost when it is stand alone and subject
+ -- to pragma Ghost or when the corresponding spec is 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);
end if;
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
end;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Subprogram_Body_Helper;
---------------------------------
------------------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Scop : constant Entity_Id := Current_Scope;
Designator : Entity_Id;
Is_Completion : Boolean;
-- Indicates whether a null procedure declaration is a completion
- -- Start of processing for Analyze_Subprogram_Declaration
-
begin
- -- The subprogram declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- Null procedures are not allowed in SPARK
if Nkind (Specification (N)) = N_Procedure_Specification
-- The null procedure acts as a body, nothing further is needed
if Is_Completion then
- Restore_Globals;
return;
end if;
end if;
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Designator);
end if;
-
- Restore_Globals;
end Analyze_Subprogram_Declaration;
--------------------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
end if;
end if;
- -- The corresponding spec of the package body may be subject to pragma
- -- Ghost with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
+ -- A package body is Ghost when the corresponding spec is Ghost. Set
+ -- 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);
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Package_Body_Helper;
------------------------------
---------------------------------
procedure Analyze_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Id : constant Node_Id := Defining_Entity (N);
Body_Required : Boolean;
PF : Boolean;
-- True when in the context of a declared pure library unit
- -- Start of processing for Analyze_Package_Declaration
-
begin
if Debug_Flag_C then
Write_Str ("==> package spec ");
Indent;
end if;
- -- The package declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Package);
-- package Pkg is ...
if From_Limited_With (Id) then
- Restore_Globals;
return;
end if;
Write_Location (Sloc (N));
Write_Eol;
end if;
-
- Restore_Globals;
end Analyze_Package_Declaration;
-----------------------------------
--------------------------------------
procedure Analyze_Private_Type_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Enclosing_Lib_Unit_Entity);
begin
- -- The private type declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
Generate_Definition (Id);
Set_Is_Pure (Id, PF);
Init_Size_Align (Id);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Private_Type_Declaration;
----------------------------------
-- there is more than one element in the list.
procedure Analyze_Exception_Renaming (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Entity (N);
- Nam : constant Node_Id := Name (N);
+ Id : constant Entity_Id := Defining_Entity (N);
+ Nam : constant Node_Id := Name (N);
begin
- -- The exception renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
Enter_Name (Id);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Exception_Renaming;
---------------------------
(N : Node_Id;
K : Entity_Kind)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- New_P : constant Entity_Id := Defining_Entity (N);
+ New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Inst : Boolean := False;
return;
end if;
- -- The generic renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
Generate_Definition (New_P);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Renaming;
-----------------------------
return False;
end In_Generic_Scope;
- -- Local variables
-
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Analyze_Object_Renaming
begin
return;
end if;
- -- The object renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("object renaming is not allowed", N);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
-- Deal with dimensions
Analyze_Dimension (N);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Object_Renaming;
------------------------------
------------------------------
procedure Analyze_Package_Renaming (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Spec : Node_Id;
- -- Start of processing for Analyze_Package_Renaming
-
begin
if Name (N) = Error then
return;
end if;
- -- The package renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- Check for Text_IO special unit (we may be renaming a Text_IO child)
Check_Text_IO_Special_Unit (Name (N));
-- subtypes again, so they are compatible with types in their class.
if not Is_Generic_Instance (Old_P) then
- Restore_Globals;
return;
else
Spec := Specification (Unit_Declaration_Node (Old_P));
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
-
- Restore_Globals;
end Analyze_Package_Renaming;
-------------------------------
-- defaulted formal subprogram when the actual for a related formal
-- type is class-wide.
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Inst_Node : Node_Id := Empty;
+ Inst_Node : Node_Id := Empty;
New_S : Entity_Id;
-- Start of processing for Analyze_Subprogram_Renaming
begin
- -- The subprogram renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during analysis and expansion are properly flagged as
- -- ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- We must test for the attribute renaming case before the Analyze
-- call because otherwise Sem_Attr will complain that the attribute
-- is missing an argument when it is analyzed.
Analyze (N);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Subprogram_Renaming;
-------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
CCase : Node_Id;
Restore_Scope : Boolean := False;
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
(N : Node_Id;
Expr_Val : out Boolean)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
- Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1));
+ Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
-- Set the Ghost mode in effect from the pragma. Due to the delayed
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_External_Property_In_Decl_Part;
---------------------------------
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
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;
+
begin
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
-- is not desired at this point.
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Expr : Node_Id;
New_Args : List_Id;
-- Start of processing for Assert
begin
- -- Ensure that analysis and expansion produce Ghost nodes if the
- -- pragma itself is Ghost.
-
- Set_Ghost_Mode (N);
-
-- Assert is an Ada 2005 RM-defined pragma
if Prag_Id = Pragma_Assert then
Pragma_Argument_Associations => New_Args));
Analyze (N);
-
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
end Assert;
----------------------
-- allowed, since they have special meaning for Check_Policy.
when Pragma_Check => Check : declare
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Cname : Name_Id;
Eloc : Source_Ptr;
Expr : Node_Id;
Str : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
- -- Ensure that analysis and expansion produce Ghost nodes if the
- -- pragma itself is Ghost.
+ -- 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);
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Check;
--------------------------
-- [,[Message =>] String_Expression]);
when Pragma_Invariant => Invariant : declare
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Discard : Boolean;
Typ : Entity_Id;
Type_Id : Node_Id;
if Class_Present (N) then
Set_Has_Inheritable_Invariants (Typ);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
end Invariant;
----------------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
return;
end Resolution_Failed;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Resolve
begin
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.
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
elsif Etype (N) = Any_Type then
Debug_A_Exit ("resolving ", N, " (done, Etype = Any_Type)");
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
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
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;
end if;
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
-- Rewrite_Renamed_Operator.
if Analyzed (N) then
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
if Nkind (N) not in N_Subexpr then
Debug_A_Exit ("resolving ", N, " (done)");
Expand (N);
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Expand (N);
end if;
+
+ Ghost_Mode := Save_Ghost_Mode;
end Resolve;
-------------
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (Typ);
Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
Expr : Node_Id;
Stmt : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Build_Default_Init_Cond_Procedure_Body
begin
return;
end if;
- -- Ensure that the analysis and expansion produce Ghost nodes if the
- -- type itself is Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now
+ -- to ensure that the analysis and expansion produce Ghost nodes.
Set_Ghost_Mode_From_Entity (Typ);
Set_Corresponding_Spec (Body_Decl, Proc_Id);
Insert_After_And_Analyze (Declaration_Node (Typ), Body_Decl);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Default_Init_Cond_Procedure_Body;
-- Local variables
---------------------------------------------------
procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Loc : constant Source_Ptr := Sloc (Typ);
- Prag : constant Node_Id :=
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Proc_Id : Entity_Id;
begin
return;
end if;
- -- Ensure that the analysis and expansion produce Ghost nodes if the
- -- type itself is Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the analysis and expansion produce Ghost nodes.
Set_Ghost_Mode_From_Entity (Typ);
Defining_Identifier => Make_Temporary (Loc, 'I'),
Parameter_Type => New_Occurrence_Of (Typ, Loc))))));
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Default_Init_Cond_Procedure_Declaration;
---------------------------
projects / gcc.git / commitdiff