+2018-05-24 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * expander.adb (Expand): Update the save and restore of the Ghost
+ region.
+ * exp_ch3.adb (Freeze_Type): Likewise.
+ * exp_disp.adb (Make_DT): Likewise.
+ * exp_util.adb (Build_DIC_Procedure_Body): Likewise.
+ (Build_DIC_Procedure_Declaration): Likewise.
+ (Build_Invariant_Procedure_Body): Likewise.
+ (Build_Invariant_Procedure_Declaration): Likewise.
+ (Make_Predicate_Call): Likewise.
+ * freeze.adb (Add_To_Result): Insert the freeze action of a living
+ entity prior to the start of the enclosing ignored Ghost region.
+ (Freeze_Entity): Update the save and restore of the Ghost region.
+ * ghost.adb (Install_Ghost_Mode): Reimplemented.
+ (Install_Ghost_Region): New routine.
+ (Mark_And_Set_Ghost_Assignment): Install a region rather than a mode.
+ (Mark_And_Set_Ghost_Body): Likewise.
+ (Mark_And_Set_Ghost_Completion): Likewise.
+ (Mark_And_Set_Ghost_Declaration): Likewise.
+ (Mark_And_Set_Ghost_Instantiation): Likewise.
+ (Mark_And_Set_Ghost_Procedure_Call): Likewise.
+ (Name_To_Ghost_Mode): New routine.
+ (Restore_Ghost_Region): New routine.
+ * ghost.ads (Install_Ghost_Region): New routine.
+ (Restore_Ghost_Region): New routine.
+ * opt.ads: Add new global variable Ignored_Ghost_Region.
+ * rtsfind.adb (Load_RTU): Update the save and restore of the Ghost
+ region. Install a clean region.
+ * sem.adb (Analyze): Likewise.
+ (Do_Analyze): Likewise.
+ * sem_ch3.adb (Analyze_Object_Declaration): Likewise
+ (Derive_Progenitor_Subprograms): Use local variable Iface_Alias to
+ capture the ultimate alias of the current primitive.
+ (Process_Full_View): Update the save and restore of the Ghost region.
+ Do not inherit DIC and invariant procedures.
+ * sem_ch5.adb (Analyze_Assignment): Update the save and restore of the
+ Ghost region.
+ * sem_ch6.adb (Analyze_Procedure_Call): Likewise.
+ (Analyze_Subprogram_Body_Helper): Likewise.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Likewise.
+ * sem_ch12.adb (Analyze_Package_Instantiation): Likewise.
+ (Analyze_Subprogram_Instantiation): Likewise.
+ (Instantiate_Package_Body): Likewise.
+ (Instantiate_Subprogram_Body): Likewise.
+ * sem_ch13.adb (Build_Predicate_Functions): Likewise.
+ (Build_Predicate_Function_Declaration): Likewise.
+ * sem_disp.adb
+ (Add_Dispatching_Operation): Do not consider DIC and invariant
+ procedures.
+ (Check_Dispatching_Operation): Use Add_Dispatching_Operation to collect
+ a dispatching subprogram.
+ (Check_Operation_From_Private_View): Likewise.
+ (Override_Dispatching_Operation): Likewise.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the save
+ and restore of the Ghost region.
+ (Analyze_Initial_Condition_In_Decl_Part): Likewise.
+ (Analyze_Pragma): Update the save and restore of the Ghost region.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Likewise.
+ * sem_util.adb (Is_Suitable_Primitive): New routine.
+ * sem_util.ads (Is_Suitable_Primitive): New routine.
+ * sinfo.ads: Update the section of Ghost regions.
+
2018-05-24 Piotr Trojanek <trojanek@adacore.com>
* doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
Def_Id : constant Entity_Id := Entity (N);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Result : Boolean := False;
end if;
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return Result;
exception
when RE_Not_Available =>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return False;
end Freeze_Type;
Name_TSD : constant Name_Id :=
New_External_Name (Tname, 'B', Suffix_Index => -1);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
AI : Elmt_Id;
AI_Tag_Elmt : Elmt_Id;
Register_CG_Node (Typ);
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return Result;
end Make_DT;
Loc : constant Source_Ptr := Sloc (Typ);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_DIC_Procedure_Body;
-------------------------------------
procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
Loc : constant Source_Ptr := Sloc (Typ);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_DIC_Procedure_Declaration;
------------------------------------
-- Local variables
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Dummy : Entity_Id;
Priv_Item : Node_Id;
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_Invariant_Procedure_Body;
-------------------------------------------
is
Loc : constant Source_Ptr := Sloc (Typ);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_Invariant_Procedure_Declaration;
--------------------------
is
Loc : constant Source_Ptr := Sloc (Expr);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Call : Node_Id;
Func_Id : Entity_Id;
Parameter_Associations => New_List (Relocate_Node (Expr)));
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return Call;
end Make_Predicate_Call;
-- Ghost mode.
procedure Expand (N : Node_Id) is
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
begin
-- If we were analyzing a default expression (or other spec expression)
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Expand;
---------------------------
N : Node_Id;
Do_Freeze_Profile : Boolean := True) return List_Id
is
- Loc : constant Source_Ptr := Sloc (N);
+ Loc : constant Source_Ptr := Sloc (N);
+
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
+
Atype : Entity_Id;
Comp : Entity_Id;
F_Node : Node_Id;
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
+ procedure Add_To_Result (Fnod : Node_Id);
+ -- Add freeze action Fnod to list Result
function After_Last_Declaration return Boolean;
-- If Loc is a freeze_entity that appears after the last declaration
-- Add_To_Result --
-------------------
- procedure Add_To_Result (N : Node_Id) is
+ procedure Add_To_Result (Fnod : Node_Id) is
begin
- if No (Result) then
- Result := New_List (N);
+ -- The Ghost mode of the enclosing context is ignored, while the
+ -- entity being frozen is living. Insert the freezing action prior
+ -- to the start of the enclosing ignored Ghost region. As a result
+ -- the freezeing action will be preserved when the ignored Ghost
+ -- context is eliminated.
+
+ if Saved_GM = Ignore
+ and then Ghost_Mode /= Ignore
+ and then Present (Ignored_Ghost_Region)
+ then
+ Insert_Action (Ignored_Ghost_Region, Fnod);
+
+ -- Otherwise add the freezing action to the result list
+
else
- Append (N, Result);
+ Append_New_To (Result, Fnod);
end if;
end Add_To_Result;
-------------------------------
procedure Freeze_Object_Declaration (E : Entity_Id) is
-
procedure Check_Large_Modular_Array (Typ : Entity_Id);
-- Check that the size of array type Typ can be computed without
-- overflow, and generates a Storage_Error otherwise. This is only
-- Build the call
-- An imported function whose result type is anonymous access
- -- creates a new anonynous access type when it is relocated into
+ -- creates a new anonymous access type when it is relocated into
-- the declarations of the body generated below. As a result, the
-- accessibility level of these two anonymous access types may not
-- be compatible even though they are essentially the same type.
end if;
end Wrap_Imported_Subprogram;
- -- Local variables
-
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
-
-- Start of processing for Freeze_Entity
begin
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return Result;
end Freeze_Entity;
package body Ghost is
+ ---------------------
+ -- Data strictures --
+ ---------------------
+
-- The following table contains the N_Compilation_Unit node for a unit that
-- is either subject to pragma Ghost with policy Ignore or contains ignored
-- Ghost code. The table is used in the removal of ignored Ghost code from
Table_Name => "Ignored_Ghost_Units");
-----------------------
- -- Local Subprograms --
+ -- Local subprograms --
-----------------------
function Ghost_Entity (N : Node_Id) return Entity_Id;
-- Find the entity of a reference to a Ghost entity. Return Empty if there
-- is no such entity.
- procedure Install_Ghost_Mode (Mode : Name_Id);
- -- Install a specific Ghost mode denoted by Mode by setting global variable
- -- Ghost_Mode.
+ procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
+ pragma Inline (Install_Ghost_Mode);
+ -- Install Ghost mode Mode as the Ghost mode in effect
+
+ procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id);
+ pragma Inline (Install_Ghost_Region);
+ -- Install a Ghost region comprised of mode Mode and ignored region start
+ -- node N.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
-- Determine whether declaration or body N is subject to aspect or pragma
-- mode Mode. Mark all formals parameters when N denotes a subprogram or a
-- body.
+ function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type;
+ pragma Inline (Name_To_Ghost_Mode);
+ -- Convert a Ghost mode denoted by name Mode into its respective enumerated
+ -- value.
+
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
-- Signal all enclosing scopes that they now contain at least one ignored
-- Ghost node denoted by N. Add the compilation unit containing N to table
procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
begin
- Ghost_Mode := Mode;
+ Install_Ghost_Region (Mode, Empty);
end Install_Ghost_Mode;
- procedure Install_Ghost_Mode (Mode : Name_Id) is
+ --------------------------
+ -- Install_Ghost_Region --
+ --------------------------
+
+ procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
begin
- if Mode = Name_Check then
- Ghost_Mode := Check;
+ -- The context is already within an ignored Ghost region. Maintain the
+ -- start of the outermost ignored Ghost region.
- elsif Mode = Name_Ignore then
- Ghost_Mode := Ignore;
+ if Present (Ignored_Ghost_Region) then
+ null;
+
+ -- The current region is the outermost ignored Ghost region. Save its
+ -- starting node.
+
+ elsif Present (N) and then Mode = Ignore then
+ Ignored_Ghost_Region := N;
- elsif Mode = Name_None then
- Ghost_Mode := None;
+ -- Otherwise the current region is not ignored, nothing to save
+
+ else
+ Ignored_Ghost_Region := Empty;
end if;
- end Install_Ghost_Mode;
+
+ Ghost_Mode := Mode;
+ end Install_Ghost_Region;
+
+ procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is
+ begin
+ Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N);
+ end Install_Ghost_Region;
-------------------------
-- Is_Ghost_Assignment --
if Present (Id) then
if Is_Checked_Ghost_Entity (Id) then
- Install_Ghost_Mode (Check);
+ Install_Ghost_Region (Check, N);
elsif Is_Ignored_Ghost_Entity (Id) then
- Install_Ghost_Mode (Ignore);
+ Install_Ghost_Region (Ignore, N);
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
Mark_Ghost_Declaration_Or_Body (N, Policy);
- -- Install the appropriate Ghost mode
+ -- Install the appropriate Ghost region
- Install_Ghost_Mode (Policy);
+ Install_Ghost_Region (Policy, N);
end Mark_And_Set_Ghost_Body;
-----------------------------------
Mark_Ghost_Declaration_Or_Body (N, Policy);
- -- Install the appropriate Ghost mode
+ -- Install the appropriate Ghost region
- Install_Ghost_Mode (Policy);
+ Install_Ghost_Region (Policy, N);
end Mark_And_Set_Ghost_Completion;
------------------------------------
Mark_Ghost_Declaration_Or_Body (N, Policy);
- -- Install the appropriate Ghost mode
+ -- Install the appropriate Ghost region
- Install_Ghost_Mode (Policy);
+ Install_Ghost_Region (Policy, N);
end Mark_And_Set_Ghost_Declaration;
--------------------------------------
Mark_Ghost_Declaration_Or_Body (N, Policy);
- -- Install the appropriate Ghost mode
+ -- Install the appropriate Ghost region
- Install_Ghost_Mode (Policy);
+ Install_Ghost_Region (Policy, N);
- -- Check ghost actuals. Given that this routine is unconditionally
+ -- Check Ghost actuals. Given that this routine is unconditionally
-- invoked with subprogram and package instantiations, this check
-- verifies the context of all the ghost entities passed in generic
-- instantiations.
if Present (Id) then
if Is_Checked_Ghost_Entity (Id) then
- Install_Ghost_Mode (Check);
+ Install_Ghost_Region (Check, N);
elsif Is_Ignored_Ghost_Entity (Id) then
- Install_Ghost_Mode (Ignore);
+ Install_Ghost_Region (Ignore, N);
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
Mark_Ghost_Declaration_Or_Body (N, Policy);
end Mark_Ghost_Renaming;
+ ------------------------
+ -- Name_To_Ghost_Mode --
+ ------------------------
+
+ function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is
+ begin
+ if Mode = Name_Check then
+ return Check;
+
+ elsif Mode = Name_Ignore then
+ return Ignore;
+
+ -- Otherwise the mode must denote one of the following:
+ --
+ -- * Disable indicates that the Ghost policy in effect is Disable
+ --
+ -- * None or No_Name indicates that the associated construct is not
+ -- subject to any Ghost annotation.
+
+ else
+ pragma Assert (Nam_In (Mode, Name_Disable, Name_None, No_Name));
+ return None;
+ end if;
+ end Name_To_Ghost_Mode;
+
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
end loop;
end Remove_Ignored_Ghost_Code;
- ------------------------
- -- Restore_Ghost_Mode --
- ------------------------
+ --------------------------
+ -- Restore_Ghost_Region --
+ --------------------------
- procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is
+ procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
begin
- Ghost_Mode := Mode;
- end Restore_Ghost_Mode;
+ Ghost_Mode := Mode;
+ Ignored_Ghost_Region := N;
+ end Restore_Ghost_Region;
--------------------
-- Set_Ghost_Mode --
procedure Initialize;
-- Initialize internal tables
- procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
- -- Set the value of global variable Ghost_Mode depending on the Ghost
- -- policy denoted by Mode.
+ procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+ pragma Inline (Install_Ghost_Region);
+ -- Install a Ghost region described by mode Mode and ignored region start
+ -- node N.
function Is_Ghost_Assignment (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes an assignment statement whose
-- * The left hand side denotes a Ghost entity
--
-- Install the Ghost mode of the assignment statement. This routine starts
- -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+ -- a Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Body
(N : Node_Id;
-- * The body appears within a Ghost region
--
-- Install the Ghost mode of the body. This routine starts a Ghost region
- -- and must be used in conjunction with Restore_Ghost_Mode.
+ -- and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
-- * The completion appears within a Ghost region
--
-- Install the Ghost mode of the completion. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
-- Mark declaration N as Ghost when:
-- * The declaration appears within a Ghost region
--
-- Install the Ghost mode of the declaration. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
-- * The instantiation appears within a Ghost region
--
-- Install the Ghost mode of the instantiation. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
-- Mark procedure call N as Ghost when:
-- * The procedure being invoked is a Ghost entity
--
-- Install the Ghost mode of the procedure call. This routine starts a
- -- Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+ -- Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_Ghost_Clause (N : Node_Id);
-- Mark use package, use type, or with clause N as Ghost when:
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
- procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
- -- Terminate a Ghost region by restoring the Ghost mode prior to the
- -- region denoted by Mode. This routine must be used in conjunction
- -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
+ procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+ pragma Inline (Restore_Ghost_Region);
+ -- Restore a Ghost region to a previous state described by mode Mode and
+ -- ignored region start node N. This routine must be used in conjunction
+ -- with the following routines:
+ --
+ -- Install_Ghost_Region
+ -- Mark_And_Set_xxx
+ -- Set_Ghost_Mode
procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
-- Install the Ghost mode of arbitrary node N. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current
Ghost_Mode : Ghost_Mode_Type := None;
-- GNAT
- -- Current Ghost mode setting
+ -- The current Ghost mode in effect
Global_Discard_Names : Boolean := False;
-- GNAT, GNATBIND
-- use of -gnateu, causing subsequent unrecognized switches to result in
-- a warning rather than an error.
+ Ignored_Ghost_Region : Node_Id := Empty;
+ -- GNAT
+ -- The start of the current ignored Ghost region. This value must always
+ -- reflect the starting node of the outermost ignored Ghost region. If a
+ -- nested ignored Ghost region is entered, the value must remain unchanged.
+
Implementation_Unit_Warnings : Boolean := True;
-- GNAT
-- Set True to active warnings for use of implementation internal units.
-- Local variables
- Save_GM : constant Ghost_Mode_Type := Ghost_Mode;
- Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- Save Ghost and SPARK mode-related data to restore on exit
-- Start of processing for Load_RTU
-- Provide a clean environment for the unit
- Install_Ghost_Mode (None);
- Install_SPARK_Mode (None, Empty);
+ Install_Ghost_Region (None, Empty);
+ Install_SPARK_Mode (None, Empty);
-- Note if secondary stack is used
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
- Restore_Ghost_Mode (Save_GM);
- Restore_SPARK_Mode (Save_SM, Save_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Load_RTU;
--------------------
-- Ghost mode.
procedure Analyze (N : Node_Id) is
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
begin
Debug_A_Entry ("analyzing ", N);
Expand_SPARK_Potential_Renaming (N);
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze;
-- Version with check(s) suppressed
-- the Ghost mode.
procedure Do_Analyze is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
-- Generally style checks are preserved across compilations, with
-- one exception: s-oscons.ads, which allows arbitrary long lines
-- unconditionally, and has no restore mechanism, because it is
-- intended as a lowest-level Pure package.
- Save_Max_Line : constant Int := Style_Max_Line_Length;
+ Saved_ML : constant Int := Style_Max_Line_Length;
List : Elist_Id;
-- Set up a clean environment before analyzing
- Install_Ghost_Mode (None);
+ Install_Ghost_Region (None, Empty);
+
Outer_Generic_Scope := Empty;
Scope_Suppress := Suppress_Options;
Scope_Stack.Table
-- Then pop entry for Standard, and pop implicit types
Pop_Scope;
- Restore_Scope_Stack (List);
- Restore_Ghost_Mode (Save_Ghost_Mode);
- Style_Max_Line_Length := Save_Max_Line;
+ Restore_Scope_Stack (List);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Style_Max_Line_Length := Saved_ML;
end Do_Analyze;
-- Local variables
Loc : constant Source_Ptr := Sloc (N);
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
Style_Check := Saved_Style_Check;
exception
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
Style_Check := Saved_Style_Check;
end Analyze_Package_Instantiation;
-- Local variables
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
exception
when Instantiation_Error =>
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Subprogram_Instantiation;
-------------------------
-- Local variables
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- Save the Ghost and SPARK mode-related data to restore on exit
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
Style_Check := Saved_Style_Check;
end Instantiate_Package_Body;
Defining_Unit_Name (Parent (Act_Decl));
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
Style_Check := Saved_Style_Check;
end Instantiate_Subprogram_Body;
-- Local variables
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
-- Start of processing for Build_Predicate_Functions
end;
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_Predicate_Functions;
------------------------------------------
is
Loc : constant Source_Ptr := Sloc (Typ);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Func_Decl : Node_Id;
Func_Id : Entity_Id;
Insert_After (Parent (Typ), Func_Decl);
Analyze (Func_Decl);
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
return Func_Decl;
end Build_Predicate_Function_Declaration;
-- Local variables
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Related_Id : Entity_Id;
Check_No_Hidden_State (Id);
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Object_Declaration;
---------------------------
(Parent_Type : Entity_Id;
Tagged_Type : Entity_Id)
is
- E : Entity_Id;
- Elmt : Elmt_Id;
- Iface : Entity_Id;
- Iface_Elmt : Elmt_Id;
- Iface_Subp : Entity_Id;
- New_Subp : Entity_Id := Empty;
- Prim_Elmt : Elmt_Id;
- Subp : Entity_Id;
- Typ : Entity_Id;
+ E : Entity_Id;
+ Elmt : Elmt_Id;
+ Iface : Entity_Id;
+ Iface_Alias : Entity_Id;
+ Iface_Elmt : Elmt_Id;
+ Iface_Subp : Entity_Id;
+ New_Subp : Entity_Id := Empty;
+ Prim_Elmt : Elmt_Id;
+ Subp : Entity_Id;
+ Typ : Entity_Id;
begin
pragma Assert (Ada_Version >= Ada_2005
Prim_Elmt := First_Elmt (Primitive_Operations (Iface));
while Present (Prim_Elmt) loop
- Iface_Subp := Node (Prim_Elmt);
+ Iface_Subp := Node (Prim_Elmt);
+ Iface_Alias := Ultimate_Alias (Iface_Subp);
-- Exclude derivation of predefined primitives except those
-- that come from source, or are inherited from one that comes
-- function "=" (Left, Right : Iface) return Boolean;
if not Is_Predefined_Dispatching_Operation (Iface_Subp)
- or else Comes_From_Source (Ultimate_Alias (Iface_Subp))
+ or else Comes_From_Source (Iface_Alias)
then
- E := Find_Primitive_Covering_Interface
- (Tagged_Type => Tagged_Type,
- Iface_Prim => Iface_Subp);
+ E :=
+ Find_Primitive_Covering_Interface
+ (Tagged_Type => Tagged_Type,
+ Iface_Prim => Iface_Subp);
-- If not found we derive a new primitive leaving its alias
-- attribute referencing the interface primitive.
-- Local variables
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Full_Indic : Node_Id;
Full_Parent : Entity_Id;
else
Full_List := Primitive_Operations (Full_T);
-
while Present (Prim_Elmt) loop
Prim := Node (Prim_Elmt);
then
Check_Controlling_Formals (Full_T, Prim);
- if not Is_Dispatching_Operation (Prim) then
+ if Is_Suitable_Primitive (Prim)
+ and then not Is_Dispatching_Operation (Prim)
+ then
Append_Elmt (Prim, Full_List);
- Set_Is_Dispatching_Operation (Prim, True);
+ Set_Is_Dispatching_Operation (Prim);
Set_DT_Position_Value (Prim, No_Uint);
end if;
elsif Is_Dispatching_Operation (Prim)
and then Disp_Typ /= Full_T
then
-
-- Verify that it is not otherwise controlled by a
-- formal or a return value of type T.
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Process_Full_View;
-----------------------------------
Save_Full_Analysis : Boolean := False;
-- Force initialization to facilitate static analysis
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
-- Start of processing for Analyze_Assignment
Analyze_Dimension (N);
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
-- If the right-hand side contains target names, expansion has been
-- disabled to prevent expansion that might move target names out of
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Actual : Node_Id;
New_N : Node_Id;
end if;
<<Leave>>
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Procedure_Call;
------------------------------
-- Local variables
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
-- Save the Ghost and SPARK mode-related data to restore on exit
<<Leave>>
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Subprogram_Body_Helper;
------------------------------------
-- Local variables
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
Saved_ISMP : constant Boolean :=
Ignore_SPARK_Mode_Pragmas_In_Instance;
-- Save the Ghost and SPARK mode-related data to restore on exit
end if;
Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Package_Body_Helper;
---------------------------------
-- for the construction of function wrappers). The list of primitive
-- operations must not contain duplicates.
- Append_Unique_Elmt (New_Op, List);
+ -- The Default_Initial_Condition and invariant procedures are not added
+ -- to the list of primitives even when they are generated for a tagged
+ -- type. These routines must not be targets of dispatching calls and
+ -- therefore must not appear in the dispatch table because they already
+ -- utilize class-wide-precondition semantics to handle inheritance and
+ -- overriding.
+
+ if Is_Suitable_Primitive (New_Op) then
+ Append_Unique_Elmt (New_Op, List);
+ end if;
end Add_Dispatching_Operation;
--------------------------
-- Attach operation to list of primitives of the synchronized type
-- itself, for ASIS use.
- Append_Elmt (Subp, Direct_Primitive_Operations (Tagged_Type));
+ Add_Dispatching_Operation (Tagged_Type, Subp);
-- If no old subprogram, then we add this as a dispatching operation,
-- but we avoid doing this if an error was posted, to prevent annoying
-- Add Old_Subp to primitive operations if not already present
if Present (Tagged_Type) and then Is_Tagged_Type (Tagged_Type) then
- Append_Unique_Elmt (Old_Subp, Primitive_Operations (Tagged_Type));
+ Add_Dispatching_Operation (Tagged_Type, Old_Subp);
-- If Old_Subp isn't already marked as dispatching then this is
-- the case of an operation of an untagged private type fulfilled
Find_Dispatching_Type (Alias (Prev_Op)))
then
Remove_Elmt (Primitive_Operations (Tagged_Type), Elmt);
- Append_Elmt (New_Op, Primitive_Operations (Tagged_Type));
+ Add_Dispatching_Operation (Tagged_Type, New_Op);
-- The new primitive replaces the overridden entity. Required to ensure
-- that overriding primitive is assigned the same dispatch table slot.
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
CCase : Node_Id;
Restore_Scope : Boolean := False;
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
begin
-- Do not analyze the pragma multiple times
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
-- restore the Ghost mode.
when Pragma_Check => Check : declare
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Cname : Name_Id;
Eloc : Source_Ptr;
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Check;
--------------------------
-- Local variables
- Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
- -- Save the Ghost mode to restore on exit
+ Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
Errors : Nat;
Restore_Scope : Boolean := False;
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
Set_Is_Analyzed_Pragma (N);
- Restore_Ghost_Mode (Saved_GM);
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
and then Ekind (Defining_Entity (N)) /= E_Subprogram_Body;
end Is_Subprogram_Stub_Without_Prior_Declaration;
+ ---------------------------
+ -- Is_Suitable_Primitive --
+ ---------------------------
+
+ function Is_Suitable_Primitive (Subp_Id : Entity_Id) return Boolean is
+ begin
+ -- The Default_Initial_Condition and invariant procedures must not be
+ -- treated as primitive operations even when they apply to a tagged
+ -- type. These routines must not act as targets of dispatching calls
+ -- because they already utilize class-wide-precondition semantics to
+ -- handle inheritance and overriding.
+
+ if Ekind (Subp_Id) = E_Procedure
+ and then (Is_DIC_Procedure (Subp_Id)
+ or else
+ Is_Invariant_Procedure (Subp_Id))
+ then
+ return False;
+ end if;
+
+ return True;
+ end Is_Suitable_Primitive;
+
--------------------------
-- Is_Suspension_Object --
--------------------------
-- Return True if N is a subprogram stub with no prior subprogram
-- declaration.
+ function Is_Suitable_Primitive (Subp_Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary subprogram Subp_Id may act as a primitive of
+ -- an arbitrary tagged type.
+
function Is_Suspension_Object (Id : Entity_Id) return Boolean;
-- Determine whether arbitrary entity Id denotes Suspension_Object defined
-- in Ada.Synchronous_Task_Control.
-- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and
-- Ghost statements. The intent of the feature is to treat Ghost constructs
-- as non-existent when Ghost assertion policy Ignore is in effect.
-
+ --
-- The corresponding nodes which map to Ghost constructs are:
-
+ --
-- Ghost entities
-- Declaration nodes
-- N_Package_Body
-- N_Subprogram_Body
-
+ --
-- Ghost statements
-- N_Assignment_Statement
-- N_Procedure_Call_Statement
-- N_Pragma
-
+ --
-- In addition, the compiler treats instantiations as Ghost entities
-
+ --
-- To achieve the removal of ignored Ghost constructs, the compiler relies
- -- on global variable Ghost_Mode and a mechanism called "Ghost regions".
- -- The values of the global variable are as follows:
-
+ -- on global variables Ghost_Mode and Ignored_Ghost_Region, which comprise
+ -- a mechanism called "Ghost regions".
+ --
+ -- The values of Ghost_Mode are as follows:
+ --
-- 1. Check - All static semantics as defined in SPARK RM 6.9 are in
-- effect. The Ghost region has mode Check.
-
+ --
-- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI
-- files, object files, and the final executable. The Ghost region
-- has mode Ignore.
-
+ --
-- 3. None - No Ghost region is in effect
-
+ --
+ -- The value of Ignored_Ghost_Region captures the node which initiates an
+ -- ignored Ghost region.
+ --
-- A Ghost region is a compiler operating mode, similar to Check_Syntax,
-- however a region is much more finely grained and depends on the policy
-- in effect. The region starts prior to the analysis of a Ghost construct
-- and ends immediately after its expansion. The region is established as
-- follows:
-
+ --
-- 1. Declarations - Prior to analysis, if the declaration is subject to
-- pragma Ghost.
-
+ --
-- 2. Renaming declarations - Same as 1) or when the renamed entity is
-- Ghost.
-
+ --
-- 3. Completing declarations - Same as 1) or when the declaration is
-- partially analyzed and the declaration completes a Ghost entity.
-
+ --
-- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is
-- partially analyzed and completes a Ghost entity.
-
+ --
-- 5. N_Assignment_Statement - After the left hand side is analyzed and
-- references a Ghost entity.
-
+ --
-- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes
-- a Ghost procedure.
-
+ --
-- 7. N_Pragma - During analysis, when the related entity is Ghost or the
-- pragma encloses a Ghost entity.
-
+ --
-- 8. Instantiations - Save as 1) or when the instantiation is partially
-- analyzed and the generic template is Ghost.
-
- -- Routines Mark_And_Set_Ghost_xxx and Set_Ghost_Mode install a new Ghost
- -- region and routine Restore_Ghost_Mode ends a Ghost region. A region may
- -- be reinstalled similarly to scopes for decoupled expansion such as the
- -- generation of dispatch tables or the creation of a predicate function.
-
+ --
+ -- The following routines install a new Ghost region:
+ --
+ -- Install_Ghost_Region
+ -- Mark_And_Set_Ghost_xxx
+ -- Set_Ghost_Mode
+ --
+ -- The following routine ends a Ghost region:
+ --
+ -- Restore_Ghost_Region
+ --
+ -- A region may be reinstalled similarly to scopes for decoupled expansion
+ -- such as the generation of dispatch tables or the creation of a predicate
+ -- function.
+ --
-- If the mode of a Ghost region is Ignore, any newly created nodes as well
-- as source entities are marked as ignored Ghost. In additon, the marking
-- process signals all enclosing scopes that an ignored Ghost node resides
-- within. The compilation unit where the node resides is also added to an
-- auxiliary table for post processing.
-
+ --
-- After the analysis and expansion of all compilation units takes place
-- as well as the instantiation of all inlined [generic] bodies, the GNAT
-- driver initiates a separate pass which removes all ignored Ghost nodes
+2018-05-24 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * gnat.dg/formal_containers.adb: New testcase.
+
2018-05-24 Rainer Orth <ro@CeBiTec.Uni-Bielefeld.DE>
* gcc.target/i386/pr85345.c: Require ifunc support.
--- /dev/null
+-- { dg-do compile }
+
+with Ada.Containers.Formal_Hashed_Sets;
+
+procedure Formal_Containers is
+ type T is new Integer;
+
+ function Eq (X : T; Y : T) return Boolean;
+
+ function Hash (X : T) return Ada.Containers.Hash_Type is (0);
+
+ package TSet is new Ada.Containers.Formal_Hashed_Sets
+ (Element_Type => T,
+ Hash => Hash,
+ Equivalent_Elements => Eq);
+
+ S : Tset.Set := TSet.Empty_Set;
+
+ function Eq (X : T; Y : T) return Boolean is
+ begin
+ return TSet.Contains (S, X) or TSet.Contains (S, Y);
+ end Eq;
+begin null; end Formal_Containers;
projects / gcc.git / commitdiff