+2015-05-26 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
+ restore the Ghost mode.
+ (Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
+ (Freeze_Type): Update the call to Set_Ghost_Mode.
+ (Restore_Globals): New routine.
+ * exp_ch5.adb Add with and use clauses for Ghost.
+ (Expand_N_Assignment_Statement): Capture, set and restore the
+ Ghost mode.
+ (Restore_Globals): New routine.
+ * exp_ch6.adb Add with and use clauses for Ghost.
+ (Expand_N_Procedure_Call_Statement): Capture, set and
+ restore the Ghost mode.
+ (Expand_N_Subprogram_Body):
+ Code cleanup. Capture, set and restore the Ghost mode.
+ (Expand_N_Subprogram_Declaration): Capture, set and restore the
+ Ghost mode.
+ (Restore_Globals): New routine.
+ * exp_ch7.adb Add with and use clauses for Ghost.
+ (Expand_N_Package_Body): Capture, set and restore the Ghost mode.
+ (Expand_N_Package_Declaration): Capture, set and restore the
+ Ghost mode.
+ (Wrap_HSS_In_Block): Create a proper identifier for the block.
+ * exp_ch8.adb Add with and use clauses for Ghost.
+ (Expand_N_Exception_Renaming_Declaration): Code
+ cleanup. Capture, set and restore the Ghost mode.
+ (Expand_N_Object_Renaming_Declaration): Capture, set and restore
+ the Ghost mode.
+ (Expand_N_Package_Renaming_Declaration): Capture, set and restore the
+ Ghost mode.
+ (Expand_N_Subprogram_Renaming_Declaration): Capture, set and
+ restore the Ghost mode.
+ * exp_ch11.adb (Expand_N_Exception_Declaration): Code
+ cleanup. Capture, set and restore the Ghost mode.
+ * exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
+ not initialize the dispatch table slot of a Ghost subprogram.
+ * exp_prag.adb Add with and use clauses for Ghost.
+ (Expand_Pragma_Check): Capture, set and restore the Ghost mode.
+ (Expand_Pragma_Contract_Cases): Capture, set and restore the
+ Ghost mode.
+ (Expand_Pragma_Initial_Condition): Capture, set and
+ restore the Ghost mode.
+ (Expand_Pragma_Loop_Variant): Capture,
+ set and restore the Ghost mode.
+ (Restore_Globals): New routine.
+ * exp_util.adb Add with and use clauses for Ghost.
+ (Make_Predicate_Call): Code cleanup. Capture, set and restore
+ the Ghost mode.
+ (Restore_Globals): New routine.
+ * freeze.adb (Freeze_Entity): Code cleanup. Update the call
+ to Set_Ghost_Mode.
+ * ghost.adb Add with and use clause for Sem_Prag.
+ (Check_Ghost_Completion): Code cleanup.
+ (Check_Ghost_Overriding): New routine.
+ (Check_Ghost_Policy): Code cleanup.
+ (Ghost_Entity): New routine.
+ (Is_Ghost_Declaration): Removed.
+ (Is_Ghost_Statement_Or_Pragma): Removed.
+ (Is_OK_Context): Reimplemented.
+ (Is_OK_Declaration): New routine.
+ (Is_OK_Pragma): New routine.
+ (Is_OK_Statement): New routine.
+ (Mark_Full_View_As_Ghost): New routine.
+ (Mark_Pragma_As_Ghost): New routine.
+ (Mark_Renaming_As_Ghost): New routine.
+ (Propagate_Ignored_Ghost_Code): Update the comment on usage.
+ (Set_From_Entity): New routine.
+ (Set_From_Policy): New routine.
+ (Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
+ (Set_Ghost_Mode_For_Freeze): Removed.
+ (Set_Ghost_Mode_From_Entity): New routine.
+ (Set_Ghost_Mode_From_Policy): Removed.
+ * ghost.ads (Check_Ghost_Overriding): New routine.
+ (Mark_Full_View_As_Ghost): New routine.
+ (Mark_Pragma_As_Ghost): New routine.
+ (Mark_Renaming_As_Ghost): New routine.
+ (Set_Ghost_Mode): Update the parameter profile. Update the
+ comment on usage.
+ (Set_Ghost_Mode_For_Freeze): Removed.
+ (Set_Ghost_Mode_From_Entity): New routine.
+ * sem_ch3.adb (Analyze_Full_Type_Declaration):
+ Capture and restore the Ghost mode. Mark a type
+ as Ghost regardless of whether it comes from source.
+ (Analyze_Incomplete_Type_Decl): Capture, set and restore the
+ Ghost mode.
+ (Analyze_Number_Declaration): Capture and restore the Ghost mode.
+ (Analyze_Object_Declaration): Capture and restore the Ghost mode.
+ (Analyze_Private_Extension_Declaration): Capture and
+ restore the Ghost mode.
+ (Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
+ (Process_Full_View): The full view inherits all Ghost-related
+ attributes from the private view.
+ (Restore_Globals): New routine.
+ * sem_ch5.adb (Analyze_Assignment): Capture and restore the
+ Ghost mode.
+ (Restore_Globals): New routine.
+ * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
+ Code cleanup. Capture and restore the Ghost mode. Mark a
+ subprogram as Ghost regarless of whether it comes from source.
+ (Analyze_Procedure_Call): Capture and restore the Ghost mode.
+ (Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
+ (Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
+ (New_Overloaded_Entity): Ensure that a
+ parent subprogram and an overriding subprogram have compatible
+ Ghost policies.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
+ the Ghost mode.
+ (Analyze_Package_Declaration): Capture and
+ restore the Ghost mode. Mark a package as Ghost when it is
+ declared in a Ghost region.
+ (Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
+ (Restore_Globals): New routine.
+ * sem_ch8.adb (Analyze_Exception_Renaming): Code
+ reformatting. Capture and restore the Ghost mode. A renaming
+ becomes Ghost when its name references a Ghost entity.
+ (Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
+ renaming becomes Ghost when its name references a Ghost entity.
+ (Analyze_Object_Renaming): Capture and restore the Ghost mode. A
+ renaming becomes Ghost when its name references a Ghost entity.
+ (Analyze_Package_Renaming): Capture and restore the Ghost mode. A
+ renaming becomes Ghost when its name references a Ghost entity.
+ (Analyze_Subprogram_Renaming): Capture and restore the Ghost
+ mode. A renaming becomes Ghost when its name references a
+ Ghost entity.
+ * sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
+ and restore the Ghost mode.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
+ restore the Ghost mode.
+ (Analyze_Generic_Subprogram_Declaration):
+ Capture and restore the Ghost mode.
+ * sem_ch13.adb Add with and use clauses for Ghost.
+ (Add_Invariant): New routine.
+ (Add_Invariants): Factor out code.
+ (Add_Predicate): New routine.
+ (Add_Predicates): Factor out code.
+ (Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
+ set and restore the Ghost mode.
+ (Build_Invariant_Procedure): Code cleanup.
+ (Build_Predicate_Functions): Capture, set and
+ restore the Ghost mode. Mark the generated functions as Ghost.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
+ Capture, set and restore the Ghost mode.
+ (Analyze_External_Property_In_Decl_Part): Capture, set and restore
+ the Ghost mode.
+ (Analyze_Initial_Condition_In_Decl_Part):
+ Capture, set and restore the Ghost mode.
+ (Analyze_Pragma):
+ Code cleanup. Capture, set and restore the Ghost mode. Flag
+ pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
+ Unreferenced_Objects as illegal when it applies to both Ghost
+ and living arguments. Pragma Ghost cannot apply to synchronized
+ objects.
+ (Check_Kind): Moved to the spec of Sem_Prag.
+ (Process_Inline): Flag the pragma as illegal when it applies to
+ both Ghost and living arguments.
+ (Restore_Globals): New routine.
+ * sem_prag.ads Add pragma Default_Initial_Condition
+ to table Assertion_Expression_Pragma. Add new table
+ Is_Aspect_Specifying_Pragma.
+ (Check_Kind): Moved from body of Sem_Prag.
+ * sem_util.adb Add with and use clauses for Ghost.
+ (Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
+ the Ghost mode.
+ (Build_Default_Init_Cond_Procedure_Declaration):
+ Capture, set and restore the Ghost mode. Mark the default
+ initial condition procedure as Ghost when it is declared
+ in a Ghost region.
+ (Is_Renaming_Declaration): New routine.
+ (Policy_In_List): Account for the single argument version of
+ Check_Pragma.
+ * sem_util.ads (Is_Renaming_Declaration): New routine.
+ * sinfo.adb (Is_Ghost_Pragma): New routine.
+ (Set_Is_Ghost_Pragma): New routine.
+ * sinfo.ads New attribute Is_Ghost_Pragma.
+ (Is_Ghost_Pragma): New routine along with pragma Inline.
+ (Set_Is_Ghost_Pragma): New routine along with pragma Inline.
+
2015-05-26 Robert Dewar <dewar@adacore.com>
* sem_ch3.adb, sem_aux.adb, sem_aux.ads, exp_ch6.adb, sprint.adb:
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
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
- Loc : constant Source_Ptr := Sloc (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
- L : List_Id := New_List;
+ Loc : constant Source_Ptr := Sloc (N);
+ Ex_Id : Entity_Id;
Flag_Id : Entity_Id;
-
- Name_Exname : constant Name_Id := New_External_Name (Chars (Id), 'E');
- Exname : constant Node_Id :=
- Make_Defining_Identifier (Loc, Name_Exname);
+ L : List_Id := New_List;
procedure Force_Static_Allocation_Of_Referenced_Objects
(Aggregate : Node_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 :=
+ Make_Defining_Identifier (Loc, New_External_Name (Chars (Id), 'E'));
+
Insert_Action (N,
Make_Object_Declaration (Loc,
- Defining_Identifier => Exname,
+ Defining_Identifier => Ex_Id,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Standard_String, Loc),
Expression =>
Make_String_Literal (Loc,
Strval => Fully_Qualified_Name_String (Id))));
- Set_Is_Statically_Allocated (Exname);
+ Set_Is_Statically_Allocated (Ex_Id);
-- Create the aggregate list for type Standard.Exception_Type:
-- Handled_By_Other component: False
Append_To (L,
Make_Attribute_Reference (Loc,
- Prefix => New_Occurrence_Of (Exname, Loc),
+ Prefix => New_Occurrence_Of (Ex_Id, Loc),
Attribute_Name => Name_Length));
-- Full_Name component: Standard.A_Char!(Nam'Address)
Append_To (L, Unchecked_Convert_To (Standard_A_Char,
Make_Attribute_Reference (Loc,
- Prefix => New_Occurrence_Of (Exname, Loc),
+ Prefix => New_Occurrence_Of (Ex_Id, Loc),
Attribute_Name => Name_Address)));
-- HTable_Ptr component: null
and then not Restriction_Active (No_Exception_Registration)
then
L := New_List (
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (RTE (RE_Register_Exception), Loc),
- Parameter_Associations => New_List (
- Unchecked_Convert_To (RTE (RE_Exception_Data_Ptr),
- Make_Attribute_Reference (Loc,
- Prefix => New_Occurrence_Of (Id, Loc),
- Attribute_Name => Name_Unrestricted_Access)))));
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (RTE (RE_Register_Exception), Loc),
+ Parameter_Associations => New_List (
+ Unchecked_Convert_To (RTE (RE_Exception_Data_Ptr),
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Occurrence_Of (Id, Loc),
+ Attribute_Name => Name_Unrestricted_Access)))));
Set_Register_Exception_Call (Id, First (L));
if not Is_Library_Level_Entity (Id) then
- Flag_Id := Make_Defining_Identifier (Loc,
- New_External_Name (Chars (Id), 'F'));
+ Flag_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Id), 'F'));
Insert_Action (N,
Make_Object_Declaration (Loc,
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;
---------------------------------------------
Def_Id : constant Entity_Id := Defining_Identifier (N);
B_Id : constant Entity_Id := Base_Type (Def_Id);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
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
Def_Id : constant Entity_Id := Defining_Identifier (N);
Expr : constant Node_Id := Expression (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Obj_Def : constant Node_Id := Object_Definition (N);
Typ : constant Entity_Id := Etype (Def_Id);
-- 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 --
-------------------------
-- Local variables
- Next_N : constant Node_Id := Next (N);
- Id_Ref : Node_Id;
+ Next_N : constant Node_Id := Next (N);
+ Id_Ref : Node_Id;
+ Tag_Assign : Node_Id;
Init_After : Node_Id := N;
-- Node after which the initialization actions are to be inserted. This
-- which case the init proc call must be inserted only after the bodies
-- of the shared variable procedures have been seen.
- Tag_Assign : Node_Id;
-
-- Start of processing for Expand_N_Object_Declaration
begin
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;
-- Ignore. Set the mode now to ensure that any nodes generated during
-- freezing are properly flagged as ignored Ghost.
- Set_Ghost_Mode_For_Freeze (Def_Id, N);
+ Set_Ghost_Mode (N, Def_Id);
-- Process any remote access-to-class-wide types designating the type
-- being frozen.
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;
-- cannot just be passed on to the back end in untransformed state.
procedure Expand_N_Assignment_Statement (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
+ 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);
Rhs : constant Node_Id := Expression (N);
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
+ -- Start of processing for Expand_N_Assignment_Statement
+
begin
+ -- The assignment statement may be Ghost if the left hand side is Ghost.
+ -- Set the mode now to ensure that any nodes generated during expansion
+ -- are properly flagged as ignored 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
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
+ Restore_Globals;
return;
end if;
Rewrite (N, Call);
Analyze (N);
+
+ Restore_Globals;
return;
end if;
end;
Convert_Aggr_In_Assignment (N);
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
+
+ Restore_Globals;
return;
end if;
if not Crep then
Expand_Bit_Packed_Element_Set (N);
+ Restore_Globals;
return;
-- Change of representation case
-- Nothing to do for valuetypes
-- ??? Set_Scope_Is_Transient (False);
+ Restore_Globals;
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;
return;
end if;
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
+ Restore_Globals;
return;
end Tagged_Case;
end loop;
Expand_Assign_Array (N, Actual_Rhs);
+ Restore_Globals;
return;
end;
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
+ Restore_Globals;
return;
-- Scalar types. This is where we perform the processing related to the
end if;
end if;
+ Restore_Globals;
+
exception
when RE_Not_Available =>
+ Restore_Globals;
return;
end Expand_N_Assignment_Statement;
with Exp_Unst; use Exp_Unst;
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;
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
+ GM : 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.
+
+ Set_Ghost_Mode (N);
Expand_Call (N);
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
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);
- H : constant Node_Id := Handled_Statement_Sequence (N);
+ HSS : constant Node_Id := Handled_Statement_Sequence (N);
Body_Id : Entity_Id;
Except_H : Node_Id;
L : List_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 --
----------------
and then not Comes_From_Source (Parent (S))
then
Loc := Sloc (Last_Stmt);
- elsif Present (End_Label (H)) then
- Loc := Sloc (End_Label (H));
+ elsif Present (End_Label (HSS)) then
+ Loc := Sloc (End_Label (HSS));
else
Loc := Sloc (Last_Stmt);
end if;
end if;
end Add_Return;
+ ---------------------
+ -- Restore_Globals --
+ ---------------------
+
+ procedure Restore_Globals is
+ begin
+ Ghost_Mode := GM;
+ end Restore_Globals;
+
-- 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.
+
+ Set_Ghost_Mode (N);
+
-- 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.
if Is_Non_Empty_List (Declarations (N)) then
L := Declarations (N);
else
- L := Statements (H);
+ L := Statements (HSS);
end if;
-- If local-exception-to-goto optimization active, insert dummy push
-- or to the last declaration if there are no statements present.
-- It is the node after which the pop's are generated.
- if Is_Non_Empty_List (Statements (H)) then
- LS := Last (Statements (H));
+ if Is_Non_Empty_List (Statements (HSS)) then
+ LS := Last (Statements (HSS));
else
LS := Last (L);
end if;
Set_Handled_Statement_Sequence (N,
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
+
+ Restore_Globals;
return;
end if;
end if;
-- the subprogram.
if Ekind_In (Spec_Id, E_Procedure, E_Generic_Procedure) then
- Add_Return (Statements (H));
+ Add_Return (Statements (HSS));
- if Present (Exception_Handlers (H)) then
- Except_H := First_Non_Pragma (Exception_Handlers (H));
+ if Present (Exception_Handlers (HSS)) then
+ Except_H := First_Non_Pragma (Exception_Handlers (HSS));
while Present (Except_H) loop
Add_Return (Statements (Except_H));
Next_Non_Pragma (Except_H);
elsif Has_Missing_Return (Spec_Id) then
declare
- Hloc : constant Source_Ptr := Sloc (H);
+ Hloc : constant Source_Ptr := Sloc (HSS);
Blok : constant Node_Id :=
Make_Block_Statement (Hloc,
- Handled_Statement_Sequence => H);
+ Handled_Statement_Sequence => HSS);
Rais : constant Node_Id :=
Make_Raise_Program_Error (Hloc,
Reason => PE_Missing_Return);
then
Unest_Bodies.Append ((Spec_Id, N));
end if;
+
+ Restore_Globals;
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
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Subp : constant Entity_Id := Defining_Entity (N);
Scop : constant Entity_Id := Scope (Subp);
- Prot_Decl : Node_Id;
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;
--------------------------------
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Lib; use Lib;
with Nlists; use Nlists;
with Nmake; use Nmake;
-----------------------
procedure Wrap_HSS_In_Block is
- Block : Node_Id;
- End_Lab : Node_Id;
+ Block : Node_Id;
+ Block_Id : Entity_Id;
+ End_Lab : Node_Id;
begin
-- Preserve end label to provide proper cross-reference information
Block :=
Make_Block_Statement (Loc, Handled_Statement_Sequence => HSS);
+ Block_Id := New_Internal_Entity (E_Block, Current_Scope, Loc, 'B');
+ Set_Identifier (Block, New_Occurrence_Of (Block_Id, Loc));
+ Set_Etype (Block_Id, Standard_Void_Type);
+ Set_Block_Node (Block_Id, Identifier (Block));
+
-- Signal the finalization machinery that this particular block
-- contains the original context.
-- 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;
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.
+
+ Set_Ghost_Mode (N);
+
-- This is done only for non-generic packages
if Ekind (Spec_Ent) = E_Package then
end;
end if;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
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;
-----------------------------
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
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;
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
- Decl : constant Node_Id := Debug_Renaming_Declaration (N);
+ GM : 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.
+
+ Set_Ghost_Mode (N);
+
+ Decl := Debug_Renaming_Declaration (N);
+
if Present (Decl) then
Insert_Action (N, Decl);
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
end if;
end Evaluation_Required;
+ -- Local variables
+
+ GM : 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.
+
+ Set_Ghost_Mode (N);
+
-- Perform name evaluation if required
if Evaluation_Required (Nam) then
if Present (Decl) then
Insert_Action (N, Decl);
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
- Decl : constant Node_Id := Debug_Renaming_Declaration (N);
+ GM : 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.
+
+ Set_Ghost_Mode (N);
+
+ Decl := Debug_Renaming_Declaration (N);
+
if Present (Decl) then
-- If we are in a compilation unit, then this is an outer
Insert_Action (N, Decl);
end if;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
-- Local variables
+ GM : 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 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.
+
+ 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.
end if;
end;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;
begin
pragma Assert (Is_Frozen (Typ));
- -- The tagged type for which the dispatch table is being build 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 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.
- Set_Ghost_Mode_For_Freeze (Typ, Typ);
+ Set_Ghost_Mode (Declaration_Node (Typ), Typ);
-- Handle cases in which there is no need to build the dispatch table
E := Ultimate_Alias (Prim);
Prim_Pos := UI_To_Int (DT_Position (E));
- -- Do not reference predefined primitives because they are
- -- located in a separate dispatch table; skip entities with
- -- attribute Interface_Alias because they are only required
- -- to build secondary dispatch tables; skip abstract and
- -- eliminated primitives; for derivations of CPP types skip
- -- primitives located in the C++ part of the dispatch table
- -- because their slot is initialized by the IC routine.
+ -- Skip predefined primitives because they are located in a
+ -- separate dispatch table.
if not Is_Predefined_Dispatching_Operation (Prim)
and then not Is_Predefined_Dispatching_Operation (E)
+
+ -- Skip entities with attribute Interface_Alias because
+ -- those are only required to build secondary dispatch
+ -- tables.
+
and then not Present (Interface_Alias (Prim))
+
+ -- Skip abstract and eliminated primitives
+
and then not Is_Abstract_Subprogram (E)
and then not Is_Eliminated (E)
+
+ -- For derivations of CPP types skip primitives located in
+ -- the C++ part of the dispatch table because their slots
+ -- are initialized by the IC routine.
+
and then (not Is_CPP_Class (Root_Type (Typ))
or else Prim_Pos > CPP_Nb_Prims)
+
+ -- Skip ignored Ghost subprograms as those will be removed
+ -- from the executable.
+
+ and then not Is_Ignored_Ghost_Entity (E)
then
pragma Assert
(UI_To_Int (DT_Position (Prim)) <= Nb_Prim);
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;
--------------------------
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));
Msg : Node_Id;
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;
---------------------------------
-- Local variables
- Aggr : constant Node_Id :=
- Expression (First
- (Pragma_Argument_Associations (CCs)));
+ Aggr : constant Node_Id :=
+ Expression (First (Pragma_Argument_Associations (CCs)));
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+
Case_Guard : Node_Id;
CG_Checks : Node_Id;
CG_Stmts : List_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.
+
+ Set_Ghost_Mode (CCs);
+
Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-- Create the counter which tracks the number of case guards that
end if;
Append_To (Stmts, Conseq_Checks);
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
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
+
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
Pack_Id := Corresponding_Spec (Spec_Or_Body);
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.
+
+ Set_Ghost_Mode (Init_Cond);
+
-- The caller should check whether the package is subject to pragma
-- Initial_Condition.
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
+ Restore_Globals;
return;
end if;
Append_To (List, Check);
Analyze (Check);
+
+ Restore_Globals;
end Expand_Pragma_Initial_Condition;
------------------------------------
-- end loop;
procedure Expand_Pragma_Loop_Variant (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
-
Last_Var : constant Node_Id := Last (Pragma_Argument_Associations (N));
+ Loc : constant Source_Ptr := Sloc (N);
Curr_Assign : List_Id := No_List;
Flag_Id : Entity_Id := Empty;
end if;
end Process_Variant;
+ -- Local variables
+
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Expand_Pragma_Loop_Variant
begin
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.
+
+ Set_Ghost_Mode (N);
+
-- Locate the enclosing loop for which this assertion applies. In the
-- case of Ada 2012 array iteration, we might be dealing with nested
-- loops. Only the outermost loop has an identifier.
Variant := First (Pragma_Argument_Associations (N));
while Present (Variant) loop
Process_Variant (Variant, Is_Last => Variant = Last_Var);
-
Next (Variant);
end loop;
-- 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;
end Expand_Pragma_Loop_Variant;
--------------------------------
with Exp_Aggr; use Exp_Aggr;
with Exp_Ch6; use Exp_Ch6;
with Exp_Ch7; use Exp_Ch7;
+with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Expr);
+ 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
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.
+
+ Set_Ghost_Mode_From_Entity (Typ);
+
-- Call special membership version if requested and available
if Mem then
- declare
- PFM : constant Entity_Id := Predicate_Function_M (Typ);
- begin
- if Present (PFM) then
- return
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (PFM, Loc),
- Parameter_Associations => New_List (Relocate_Node (Expr)));
- end if;
- end;
+ 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)));
+
+ Restore_Globals;
+ return Call;
+ end if;
end if;
-- Case of calling normal predicate function
- return
- Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Predicate_Function (Typ), Loc),
- Parameter_Associations => New_List (Relocate_Node (Expr)));
+ Call :=
+ Make_Function_Call (Loc,
+ Name =>
+ New_Occurrence_Of (Predicate_Function (Typ), Loc),
+ Parameter_Associations => New_List (Relocate_Node (Expr)));
+
+ Restore_Globals;
+ return Call;
end Make_Predicate_Call;
--------------------------
Formal : Entity_Id;
Indx : Node_Id;
- Test_E : Entity_Id := E;
- -- This could use a comment ???
+ Has_Default_Initialization : Boolean := False;
+ -- This flag gets set to true for a variable with default initialization
Late_Freezing : Boolean := False;
-- Used to detect attempt to freeze function declared in another unit
Result : List_Id := No_List;
-- List of freezing actions, left at No_List if none
- Has_Default_Initialization : Boolean := False;
- -- This flag gets set to true for a variable with default initialization
+ Test_E : Entity_Id := E;
+ -- This could use a comment ???
procedure Add_To_Result (N : Node_Id);
-- N is a freezing action to be appended to the Result
-- Ignore. Set the mode now to ensure that any nodes generated during
-- freezing are properly flagged as ignored Ghost.
- Set_Ghost_Mode_For_Freeze (E, N);
+ Set_Ghost_Mode_From_Entity (E);
-- 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
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
-- Local Subprograms --
-----------------------
+ 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.
+
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
- -- Subsidiary to Set_Ghost_Mode_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.
+ -- 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.
----------------------------
-- Add_Ignored_Ghost_Unit --
then
Error_Msg_Sloc := Sloc (Full_View);
- 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", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
+ Error_Msg_N
+ ("\& completed # with ghost policy `Ignore`", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
- 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", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
+ Error_Msg_N
+ ("\& completed # with ghost policy `Check`", Partial_View);
end if;
end Check_Ghost_Completion;
-------------------------
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
- function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
- -- Determine whether node Decl is a Ghost declaration or appears
- -- within a Ghost declaration.
-
- function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
- -- Determine whether statement or pragma N is Ghost or appears within
- -- a Ghost statement or pragma. To qualify as such, N must either
- -- 1) Occur within a ghost subprogram or package
- -- 2) Denote a call to a ghost procedure
- -- 3) Denote an assignment statement whose target is a ghost
- -- variable.
- -- 4) Denote a pragma that mentions a ghost entity
-
- --------------------------
- -- Is_Ghost_Declaration --
- --------------------------
-
- function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
- Par : Node_Id;
+ 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
+
+ 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
+
+ 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
+
+ -----------------------
+ -- Is_OK_Declaration --
+ -----------------------
+
+ function Is_OK_Declaration (Decl : Node_Id) return Boolean is
+ function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
+ -- Determine whether node Ren_Decl denotes a renaming declaration
+ -- with a Ghost name.
+
+ -----------------------
+ -- 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;
Subp_Id : Entity_Id;
+ -- Start of processing for Is_OK_Declaration
+
begin
- -- Climb the parent chain looking for an object declaration
+ if Is_Declaration (Decl) then
- Par := Decl;
- while Present (Par) loop
- if Is_Declaration (Par) then
+ -- A renaming declaration is Ghost when it renames a Ghost
+ -- entity.
- -- A declaration is Ghost when it appears within a Ghost
- -- package or subprogram.
+ if Is_Ghost_Renaming (Decl) then
+ return True;
- if Ghost_Mode > None then
- return True;
+ -- The declaration may not have been analyzed yet, determine
+ -- whether it is subject to pragma Ghost.
- -- Otherwise the declaration may not have been analyzed yet,
- -- determine whether it is subject to aspect/pragma Ghost.
+ elsif Is_Subject_To_Ghost (Decl) then
+ return True;
- else
- return Is_Subject_To_Ghost (Par);
- end if;
+ -- The declaration appears within an assertion expression
- -- Special cases
+ elsif In_Assertion_Expr > 0 then
+ return True;
+ end if;
- -- A reference to a Ghost entity may appear as the default
- -- expression of a formal parameter of a subprogram body. This
- -- context must be treated as suitable because the relation
- -- between the spec and the body has not been established and
- -- the body is not marked as Ghost yet. The real check was
- -- performed on the spec.
+ -- Special cases
- elsif Nkind (Par) = N_Parameter_Specification
- and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
- then
- return True;
+ -- A reference to a Ghost entity may appear as the default
+ -- expression of a formal parameter of a subprogram body. This
+ -- context must be treated as suitable because the relation
+ -- between the spec and the body has not been established and
+ -- the body is not marked as Ghost yet. The real check was
+ -- performed on the spec.
- -- References to Ghost entities may be relocated in internally
- -- generated bodies.
+ elsif Nkind (Decl) = N_Parameter_Specification
+ and then Nkind (Parent (Parent (Decl))) = N_Subprogram_Body
+ then
+ return True;
- elsif Nkind (Par) = N_Subprogram_Body
- and then not Comes_From_Source (Par)
- then
- Subp_Id := Corresponding_Spec (Par);
+ -- References to Ghost entities may be relocated in internally
+ -- generated bodies.
- -- The original context is an expression function that has
- -- been split into a spec and a body. The context is OK as
- -- long as the the initial declaration is Ghost.
+ elsif Nkind (Decl) = N_Subprogram_Body
+ and then not Comes_From_Source (Decl)
+ then
+ Subp_Id := Corresponding_Spec (Decl);
- if Present (Subp_Id) then
- Subp_Decl :=
- Original_Node (Unit_Declaration_Node (Subp_Id));
+ -- The original context is an expression function that has
+ -- been split into a spec and a body. The context is OK as
+ -- long as the initial declaration is Ghost.
- if Nkind (Subp_Decl) = N_Expression_Function then
- return Is_Subject_To_Ghost (Subp_Decl);
- end if;
+ if Present (Subp_Id) then
+ Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id));
+
+ if Nkind (Subp_Decl) = N_Expression_Function then
+ return Is_Subject_To_Ghost (Subp_Decl);
end if;
- -- Otherwise this is either an internal body or an internal
- -- completion. Both are OK because the real check was done
- -- before expansion activities.
+ -- Otherwise this is either an internal body or an internal
+ -- completion. Both are OK because the real check was done
+ -- before expansion activities.
+ else
return True;
end if;
-
- -- Prevent the search from going too far
-
- if Is_Body_Or_Package_Declaration (Par) then
- return False;
- end if;
-
- Par := Parent (Par);
- end loop;
+ end if;
return False;
- end Is_Ghost_Declaration;
+ end Is_OK_Declaration;
- ----------------------------------
- -- Is_Ghost_Statement_Or_Pragma --
- ----------------------------------
+ ------------------
+ -- Is_OK_Pragma --
+ ------------------
- function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
- function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
- -- Determine whether an arbitrary node denotes a reference to a
- -- Ghost entity.
+ function Is_OK_Pragma (Prag : Node_Id) return Boolean is
+ procedure Check_Policies (Prag_Nam : Name_Id);
+ -- Verify that the Ghost policy in effect is the same as the
+ -- assertion policy for pragma name Prag_Nam. Emit an error if
+ -- this is not the case.
- -------------------------------
- -- Is_Ghost_Entity_Reference --
- -------------------------------
+ --------------------
+ -- Check_Policies --
+ --------------------
- function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
- Ref : Node_Id;
+ procedure Check_Policies (Prag_Nam : Name_Id) is
+ AP : constant Name_Id := Check_Kind (Prag_Nam);
+ GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
- -- When the reference extracts a subcomponent, recover the
- -- related object (SPARK RM 6.9(1)).
-
- Ref := N;
- while Nkind_In (Ref, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component,
- N_Slice)
- loop
- Ref := Prefix (Ref);
- end loop;
-
- return
- Is_Entity_Name (Ref)
- and then Present (Entity (Ref))
- and then Is_Ghost_Entity (Entity (Ref));
- end Is_Ghost_Entity_Reference;
+ -- If the Ghost policy in effect at the point of a Ghost entity
+ -- reference is Ignore, then the assertion policy of the pragma
+ -- must be Ignore (SPARK RM 6.9(18)).
+
+ if GP = Name_Ignore and then AP /= Name_Ignore then
+ Error_Msg_N
+ ("incompatible ghost policies in effect", Ghost_Ref);
+ Error_Msg_NE
+ ("\ghost entity & has policy `Ignore`",
+ Ghost_Ref, Ghost_Id);
+
+ Error_Msg_Name_1 := AP;
+ Error_Msg_N
+ ("\assertion expression has policy %", Ghost_Ref);
+ end if;
+ end Check_Policies;
-- Local variables
- Arg : Node_Id;
- Stmt : Node_Id;
+ Arg : Node_Id;
+ Arg_Id : Entity_Id;
+ Prag_Id : Pragma_Id;
+ Prag_Nam : Name_Id;
- -- Start of processing for Is_Ghost_Statement_Or_Pragma
+ -- Start of processing for Is_OK_Pragma
begin
- if Nkind (N) = N_Pragma then
+ if Nkind (Prag) = N_Pragma then
+ Prag_Id := Get_Pragma_Id (Prag);
+ Prag_Nam := Original_Aspect_Pragma_Name (Prag);
- -- A pragma is Ghost when it appears within a Ghost package or
- -- subprogram.
+ -- A pragma that applies to a Ghost construct or specifies an
+ -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
- if Ghost_Mode > None then
+ if Is_Ghost_Pragma (Prag) then
return True;
- end if;
- -- A pragma is Ghost when it mentions a Ghost entity
+ -- An assertion expression is a Ghost pragma when it contains a
+ -- reference to a Ghost entity (SPARK RM 6.9(11)).
- Arg := First (Pragma_Argument_Associations (N));
- while Present (Arg) loop
- if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
- return True;
- end if;
+ elsif Assertion_Expression_Pragma (Prag_Id) then
- Next (Arg);
- end loop;
- end if;
+ -- Predicates are excluded from this category when they do
+ -- not apply to a Ghost subtype (SPARK RM 6.9(12)).
- Stmt := N;
- while Present (Stmt) loop
- if Is_Statement (Stmt) then
+ if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
+ Name_Predicate,
+ Name_Static_Predicate)
+ then
+ return False;
- -- A statement is Ghost when it appears within a Ghost
- -- package or subprogram.
+ -- Otherwise ensure that the assertion policy and the Ghost
+ -- policy are compatible (SPARK RM 6.9(18)).
- if Ghost_Mode > None then
+ else
+ Check_Policies (Prag_Nam);
return True;
+ end if;
- -- An assignment statement or a procedure call is Ghost when
- -- the name denotes a Ghost entity.
+ -- Several pragmas that may apply to a non-Ghost entity are
+ -- treated as Ghost when they contain a reference to a Ghost
+ -- entity (SPARK RM 6.9(12)).
- elsif Nkind_In (Stmt, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- return Is_Ghost_Entity_Reference (Name (Stmt));
- end if;
+ elsif Nam_In (Prag_Nam, Name_Global,
+ Name_Depends,
+ Name_Initializes,
+ Name_Refined_Global,
+ Name_Refined_Depends,
+ Name_Refined_State)
+ then
+ return True;
- -- Prevent the search from going too far
+ -- Otherwise a normal pragma is Ghost when it encloses a Ghost
+ -- name (SPARK RM 6.9(3)).
- elsif Is_Body_Or_Package_Declaration (Stmt) then
- return False;
- end if;
+ else
+ Arg := First (Pragma_Argument_Associations (Prag));
+ while Present (Arg) loop
+ Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
- Stmt := Parent (Stmt);
- end loop;
+ if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
+ return True;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+ end if;
return False;
- end Is_Ghost_Statement_Or_Pragma;
+ end Is_OK_Pragma;
- -- Start of processing for Is_OK_Ghost_Context
+ ---------------------
+ -- Is_OK_Statement --
+ ---------------------
- begin
- -- The Ghost entity appears within an assertion expression
+ function Is_OK_Statement (Stmt : Node_Id) return Boolean is
+ Nam_Id : Entity_Id;
- if In_Assertion_Expr > 0 then
- return True;
+ begin
+ -- An assignment statement or a procedure call is Ghost when the
+ -- name denotes a Ghost entity.
- -- The Ghost entity is part of a declaration or its completion
+ if Nkind_In (Stmt, N_Assignment_Statement,
+ N_Procedure_Call_Statement)
+ then
+ Nam_Id := Ghost_Entity (Name (Stmt));
- elsif Is_Ghost_Declaration (Context) then
- return True;
+ return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
+
+ -- 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
+ and then Nkind (Original_Node (Stmt)) = N_Pragma
+ and then Assertion_Expression_Pragma
+ (Get_Pragma_Id (Original_Node (Stmt)))
+ then
+ return True;
+ end if;
+
+ return False;
+ end Is_OK_Statement;
+
+ -- Local variables
- -- The Ghost entity is referenced within a Ghost statement
+ Par : Node_Id;
- elsif Is_Ghost_Statement_Or_Pragma (Context) then
+ -- Start of processing for Is_OK_Ghost_Context
+
+ begin
+ -- The context is Ghost when it appears within a Ghost package or
+ -- subprogram.
+
+ if Ghost_Mode > None then
return True;
-- Routine Expand_Record_Extension creates a parent subtype without
elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
+ -- Otherwise climb the parent chain looking for a suitable Ghost
+ -- context.
+
else
+ Par := Context;
+ while Present (Par) loop
+ if Is_Ignored_Ghost_Node (Par) then
+ return True;
+
+ -- A reference to a Ghost entity can appear within an aspect
+ -- specification (SPARK RM 6.9(11)).
+
+ elsif Nkind (Par) = N_Aspect_Specification then
+ return True;
+
+ elsif Is_OK_Declaration (Par) then
+ return True;
+
+ elsif Is_OK_Pragma (Par) then
+ return True;
+
+ elsif Is_OK_Statement (Par) then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ return False;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
return False;
end if;
end Is_OK_Ghost_Context;
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
- Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
- Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+ Error_Msg_NE ("\& declared with ghost policy `Check`", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy `Ignore`", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
- Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
- Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+ Error_Msg_NE ("\& declared with ghost policy `Ignore`", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy `Check`", Err_N, Id);
end if;
end Check_Ghost_Policy;
end if;
end Check_Ghost_Derivation;
+ ----------------------------
+ -- Check_Ghost_Overriding --
+ ----------------------------
+
+ procedure Check_Ghost_Overriding
+ (Subp : Entity_Id;
+ Overridden_Subp : Entity_Id)
+ is
+ Par_Subp : Entity_Id;
+
+ begin
+ if Present (Subp) and then Present (Overridden_Subp) then
+ Par_Subp := Ultimate_Alias (Overridden_Subp);
+
+ -- The Ghost policy in effect at the point of declaration of a parent
+ -- and an overriding subprogram must match (SPARK RM 6.9(17)).
+
+ if Is_Checked_Ghost_Entity (Par_Subp)
+ and then Is_Ignored_Ghost_Entity (Subp)
+ then
+ Error_Msg_N ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Par_Subp);
+ Error_Msg_N ("\& declared # with ghost policy `Check`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
+
+ elsif Is_Ignored_Ghost_Entity (Par_Subp)
+ and then Is_Checked_Ghost_Entity (Subp)
+ then
+ Error_Msg_N ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Par_Subp);
+ Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N ("\overridden # with ghost policy `Check`", Subp);
+ end if;
+ end if;
+ end Check_Ghost_Overriding;
+
+ ------------------
+ -- Ghost_Entity --
+ ------------------
+
+ function Ghost_Entity (N : Node_Id) return Entity_Id is
+ Ref : Node_Id;
+
+ begin
+ -- When the reference extracts a subcomponent, recover the related
+ -- object (SPARK RM 6.9(1)).
+
+ Ref := N;
+ while Nkind_In (Ref, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component,
+ N_Slice)
+ loop
+ Ref := Prefix (Ref);
+ end loop;
+
+ if Is_Entity_Name (Ref) then
+ return Entity (Ref);
+ else
+ return Empty;
+ end if;
+ end Ghost_Entity;
+
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
Ignored_Ghost_Units.Release;
end Lock;
+ -----------------------------
+ -- Mark_Full_View_As_Ghost --
+ -----------------------------
+
+ procedure Mark_Full_View_As_Ghost
+ (Priv_Typ : Entity_Id;
+ Full_Typ : Entity_Id)
+ is
+ Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
+
+ begin
+ if Is_Checked_Ghost_Entity (Priv_Typ) then
+ Set_Is_Checked_Ghost_Entity (Full_Typ);
+
+ 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);
+ end if;
+ end Mark_Full_View_As_Ghost;
+
+ --------------------------
+ -- Mark_Pragma_As_Ghost --
+ --------------------------
+
+ procedure Mark_Pragma_As_Ghost
+ (Prag : Node_Id;
+ Context_Id : Entity_Id)
+ is
+ begin
+ if Is_Checked_Ghost_Entity (Context_Id) then
+ Set_Is_Ghost_Pragma (Prag);
+
+ elsif Is_Ignored_Ghost_Entity (Context_Id) then
+ Set_Is_Ghost_Pragma (Prag);
+ Set_Is_Ignored_Ghost_Node (Prag);
+ Propagate_Ignored_Ghost_Code (Prag);
+ end if;
+ end Mark_Pragma_As_Ghost;
+
+ ----------------------------
+ -- Mark_Renaming_As_Ghost --
+ ----------------------------
+
+ procedure Mark_Renaming_As_Ghost
+ (Ren_Decl : Node_Id;
+ Nam_Id : Entity_Id)
+ is
+ Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
+
+ begin
+ if Is_Checked_Ghost_Entity (Nam_Id) then
+ Set_Is_Checked_Ghost_Entity (Ren_Id);
+
+ 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);
+ end if;
+ end Mark_Renaming_As_Ghost;
+
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
-- Set_Ghost_Mode --
--------------------
- procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is
- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+ 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 Id.
+ -- entity Ent_Id.
- procedure Set_Ghost_Mode_From_Policy;
+ 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_Ghost_Mode_From_Entity (Id : Entity_Id) is
+ procedure Set_From_Entity (Ent_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;
+ 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);
end if;
- end Set_Ghost_Mode_From_Entity;
+ end Set_From_Entity;
- --------------------------------
- -- Set_Ghost_Mode_From_Policy --
- --------------------------------
+ ---------------------
+ -- Set_From_Policy --
+ ---------------------
- procedure Set_Ghost_Mode_From_Policy is
+ procedure Set_From_Policy is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
- end Set_Ghost_Mode_From_Policy;
+ end Set_From_Policy;
-- Local variables
- Nam : Node_Id;
+ Nam_Id : Entity_Id;
-- Start of processing for Set_Ghost_Mode
if Is_Declaration (N) then
if Is_Subject_To_Ghost (N) then
- Set_Ghost_Mode_From_Policy;
+ Set_From_Policy;
-- The declaration denotes the completion of a deferred constant,
-- pragma Ghost appears on the partial declaration.
elsif Nkind (N) = N_Object_Declaration
and then Constant_Present (N)
- and then Present (Prev_Id)
+ and then Present (Id)
then
- Set_Ghost_Mode_From_Entity (Prev_Id);
+ Set_From_Entity (Id);
-- 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 (Prev_Id)
+ and then Present (Id)
then
- Set_Ghost_Mode_From_Entity (Prev_Id);
+ Set_From_Entity (Id);
end if;
-- The input denotes an assignment or a procedure call. In this case
elsif Nkind_In (N, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
- -- When the reference extracts a subcomponent, recover the related
- -- object (SPARK RM 6.9(1)).
-
- Nam := Name (N);
- while Nkind_In (Nam, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component,
- N_Slice)
- loop
- Nam := Prefix (Nam);
- end loop;
+ Nam_Id := Ghost_Entity (Name (N));
- if Is_Entity_Name (Nam)
- and then Present (Entity (Nam))
- then
- Set_Ghost_Mode_From_Entity (Entity (Nam));
+ if Present (Nam_Id) then
+ Set_From_Entity (Nam_Id);
end if;
-- The input denotes a package or subprogram body
elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
- if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id))
+ if (Present (Id) and then Is_Ghost_Entity (Id))
or else Is_Subject_To_Ghost (N)
then
- Set_Ghost_Mode_From_Policy;
+ Set_From_Policy;
+ end if;
+
+ -- The input denotes a pragma
+
+ elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
+ if Is_Ignored_Ghost_Node (N) then
+ Ghost_Mode := Ignore;
+ else
+ Ghost_Mode := Check;
end if;
+
+ -- The input denotes a freeze node
+
+ elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
+ Set_From_Entity (Id);
end if;
end Set_Ghost_Mode;
- -------------------------------
- -- Set_Ghost_Mode_For_Freeze --
- -------------------------------
+ --------------------------------
+ -- Set_Ghost_Mode_From_Entity --
+ --------------------------------
- procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
+ 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;
- Propagate_Ignored_Ghost_Code (N);
end if;
- end Set_Ghost_Mode_For_Freeze;
+ end Set_Ghost_Mode_From_Entity;
-------------------------
-- Set_Is_Ghost_Entity --
-- --
-- S p e c --
-- --
--- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- Verify that the parent type and all progenitors of derived type or type
-- extension Typ are Ghost. If this is not the case, issue an error.
+ procedure Check_Ghost_Overriding
+ (Subp : Entity_Id;
+ Overridden_Subp : Entity_Id);
+ -- Verify that the Ghost policy of parent subprogram Overridden_Subp is the
+ -- same as the Ghost policy of overriding subprogram Subp. Emit an error if
+ -- this is not the case.
+
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
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_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_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 Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
-- units.
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
- procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty);
+ procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
-- Set the value of global variable Ghost_Mode depending on the following
-- scenarios:
--
-- If this is the case, the Ghost_Mode is set based on the current Ghost
-- policy in effect. Special cases:
--
- -- N is the completion of a deferred constant, Prev_Id denotes the
- -- entity of the partial declaration.
+ -- N is the completion of a deferred constant, the Ghost_Mode is set
+ -- based on the mode of partial declaration entity denoted by Id.
+ --
+ -- 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.
+ --
+ -- If N is an assignment statement or a procedure call, the Ghost_Mode is
+ -- set based on the mode of the name.
--
- -- N is the full view of a private type, Prev_Id denotes the entity
- -- of the partial declaration.
+ -- 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.
--
- -- If N is an assignment statement or a procedure call, determine whether
- -- the name of N denotes a reference to a Ghost entity. If this is the
- -- case, the Global_Mode is set based on the mode of the name.
+ -- If N is a pragma, the Ghost_Mode is set based on the mode of the
+ -- pragma.
--
- -- If N denotes a package or a subprogram body, determine whether the
- -- corresponding spec Prev_Id is a Ghost entity or the body is subject
- -- to pragma Ghost. If this is the case, the Global_Mode is set based on
- -- the current Ghost policy in effect.
+ -- If N is a freeze node, the Global_Mode is set based on the mode of
+ -- 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.
- procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id);
- -- Set the value of global variable Ghost_Mode depending on the mode of
- -- entity Id. N denotes the context of the freeze.
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+ -- Set the valye of global variable Ghost_Mode depending on the mode of
+ -- 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.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
- -- Set the relevant ghost attribute of entity Id depending on the current
+ -- Set the relevant Ghost attributes of entity Id depending on the current
-- Ghost assertion policy in effect.
end Ghost;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-----------------------------------
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);
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);
- Id : Entity_Id;
- New_N : Node_Id;
- Save_Parent : Node_Id;
- Renaming : Node_Id;
Decls : constant List_Id :=
Visible_Declarations (Specification (N));
Decl : Node_Id;
+ Id : Entity_Id;
+ New_N : Node_Id;
+ Renaming : Node_Id;
+ Save_Parent : Node_Id;
begin
-- The generic package declaration may be subject to pragma Ghost with
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;
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;
-----------------------------------
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
function Build_Invariant_Procedure_Declaration
(Typ : Entity_Id) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Typ);
- Object_Entity : constant Entity_Id :=
- Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
- Spec : Node_Id;
- SId : Entity_Id;
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Decl : Node_Id;
+ Obj_Id : Entity_Id;
+ SId : Entity_Id;
begin
- Set_Etype (Object_Entity, Typ);
-
- -- Check for duplicate definiations.
+ -- Check for duplicate definiations
if Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)) then
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.
+
+ Set_Ghost_Mode_From_Entity (Typ);
+
SId :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Typ), "Invariant"));
Set_Is_Invariant_Procedure (SId);
Set_Invariant_Procedure (Typ, SId);
- Spec :=
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => SId,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
- Parameter_Type => New_Occurrence_Of (Typ, Loc))));
+ -- Mark the invariant procedure explicitly as Ghost because it does not
+ -- come from source.
+
+ if Ghost_Mode > None then
+ Set_Is_Ghost_Entity (SId);
+ end if;
+
+ Obj_Id := Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
+ Set_Etype (Obj_Id, Typ);
+
+ Decl :=
+ Make_Subprogram_Declaration (Loc,
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => SId,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ 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;
- return Make_Subprogram_Declaration (Loc, Specification => Spec);
+ return Decl;
end Build_Invariant_Procedure_Declaration;
-------------------------------
-- end typInvariant;
procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
+ Priv_Decls : constant List_Id := Private_Declarations (N);
+ Vis_Decls : constant List_Id := Visible_Declarations (N);
+
Loc : constant Source_Ptr := Sloc (Typ);
Stmts : List_Id;
Spec : Node_Id;
PDecl : Node_Id;
PBody : Node_Id;
- Nam : Name_Id;
- -- Name for Check pragma, usually Invariant, but might be Type_Invariant
- -- if we come from a Type_Invariant aspect, we make sure to build the
- -- Check pragma with the right name, so that Check_Policy works right.
+ Object_Entity : Node_Id;
+ -- The entity of the formal for the procedure
- Visible_Decls : constant List_Id := Visible_Declarations (N);
- Private_Decls : constant List_Id := Private_Declarations (N);
+ Object_Name : Name_Id;
+ -- Name for argument of invariant procedure
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
-- Appends statements to Stmts for any invariants in the rep item chain
-- "inherited" to the exception message and generating an informational
-- message about the inheritance of an invariant.
- Object_Name : Name_Id;
- -- Name for argument of invariant procedure
-
- Object_Entity : Node_Id;
- -- The entity of the formal for the procedure
-
--------------------
-- Add_Invariants --
--------------------
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
- Ritem : Node_Id;
- Arg1 : Node_Id;
- Arg2 : Node_Id;
- Arg3 : Node_Id;
- Exp : Node_Id;
- Loc : Source_Ptr;
- Assoc : List_Id;
- Str : String_Id;
-
- procedure Replace_Type_Reference (N : Node_Id);
- -- Replace a single occurrence N of the subtype name with a reference
- -- to the formal of the predicate function. N can be an identifier
- -- referencing the subtype, or a selected component, representing an
- -- appropriately qualified occurrence of the subtype name.
-
- procedure Replace_Type_References is
- new Replace_Type_References_Generic (Replace_Type_Reference);
- -- Traverse an expression replacing all occurrences of the subtype
- -- name with appropriate references to the object that is the formal
- -- parameter of the predicate function. Note that we must ensure
- -- that the type and entity information is properly set in the
- -- replacement node, since we will do a Preanalyze call of this
- -- expression without proper visibility of the procedure argument.
+ procedure Add_Invariant (Prag : Node_Id);
+ -- Create a runtime check to verify the exression of invariant pragma
+ -- Prag. All generated code is added to list Stmts.
- ----------------------------
- -- Replace_Type_Reference --
- ----------------------------
+ -------------------
+ -- Add_Invariant --
+ -------------------
- -- Note: See comments in Add_Predicates.Replace_Type_Reference
- -- regarding handling of Sloc and Comes_From_Source.
+ procedure Add_Invariant (Prag : Node_Id) is
+ procedure Replace_Type_Reference (N : Node_Id);
+ -- Replace a single occurrence N of the subtype name with a
+ -- reference to the formal of the predicate function. N can be an
+ -- identifier referencing the subtype, or a selected component,
+ -- representing an appropriately qualified occurrence of the
+ -- subtype name.
+
+ procedure Replace_Type_References is
+ new Replace_Type_References_Generic (Replace_Type_Reference);
+ -- Traverse an expression replacing all occurrences of the subtype
+ -- name with appropriate references to the formal of the predicate
+ -- function. Note that we must ensure that the type and entity
+ -- information is properly set in the replacement node, since we
+ -- will do a Preanalyze call of this expression without proper
+ -- visibility of the procedure argument.
+
+ ----------------------------
+ -- Replace_Type_Reference --
+ ----------------------------
+
+ -- Note: See comments in Add_Predicates.Replace_Type_Reference
+ -- regarding handling of Sloc and Comes_From_Source.
+
+ procedure Replace_Type_Reference (N : Node_Id) is
+ Nloc : constant Source_Ptr := Sloc (N);
- procedure Replace_Type_Reference (N : Node_Id) is
- begin
+ begin
+ -- Add semantic information to node to be rewritten, for ASIS
+ -- navigation needs.
- -- Add semantic information to node to be rewritten, for ASIS
- -- navigation needs.
+ if Nkind (N) = N_Identifier then
+ Set_Entity (N, T);
+ Set_Etype (N, T);
- if Nkind (N) = N_Identifier then
- Set_Entity (N, T);
- Set_Etype (N, T);
+ elsif Nkind (N) = N_Selected_Component then
+ Analyze (Prefix (N));
+ Set_Entity (Selector_Name (N), T);
+ Set_Etype (Selector_Name (N), T);
+ end if;
- elsif Nkind (N) = N_Selected_Component then
- Analyze (Prefix (N));
- Set_Entity (Selector_Name (N), T);
- Set_Etype (Selector_Name (N), T);
- end if;
+ -- Invariant'Class, replace with T'Class (obj)
- -- Invariant'Class, replace with T'Class (obj)
- -- In ASIS mode, an inherited item is analyzed already, and the
- -- replacement has been done, so do not repeat transformation
- -- to prevent ill-formed tree.
+ if Class_Present (Prag) then
- if Class_Present (Ritem) then
- if ASIS_Mode
- and then Nkind (Parent (N)) = N_Attribute_Reference
- and then Attribute_Name (Parent (N)) = Name_Class
- then
- null;
+ -- In ASIS mode, an inherited item is already analyzed,
+ -- and the replacement has been done, so do not repeat
+ -- the transformation to prevent a malformed tree.
- else
- Rewrite (N,
- Make_Type_Conversion (Sloc (N),
- Subtype_Mark =>
- Make_Attribute_Reference (Sloc (N),
- Prefix => New_Occurrence_Of (T, Sloc (N)),
- Attribute_Name => Name_Class),
- Expression =>
- Make_Identifier (Sloc (N), Object_Name)));
+ if ASIS_Mode
+ and then Nkind (Parent (N)) = N_Attribute_Reference
+ and then Attribute_Name (Parent (N)) = Name_Class
+ then
+ null;
- Set_Entity (Expression (N), Object_Entity);
- Set_Etype (Expression (N), Typ);
- end if;
+ else
+ Rewrite (N,
+ Make_Type_Conversion (Nloc,
+ Subtype_Mark =>
+ Make_Attribute_Reference (Nloc,
+ Prefix => New_Occurrence_Of (T, Nloc),
+ Attribute_Name => Name_Class),
+ Expression => Make_Identifier (Nloc, Object_Name)));
+
+ Set_Entity (Expression (N), Object_Entity);
+ Set_Etype (Expression (N), Typ);
+ end if;
- -- Invariant, replace with obj
+ -- Invariant, replace with obj
- else
- Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
- Set_Entity (N, Object_Entity);
- Set_Etype (N, Typ);
- end if;
+ else
+ Rewrite (N, Make_Identifier (Nloc, Object_Name));
+ Set_Entity (N, Object_Entity);
+ Set_Etype (N, Typ);
+ end if;
- Set_Comes_From_Source (N, True);
- end Replace_Type_Reference;
+ Set_Comes_From_Source (N, True);
+ end Replace_Type_Reference;
- -- Start of processing for Add_Invariants
+ -- Local variables
- begin
- Ritem := First_Rep_Item (T);
- while Present (Ritem) loop
- if Nkind (Ritem) = N_Pragma
- and then Pragma_Name (Ritem) = Name_Invariant
- then
- Arg1 := First (Pragma_Argument_Associations (Ritem));
- Arg2 := Next (Arg1);
- Arg3 := Next (Arg2);
+ Asp : constant Node_Id := Corresponding_Aspect (Prag);
+ Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
+ Ploc : constant Source_Ptr := Sloc (Prag);
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
+ Arg3 : Node_Id;
+ Assoc : List_Id;
+ Expr : Node_Id;
+ Str : String_Id;
- Arg1 := Get_Pragma_Arg (Arg1);
- Arg2 := Get_Pragma_Arg (Arg2);
+ -- Start of processing for Add_Invariant
- -- For Inherit case, ignore Invariant, process only Class case
+ begin
+ -- Extract the arguments of the invariant pragma
- if Inherit then
- if not Class_Present (Ritem) then
- goto Continue;
- end if;
+ Arg1 := First (Pragma_Argument_Associations (Prag));
+ Arg2 := Next (Arg1);
+ Arg3 := Next (Arg2);
- -- For Inherit false, process only item for right type
+ Arg1 := Get_Pragma_Arg (Arg1);
+ Arg2 := Get_Pragma_Arg (Arg2);
- else
- if Entity (Arg1) /= Typ then
- goto Continue;
- end if;
- end if;
+ -- The caller requests processing of all Invariant'Class pragmas,
+ -- but the current pragma does not fall in this category. Return
+ -- as there is nothing left to do.
- if No (Stmts) then
- Stmts := Empty_List;
+ if Inherit then
+ if not Class_Present (Prag) then
+ return;
end if;
- Exp := New_Copy_Tree (Arg2);
+ -- Otherwise the pragma must apply to the current type
- -- Preserve sloc of original pragma Invariant
+ elsif Entity (Arg1) /= T then
+ return;
+ end if;
- Loc := Sloc (Ritem);
+ Expr := New_Copy_Tree (Arg2);
- -- We need to replace any occurrences of the name of the type
- -- with references to the object, converted to type'Class in
- -- the case of Invariant'Class aspects.
+ -- Replace all occurrences of the type's name with references to
+ -- the formal parameter of the invariant procedure.
- Replace_Type_References (Exp, T);
+ Replace_Type_References (Expr, T);
- -- If this invariant comes from an aspect, find the aspect
- -- specification, and replace the saved expression because
- -- we need the subtype references replaced for the calls to
- -- Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
- -- and Check_Aspect_At_End_Of_Declarations.
+ -- If the invariant pragma comes from an aspect, replace the saved
+ -- expression because we need the subtype references replaced for
+ -- the calls to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
+ -- routines.
- if From_Aspect_Specification (Ritem) then
- declare
- Aitem : Node_Id;
+ if Present (Asp) then
+ Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
+ end if;
- begin
- -- Loop to find corresponding aspect, note that this
- -- must be present given the pragma is marked delayed.
+ -- Preanalyze the invariant expression to capture the visibility
+ -- of the proper package part. In general the expression is not
+ -- fully analyzed until the body of the invariant procedure is
+ -- analyzed at the end of the private part, but that yields the
+ -- wrong visibility.
- -- Note: in practice Next_Rep_Item (Ritem) is Empty so
- -- this loop does nothing. Furthermore, why isn't this
- -- simply Corresponding_Aspect ???
+ -- Historic note: we used to set N as the parent, but a package
+ -- specification as the parent of an expression is bizarre.
- Aitem := Next_Rep_Item (Ritem);
- while Present (Aitem) loop
- if Nkind (Aitem) = N_Aspect_Specification
- and then Aspect_Rep_Item (Aitem) = Ritem
- then
- Set_Entity
- (Identifier (Aitem), New_Copy_Tree (Exp));
- exit;
- end if;
+ Set_Parent (Expr, Parent (Arg2));
+ Preanalyze_Assert_Expression (Expr, Any_Boolean);
- Aitem := Next_Rep_Item (Aitem);
- end loop;
- end;
- end if;
-
- -- Now we need to preanalyze the expression to properly capture
- -- the visibility in the visible part. The expression will not
- -- be analyzed for real until the body is analyzed, but that is
- -- at the end of the private part and has the wrong visibility.
+ -- A class-wide invariant may be inherited in a separate unit,
+ -- where the corresponding expression cannot be resolved by
+ -- visibility, because it refers to a local function. Propagate
+ -- semantic information to the original representation item, to
+ -- be used when an invariant procedure for a derived type is
+ -- constructed.
- Set_Parent (Exp, N);
- Preanalyze_Assert_Expression (Exp, Any_Boolean);
+ -- ??? Unclear how to handle class-wide invariants that are not
+ -- function calls.
- -- A class-wide invariant may be inherited in a separate unit,
- -- where the corresponding expression cannot be resolved by
- -- visibility, because it refers to a local function. Propagate
- -- semantic information to the original representation item, to
- -- be used when an invariant procedure for a derived type is
- -- constructed.
+ if not Inherit
+ and then Class_Present (Prag)
+ and then Nkind (Expr) = N_Function_Call
+ and then Nkind (Arg2) = N_Indexed_Component
+ then
+ Rewrite (Arg2,
+ Make_Function_Call (Ploc,
+ Name =>
+ New_Occurrence_Of (Entity (Name (Expr)), Ploc),
+ Parameter_Associations =>
+ New_Copy_List (Expressions (Arg2))));
+ end if;
- -- Unclear how to handle class-wide invariants that are not
- -- function calls ???
+ -- In ASIS mode, even if assertions are not enabled, we must
+ -- analyze the original expression in the aspect specification
+ -- because it is part of the original tree.
- if not Inherit
- and then Class_Present (Ritem)
- and then Nkind (Exp) = N_Function_Call
- and then Nkind (Arg2) = N_Indexed_Component
- then
- Rewrite (Arg2,
- Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Entity (Name (Exp)), Loc),
- Parameter_Associations =>
- New_Copy_List (Expressions (Arg2))));
- end if;
-
- -- In ASIS mode, even if assertions are not enabled, we must
- -- analyze the original expression in the aspect specification
- -- because it is part of the original tree.
+ if ASIS_Mode and then Present (Asp) then
+ declare
+ Orig_Expr : constant Node_Id := Expression (Asp);
+ begin
+ Replace_Type_References (Orig_Expr, T);
+ Preanalyze_Assert_Expression (Orig_Expr, Any_Boolean);
+ end;
+ end if;
- if ASIS_Mode and then From_Aspect_Specification (Ritem) then
- declare
- Inv : constant Node_Id :=
- Expression (Corresponding_Aspect (Ritem));
- begin
- Replace_Type_References (Inv, T);
- Preanalyze_Assert_Expression (Inv, Standard_Boolean);
- end;
- end if;
+ -- An ignored invariant must not generate a runtime check. Add a
+ -- null statement to ensure that the invariant procedure does get
+ -- a completing body.
- -- Get name to be used for Check pragma. Using the original
- -- name ensures that 'Class case is properly handled.
+ if No (Stmts) then
+ Stmts := Empty_List;
+ end if;
- Nam := Original_Aspect_Pragma_Name (Ritem);
+ if Is_Ignored (Prag) then
+ Append_To (Stmts, Make_Null_Statement (Ploc));
- -- Build first two arguments for Check pragma
+ -- Otherwise the invariant is checked. Build a Check pragma to
+ -- verify the expression at runtime.
- Assoc :=
- New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Chars => Nam)),
- Make_Pragma_Argument_Association (Loc,
- Expression => Exp));
+ else
+ Assoc := New_List (
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Make_Identifier (Ploc, Nam)),
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Expr));
- -- Add message if present in Invariant pragma
+ -- Handle the String argument (if any)
if Present (Arg3) then
Str := Strval (Get_Pragma_Arg (Arg3));
- -- If inherited case, and message starts "failed invariant",
- -- change it to be "failed inherited invariant".
+ -- When inheriting an invariant, modify the message from
+ -- "failed invariant" to "failed inherited invariant".
if Inherit then
String_To_Name_Buffer (Str);
end if;
Append_To (Assoc,
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_String_Literal (Loc, Str)));
+ Make_Pragma_Argument_Association (Ploc,
+ Expression => Make_String_Literal (Ploc, Str)));
end if;
- -- Add Check pragma to list of statements
+ -- Generate:
+ -- pragma Check (Nam, Expr, Str);
Append_To (Stmts,
- Make_Pragma (Loc,
+ Make_Pragma (Ploc,
Pragma_Identifier =>
- Make_Identifier (Loc, Name_Check),
+ Make_Identifier (Ploc, Name_Check),
Pragma_Argument_Associations => Assoc));
+ end if;
- -- If Inherited case and option enabled, output info msg. Note
- -- that we know this is a case of Invariant'Class.
+ -- Output an info message when inheriting an invariant and the
+ -- listing option is enabled.
- if Inherit and Opt.List_Inherited_Aspects then
- Error_Msg_Sloc := Sloc (Ritem);
- Error_Msg_N
- ("info: & inherits `Invariant''Class` aspect from #?L?",
- Typ);
- end if;
+ if Inherit and Opt.List_Inherited_Aspects then
+ Error_Msg_Sloc := Sloc (Prag);
+ Error_Msg_N
+ ("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
+ end if;
+ end Add_Invariant;
+
+ -- Local variables
+
+ Ritem : Node_Id;
+
+ -- Start of processing for Add_Invariants
+
+ begin
+ Ritem := First_Rep_Item (T);
+ while Present (Ritem) loop
+ if Nkind (Ritem) = N_Pragma
+ and then Pragma_Name (Ritem) = Name_Invariant
+ then
+ Add_Invariant (Ritem);
end if;
- <<Continue>>
Next_Rep_Item (Ritem);
end loop;
end Add_Invariants;
-- If declaration is already analyzed, it was processed by the
-- generated pragma.
- if Present (Private_Decls) then
+ if Present (Priv_Decls) then
-- The spec goes at the end of visible declarations, but they have
-- already been analyzed, so we need to explicitly do the analyze.
if not Analyzed (PDecl) then
- Append_To (Visible_Decls, PDecl);
+ Append_To (Vis_Decls, PDecl);
Analyze (PDecl);
end if;
-- analyze call. We skip this if there are no private declarations
-- (this is an error that will be caught elsewhere);
- Append_To (Private_Decls, PBody);
+ Append_To (Priv_Decls, PBody);
-- If the invariant appears on the full view of a type, the
-- analysis of the private part is complete, and we must
-- that the type is about to be frozen.
elsif not Is_Private_Type (Typ) then
- Append_To (Visible_Decls, PDecl);
- Append_To (Visible_Decls, PBody);
+ Append_To (Vis_Decls, PDecl);
+ Append_To (Vis_Decls, PBody);
Analyze (PDecl);
Analyze (PBody);
end if;
-- Inheritance of predicates for the parent type is done by calling the
-- Predicate_Function of the parent type, using Add_Call above.
- function Test_RE (N : Node_Id) return Traverse_Result;
- -- Used in Test_REs, tests one node for being a raise expression, and if
- -- so sets Raise_Expression_Present True.
-
- procedure Test_REs is new Traverse_Proc (Test_RE);
- -- Tests to see if Expr contains any raise expressions
-
function Process_RE (N : Node_Id) return Traverse_Result;
-- Used in Process REs, tests if node N is a raise expression, and if
-- so, marks it to be converted to return False.
procedure Process_REs is new Traverse_Proc (Process_RE);
-- Marks any raise expressions in Expr_M to return False
+ function Test_RE (N : Node_Id) return Traverse_Result;
+ -- Used in Test_REs, tests one node for being a raise expression, and if
+ -- so sets Raise_Expression_Present True.
+
+ procedure Test_REs is new Traverse_Proc (Test_RE);
+ -- Tests to see if Expr contains any raise expressions
+
--------------
-- Add_Call --
--------------
--------------------
procedure Add_Predicates is
- Ritem : Node_Id;
- Arg1 : Node_Id;
- Arg2 : Node_Id;
-
- procedure Replace_Type_Reference (N : Node_Id);
- -- Replace a single occurrence N of the subtype name with a reference
- -- to the formal of the predicate function. N can be an identifier
- -- referencing the subtype, or a selected component, representing an
- -- appropriately qualified occurrence of the subtype name.
+ procedure Add_Predicate (Prag : Node_Id);
+ -- Concatenate the expression of predicate pragma Prag to Expr by
+ -- using a short circuit "and then" operator.
- procedure Replace_Type_References is
- new Replace_Type_References_Generic (Replace_Type_Reference);
- -- Traverse an expression changing every occurrence of an identifier
- -- whose name matches the name of the subtype with a reference to
- -- the formal parameter of the predicate function.
+ -------------------
+ -- Add_Predicate --
+ -------------------
- ----------------------------
- -- Replace_Type_Reference --
- ----------------------------
+ procedure Add_Predicate (Prag : Node_Id) is
+ procedure Replace_Type_Reference (N : Node_Id);
+ -- Replace a single occurrence N of the subtype name with a
+ -- reference to the formal of the predicate function. N can be an
+ -- identifier referencing the subtype, or a selected component,
+ -- representing an appropriately qualified occurrence of the
+ -- subtype name.
+
+ procedure Replace_Type_References is
+ new Replace_Type_References_Generic (Replace_Type_Reference);
+ -- Traverse an expression changing every occurrence of an
+ -- identifier whose name matches the name of the subtype with a
+ -- reference to the formal parameter of the predicate function.
+
+ ----------------------------
+ -- Replace_Type_Reference --
+ ----------------------------
+
+ procedure Replace_Type_Reference (N : Node_Id) is
+ begin
+ Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
+ -- Use the Sloc of the usage name, not the defining name
- procedure Replace_Type_Reference (N : Node_Id) is
- begin
- Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
- -- Use the Sloc of the usage name, not the defining name
+ Set_Etype (N, Typ);
+ Set_Entity (N, Object_Entity);
- Set_Etype (N, Typ);
- Set_Entity (N, Object_Entity);
+ -- We want to treat the node as if it comes from source, so
+ -- that ASIS will not ignore it.
- -- We want to treat the node as if it comes from source, so that
- -- ASIS will not ignore it
+ Set_Comes_From_Source (N, True);
+ end Replace_Type_Reference;
- Set_Comes_From_Source (N, True);
- end Replace_Type_Reference;
+ -- Local variables
- -- Start of processing for Add_Predicates
+ Asp : constant Node_Id := Corresponding_Aspect (Prag);
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
- begin
- Ritem := First_Rep_Item (Typ);
+ -- Start of processing for Add_Predicate
- while Present (Ritem) loop
- if Nkind (Ritem) = N_Pragma
- and then Pragma_Name (Ritem) = Name_Predicate
- then
- -- Acquire arguments. The expression itself is copied for use
- -- in the predicate function, to preserve the original version
- -- for ASIS use.
-
- Arg1 := First (Pragma_Argument_Associations (Ritem));
- Arg2 := Next (Arg1);
+ begin
+ -- Extract the arguments of the pragma. The expression itself
+ -- is copied for use in the predicate function, to preserve the
+ -- original version for ASIS use.
- Arg1 := Get_Pragma_Arg (Arg1);
- Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
+ Arg1 := First (Pragma_Argument_Associations (Prag));
+ Arg2 := Next (Arg1);
- -- See if this predicate pragma is for the current type or for
- -- its full view. A predicate on a private completion is placed
- -- on the partial view beause this is the visible entity that
- -- is frozen.
+ Arg1 := Get_Pragma_Arg (Arg1);
+ Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
- if Entity (Arg1) = Typ
- or else Full_View (Entity (Arg1)) = Typ
- then
- -- We have a match, this entry is for our subtype
+ -- When the predicate pragma applies to the current type or its
+ -- full view, replace all occurrences of the subtype name with
+ -- references to the formal parameter of the predicate function.
- -- We need to replace any occurrences of the name of the
- -- type with references to the object.
+ if Entity (Arg1) = Typ
+ or else Full_View (Entity (Arg1)) = Typ
+ then
+ Replace_Type_References (Arg2, Typ);
- Replace_Type_References (Arg2, Typ);
+ -- If the predicate pragma comes from an aspect, replace the
+ -- saved expression because we need the subtype references
+ -- replaced for the calls to Preanalyze_Spec_Expression in
+ -- Check_Aspect_At_xxx routines.
- -- If this predicate comes from an aspect, find the aspect
- -- specification, and replace the saved expression because
- -- we need the subtype references replaced for the calls to
- -- Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
- -- and Check_Aspect_At_End_Of_Declarations.
+ if Present (Asp) then
- if From_Aspect_Specification (Ritem) then
- declare
- Aitem : Node_Id;
- Orig_Expr : constant Node_Id :=
- Expression (Corresponding_Aspect (Ritem));
+ -- For ASIS use, perform semantic analysis of the original
+ -- predicate expression, which is otherwise not utilized.
- begin
+ if ASIS_Mode then
+ Preanalyze_And_Resolve (Expression (Asp));
+ end if;
- -- For ASIS use, perform semantic analysis of the
- -- original predicate expression, which is otherwise
- -- not utilized.
+ Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2));
+ end if;
- if ASIS_Mode then
- Preanalyze_And_Resolve (Orig_Expr);
- end if;
+ -- Concatenate to the existing predicate expressions by using
+ -- "and then".
- -- Loop to find corresponding aspect, note that this
- -- must be present given the pragma is marked delayed.
+ if Present (Expr) then
+ Expr :=
+ Make_And_Then (Loc,
+ Left_Opnd => Relocate_Node (Expr),
+ Right_Opnd => Relocate_Node (Arg2));
- Aitem := Next_Rep_Item (Ritem);
- loop
- if Nkind (Aitem) = N_Aspect_Specification
- and then Aspect_Rep_Item (Aitem) = Ritem
- then
- Set_Entity
- (Identifier (Aitem), New_Copy_Tree (Arg2));
- exit;
- end if;
+ -- Otherwise this is the first predicate expression
- Aitem := Next_Rep_Item (Aitem);
- end loop;
- end;
- end if;
+ else
+ Expr := Relocate_Node (Arg2);
+ end if;
+ end if;
+ end Add_Predicate;
- -- Now we can add the expression
+ -- Local variables
- if No (Expr) then
- Expr := Relocate_Node (Arg2);
+ Ritem : Node_Id;
- -- There already was a predicate, so add to it
+ -- Start of processing for Add_Predicates
- else
- Expr :=
- Make_And_Then (Loc,
- Left_Opnd => Relocate_Node (Expr),
- Right_Opnd => Relocate_Node (Arg2));
- end if;
- end if;
+ begin
+ Ritem := First_Rep_Item (Typ);
+ while Present (Ritem) loop
+ if Nkind (Ritem) = N_Pragma
+ and then Pragma_Name (Ritem) = Name_Predicate
+ then
+ Add_Predicate (Ritem);
end if;
Next_Rep_Item (Ritem);
end if;
end Test_RE;
+ -- Local variables
+
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Build_Predicate_Functions
begin
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.
+
+ Set_Ghost_Mode_From_Entity (Typ);
+
-- Prepare to construct predicate expression
Expr := Empty;
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;
+
Spec :=
Make_Function_Specification (Loc,
Defining_Unit_Name => SId,
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,
end if;
end;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
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;
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
end if;
if Etype (T) = Any_Type then
+ Restore_Globals;
return;
end if;
-- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Comes_From_Source (T) and then Ghost_Mode > None then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
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);
- T : Entity_Id;
+ F : constant Boolean := Is_Pure (Current_Scope);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ 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
- Id : constant Entity_Id := Defining_Identifier (N);
+ 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);
- T : Entity_Id;
+ 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
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);
- T : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (N);
Act_T : Entity_Id;
+ T : Entity_Id;
E : Node_Id := Expression (N);
-- E is set to Expression (N) throughout this routine. When
-- 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 --
+ ---------------------
+
+ procedure Restore_Globals is
+ begin
+ Ghost_Mode := GM;
+ end Restore_Globals;
+
-- Start of processing for Analyze_Object_Declaration
begin
and then Analyzed (N)
and then No (Expression (N))
then
+ Restore_Globals;
return;
end if;
Set_Renamed_Object (Id, E);
Freeze_Before (N, T);
Set_Is_Frozen (Id);
+
+ Restore_Globals;
return;
else
-- Deal with setting In_Private_Part flag if in private part
- if Ekind (Scope (Id)) = E_Package and then In_Private_Part (Scope (Id))
+ if Ekind (Scope (Id)) = E_Package
+ and then In_Private_Part (Scope (Id))
then
Set_In_Private_Part (Id);
end if;
if Ekind (Id) = E_Variable then
Check_No_Hidden_State (Id);
end if;
+
+ Restore_Globals;
end Analyze_Object_Declaration;
---------------------------
-------------------------------------------
procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
- T : constant Entity_Id := Defining_Identifier (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Indic : constant Node_Id := Subtype_Indication (N);
- Parent_Type : Entity_Id;
+ 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
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);
- T : Entity_Id;
R_Checks : Check_Result;
+ T : Entity_Id;
begin
-- The subtype declaration may be subject to pragma Ghost with policy
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 Post_Error is
-
procedure Missing_Body;
-- Output missing body message
begin
if not Comes_From_Source (E) then
-
if Ekind_In (E, E_Task_Type, E_Protected_Type) then
-- It may be an anonymous protected type created for a
Private_To_Full_View => True);
end if;
- -- Propagate the attributes related to pragma Ghost from the private to
- -- the full view.
-
if Is_Ghost_Entity (Priv_T) then
- Set_Is_Ghost_Entity (Full_T);
-- 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_Derived_Type (Full_T) then
Check_Ghost_Derivation (Full_T);
end if;
+
+ -- 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 invariants to full type
------------------------
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);
T1 : Entity_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 --
-------------------------
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
+ Restore_Globals;
return;
end if;
end if;
"specified??", Lhs);
end if;
+ Restore_Globals;
return;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
+ Restore_Globals;
return;
-- Error of assigning to limited type. We do however allow this in
("left hand of assignment must not be limited type", Lhs);
Explain_Limited_Type (T1, Lhs);
end if;
+
+ Restore_Globals;
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;
return;
end if;
if Rhs = Error then
Kill_Lhs;
+ Restore_Globals;
return;
end if;
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
+ Restore_Globals;
return;
end if;
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
+ Restore_Globals;
return;
end if;
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
+ Restore_Globals;
return;
-- If we know the right hand side is non-null, then we convert to the
end;
Analyze_Dimension (N);
+ Restore_Globals;
end Analyze_Assignment;
-----------------------------
---------------------------------------------
procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id) is
- Designator : constant Entity_Id :=
- Analyze_Subprogram_Specification (Specification (N));
- Scop : constant Entity_Id := Current_Scope;
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ 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
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
- Generate_Definition (Designator);
+ Generate_Definition (Subp_Id);
- Set_Is_Abstract_Subprogram (Designator);
- New_Overloaded_Entity (Designator);
- Check_Delayed_Subprogram (Designator);
+ Set_Is_Abstract_Subprogram (Subp_Id);
+ New_Overloaded_Entity (Subp_Id);
+ Check_Delayed_Subprogram (Subp_Id);
- Set_Categorization_From_Scope (Designator, Scop);
+ Set_Categorization_From_Scope (Subp_Id, Scop);
-- An abstract subprogram declared within a Ghost region is rendered
-- Ghost (SPARK RM 6.9(2)).
- if Comes_From_Source (Designator) and then Ghost_Mode > None then
- Set_Is_Ghost_Entity (Designator);
+ if Ghost_Mode > None then
+ Set_Is_Ghost_Entity (Subp_Id);
end if;
- if Ekind (Scope (Designator)) = E_Protected_Type then
- Error_Msg_N
- ("abstract subprogram not allowed in protected type", N);
+ if Ekind (Scope (Subp_Id)) = E_Protected_Type then
+ Error_Msg_N ("abstract subprogram not allowed in protected type", N);
-- Issue a warning if the abstract subprogram is neither a dispatching
-- operation nor an operation that overrides an inherited subprogram or
-- predefined operator, since this most likely indicates a mistake.
elsif Warn_On_Redundant_Constructs
- and then not Is_Dispatching_Operation (Designator)
- and then not Present (Overridden_Operation (Designator))
- and then (not Is_Operator_Symbol_Name (Chars (Designator))
- or else Scop /= Scope (Etype (First_Formal (Designator))))
+ and then not Is_Dispatching_Operation (Subp_Id)
+ and then not Present (Overridden_Operation (Subp_Id))
+ and then (not Is_Operator_Symbol_Name (Chars (Subp_Id))
+ or else Scop /= Scope (Etype (First_Formal (Subp_Id))))
then
Error_Msg_N
("abstract subprogram is not dispatching or overriding?r?", N);
end if;
- Generate_Reference_To_Formals (Designator);
- Check_Eliminated (Designator);
+ Generate_Reference_To_Formals (Subp_Id);
+ Check_Eliminated (Subp_Id);
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Designator);
+ 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
- Loc : constant Source_Ptr := Sloc (N);
- P : constant Node_Id := Name (N);
- Actuals : constant List_Id := Parameter_Associations (N);
- Actual : Node_Id;
- New_N : Node_Id;
+ 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);
+ Loc : constant Source_Ptr := Sloc (N);
+ P : constant Node_Id := Name (N);
+ Actual : Node_Id;
+ New_N : Node_Id;
+
-- Start of processing for Analyze_Procedure_Call
begin
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
+ Restore_Globals;
return;
elsif Is_Entity_Name (P)
else
Error_Msg_N ("invalid procedure or entry call", N);
end if;
+
+ Restore_Globals;
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 --
----------------------------
Check_Missing_Return;
end if;
+ Restore_Globals;
return;
else
-- enter name will post error.
Enter_Name (Body_Id);
+ Restore_Globals;
return;
end if;
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
+ Restore_Globals;
return;
else
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
+ Restore_Globals;
return;
end if;
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
+ Restore_Globals;
return;
else
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
+ Restore_Globals;
return;
end if;
end if;
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
+ Restore_Globals;
return;
end if;
Set_Has_Nested_Subprogram (Ent);
end if;
end;
+
+ Restore_Globals;
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
Analyze_Null_Procedure (N, Is_Completion);
- if Is_Completion then
-
- -- The null procedure acts as a body, nothing further is needed
+ -- 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;
--------------------------------------
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
+
+ -- The Ghost policy in effect at the point of declaration of a
+ -- parent subprogram and an overriding subprogram must match
+ -- (SPARK RM 6.9(17)).
+
+ Check_Ghost_Overriding (S, Overridden_Subp);
end if;
-- If there is a homonym that is not overloadable, then we have an
if Comes_From_Source (E) then
Check_Overriding_Indicator (E, S, Is_Primitive => False);
+
+ -- The Ghost policy in effect at the point of declaration
+ -- of a parent subprogram and an overriding subprogram
+ -- must match (SPARK RM 6.9(17)).
+
+ Check_Ghost_Overriding (E, S);
end if;
return;
Check_Overriding_Indicator (S, E, Is_Primitive => True);
+ -- The Ghost policy in effect at the point of declaration
+ -- of a parent subprogram and an overriding subprogram
+ -- must match (SPARK RM 6.9(17)).
+
+ Check_Ghost_Overriding (S, E);
+
-- If S is a user-defined subprogram or a null procedure
-- expanded to override an inherited null procedure, or a
-- predefined dispatching primitive then indicate that E
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
+ -- The Ghost policy in effect at the point of declaration of a parent
+ -- subprogram and an overriding subprogram must match
+ -- (SPARK RM 6.9(17)).
+
+ Check_Ghost_Overriding (S, Overridden_Subp);
+
-- Overloading is not allowed in SPARK, except for operators
if Nkind (S) /= N_Defining_Operator_Symbol then
-- Local variables
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
Qualify_Entity_Names (N);
end if;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Analyze_Package_Body_Helper;
------------------------------
---------------------------------
procedure Analyze_Package_Declaration (N : Node_Id) is
- Id : constant Node_Id := Defining_Entity (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
- PF : Boolean;
- -- True when in the context of a declared pure library unit
+ 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;
-- True when this package declaration requires a corresponding body
Comp_Unit : Boolean;
-- True when this package declaration is not a nested declaration
+ PF : Boolean;
+ -- True when in the context of a declared pure library unit
+
+ -- Start of processing for Analyze_Package_Declaration
+
begin
if Debug_Flag_C then
Write_Str ("==> package spec ");
Set_SPARK_Aux_Pragma_Inherited (Id, True);
end if;
+ -- A package declared within a Ghost refion is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Ghost_Mode > None 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.
-- package Pkg is ...
if From_Limited_With (Id) then
+ Restore_Globals;
return;
end if;
end if;
Comp_Unit := Nkind (Parent (N)) = N_Compilation_Unit;
+
if Comp_Unit then
-- Set Body_Required indication on the compilation unit node, and
if not Body_Required then
Set_Suppress_Elaboration_Warnings (Id);
end if;
-
end if;
End_Package_Scope (Id);
Write_Location (Sloc (N));
Write_Eol;
end if;
+
+ Restore_Globals;
end Analyze_Package_Declaration;
-----------------------------------
--------------------------------------
procedure Analyze_Private_Type_Declaration (N : Node_Id) is
- PF : constant Boolean := Is_Pure (Enclosing_Lib_Unit_Entity);
+ 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
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
- Id : constant Node_Id := Defining_Identifier (N);
- Nam : constant Node_Id := Name (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Id : constant Entity_Id := Defining_Entity (N);
+ Nam : constant Node_Id := Name (N);
begin
-- The exception renaming declaration may be subject to pragma Ghost
Enter_Name (Id);
Analyze (Nam);
- Set_Ekind (Id, E_Exception);
- Set_Etype (Id, Standard_Exception_Type);
- Set_Is_Pure (Id, Is_Pure (Current_Scope));
+ Set_Ekind (Id, E_Exception);
+ Set_Etype (Id, Standard_Exception_Type);
+ Set_Is_Pure (Id, Is_Pure (Current_Scope));
- if not Is_Entity_Name (Nam)
- or else Ekind (Entity (Nam)) /= E_Exception
+ if Is_Entity_Name (Nam)
+ and then Present (Entity (Nam))
+ and then Ekind (Entity (Nam)) = E_Exception
then
- Error_Msg_N ("invalid exception name in renaming", Nam);
- else
if Present (Renamed_Object (Entity (Nam))) then
Set_Renamed_Object (Id, Renamed_Object (Entity (Nam)));
else
Set_Renamed_Object (Id, Entity (Nam));
end if;
- -- An exception renaming is Ghost if the renamed entity is Ghost or
- -- the construct appears within a Ghost scope.
+ -- The exception renaming declaration may become Ghost if it renames
+ -- a Ghost entity.
- if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
+ Mark_Renaming_As_Ghost (N, Entity (Nam));
+ else
+ Error_Msg_N ("invalid exception name in renaming", Nam);
end if;
-- Implementation-defined aspect specifications can appear in a renaming
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
- New_P : constant Entity_Id := Defining_Entity (N);
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
- Inst : Boolean := False; -- prevent junk warning
+ Inst : Boolean := False; -- prevent junk warning
begin
if Name (N) = Error then
else
if Present (Renamed_Object (Old_P)) then
- Set_Renamed_Object (New_P, Renamed_Object (Old_P));
+ Set_Renamed_Object (New_P, Renamed_Object (Old_P));
else
Set_Renamed_Object (New_P, Old_P);
end if;
Set_Etype (New_P, Etype (Old_P));
Set_Has_Completion (New_P);
- -- An generic renaming is Ghost if the renamed entity is Ghost or the
- -- construct appears within a Ghost scope.
+ -- The generic renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
- if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
- Set_Is_Ghost_Entity (New_P);
- end if;
+ 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);
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;
-----------------------------
-----------------------------
procedure Analyze_Object_Renaming (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
Id : constant Entity_Id := Defining_Identifier (N);
- Dec : Node_Id;
+ Loc : constant Source_Ptr := Sloc (N);
Nam : constant Node_Id := Name (N);
+ Dec : Node_Id;
T : Entity_Id;
T2 : Entity_Id;
return False;
end In_Generic_Scope;
+ -- Local variables
+
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Object_Renaming
begin
Set_Is_True_Constant (Id, True);
end if;
- -- An object renaming is Ghost if the renamed entity is Ghost or the
- -- construct appears within a Ghost scope.
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
- if (Is_Entity_Name (Nam)
- and then Is_Ghost_Entity (Entity (Nam)))
- or else Ghost_Mode > None
- then
- Set_Is_Ghost_Entity (Id);
+ 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
-- 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;
Check_Library_Unit_Renaming (N, Old_P);
Generate_Reference (Old_P, Name (N));
- -- A package renaming is Ghost if the renamed entity is Ghost or
- -- the construct appears within a Ghost scope.
+ -- The package renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
- if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
- Set_Is_Ghost_Entity (New_P);
- end if;
+ 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
-- 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;
New_S : Entity_Id;
Set_Is_Pure (New_S, Is_Pure (Entity (Nam)));
Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam)));
- -- A subprogram renaming is Ghost if the renamed entity is Ghost or
- -- the construct appears within a Ghost scope.
+ -- The subprogram renaming declaration may become Ghost if it renames
+ -- a Ghost entity.
- if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
- Set_Is_Ghost_Entity (New_S);
- end if;
+ Mark_Renaming_As_Ghost (N, Entity (Nam));
-- Ada 2005 (AI-423): Check the consistency of null exclusions
-- between a subprogram and its correct renaming.
if Present (F1) and then Present (Default_Value (F1)) then
if Present (Next_Formal (F1)) then
Error_Msg_NE
- ("\missing specification for &" &
- " and other formals with defaults", Spec, F1);
+ ("\missing specification for & and other formals with "
+ & "defaults", Spec, F1);
else
- Error_Msg_NE
- ("\missing specification for &", Spec, F1);
+ Error_Msg_NE ("\missing specification for &", Spec, F1);
end if;
end if;
and then Chars (Current_Scope) /= Chars (Old_S)
then
Error_Msg_N
- ("redundant renaming, entity is directly visible?r?", Name (N));
+ ("redundant renaming, entity is directly visible?r?", Name (N));
end if;
-- Implementation-defined aspect specifications can appear in a renaming
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;
-------------------------
-- Query whether a particular item appears in a mixed list of nodes and
-- entities. It is assumed that all nodes in the list have entities.
- function Check_Kind (Nam : Name_Id) return Name_Id;
- -- This function is used in connection with pragmas Assert, Check,
- -- and assertion aspects and pragmas, to determine if Check pragmas
- -- (or corresponding assertion aspects or pragmas) are currently active
- -- as determined by the presence of -gnata on the command line (which
- -- sets the default), and the appearance of pragmas Check_Policy and
- -- Assertion_Policy as configuration pragmas either in a configuration
- -- pragma file, or at the start of the current unit, or locally given
- -- Check_Policy and Assertion_Policy pragmas that are currently active.
- --
- -- The value returned is one of the names Check, Ignore, Disable (On
- -- returns Check, and Off returns Ignore).
- --
- -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
- -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
- -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
- -- _Post, _Invariant, or _Type_Invariant, which are special names used
- -- in identifiers to represent these attribute references.
-
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Spec_Id : Entity_Id);
-- 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));
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
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
+ -- point of analysis may not necessarely be the same. Use the mode in
+ -- effect at the point of declaration.
+
+ Set_Ghost_Mode (N);
Set_Analyzed (N);
-- Single and multiple contract cases must appear in aggregate form. If
else
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;
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));
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
+ -- point of analysis may not necessarely be the same. Use the mode in
+ -- effect at the point of declaration.
+
+ Set_Ghost_Mode (N);
Error_Msg_Name_1 := Pragma_Name (N);
-- An external property pragma must apply to an effectively volatile
SPARK_Msg_N ("expression of % must be static", Expr);
end if;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
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));
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
+ -- point of analysis may not necessarely be the same. Use the mode in
+ -- effect at the point of declaration.
+
+ Set_Ghost_Mode (N);
Set_Analyzed (N);
-- The expression is preanalyzed because it has not been moved to its
-- 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;
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
Spec_Id := Corresponding_Spec_Of (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);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
-- Fully analyze the pragma when it appears inside a subprogram body
procedure Analyze_Pre_Post_Condition is
Prag_Iden : constant Node_Id := Pragma_Identifier (N);
Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
Duplicates_OK : Boolean := False;
-- Flag set when a pre/postcondition allows multiple pragmas of the
return;
end if;
+ 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_Pragma_As_Ghost (N, Subp_Id);
+
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
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_Pragma_As_Ghost (N, Spec_Id);
+
-- If we get here, then the pragma is legal
if Nam_In (Pname, Name_Refined_Depends,
------------------------------------------------
procedure Process_Atomic_Independent_Shared_Volatile is
- E_Id : Node_Id;
- E : Entity_Id;
D : Node_Id;
+ E : Entity_Id;
+ E_Id : Node_Id;
K : Node_Kind;
Utyp : Entity_Id;
D := Declaration_Node (E);
K := Nkind (D);
+ -- 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);
+
-- Check duplicate before we chain ourselves
Check_Duplicate_Pragma (E);
else
Process_Convention (C, Def_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, Def_Id);
Kill_Size_Check_Code (Def_Id);
Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False);
end if;
--------------------
procedure Process_Inline (Status : Inline_Status) is
- Assoc : Node_Id;
- Decl : Node_Id;
- Subp_Id : Node_Id;
- Subp : Entity_Id;
- Applies : Boolean;
+ Applies : Boolean;
+ Assoc : Node_Id;
+ Decl : Node_Id;
+ Subp : Entity_Id;
+ Subp_Id : Node_Id;
+
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost subprograms is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost subprogram encountered while
+ -- processing the arguments of the pragma.
procedure Make_Inline (Subp : Entity_Id);
-- Subp is the defining unit name of the subprogram declaration. Set
Set_Is_Inlined (Subp, True);
end if;
end case;
+
+ -- 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);
+
+ -- Capture the entity of the first Ghost subprogram being
+ -- processed for error detection purposes.
+
+ if Is_Ghost_Entity (Subp) then
+ if No (Ghost_Id) then
+ Ghost_Id := Subp;
+ end if;
+
+ -- Otherwise the subprogram is non-Ghost. It is illegal to mix
+ -- references to Ghost and non-Ghost entities (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id) and then not Ghost_Error_Posted then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and non-ghost subprograms",
+ N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Subp);
+ end if;
end Set_Inline_Flags;
-- Start of processing for Process_Inline
Proc_Scope : constant Entity_Id := Scope (Handler_Proc);
begin
+ -- 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_Proc);
Set_Is_Interrupt_Handler (Handler_Proc);
-- If the pragma is not associated with a handler procedure within a
procedure Process_Suppress_Unsuppress (Suppress_Case : Boolean) is
C : Check_Id;
- E_Id : Node_Id;
E : Entity_Id;
+ E_Id : Node_Id;
In_Package_Spec : constant Boolean :=
Is_Package_Or_Generic_Package (Current_Scope)
-- on user code: we want to generate checks for analysis purposes, as
-- set respectively by -gnatC and -gnatd.F
- if (CodePeer_Mode or GNATprove_Mode)
- and then Comes_From_Source (N)
+ if Comes_From_Source (N)
+ and then (CodePeer_Mode or GNATprove_Mode)
then
return;
end if;
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_Pragma_As_Ghost (N, E);
+
-- Enforce RM 11.5(7) which requires that for a pragma that
-- appears within a package spec, the named entity must be
-- within the package spec. We allow the package name itself
-- An abstract state declared within a Ghost region becomes
-- Ghost (SPARK RM 6.9(2)).
- if Ghost_Mode > None then
+ if Ghost_Mode > None or else Is_Ghost_Entity (Pack_Id) then
Set_Is_Ghost_Entity (State_Id);
end if;
Pack_Id := Defining_Entity (Pack_Decl);
- Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-
- -- Mark the associated package as Ghost if it is subject to aspect
- -- or pragma Ghost as this affects the declaration of an abstract
- -- state.
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
- if Is_Subject_To_Ghost (Unit_Declaration_Node (Pack_Id)) then
- Set_Is_Ghost_Entity (Pack_Id);
- end if;
+ Mark_Pragma_As_Ghost (N, Pack_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
States := Expression (Get_Argument (N, Pack_Id));
Lib_Entity := Find_Lib_Unit_Name;
+ -- 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);
+
-- This pragma should only apply to a RCI unit (RM E.2.3(23))
- if Present (Lib_Entity)
- and then not Debug_Flag_U
- then
+ if Present (Lib_Entity) and then not Debug_Flag_U then
if not Is_Remote_Call_Interface (Lib_Entity) then
Error_Pragma ("pragma% only apply to rci unit");
else
Set_Has_All_Calls_Remote (Lib_Entity);
end if;
-
end if;
end All_Calls_Remote;
-- not analyzed.
when Pragma_Annotate => Annotate : declare
- Arg : Node_Id;
- Exp : Node_Id;
+ Arg : Node_Id;
+ Expr : Node_Id;
+ Nam_Arg : Node_Id;
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- -- See if last argument is Entity => local_Name, and if so process
- -- and then remove it for remaining processing.
+ Nam_Arg := Last (Pragma_Argument_Associations (N));
- declare
- Last_Arg : constant Node_Id :=
- Last (Pragma_Argument_Associations (N));
+ -- Determine whether the last argument is "Entity => local_NAME"
+ -- and if it is, perform the required semantic checks. Remove the
+ -- argument from further processing.
- begin
- if Nkind (Last_Arg) = N_Pragma_Argument_Association
- and then Chars (Last_Arg) = Name_Entity
- then
- Check_Arg_Is_Local_Name (Last_Arg);
- Arg_Count := Arg_Count - 1;
+ if Nkind (Nam_Arg) = N_Pragma_Argument_Association
+ and then Chars (Nam_Arg) = Name_Entity
+ then
+ Check_Arg_Is_Local_Name (Nam_Arg);
+ Arg_Count := Arg_Count - 1;
- -- Not allowed in compiler units (bootstrap issues)
+ -- A pragma that applies to a Ghost entity becomes Ghost for
+ -- the purposes of legality checks and removal of ignored Ghost
+ -- code.
- Check_Compiler_Unit ("Entity for pragma Annotate", N);
+ 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)));
end if;
- end;
- -- Continue processing with last argument removed for now
+ -- Not allowed in compiler units (bootstrap issues)
+
+ Check_Compiler_Unit ("Entity for pragma Annotate", N);
+ end if;
+
+ -- Continue the processing with last argument removed for now
Check_Arg_Is_Identifier (Arg1);
Check_No_Identifiers;
Store_Note (N);
- -- Second parameter is optional, it is never analyzed
+ -- The second parameter is optional, it is never analyzed
if No (Arg2) then
null;
- -- Here if we have a second parameter
+ -- Otherwise there is a second parameter
else
- -- Second parameter must be identifier
+ -- The second parameter must be an identifier
Check_Arg_Is_Identifier (Arg2);
- -- Process remaining parameters if any
+ -- Process the remaining parameters (if any)
Arg := Next (Arg2);
while Present (Arg) loop
- Exp := Get_Pragma_Arg (Arg);
- Analyze (Exp);
+ Expr := Get_Pragma_Arg (Arg);
+ Analyze (Expr);
- if Is_Entity_Name (Exp) then
+ if Is_Entity_Name (Expr) then
null;
-- For string literals, we assume Standard_String as the
-- type, unless the string contains wide or wide_wide
-- characters.
- elsif Nkind (Exp) = N_String_Literal then
- if Has_Wide_Wide_Character (Exp) then
- Resolve (Exp, Standard_Wide_Wide_String);
- elsif Has_Wide_Character (Exp) then
- Resolve (Exp, Standard_Wide_String);
+ elsif Nkind (Expr) = N_String_Literal then
+ if Has_Wide_Wide_Character (Expr) then
+ Resolve (Expr, Standard_Wide_Wide_String);
+ elsif Has_Wide_Character (Expr) then
+ Resolve (Expr, Standard_Wide_String);
else
- Resolve (Exp, Standard_String);
+ Resolve (Expr, Standard_String);
end if;
- elsif Is_Overloaded (Exp) then
- Error_Pragma_Arg
- ("ambiguous argument for pragma%", Exp);
+ elsif Is_Overloaded (Expr) then
+ Error_Pragma_Arg ("ambiguous argument for pragma%", Expr);
else
- Resolve (Exp);
+ Resolve (Expr);
end if;
Next (Arg);
-- Local variables
- Expr : Node_Id;
- Newa : List_Id;
+ 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
-- assertion pragma contains attribute Loop_Entry, ensure that
-- the related pragma is within a loop.
- if Prag_Id = Pragma_Loop_Invariant
+ if Prag_Id = Pragma_Loop_Invariant
or else Prag_Id = Pragma_Loop_Variant
or else Contains_Loop_Entry (Expr)
then
-- Perform preanalysis to deal with embedded Loop_Entry
-- attributes.
- Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
+ Preanalyze_Assert_Expression (Expr, Any_Boolean);
end if;
-- Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating
-- Assume, or Assert_And_Cut pragma can be retrieved from the
-- pragma kind of Original_Node(N).
- Newa := New_List (
+ New_Args := New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Make_Identifier (Loc, Pname)),
Make_Pragma_Argument_Association (Sloc (Expr),
-- ASIS use, before rewriting.
Preanalyze_And_Resolve (Expression (Arg2), Standard_String);
- Append_To (Newa, New_Copy_Tree (Arg2));
+ Append_To (New_Args, New_Copy_Tree (Arg2));
end if;
-- Rewrite as Check pragma
Rewrite (N,
Make_Pragma (Loc,
Chars => Name_Check,
- Pragma_Argument_Associations => Newa));
+ Pragma_Argument_Associations => New_Args));
+
Analyze (N);
+
+ -- Restore the original Ghost mode once analysis and expansion
+ -- have taken place.
+
+ Ghost_Mode := GM;
end Assert;
----------------------
then
Obj_Id := Entity (Obj);
+ -- 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);
+
-- Detect a duplicate pragma. Note that it is not efficient to
-- examine preceding statements as Boolean aspects may appear
-- anywhere between the related object declaration and its
-- pragma Asynchronous (LOCAL_NAME);
when Pragma_Asynchronous => Asynchronous : declare
- Nm : Entity_Id;
C_Ent : Entity_Id;
+ Decl : Node_Id;
+ Formal : Entity_Id;
L : List_Id;
+ Nm : Entity_Id;
S : Node_Id;
- N : Node_Id;
- Formal : Entity_Id;
procedure Process_Async_Pragma;
-- Common processing for procedure and access-to-procedure case
Analyze (Get_Pragma_Arg (Arg1));
Nm := Entity (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, Nm);
+
if not Is_Remote_Call_Interface (C_Ent)
and then not Is_Remote_Types (C_Ent)
then
("pragma% cannot be applied to function", Arg1);
elsif Is_Remote_Access_To_Subprogram_Type (Nm) then
- if Is_Record_Type (Nm) then
+ if Is_Record_Type (Nm) then
-- A record type that is the Equivalent_Type for a remote
-- access-to-subprogram type.
- N := Declaration_Node (Corresponding_Remote_Type (Nm));
+ Decl := Declaration_Node (Corresponding_Remote_Type (Nm));
- else
- -- A non-expanded RAS type (distribution is not enabled)
+ else
+ -- A non-expanded RAS type (distribution is not enabled)
- N := Declaration_Node (Nm);
- end if;
+ Decl := Declaration_Node (Nm);
+ end if;
- if Nkind (N) = N_Full_Type_Declaration
- and then Nkind (Type_Definition (N)) =
+ if Nkind (Decl) = N_Full_Type_Declaration
+ and then Nkind (Type_Definition (Decl)) =
N_Access_Procedure_Definition
then
- L := Parameter_Specifications (Type_Definition (N));
+ L := Parameter_Specifications (Type_Definition (Decl));
Process_Async_Pragma;
if Is_Asynchronous (Nm)
when Pragma_Atomic_Components |
Pragma_Volatile_Components =>
-
Atomic_Components : declare
- E_Id : Node_Id;
- E : Entity_Id;
D : Node_Id;
+ E : Entity_Id;
+ E_Id : Node_Id;
K : Node_Kind;
begin
E := Entity (E_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, E);
Check_Duplicate_Pragma (E);
if Rep_Item_Too_Early (E, N)
-- allowed, since they have special meaning for Check_Policy.
when Pragma_Check => Check : declare
- Expr : Node_Id;
- Eloc : Source_Ptr;
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Cname : Name_Id;
+ Eloc : Source_Ptr;
+ Expr : Node_Id;
Str : Node_Id;
begin
+ -- Ensure that analysis and expansion produce Ghost nodes if the
+ -- pragma itself is Ghost.
+
+ Set_Ghost_Mode (N);
+
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
Check_At_Most_N_Arguments (3);
case Cname is
when Name_Assertions =>
Error_Pragma_Arg
- ("""Assertions"" is not allowed as a check kind "
- & "for pragma%", Arg1);
+ ("""Assertions"" is not allowed as a check kind for "
+ & "pragma%", Arg1);
when Name_Statement_Assertions =>
Error_Pragma_Arg
-- Deal with SCO generation
case Cname is
- when Name_Predicate |
- Name_Invariant =>
- -- Nothing to do: since checks occur in client units,
- -- the SCO for the aspect in the declaration unit is
- -- conservatively always enabled.
+ -- Nothing to do for invariants and predicates as the checks
+ -- occur in the client units. The SCO for the aspect in the
+ -- declaration unit is conservatively always enabled.
+ when Name_Invariant | Name_Predicate =>
null;
- when others =>
+ -- Otherwise mark aspect/pragma SCO as enabled
+ when others =>
if Is_Checked (N) and then not Split_PPC (N) then
-
- -- Mark aspect/pragma SCO as enabled
-
Set_SCO_Pragma_Enabled (Loc);
end if;
end case;
Left_Opnd => Make_Identifier (Eloc, Name_False),
Right_Opnd => Expr),
Then_Statements => New_List (
- Make_Null_Statement (Eloc))));
+ Make_Null_Statement (Eloc))));
-- Now go ahead and analyze the if statement
Analyze_And_Resolve (Expr, Any_Boolean);
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion
+ -- have taken place.
+
+ Ghost_Mode := GM;
end Check;
--------------------------
Spec_Id := Corresponding_Spec_Of (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);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
-- Fully analyze the pragma when it appears inside a subprogram
Check_Ada_83_Warning;
Check_Arg_Count (2);
Process_Convention (C, E);
+
+ -- 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);
end Convention;
---------------------------
Stmt := Prev (Stmt);
end loop;
+ -- 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);
Set_Has_Default_Init_Cond (Typ);
Set_Has_Inherited_Default_Init_Cond (Typ, False);
-- pragma Default_Storage_Pool (storage_pool_NAME | null);
- when Pragma_Default_Storage_Pool =>
+ when Pragma_Default_Storage_Pool => Default_Storage_Pool : declare
+ Pool : Node_Id;
+
+ begin
Ada_2012_Pragma;
Check_Arg_Count (1);
Check_Is_In_Decl_Part_Or_Package_Spec;
end if;
- -- Case of Default_Storage_Pool (null);
+ if Present (Arg1) then
+ Pool := Get_Pragma_Arg (Arg1);
+
+ -- Case of Default_Storage_Pool (null);
- if Nkind (Expression (Arg1)) = N_Null then
- Analyze (Expression (Arg1));
+ if Nkind (Pool) = N_Null then
+ Analyze (Pool);
- -- This is an odd case, this is not really an expression, so
- -- we don't have a type for it. So just set the type to Empty.
+ -- This is an odd case, this is not really an expression,
+ -- so we don't have a type for it. So just set the type to
+ -- Empty.
- Set_Etype (Expression (Arg1), Empty);
+ Set_Etype (Pool, Empty);
- -- Case of Default_Storage_Pool (storage_pool_NAME);
+ -- Case of Default_Storage_Pool (storage_pool_NAME);
- else
- -- If it's a configuration pragma, then the only allowed
- -- argument is "null".
+ else
+ -- If it's a configuration pragma, then the only allowed
+ -- argument is "null".
- if Is_Configuration_Pragma then
- Error_Pragma_Arg ("NULL expected", Arg1);
- end if;
+ if Is_Configuration_Pragma then
+ Error_Pragma_Arg ("NULL expected", Arg1);
+ end if;
- -- The expected type for a non-"null" argument is
- -- Root_Storage_Pool'Class, and the pool must be a variable.
+ -- The expected type for a non-"null" argument is
+ -- Root_Storage_Pool'Class, and the pool must be a variable.
- Analyze_And_Resolve
- (Get_Pragma_Arg (Arg1),
- Typ => Class_Wide_Type (RTE (RE_Root_Storage_Pool)));
+ Analyze_And_Resolve
+ (Pool, Class_Wide_Type (RTE (RE_Root_Storage_Pool)));
- if not Is_Variable (Expression (Arg1)) then
- Error_Pragma_Arg
- ("default storage pool must be a variable", Arg1);
+ if Is_Variable (Pool) then
+
+ -- 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, Entity (Pool));
+
+ else
+ Error_Pragma_Arg
+ ("default storage pool must be a variable", Arg1);
+ end if;
end if;
- end if;
- -- Finally, record the pool name (or null). Freeze.Freeze_Entity
- -- for an access type will use this information to set the
- -- appropriate attributes of the access type.
+ -- Record the pool name (or null). Freeze.Freeze_Entity for an
+ -- access type will use this information to set the appropriate
+ -- attributes of the access type.
- Default_Pool := Expression (Arg1);
+ Default_Pool := Pool;
+ end if;
+ end Default_Storage_Pool;
-------------
-- Depends --
when Pragma_Discard_Names => Discard_Names : declare
E : Entity_Id;
- E_Id : Entity_Id;
+ E_Id : Node_Id;
begin
Check_Ada_83_Warning;
E := Entity (E_Id);
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_Pragma_As_Ghost (N, E);
+
if (Is_First_Subtype (E)
and then
(Is_Enumeration_Type (E) or else Is_Tagged_Type (E)))
Error_Pragma_Arg
("inappropriate entity for pragma%", Arg1);
end if;
-
end if;
end if;
end Discard_Names;
Arg := Get_Pragma_Arg (Arg1);
Ent := Defining_Identifier (Parent (P));
+ -- 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);
+
-- The expression must be analyzed in the special manner
-- described in "Handling of Default and Per-Object
-- Expressions" in sem.ads.
Cunit_Node := Cunit (Current_Sem_Unit);
Cunit_Ent := Cunit_Entity (Current_Sem_Unit);
+ -- 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);
+
if Nkind_In (Unit (Cunit_Node), N_Package_Body,
N_Subprogram_Body)
then
else
Process_Convention (C, Def_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, Def_Id);
+
if Ekind (Def_Id) /= E_Constant then
Note_Possible_Modification
(Get_Pragma_Arg (Arg2), Sure => False);
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ -- 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.
+
+ Mark_Pragma_As_Ghost (N, Spec_Id);
+
-- Examine the formals of the related subprogram
Formal := First_Formal (Spec_Id);
Error_Msg_NE
("\subprogram & lacks parameter of specific tagged or "
& "generic private type", N, Spec_Id);
+
return;
end if;
-- [, [Link_Name =>] static_string_EXPRESSION ]);
when Pragma_External => External : declare
- Def_Id : Entity_Id;
-
- C : Convention_Id;
- pragma Warnings (Off, C);
+ C : Convention_Id;
+ E : Entity_Id;
+ pragma Warnings (Off, C);
begin
GNAT_Pragma;
Name_Link_Name));
Check_At_Least_N_Arguments (2);
Check_At_Most_N_Arguments (4);
- Process_Convention (C, Def_Id);
+ Process_Convention (C, E);
+
+ -- 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);
+
Note_Possible_Modification
(Get_Pragma_Arg (Arg2), Sure => False);
- Process_Interface_Name (Def_Id, Arg3, Arg4);
- Set_Exported (Def_Id, Arg2);
+ Process_Interface_Name (E, Arg3, Arg4);
+ Set_Exported (E, Arg2);
end External;
--------------------------
-- pragma Favor_Top_Level (type_NAME);
when Pragma_Favor_Top_Level => Favor_Top_Level : declare
- Named_Entity : Entity_Id;
+ Typ : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
Check_Arg_Is_Local_Name (Arg1);
- Named_Entity := Entity (Get_Pragma_Arg (Arg1));
+ Typ := Entity (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, Typ);
-- If it's an access-to-subprogram type (in particular, not a
-- subtype), set the flag on that type.
- if Is_Access_Subprogram_Type (Named_Entity) then
- Set_Can_Use_Internal_Rep (Named_Entity, False);
+ if Is_Access_Subprogram_Type (Typ) then
+ Set_Can_Use_Internal_Rep (Typ, False);
-- Otherwise it's an error (name denotes the wrong sort of entity)
end if;
-- Protected and task types cannot be subject to pragma Ghost
+ -- (SPARK RM 6.9(19)).
elsif Nkind (Stmt) = N_Protected_Type_Declaration then
Error_Pragma ("pragma % cannot apply to a protected type");
return;
end if;
end if;
+
+ -- A synchronized object cannot be subject to pragma Ghost
+ -- (SPARK RM 6.9(19)).
+
+ elsif Ekind (Id) = E_Variable then
+ if Is_Protected_Type (Etype (Id)) then
+ Error_Pragma ("pragma % cannot apply to a protected object");
+ return;
+
+ elsif Is_Task_Type (Etype (Id)) then
+ Error_Pragma ("pragma % cannot apply to a task object");
+ return;
+ end if;
end if;
-- Analyze the Boolean expression (if any)
-- pragma Independent_Components (array_or_record_LOCAL_NAME);
when Pragma_Independent_Components => Independent_Components : declare
+ C : Node_Id;
+ D : Node_Id;
E_Id : Node_Id;
E : Entity_Id;
- D : Node_Id;
K : Node_Kind;
- C : Node_Id;
begin
Check_Ada_83_Warning;
E := Entity (E_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, E);
+
-- Check duplicate before we chain ourselves
Check_Duplicate_Pragma (E);
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_Pragma_As_Ghost (N, Pack_Id);
+
-- Verify the declaration order of pragma Initial_Condition with
-- respect to pragmas Abstract_State and Initializes when SPARK
-- checks are enabled.
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_Pragma_As_Ghost (N, Pack_Id);
Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-- Verify the declaration order of pragmas Abstract_State and
-- [,[Message =>] String_Expression]);
when Pragma_Invariant => Invariant : declare
- Type_Id : Node_Id;
- Typ : Entity_Id;
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
Discard : Boolean;
+ Typ : Entity_Id;
+ Type_Id : Node_Id;
begin
GNAT_Pragma;
("pragma% only allowed for private type", Arg1);
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_Pragma_As_Ghost (N, Typ);
+
-- Not allowed for abstract type in the non-class case (it is
-- allowed to use Invariant'Class for abstract types).
("pragma% not allowed for abstract type", Arg1);
end if;
+ -- Link the pragma on to the rep item chain, for processing when
+ -- the type is frozen.
+
+ Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
+
-- Note that the type has at least one invariant, and also that
-- it has inheritable invariants if we have Invariant'Class
-- or Type_Invariant'Class. Build the corresponding invariant
Set_Has_Inheritable_Invariants (Typ);
end if;
- -- The remaining processing is simply to link the pragma on to
- -- the rep item chain, for processing when the type is frozen.
- -- This is accomplished by a call to Rep_Item_Too_Late.
+ -- Restore the original Ghost mode once analysis and expansion
+ -- have taken place.
- Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
+ Ghost_Mode := GM;
end Invariant;
----------------------
--------------------
-- pragma Linker_Section (
- -- [Entity =>] LOCAL_NAME
- -- [Section =>] static_string_EXPRESSION);
+ -- [Entity =>] LOCAL_NAME
+ -- [Section =>] static_string_EXPRESSION);
when Pragma_Linker_Section => Linker_Section : declare
Arg : Node_Id;
Ent : Entity_Id;
LPE : Node_Id;
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost subprograms is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost subprogram encountered while
+ -- processing the arguments of the pragma.
+
begin
GNAT_Pragma;
Check_Arg_Order ((Name_Entity, Name_Section));
Set_Linker_Section_Pragma (Ent, N);
+ -- 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);
+
-- Subprograms
when Subprogram_Kind =>
loop
if No (Linker_Section_Pragma (Ent)) then
Set_Linker_Section_Pragma (Ent, N);
+
+ -- 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);
+
+ -- Capture the entity of the first Ghost subprogram
+ -- being processed for error detection purposes.
+
+ if Is_Ghost_Entity (Ent) then
+ if No (Ghost_Id) then
+ Ghost_Id := Ent;
+ end if;
+
+ -- Otherwise the subprogram is non-Ghost. It is
+ -- illegal to mix references to Ghost and non-Ghost
+ -- entities (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id)
+ and then not Ghost_Error_Posted
+ then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and "
+ & "non-ghost subprograms", N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE
+ ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Ent);
+ Error_Msg_NE
+ ("\& # declared as non-ghost", N, Ent);
+ end if;
end if;
Ent := Homonym (Ent);
-- pragma No_Elaboration_Code_All;
- when Pragma_No_Elaboration_Code_All => NECA : declare
- begin
+ when Pragma_No_Elaboration_Code_All =>
GNAT_Pragma;
Check_Valid_Library_Unit_Pragma;
if In_Extended_Main_Source_Unit (N) then
Opt.No_Elab_Code_All_Pragma := N;
end if;
- end NECA;
---------------
-- No_Inline --
-- pragma No_Return (procedure_LOCAL_NAME {, procedure_Local_Name});
when Pragma_No_Return => No_Return : declare
- Id : Node_Id;
+ Arg : Node_Id;
E : Entity_Id;
Found : Boolean;
- Arg : Node_Id;
+ Id : Node_Id;
+
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost subprograms is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost procedure encountered while
+ -- processing the arguments of the pragma.
begin
Ada_2005_Pragma;
-- Loop to find matching procedures
E := Entity (Id);
+
Found := False;
while Present (E)
and then Scope (E) = Current_Scope
if Ekind_In (E, E_Procedure, E_Generic_Procedure) then
Set_No_Return (E);
+ -- 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);
+
+ -- Capture the entity of the first Ghost procedure being
+ -- processed for error detection purposes.
+
+ if Is_Ghost_Entity (E) then
+ if No (Ghost_Id) then
+ Ghost_Id := E;
+ end if;
+
+ -- Otherwise the subprogram is non-Ghost. It is illegal
+ -- to mix references to Ghost and non-Ghost entities
+ -- (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id)
+ and then not Ghost_Error_Posted
+ then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and non-ghost "
+ & "procedures", N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (E);
+ Error_Msg_NE ("\& # declared as non-ghost", N, E);
+ end if;
+
-- Set flag on any alias as well
if Is_Overloadable (E) and then Present (Alias (E)) then
-- pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME);
when Pragma_No_Tagged_Streams => No_Tagged_Strms : declare
- E_Id : Node_Id;
E : Entity_Id;
+ E_Id : Node_Id;
begin
GNAT_Pragma;
-- [,[Version =>] Ada_05]] );
when Pragma_Obsolescent => Obsolescent : declare
- Ename : Node_Id;
Decl : Node_Id;
+ Ename : Node_Id;
procedure Set_Obsolescent (E : Entity_Id);
-- Given an entity Ent, mark it as obsolescent if appropriate
Active := True;
Ent := E;
+ -- 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);
+
-- Entity name was given
if Present (Ename) then
when Pragma_Pack => Pack : declare
Assoc : constant Node_Id := Arg1;
- Type_Id : Node_Id;
- Typ : Entity_Id;
Ctyp : Entity_Id;
Ignore : Boolean := False;
+ Typ : Entity_Id;
+ Type_Id : Node_Id;
begin
Check_No_Identifiers;
Typ := Underlying_Type (Typ);
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_Pragma_As_Ghost (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");
end if;
Item_Id := Defining_Entity (Stmt);
State := 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);
+
-- Detect any discrepancies between the placement of the object
-- or package instantiation with respect to state space and the
-- encapsulating state.
Check_First_Subtype (Arg1);
Ent := Entity (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, Ent);
+
-- The pragma may come from an aspect on a private declaration,
-- even if the freeze point at which this is analyzed in the
-- private part after the full view.
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);
+
-- Check for duplication before inserting in list of
-- representation items.
-- [Check =>] boolean_EXPRESSION);
when Pragma_Predicate => Predicate : declare
- Type_Id : Node_Id;
- Typ : Entity_Id;
Discard : Boolean;
+ Typ : Entity_Id;
+ Type_Id : Node_Id;
begin
GNAT_Pragma;
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_Pragma_As_Ghost (N, Typ);
+
-- The remaining processing is simply to link the pragma on to
-- the rep item chain, for processing when the type is frozen.
-- This is accomplished by a call to Rep_Item_Too_Late. We also
end if;
Ent := Find_Lib_Unit_Name;
+
+ -- 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);
Check_Duplicate_Pragma (Ent);
-- This filters out pragmas inside generic parents that show up
end if;
Ent := Find_Lib_Unit_Name;
+
+ -- 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);
Set_Is_Pure (Ent);
Set_Has_Pragma_Pure (Ent);
Set_Suppress_Elaboration_Warnings (Ent);
-- pragma Pure_Function ([Entity =>] function_LOCAL_NAME);
when Pragma_Pure_Function => Pure_Function : declare
- E_Id : Node_Id;
- E : Entity_Id;
Def_Id : Entity_Id;
+ E : Entity_Id;
+ E_Id : Node_Id;
Effective : Boolean := False;
begin
E := Entity (E_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, E);
+
if Present (E) then
loop
Def_Id := Get_Base_Subprogram (E);
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_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)).
-- Item chain of Ent since it is rewritten by the expander as a
-- procedure call statement that will break the chain.
- Set_Has_Relative_Deadline_Pragma (P, True);
+ Set_Has_Relative_Deadline_Pragma (P);
end Relative_Deadline;
------------------------
E := Entity (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, E);
+
if Nkind (Parent (E)) = N_Formal_Type_Declaration
and then Ekind (E) = E_General_Access_Type
and then Is_Class_Wide_Type (Directly_Designated_Type (E))
K := Nkind (Unit (Cunit_Node));
Cunit_Ent := Cunit_Entity (Current_Sem_Unit);
+ -- 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);
+
if K = N_Package_Declaration
or else K = N_Generic_Package_Declaration
or else K = N_Subprogram_Declaration
Cunit_Node := Cunit (Current_Sem_Unit);
Cunit_Ent := Cunit_Entity (Current_Sem_Unit);
+ -- 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);
+
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
then
Cunit_Node := Cunit (Current_Sem_Unit);
Cunit_Ent := Cunit_Entity (Current_Sem_Unit);
+ -- 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);
+
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
then
when Pragma_Simple_Storage_Pool_Type =>
Simple_Storage_Pool_Type : declare
- Type_Id : Node_Id;
Typ : Entity_Id;
+ Type_Id : Node_Id;
begin
GNAT_Pragma;
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_Pragma_As_Ghost (N, Typ);
+
-- We require the pragma to apply to a type declared in a package
-- declaration, but not (immediately) within a package body.
-- pragma Suppress_Debug_Info ([Entity =>] LOCAL_NAME);
- when Pragma_Suppress_Debug_Info =>
+ when Pragma_Suppress_Debug_Info => Suppress_Debug_Info : declare
+ Nam_Id : Entity_Id;
+
+ begin
GNAT_Pragma;
Check_Arg_Count (1);
Check_Optional_Identifier (Arg1, Name_Entity);
Check_Arg_Is_Local_Name (Arg1);
- Set_Debug_Info_Off (Entity (Get_Pragma_Arg (Arg1)));
+
+ Nam_Id := Entity (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, Nam_Id);
+ Set_Debug_Info_Off (Nam_Id);
+ end Suppress_Debug_Info;
----------------------------------
-- Suppress_Exception_Locations --
-- pragma Suppress_Initialization ([Entity =>] type_Name);
when Pragma_Suppress_Initialization => Suppress_Init : declare
- E_Id : Node_Id;
E : Entity_Id;
+ E_Id : Node_Id;
begin
GNAT_Pragma;
E := Entity (E_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, E);
+
if not Is_Type (E) and then Ekind (E) /= E_Variable then
Error_Pragma_Arg
("pragma% requires variable, type or subtype", Arg1);
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_Pragma_As_Ghost (N, Subp_Id);
+
-- Preanalyze the original aspect argument "Name" for ASIS or for
-- a generic subprogram to properly capture global references.
-- pragma Thread_Local_Storage ([Entity =>] LOCAL_NAME);
when Pragma_Thread_Local_Storage => Thread_Local_Storage : declare
- Id : Node_Id;
E : Entity_Id;
+ Id : Node_Id;
begin
GNAT_Pragma;
E := Entity (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, E);
+
if Rep_Item_Too_Early (E, N)
- or else Rep_Item_Too_Late (E, N)
+ or else
+ Rep_Item_Too_Late (E, N)
then
raise Pragma_Exit;
end if;
when Pragma_Unchecked_Union => Unchecked_Union : declare
Assoc : constant Node_Id := Arg1;
Type_Id : constant Node_Id := Get_Pragma_Arg (Assoc);
- Typ : Entity_Id;
- Tdef : Node_Id;
Clist : Node_Id;
- Vpart : Node_Id;
Comp : Node_Id;
+ Tdef : Node_Id;
+ Typ : Entity_Id;
Variant : Node_Id;
+ Vpart : Node_Id;
begin
Ada_2005_Pragma;
Typ := Entity (Type_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, Typ);
+
if Typ = Any_Type
or else Rep_Item_Too_Early (Typ, N)
then
elsif not Has_Discriminants (Typ) then
Error_Msg_N
- ("unchecked union must have one discriminant", Typ);
+ ("unchecked union must have one discriminant", Typ);
return;
-- Note: in previous versions of GNAT we used to check for limited
Error_Pragma_Arg ("pragma% requires type", Arg1);
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_Pragma_As_Ghost (N, E_Id);
Set_Universal_Aliasing (Implementation_Base_Type (E_Id));
Record_Rep_Item (E_Id, N);
end Universal_Alias;
-- pragma Unmodified (LOCAL_NAME {, LOCAL_NAME});
when Pragma_Unmodified => Unmodified : declare
- Arg_Node : Node_Id;
+ Arg : Node_Id;
Arg_Expr : Node_Id;
- Arg_Ent : Entity_Id;
+ Arg_Id : Entity_Id;
+
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost variables is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost variable encountered while
+ -- processing the arguments of the pragma.
begin
GNAT_Pragma;
-- Loop through arguments
- Arg_Node := Arg1;
- while Present (Arg_Node) loop
- Check_No_Identifier (Arg_Node);
+ Arg := Arg1;
+ while Present (Arg) loop
+ Check_No_Identifier (Arg);
-- Note: the analyze call done by Check_Arg_Is_Local_Name will
-- in fact generate reference, so that the entity will have a
-- Has_Pragma_Unreferenced flag is set, so that no warning is
-- generated for this reference.
- Check_Arg_Is_Local_Name (Arg_Node);
- Arg_Expr := Get_Pragma_Arg (Arg_Node);
+ Check_Arg_Is_Local_Name (Arg);
+ Arg_Expr := Get_Pragma_Arg (Arg);
if Is_Entity_Name (Arg_Expr) then
- Arg_Ent := Entity (Arg_Expr);
+ Arg_Id := Entity (Arg_Expr);
+
+ if Is_Assignable (Arg_Id) then
+ Set_Has_Pragma_Unmodified (Arg_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, Arg_Id);
+
+ -- Capture the entity of the first Ghost variable being
+ -- processed for error detection purposes.
+
+ if Is_Ghost_Entity (Arg_Id) then
+ if No (Ghost_Id) then
+ Ghost_Id := Arg_Id;
+ end if;
+
+ -- Otherwise the variable is non-Ghost. It is illegal
+ -- to mix references to Ghost and non-Ghost entities
+ -- (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id)
+ and then not Ghost_Error_Posted
+ then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and non-ghost "
+ & "variables", N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Arg_Id);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id);
+ end if;
+
+ -- Otherwise the pragma referenced an illegal entity
- if not Is_Assignable (Arg_Ent) then
- Error_Pragma_Arg
- ("pragma% can only be applied to a variable",
- Arg_Expr);
else
- Set_Has_Pragma_Unmodified (Arg_Ent);
+ Error_Pragma_Arg
+ ("pragma% can only be applied to a variable", Arg_Expr);
end if;
end if;
- Next (Arg_Node);
+ Next (Arg);
end loop;
end Unmodified;
-- pragma Unreferenced (library_unit_NAME {, library_unit_NAME}
when Pragma_Unreferenced => Unreferenced : declare
- Arg_Node : Node_Id;
+ Arg : Node_Id;
Arg_Expr : Node_Id;
- Arg_Ent : Entity_Id;
+ Arg_Id : Entity_Id;
Citem : Node_Id;
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost names is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost name encountered while processing
+ -- the arguments of the pragma.
+
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
-- Par.Prag) that the arguments are either identifiers or
-- selected components.
- Arg_Node := Arg1;
- while Present (Arg_Node) loop
+ Arg := Arg1;
+ while Present (Arg) loop
Citem := First (List_Containing (N));
while Citem /= N loop
+ Arg_Expr := Get_Pragma_Arg (Arg);
+
if Nkind (Citem) = N_With_Clause
- and then
- Same_Name (Name (Citem), Get_Pragma_Arg (Arg_Node))
+ and then Same_Name (Name (Citem), Arg_Expr)
then
Set_Has_Pragma_Unreferenced
(Cunit_Entity
(Get_Source_Unit
(Library_Unit (Citem))));
- Set_Elab_Unit_Name
- (Get_Pragma_Arg (Arg_Node), Name (Citem));
+ Set_Elab_Unit_Name (Arg_Expr, Name (Citem));
exit;
end if;
if Citem = N then
Error_Pragma_Arg
- ("argument of pragma% is not withed unit", Arg_Node);
+ ("argument of pragma% is not withed unit", Arg);
end if;
- Next (Arg_Node);
+ Next (Arg);
end loop;
-- Case of not in list of context items
else
- Arg_Node := Arg1;
- while Present (Arg_Node) loop
- Check_No_Identifier (Arg_Node);
+ Arg := Arg1;
+ while Present (Arg) loop
+ Check_No_Identifier (Arg);
-- Note: the analyze call done by Check_Arg_Is_Local_Name
-- will in fact generate reference, so that the entity will
-- before the Has_Pragma_Unreferenced flag is set, so that
-- no warning is generated for this reference.
- Check_Arg_Is_Local_Name (Arg_Node);
- Arg_Expr := Get_Pragma_Arg (Arg_Node);
+ Check_Arg_Is_Local_Name (Arg);
+ Arg_Expr := Get_Pragma_Arg (Arg);
if Is_Entity_Name (Arg_Expr) then
- Arg_Ent := Entity (Arg_Expr);
+ Arg_Id := Entity (Arg_Expr);
-- If the entity is overloaded, the pragma applies to the
-- most recent overloading, as documented. In this case,
-- must be done here explicitly.
if Is_Overloaded (Arg_Expr) then
- Generate_Reference (Arg_Ent, N);
+ Generate_Reference (Arg_Id, N);
end if;
- Set_Has_Pragma_Unreferenced (Arg_Ent);
+ Set_Has_Pragma_Unreferenced (Arg_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, Arg_Id);
+
+ -- Capture the entity of the first Ghost name being
+ -- processed for error detection purposes.
+
+ if Is_Ghost_Entity (Arg_Id) then
+ if No (Ghost_Id) then
+ Ghost_Id := Arg_Id;
+ end if;
+
+ -- Otherwise the name is non-Ghost. It is illegal to mix
+ -- references to Ghost and non-Ghost entities
+ -- (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id)
+ and then not Ghost_Error_Posted
+ then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and non-ghost names",
+ N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Arg_Id);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id);
+ end if;
end if;
- Next (Arg_Node);
+ Next (Arg);
end loop;
end if;
end Unreferenced;
-- pragma Unreferenced_Objects (LOCAL_NAME {, LOCAL_NAME});
when Pragma_Unreferenced_Objects => Unreferenced_Objects : declare
- Arg_Node : Node_Id;
+ Arg : Node_Id;
Arg_Expr : Node_Id;
+ Arg_Id : Entity_Id;
+
+ Ghost_Error_Posted : Boolean := False;
+ -- Flag set when an error concerning the illegal mix of Ghost and
+ -- non-Ghost types is emitted.
+
+ Ghost_Id : Entity_Id := Empty;
+ -- The entity of the first Ghost type encountered while processing
+ -- the arguments of the pragma.
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- Arg_Node := Arg1;
- while Present (Arg_Node) loop
- Check_No_Identifier (Arg_Node);
- Check_Arg_Is_Local_Name (Arg_Node);
- Arg_Expr := Get_Pragma_Arg (Arg_Node);
+ Arg := Arg1;
+ while Present (Arg) loop
+ Check_No_Identifier (Arg);
+ Check_Arg_Is_Local_Name (Arg);
+ Arg_Expr := Get_Pragma_Arg (Arg);
+
+ if Is_Entity_Name (Arg_Expr) then
+ Arg_Id := Entity (Arg_Expr);
- if not Is_Entity_Name (Arg_Expr)
- or else not Is_Type (Entity (Arg_Expr))
- then
+ if Is_Type (Arg_Id) then
+ Set_Has_Pragma_Unreferenced_Objects (Arg_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, Arg_Id);
+
+ -- Capture the entity of the first Ghost type being
+ -- processed for error detection purposes.
+
+ if Is_Ghost_Entity (Arg_Id) then
+ if No (Ghost_Id) then
+ Ghost_Id := Arg_Id;
+ end if;
+
+ -- Otherwise the type is non-Ghost. It is illegal to mix
+ -- references to Ghost and non-Ghost entities
+ -- (SPARK RM 6.9).
+
+ elsif Present (Ghost_Id)
+ and then not Ghost_Error_Posted
+ then
+ Ghost_Error_Posted := True;
+
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_N
+ ("pragma % cannot mention ghost and non-ghost types",
+ N);
+
+ Error_Msg_Sloc := Sloc (Ghost_Id);
+ Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+ Error_Msg_Sloc := Sloc (Arg_Id);
+ Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id);
+ end if;
+ else
+ Error_Pragma_Arg
+ ("argument for pragma% must be type or subtype", Arg);
+ end if;
+ else
Error_Pragma_Arg
- ("argument for pragma% must be type or subtype", Arg_Node);
+ ("argument for pragma% must be type or subtype", Arg);
end if;
- Set_Has_Pragma_Unreferenced_Objects (Entity (Arg_Expr));
- Next (Arg_Node);
+ Next (Arg);
end loop;
end Unreferenced_Objects;
GNAT_Pragma;
Process_Atomic_Independent_Shared_Volatile;
- -------------------------
+ -------------------------
-- Volatile_Components --
-------------------------
-- 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));
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
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
+ -- point of analysis may not necessarely be the same. Use the mode in
+ -- effect at the point of declaration.
+
+ Set_Ghost_Mode (N);
+
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
-- 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;
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
package Sem_Prag is
+ -- The following table lists all pragmas that emulate an Ada 2012 aspect
+
+ Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Abstract_State => True,
+ Pragma_All_Calls_Remote => True,
+ Pragma_Annotate => True,
+ Pragma_Async_Readers => True,
+ Pragma_Async_Writers => True,
+ Pragma_Asynchronous => True,
+ Pragma_Atomic => True,
+ Pragma_Atomic_Components => True,
+ Pragma_Attach_Handler => True,
+ Pragma_Contract_Cases => True,
+ Pragma_Convention => True,
+ Pragma_CPU => True,
+ Pragma_Default_Initial_Condition => True,
+ Pragma_Default_Storage_Pool => True,
+ Pragma_Depends => True,
+ Pragma_Discard_Names => True,
+ Pragma_Dispatching_Domain => True,
+ Pragma_Effective_Reads => True,
+ Pragma_Effective_Writes => True,
+ Pragma_Elaborate_Body => True,
+ Pragma_Export => True,
+ Pragma_Extensions_Visible => True,
+ Pragma_Favor_Top_Level => True,
+ Pragma_Ghost => True,
+ Pragma_Global => True,
+ Pragma_Import => True,
+ Pragma_Independent => True,
+ Pragma_Independent_Components => True,
+ Pragma_Initial_Condition => True,
+ Pragma_Initializes => True,
+ Pragma_Inline => True,
+ Pragma_Inline_Always => True,
+ Pragma_Interrupt_Handler => True,
+ Pragma_Interrupt_Priority => True,
+ Pragma_Invariant => True,
+ Pragma_Linker_Section => True,
+ Pragma_Lock_Free => True,
+ Pragma_No_Elaboration_Code_All => True,
+ Pragma_No_Return => True,
+ Pragma_Obsolescent => True,
+ Pragma_Pack => True,
+ Pragma_Part_Of => True,
+ Pragma_Persistent_BSS => True,
+ Pragma_Post => True,
+ Pragma_Post_Class => True,
+ Pragma_Postcondition => True,
+ Pragma_Pre => True,
+ Pragma_Pre_Class => True,
+ Pragma_Precondition => True,
+ Pragma_Predicate => True,
+ Pragma_Preelaborable_Initialization => True,
+ Pragma_Preelaborate => True,
+ Pragma_Priority => True,
+ Pragma_Pure => True,
+ Pragma_Pure_Function => True,
+ Pragma_Refined_Depends => True,
+ Pragma_Refined_Global => True,
+ Pragma_Refined_Post => True,
+ Pragma_Refined_State => True,
+ Pragma_Relative_Deadline => True,
+ Pragma_Remote_Access_Type => True,
+ Pragma_Remote_Call_Interface => True,
+ Pragma_Remote_Types => True,
+ Pragma_Shared => True,
+ Pragma_Shared_Passive => True,
+ Pragma_Simple_Storage_Pool_Type => True,
+ Pragma_SPARK_Mode => True,
+ Pragma_Storage_Size => True,
+ Pragma_Suppress => True,
+ Pragma_Suppress_Debug_Info => True,
+ Pragma_Suppress_Initialization => True,
+ Pragma_Test_Case => True,
+ Pragma_Thread_Local_Storage => True,
+ Pragma_Type_Invariant => True,
+ Pragma_Unchecked_Union => True,
+ Pragma_Universal_Aliasing => True,
+ Pragma_Universal_Data => True,
+ Pragma_Unmodified => True,
+ Pragma_Unreferenced => True,
+ Pragma_Unreferenced_Objects => True,
+ Pragma_Unsuppress => True,
+ Pragma_Volatile => True,
+ Pragma_Volatile_Components => True,
+ Pragma_Volatile_Full_Access => True,
+ Pragma_Warnings => True,
+ others => False);
+
-- The following table lists all pragmas that act as an assertion
-- expression.
Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
- (Pragma_Assert => True,
- Pragma_Assert_And_Cut => True,
- Pragma_Assume => True,
- Pragma_Check => True,
- Pragma_Contract_Cases => True,
- Pragma_Initial_Condition => True,
- Pragma_Invariant => True,
- Pragma_Loop_Invariant => True,
- Pragma_Loop_Variant => True,
- Pragma_Post => True,
- Pragma_Post_Class => True,
- Pragma_Postcondition => True,
- Pragma_Pre => True,
- Pragma_Pre_Class => True,
- Pragma_Precondition => True,
- Pragma_Predicate => True,
- Pragma_Refined_Post => True,
- Pragma_Test_Case => True,
- Pragma_Type_Invariant => True,
- Pragma_Type_Invariant_Class => True,
- others => False);
+ (Pragma_Assert => True,
+ Pragma_Assert_And_Cut => True,
+ Pragma_Assume => True,
+ Pragma_Check => True,
+ Pragma_Contract_Cases => True,
+ Pragma_Default_Initial_Condition => True,
+ Pragma_Initial_Condition => True,
+ Pragma_Invariant => True,
+ Pragma_Loop_Invariant => True,
+ Pragma_Loop_Variant => True,
+ Pragma_Post => True,
+ Pragma_Post_Class => True,
+ Pragma_Postcondition => True,
+ Pragma_Pre => True,
+ Pragma_Pre_Class => True,
+ Pragma_Precondition => True,
+ Pragma_Predicate => True,
+ Pragma_Refined_Post => True,
+ Pragma_Test_Case => True,
+ Pragma_Type_Invariant => True,
+ Pragma_Type_Invariant_Class => True,
+ others => False);
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
+ function Check_Kind (Nam : Name_Id) return Name_Id;
+ -- This function is used in connection with pragmas Assert, Check,
+ -- and assertion aspects and pragmas, to determine if Check pragmas
+ -- (or corresponding assertion aspects or pragmas) are currently active
+ -- as determined by the presence of -gnata on the command line (which
+ -- sets the default), and the appearance of pragmas Check_Policy and
+ -- Assertion_Policy as configuration pragmas either in a configuration
+ -- pragma file, or at the start of the current unit, or locally given
+ -- Check_Policy and Assertion_Policy pragmas that are currently active.
+ --
+ -- The value returned is one of the names Check, Ignore, Disable (On
+ -- returns Check, and Off returns Ignore).
+ --
+ -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
+ -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
+ -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
+ -- _Post, _Invariant, or _Type_Invariant, which are special names used
+ -- in identifiers to represent these attribute references.
+
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet.Sp; use Namet.Sp;
-- 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);
return;
end if;
+ -- Ensure that the analysis and expansion produce Ghost nodes if the
+ -- type itself is Ghost.
+
+ Set_Ghost_Mode_From_Entity (Typ);
+
Param_Id := First_Formal (Proc_Id);
-- The pragma has an argument. Note that the argument is analyzed
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;
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 :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
return;
end if;
- Proc_Id :=
+ -- Ensure that the analysis and expansion produce Ghost nodes if the
+ -- type itself is Ghost.
+
+ Set_Ghost_Mode_From_Entity (Typ);
+
+ Proc_Id :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Typ), "Default_Init_Cond"));
Set_Is_Default_Init_Cond_Procedure (Proc_Id);
Set_Default_Init_Cond_Procedure (Typ, Proc_Id);
+ -- Mark the default initial condition procedure explicitly as Ghost
+ -- because it does not come from source.
+
+ if Ghost_Mode > None then
+ Set_Is_Ghost_Entity (Proc_Id);
+ end if;
+
-- Generate:
-- procedure <Typ>Default_Init_Cond (Inn : <Typ>);
Make_Parameter_Specification (Loc,
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;
end Build_Default_Init_Cond_Procedure_Declaration;
---------------------------
return False;
end Is_Renamed_Entry;
+ -----------------------------
+ -- Is_Renaming_Declaration --
+ -----------------------------
+
+ function Is_Renaming_Declaration (N : Node_Id) return Boolean is
+ begin
+ case Nkind (N) is
+ when N_Exception_Renaming_Declaration |
+ N_Generic_Function_Renaming_Declaration |
+ N_Generic_Package_Renaming_Declaration |
+ N_Generic_Procedure_Renaming_Declaration |
+ N_Object_Renaming_Declaration |
+ N_Package_Renaming_Declaration |
+ N_Subprogram_Renaming_Declaration =>
+ return True;
+
+ when others =>
+ return False;
+ end case;
+ end Is_Renaming_Declaration;
+
----------------------------
-- Is_Reversible_Iterator --
----------------------------
--------------------
function Policy_In_List (List : Node_Id) return Name_Id is
- Arg : Node_Id;
- Expr : Node_Id;
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
Prag : Node_Id;
begin
Prag := List;
while Present (Prag) loop
- Arg := First (Pragma_Argument_Associations (Prag));
- Expr := Get_Pragma_Arg (Arg);
+ Arg1 := First (Pragma_Argument_Associations (Prag));
+ Arg2 := Next (Arg1);
+
+ Arg1 := Get_Pragma_Arg (Arg1);
+ Arg2 := Get_Pragma_Arg (Arg2);
- -- The current Check_Policy pragma matches the requested policy,
- -- return the second argument which denotes the policy identifier.
+ -- The current Check_Policy pragma matches the requested policy or
+ -- appears in the single argument form (Assertion, policy_id).
- if Chars (Expr) = Policy then
- return Chars (Get_Pragma_Arg (Next (Arg)));
+ if Nam_In (Chars (Arg1), Name_Assertion, Policy) then
+ return Chars (Arg2);
end if;
Prag := Next_Pragma (Prag);
begin
Comp := First_Entity (Typ);
while Present (Comp) loop
- if Ekind (Comp) = E_Component
- and then Requires_Transient_Scope (Etype (Comp))
- then
- return True;
- else
- Next_Entity (Comp);
+ if Ekind (Comp) = E_Component then
+ -- ???It's not cleare we need a full recursive call to
+ -- Requires_Transient_Scope here. Note that the following
+ -- can't happen.
+
+ pragma Assert (Is_Definite_Subtype (Etype (Comp)));
+ pragma Assert (not Has_Controlled_Component (Etype (Comp)));
+
+ if Requires_Transient_Scope (Etype (Comp)) then
+ return True;
+ end if;
end if;
+
+ Next_Entity (Comp);
end loop;
end;
-- All other cases do not require a transient scope
else
+ pragma Assert (Is_Protected_Type (Typ) or else Is_Task_Type (Typ));
return False;
end if;
end Requires_Transient_Scope;
function Is_Renamed_Entry (Proc_Nam : Entity_Id) return Boolean;
-- Return True if Proc_Nam is a procedure renaming of an entry
+ function Is_Renaming_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a renaming declaration
+
function Is_Reversible_Iterator (Typ : Entity_Id) return Boolean;
-- AI05-0139-2: Check whether Typ is derived from the predefined interface
-- Ada.Iterator_Interfaces.Reversible_Iterator.
return Flag2 (N);
end Is_Generic_Contract_Pragma;
+ function Is_Ghost_Pragma
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ return Flag3 (N);
+ end Is_Ghost_Pragma;
+
function Is_Ignored
(N : Node_Id) return Boolean is
begin
Set_Flag2 (N, Val);
end Set_Is_Generic_Contract_Pragma;
+ procedure Set_Is_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_Ghost_Pragma;
+
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True) is
begin
-- 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)
-- 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_Inherited (Flag4-Sem)
-- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
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
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
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_In_Discriminant_Check);
pragma Inline (Is_Inherited);
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_In_Discriminant_Check);
pragma Inline (Set_Is_Inherited);
projects / gcc.git / commitdiff