+2014-10-31 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb Add an entry for aspect Ghost in table
+ Canonical_Aspect.
+ * aspects.ads Add an entry for aspect Ghost in tables
+ Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and
+ Implementation_Defined_Aspect.
+ * einfo.adb: Flags 277 and 278 are now in use.
+ (Is_Checked_Ghost_Entity): New routine.
+ (Is_Ghost_Entity): Removed.
+ (Is_Ghost_Subprogram): Removed.
+ (Is_Ignored_Ghost_Entity): New routine.
+ (Set_Is_Checked_Ghost_Entity): New routine.
+ (Set_Is_Ignored_Ghost_Entity): New routine.
+ (Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and
+ Is_Ignored_Ghost_Entity.
+ * einfo.ads: Add new flags Is_Checked_Ghost_Entity
+ and Is_Ignored_Ghost_Entity along with usage in nodes.
+ (Is_Checked_Ghost_Entity): New routine and pragma Inline.
+ (Is_Ghost_Entity): Removed along with synthesized flag
+ description and usage in nodes.
+ (Is_Ghost_Subprogram): Removed along with synthesized flag description
+ and usage in nodes.
+ (Is_Ignored_Ghost_Entity): New routine and pragma Inline.
+ (Set_Is_Checked_Ghost_Entity): New routine and pragma Inline.
+ (Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline.
+ * freeze.adb (Freeze_Entity): A Ghost type cannot be effectively
+ volatile.
+ * par-prag.adb Pragma Ghost does not need special handling by
+ the parser.
+ * repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost.
+ * sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check.
+ * sem_ch3.adb (Analyze_Full_Type_Declaration): Mark
+ the type as Ghost when its enclosing context is Ghost.
+ (Analyze_Incomplete_Type_Decl): Mark the type as Ghost when
+ its enclosing context is Ghost.
+ (Analyze_Number_Declaration): Mark the number as Ghost when its
+ enclosing context is Ghost.
+ (Analyze_Object_Declaration): Mark the object as Ghost when its
+ enclosing context is Ghost. Verify the Ghost policy between
+ initial declaration and completion of a deferred constant.
+ (Analyze_Object_Contract): A Ghost variable cannot be effectively
+ volatile, imported or exported.
+ (Build_Derived_Record_Type): Mark a type extension as Ghost when it
+ implements a Ghost interface.
+ (Build_Record_Type): Inherit volatility and "ghostness" from
+ the parent type.
+ (Check_Completion): A Ghost entity declared
+ in a non-Ghost package does not require completion in a body.
+ (Implements_Ghost_Interface): New routine.
+ (Process_Full_View): Inherit "ghostness" from the partial view. Verify
+ the Ghost policy between the partial and full views. Verify the
+ completion of a Ghost type extension.
+ * sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed.
+ * sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first.
+ * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark
+ the subprogram as Ghost when its enclosing context is Ghost.
+ (Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost
+ when its enclosing context is Ghost. Verify the Ghost policy
+ between the spec and body.
+ (Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its
+ enclosing context is Ghost. Verify the Ghost policy between the spec
+ and body.
+ (Check_Conformance): A Ghost subprogram profile and a non-Ghost
+ subprogram profile are not subtype conformant.
+ (Convention_Of): Removed.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the
+ "ghostness" from the spec. Verify the Ghost policy between
+ the spec and body.
+ (Analyze_Private_Type_Declaration): Mark the type as Ghost when its
+ enclosing context is Ghost.
+ (Requires_Completion_In_Body): New routine.
+ (Unit_Requires_Body): Use Requires_Completion_In_Body.
+ (Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update
+ comment on usage and all uses of P in the body. Use
+ Requires_Completion_In_Body.
+ * sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P
+ to Pack_Id, update comment on usage and all uses of P in the body.
+ * sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness"
+ from the renamed excention.
+ (Analyze_Generic_Renaming): Inherit the "ghostness" from the
+ renamed generic subprogram.
+ (Analyze_Object_Renaming): Inherit the "ghostness" from the renamed
+ object.
+ (Analyze_Package_Renaming): Inherit the "ghostness" from the
+ renamed package.
+ (Analyze_Subprogram_Renaming): Inherit the "ghostness" from the
+ renamed subprogram.
+ * sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception
+ as Ghost when its enclosing context is Ghost.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration,
+ Analyze_Generic_Subprogram_Declaration): Mark an exception as
+ Ghost when its enclosing context is Ghost.
+ (Preanalyze_Actuals): Remove obsolete check.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+ for aspect Ghost.
+ (Check_Aspect_At_Freeze_Point): Aspects
+ Depends and Global do no need special checking at freeze point.
+ (Insert_After_SPARK_Mode): Update comment on usage.
+ * sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost.
+ * sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags.
+ (Analyze_Abstract_State): Update the grammar of the pragma. Add
+ formal parameter Pack_Id along with comment on usage. Mark an
+ abstract state as Ghost when its enclosing context is Ghost. Add
+ processing for option Ghost.
+ (Analyze_Constituent): Verify
+ that a Ghost abstract state is refined by Ghost constituents.
+ (Analyze_Pragma): "Ghost" is now a valid policy. Add checks
+ related to the use and placement of Check_Policy Ghost. Add
+ processing for pragma Ghost.
+ (Check_Ghost_Constituent): New routine.
+ (Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion.
+ (Process_Convention): Remove obsolete check.
+ (Set_Convention_From_Pragma): Remove the processing for convention
+ Ghost.
+ * sem_res.adb (Check_Ghost_Context): New routine.
+ (Resolve_Call): Verify that a reference to a Ghost entity appears in a
+ suitable context. Verify the Ghost polity between point of declaration
+ and point of use.
+ (Resolve_Entity_Name): Verify that a reference to
+ a Ghost entity appears in a suitable context. Verify the Ghost
+ polity between point of declaration and point of use.
+ * sem_util.adb (Check_Ghost_Completion): New routine.
+ (Check_Ghost_Derivation): New routine.
+ (Incomplete_Or_Partial_View): New routine.
+ (Incomplete_Or_Private_View): Removed.
+ (Is_Ghost_Entity): New routine.
+ (Is_Ghost_Statement_Or_Pragma): New routine.
+ (Is_Subject_To_Ghost): New routine.
+ (Policy_In_Effect): New routine.
+ (Set_Is_Ghost_Entity): New routine.
+ (Within_Ghost_Scope): New routine.
+ * sem_util.ads (Check_Ghost_Completion): New routine.
+ (Check_Ghost_Derivation): New routine.
+ (Incomplete_Or_Partial_View): New routine.
+ (Incomplete_Or_Private_View): Removed.
+ (Is_Ghost_Entity): New routine.
+ (Is_Ghost_Statement_Or_Pragma): New routine.
+ (Is_Subject_To_Ghost): New routine.
+ (Policy_In_Effect): New routine.
+ (Set_Is_Ghost_Entity): New routine.
+ (Within_Ghost_Scope): New routine.
+ * snames.adb-tmpl (Get_Convention_Id): Remove the entry for
+ convention Ghost.
+ (Get_Convention_Name): Remove the entry for convention Ghost.
+ * snames.ads-tmpl Remove the convention id for Ghost. Add a
+ pragma id for Ghost.
+
+2014-10-31 Sergey Rybin <rybin@adacore.com frybin>
+
+ * gnat_ugn.texi: Add description of --RTS option for ASIS tools.
+
2014-10-31 Olivier Hainque <hainque@adacore.com>
* gcc-interface/Makefile.in (arm-vxworks): Update target pairs.
Aspect_External_Name => Aspect_External_Name,
Aspect_External_Tag => Aspect_External_Tag,
Aspect_Favor_Top_Level => Aspect_Favor_Top_Level,
+ Aspect_Ghost => Aspect_Ghost,
Aspect_Global => Aspect_Global,
Aspect_Implicit_Dereference => Aspect_Implicit_Dereference,
Aspect_Import => Aspect_Import,
Aspect_Extensions_Visible, -- GNAT
Aspect_External_Name,
Aspect_External_Tag,
+ Aspect_Ghost, -- GNAT
Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
Aspect_Initial_Condition, -- GNAT
Aspect_Effective_Writes => True,
Aspect_Extensions_Visible => True,
Aspect_Favor_Top_Level => True,
+ Aspect_Ghost => True,
Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Invariant => True,
Aspect_Extensions_Visible => Optional_Expression,
Aspect_External_Name => Expression,
Aspect_External_Tag => Expression,
+ Aspect_Ghost => Optional_Expression,
Aspect_Global => Expression,
Aspect_Implicit_Dereference => Name,
Aspect_Initial_Condition => Expression,
Aspect_External_Name => Name_External_Name,
Aspect_External_Tag => Name_External_Tag,
Aspect_Favor_Top_Level => Name_Favor_Top_Level,
+ Aspect_Ghost => Name_Ghost,
Aspect_Global => Name_Global,
Aspect_Implicit_Dereference => Name_Implicit_Dereference,
Aspect_Import => Name_Import,
Aspect_Effective_Reads => Never_Delay,
Aspect_Effective_Writes => Never_Delay,
Aspect_Extensions_Visible => Never_Delay,
+ Aspect_Ghost => Never_Delay,
Aspect_Global => Never_Delay,
Aspect_Initial_Condition => Never_Delay,
Aspect_Initializes => Never_Delay,
-- (Has_Protected) Flag271
-- (SSO_Set_Low_By_Default) Flag272
-- (SSO_Set_High_By_Default) Flag273
-
-- Is_Generic_Actual_Subprogram Flag274
-- No_Predicate_On_Actual Flag275
-- No_Dynamic_Predicate_On_Actual Flag276
+ -- Is_Checked_Ghost_Entity Flag277
+ -- Is_Ignored_Ghost_Entity Flag278
- -- (unused) Flag275
- -- (unused) Flag276
- -- (unused) Flag277
- -- (unused) Flag278
-- (unused) Flag279
-- (unused) Flag280
return Flag63 (Id);
end Is_Character_Type;
+ function Is_Checked_Ghost_Entity (Id : E) return B is
+ begin
+ pragma Assert (Nkind (Id) in N_Entity);
+ return Flag277 (Id);
+ end Is_Checked_Ghost_Entity;
+
function Is_Child_Unit (Id : E) return B is
begin
return Flag73 (Id);
return Flag171 (Id);
end Is_Hidden_Open_Scope;
+ function Is_Ignored_Ghost_Entity (Id : E) return B is
+ begin
+ pragma Assert (Nkind (Id) in N_Entity);
+ return Flag278 (Id);
+ end Is_Ignored_Ghost_Entity;
+
function Is_Immediately_Visible (Id : E) return B is
begin
pragma Assert (Nkind (Id) in N_Entity);
Set_Flag63 (Id, V);
end Set_Is_Character_Type;
+ procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Formal (Id)
+ or else Is_Object (Id)
+ or else Is_Package_Or_Generic_Package (Id)
+ or else Is_Subprogram_Or_Generic_Subprogram (Id)
+ or else Is_Type (Id)
+ or else Ekind (Id) = E_Abstract_State
+ or else Ekind (Id) = E_Component
+ or else Ekind (Id) = E_Discriminant
+ or else Ekind (Id) = E_Package_Body
+ or else Ekind (Id) = E_Subprogram_Body);
+ Set_Flag277 (Id, V);
+ end Set_Is_Checked_Ghost_Entity;
+
procedure Set_Is_Child_Unit (Id : E; V : B := True) is
begin
Set_Flag73 (Id, V);
procedure Set_Is_Generic_Actual_Subprogram (Id : E; V : B := True) is
begin
- pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+ pragma Assert (Ekind_In (Id, E_Function, E_Procedure));
Set_Flag274 (Id, V);
end Set_Is_Generic_Actual_Subprogram;
Set_Flag171 (Id, V);
end Set_Is_Hidden_Open_Scope;
+ procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Formal (Id)
+ or else Is_Object (Id)
+ or else Is_Package_Or_Generic_Package (Id)
+ or else Is_Subprogram_Or_Generic_Subprogram (Id)
+ or else Is_Type (Id)
+ or else Ekind (Id) = E_Abstract_State
+ or else Ekind (Id) = E_Component
+ or else Ekind (Id) = E_Discriminant
+ or else Ekind (Id) = E_Package_Body
+ or else Ekind (Id) = E_Subprogram_Body);
+ Set_Flag278 (Id, V);
+ end Set_Is_Ignored_Ghost_Entity;
+
procedure Set_Is_Immediately_Visible (Id : E; V : B := True) is
begin
pragma Assert (Nkind (Id) in N_Entity);
return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer;
end Is_Finalizer;
- ---------------------
- -- Is_Ghost_Entity --
- ---------------------
-
- -- Note: coding below allows for ghost variables. They are not currently
- -- implemented, so we will always get False for variables, but that is
- -- expected to change in the future.
-
- function Is_Ghost_Entity (Id : E) return B is
- begin
- if Present (Id) and then Ekind (Id) = E_Variable then
- return Convention (Id) = Convention_Ghost;
- else
- return Is_Ghost_Subprogram (Id);
- end if;
- end Is_Ghost_Entity;
-
- -------------------------
- -- Is_Ghost_Subprogram --
- -------------------------
-
- function Is_Ghost_Subprogram (Id : E) return B is
- begin
- if Present (Id) and then Ekind_In (Id, E_Function, E_Procedure) then
- return Convention (Id) = Convention_Ghost;
- else
- return False;
- end if;
- end Is_Ghost_Subprogram;
-
-------------------
-- Is_Null_State --
-------------------
W ("Is_CPP_Class", Flag74 (Id));
W ("Is_Called", Flag102 (Id));
W ("Is_Character_Type", Flag63 (Id));
+ W ("Is_Checked_Ghost_Entity", Flag277 (Id));
W ("Is_Child_Unit", Flag73 (Id));
W ("Is_Class_Wide_Equivalent_Type", Flag35 (Id));
W ("Is_Compilation_Unit", Flag149 (Id));
W ("Is_Hidden", Flag57 (Id));
W ("Is_Hidden_Non_Overridden_Subpgm", Flag2 (Id));
W ("Is_Hidden_Open_Scope", Flag171 (Id));
+ W ("Is_Ignored_Ghost_Entity", Flag278 (Id));
W ("Is_Immediately_Visible", Flag7 (Id));
W ("Is_Implementation_Defined", Flag254 (Id));
W ("Is_Imported", Flag24 (Id));
-- Defined in all entities. Set for character types and subtypes,
-- i.e. enumeration types that have at least one character literal.
+-- Is_Checked_Ghost_Entity (Flag277)
+-- Applies to all entities. Set for abstract states, [generic] packages,
+-- [generic] subprograms, components, discriminants, formal parameters,
+-- objects, package bodies, subprogram bodies, and [sub]types subject to
+-- pragma Ghost or inherit "ghostness" from an enclosing construct, and
+-- subject to Assertion_Policy Ghost => Check.
+
-- Is_Child_Unit (Flag73)
-- Defined in all entities. Set only for defining entities of program
-- units that are child units (but False for subunits).
-- package, generic function, generic procedure), and False for all
-- other entities.
--- Is_Ghost_Entity (synthesized)
--- Applies to all entities. Yields True for a subprogram or a whole
--- object that has convention Ghost. For now only functions can have
--- Ghost convention, so this will be false for other than functions,
--- but we expect that to change in the future.
-
--- Is_Ghost_Subprogram (synthesized)
--- Applies to all entities. Yields True for a subprogram that has a Ghost
--- convention. Note: for now, only ghost functions are allowed, so this
--- will always be false for procedures, but that is expected to change in
--- the future.
-
-- Is_Hidden (Flag57)
-- Defined in all entities. Set for all entities declared in the
-- private part or body of a package. Also marks generic formals of a
-- instantiation of a child unit, and whose entities are not visible
-- during analysis of the instance.
+-- Is_Ignored_Ghost_Entity (Flag278)
+-- Applies to all entities. Set for abstract states, [generic] packages,
+-- [generic] subprograms, components, discriminants, formal parameters,
+-- objects, package bodies, subprogram bodies, and [sub]types subject to
+-- pragma Ghost or inherit "ghostness" from an enclosing construct, and
+-- subject to Assertion_Policy Ghost => Ignore.
+
-- Is_Immediately_Visible (Flag7)
-- Defined in all entities. Set if entity is immediately visible, i.e.
-- is defined in some currently open scope (RM 8.3(4)).
-- Is_Bit_Packed_Array (Flag122) (base type only)
-- Is_Aliased (Flag15)
-- Is_Character_Type (Flag63)
+ -- Is_Checked_Ghost_Entity (Flag277)
-- Is_Child_Unit (Flag73)
-- Is_Compilation_Unit (Flag149)
-- Is_Completely_Hidden (Flag103)
-- Is_Generic_Type (Flag13)
-- Is_Hidden (Flag57)
-- Is_Hidden_Open_Scope (Flag171)
+ -- Is_Ignored_Ghost_Entity (Flag278)
-- Is_Immediately_Visible (Flag7)
-- Is_Implementation_Defined (Flag254)
-- Is_Imported (Flag24)
-- Address_Clause (synth)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
- -- Is_Ghost_Entity (synth) (non-generic case only)
- -- Is_Ghost_Subprogram (synth) (non-generic case only)
-- Last_Formal (synth)
-- Number_Formals (synth)
-- Scope_Depth (synth)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
-- Is_Finalizer (synth)
- -- Is_Ghost_Entity (synth) (non-generic case only)
- -- Is_Ghost_Subprogram (synth) (non-generic case only)
-- Last_Formal (synth)
-- Number_Formals (synth)
-- Treat_As_Volatile (Flag41)
-- Address_Clause (synth)
-- Alignment_Clause (synth)
- -- Is_Ghost_Entity (synth)
-- Size_Clause (synth)
-- E_Void
function Is_CPP_Class (Id : E) return B;
function Is_Called (Id : E) return B;
function Is_Character_Type (Id : E) return B;
+ function Is_Checked_Ghost_Entity (Id : E) return B;
function Is_Child_Unit (Id : E) return B;
function Is_Class_Wide_Equivalent_Type (Id : E) return B;
function Is_Compilation_Unit (Id : E) return B;
function Is_Hidden (Id : E) return B;
function Is_Hidden_Non_Overridden_Subpgm (Id : E) return B;
function Is_Hidden_Open_Scope (Id : E) return B;
+ function Is_Ignored_Ghost_Entity (Id : E) return B;
function Is_Immediately_Visible (Id : E) return B;
function Is_Implementation_Defined (Id : E) return B;
function Is_Imported (Id : E) return B;
function Is_Dynamic_Scope (Id : E) return B;
function Is_External_State (Id : E) return B;
function Is_Finalizer (Id : E) return B;
- function Is_Ghost_Entity (Id : E) return B;
- function Is_Ghost_Subprogram (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
function Is_Packed_Array (Id : E) return B;
procedure Set_Is_CPP_Class (Id : E; V : B := True);
procedure Set_Is_Called (Id : E; V : B := True);
procedure Set_Is_Character_Type (Id : E; V : B := True);
+ procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True);
procedure Set_Is_Child_Unit (Id : E; V : B := True);
procedure Set_Is_Class_Wide_Equivalent_Type (Id : E; V : B := True);
procedure Set_Is_Compilation_Unit (Id : E; V : B := True);
procedure Set_Is_Hidden (Id : E; V : B := True);
procedure Set_Is_Hidden_Non_Overridden_Subpgm (Id : E; V : B := True);
procedure Set_Is_Hidden_Open_Scope (Id : E; V : B := True);
+ procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True);
procedure Set_Is_Immediately_Visible (Id : E; V : B := True);
procedure Set_Is_Implementation_Defined (Id : E; V : B := True);
procedure Set_Is_Imported (Id : E; V : B := True);
pragma Inline (Is_CPP_Class);
pragma Inline (Is_Called);
pragma Inline (Is_Character_Type);
+ pragma Inline (Is_Checked_Ghost_Entity);
pragma Inline (Is_Child_Unit);
pragma Inline (Is_Class_Wide_Equivalent_Type);
pragma Inline (Is_Class_Wide_Type);
pragma Inline (Is_Hidden);
pragma Inline (Is_Hidden_Non_Overridden_Subpgm);
pragma Inline (Is_Hidden_Open_Scope);
+ pragma Inline (Is_Ignored_Ghost_Entity);
pragma Inline (Is_Immediately_Visible);
pragma Inline (Is_Implementation_Defined);
pragma Inline (Is_Imported);
pragma Inline (Set_Is_CPP_Class);
pragma Inline (Set_Is_Called);
pragma Inline (Set_Is_Character_Type);
+ pragma Inline (Set_Is_Checked_Ghost_Entity);
pragma Inline (Set_Is_Child_Unit);
pragma Inline (Set_Is_Class_Wide_Equivalent_Type);
pragma Inline (Set_Is_Compilation_Unit);
pragma Inline (Set_Is_Hidden);
pragma Inline (Set_Is_Hidden_Non_Overridden_Subpgm);
pragma Inline (Set_Is_Hidden_Open_Scope);
+ pragma Inline (Set_Is_Ignored_Ghost_Entity);
pragma Inline (Set_Is_Immediately_Visible);
pragma Inline (Set_Is_Implementation_Defined);
pragma Inline (Set_Is_Imported);
end if;
end;
+ -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
+
+ if Is_Ghost_Entity (E)
+ and then Is_Effectively_Volatile (E)
+ then
+ SPARK_Msg_N ("ghost type & cannot be volatile", E);
+ end if;
+
-- Deal with special cases of freezing for subtype
if E /= Base_Type (E) then
has the value @var{value}. Has no effect if no project is specified as
tool argument.
+@item --RTS=@var{rts-path}
+@cindex @option{--RTS} (@command{gnatelim})
+Specifies the default location of the runtime library. Same meaning as the
+equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}).
+
@item -files=@var{filename}
@cindex @option{-files} (@code{gnatelim})
Take the argument source files from the specified file. This file should be an
@item -gnatec=@var{path}
@cindex @option{-gnatec} (@command{gnatpp})
-@item --RTS=@var{path}
-@cindex @option{--RTS} (@command{gnatpp})
-
@end table
@node Output File Control
has the value @var{value}. Has no effect if no project is specified as
tool argument.
+@item --RTS=@var{rts-path}
+@cindex @option{--RTS} (@command{gnatpp})
+Specifies the default location of the runtime library. Same meaning as the
+equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}).
+
@item --incremental
@cindex @option{--incremental} @command{gnatpp}
Incremental processing on a per-file basis. Source files are only
the argument project has the value @var{value}. Has no effect if no
project is specified as tool argument.
+--RTS=@var{rts-path} -- Specifies the default location of the runtime
+ library. Same meaning as the equivalent @command{gnatmake} flag
+ (@pxref{Switches for gnatmake}).
+
--incremental -- incremental processing on a per-file basis. Source files are
only processed if they have been modified, or if files they depend
on have been modified. This is similar to the way gnatmake/gprbuild
has the value @var{value}. Has no effect if no project is specified as
tool argument.
+@item --RTS=@var{rts-path}
+@cindex @option{--RTS} (@command{gnatmetric})
+Specifies the default location of the runtime library. Same meaning as the
+equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}).
+
@item --subdirs=@var{dir}
@cindex @option{--subdirs=@var{dir}} @command{gnatmetric}
Use the specified subdirectory of the project objects file (or of the
has the value @var{value}. Has no effect if no project is specified as
tool argument.
+@item --RTS=@var{rts-path}
+@cindex @option{--RTS} (@command{gnatstub})
+Specifies the default location of the runtime library. Same meaning as the
+equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}).
+
@item --subunits
@cindex @option{--subunits} (@command{gnatstub})
Generate subunits for body stubs. If this switch is specified,
@cindex @option{-X} (@command{gnattest})
Indicate that external variable @var{name} has the value @var{value}.
+@item --RTS=@var{rts-path}
+@cindex @option{--RTS} (@command{gnattest})
+Specifies the default location of the runtime library. Same meaning as the
+equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}).
+
@item -q
@cindex @option{-q} (@command{gnattest})
Suppresses noncritical output messages.
Pragma_Favor_Top_Level |
Pragma_Fast_Math |
Pragma_Finalize_Storage_Only |
+ Pragma_Ghost |
Pragma_Global |
Pragma_Ident |
Pragma_Implementation_Defined |
Write_Line ("Intrinsic");
when Convention_Entry =>
Write_Line ("Entry");
- when Convention_Ghost =>
- Write_Line ("Ghost");
when Convention_Protected =>
Write_Line ("Protected");
when Convention_Assembler =>
elsif Aname = Name_Unchecked_Access then
Error_Attr ("attribute% cannot be applied to a subprogram", P);
-
- elsif Is_Ghost_Subprogram (Entity (P)) then
- Error_Attr_P
- ("prefix of % attribute cannot be a ghost subprogram");
end if;
-- Issue an error if the prefix denotes an eliminated subprogram
Set_Is_Statically_Allocated (Id);
Set_Is_Pure (Id, PF);
+ -- An exception declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
+ -- A generic package declared within a Ghost scope is rendered Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
Set_Etype (Id, Standard_Void_Type);
end if;
+ -- A generic subprogram declared within a Ghost scope is rendered Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
-- For a library unit, we have reconstructed the entity for the unit,
-- and must reset it in the library tables. We also make sure that
-- Body_Required is set properly in the original compilation unit node.
Analyze (Act);
end if;
- -- Ensure that a ghost subprogram does not act as generic actual
-
- if Is_Entity_Name (Act)
- and then Is_Ghost_Subprogram (Entity (Act))
- then
- Error_Msg_N
- ("ghost subprogram & cannot act as generic actual", Act);
- Abandon_Instantiation (Act);
-
- elsif Errs /= Serious_Errors_Detected then
+ if Errs /= Serious_Errors_Detected then
-- Do a minimal analysis of the generic, to prevent spurious
-- warnings complaining about the generic being unreferenced,
(Prag : Node_Id;
Ins_Nod : Node_Id;
Decls : List_Id);
- -- Subsidiary to the analysis of aspects Abstract_State, Initializes,
- -- Initial_Condition and Refined_State. Insert node Prag before node
- -- Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip SPARK_Mode.
- -- Decls is the associated declarative list where Prag is to reside.
+ -- Subsidiary to the analysis of aspects Abstract_State, Ghost,
+ -- Initializes, Initial_Condition and Refined_State. Insert node Prag
+ -- before node Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip
+ -- SPARK_Mode. Decls is the associated declarative list where Prag is to
+ -- reside.
procedure Insert_Pragma (Prag : Node_Id);
-- Subsidiary to the analysis of aspects Attach_Handler, Contract_Cases,
end loop;
end if;
- -- Pragma Abstract_State must be inserted after pragma
- -- SPARK_Mode in the tree. This ensures that any error
- -- messages dependent on SPARK_Mode will be properly
- -- enabled/suppressed.
+ -- When aspects Abstract_State, Ghost,
+ -- Initial_Condition and Initializes are out of order,
+ -- ensure that pragma SPARK_Mode is always at the top
+ -- of the declarations to properly enabled/suppress
+ -- errors.
Insert_After_SPARK_Mode
(Prag => Aitem,
Insert_Pragma (Aitem);
goto Continue;
+ -- Aspect Ghost is never delayed because it is equivalent to a
+ -- source pragma which appears at the top of [generic] package
+ -- declarations or after an object, a [generic] subprogram, or
+ -- a type declaration.
+
+ when Aspect_Ghost => Ghost : declare
+ Decls : List_Id;
+
+ begin
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Ghost);
+
+ Decorate (Aspect, Aitem);
+
+ -- When the aspect applies to a [generic] package, insert
+ -- the pragma at the top of the visible declarations. This
+ -- emulates the placement of a source pragma.
+
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decls := Visible_Declarations (Specification (N));
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (N, Decls);
+ end if;
+
+ -- When aspects Abstract_State, Ghost, Initial_Condition
+ -- and Initializes are out of order, ensure that pragma
+ -- SPARK_Mode is always at the top of the declarations to
+ -- properly enabled/suppress errors.
+
+ Insert_After_SPARK_Mode
+ (Prag => Aitem,
+ Ins_Nod => First (Decls),
+ Decls => Decls);
+
+ -- Otherwise the context is an object, [generic] subprogram
+ -- or type declaration.
+
+ else
+ Insert_Pragma (Aitem);
+ end if;
+
+ goto Continue;
+ end Ghost;
+
-- Global
-- Aspect Global is never delayed because it is equivalent to
Set_Visible_Declarations (Context, Decls);
end if;
- -- When aspects Abstract_State, Initial_Condition and
- -- Initializes are out of order, ensure that pragma
- -- SPARK_Mode is always at the top of the declarative
- -- list to properly enable/suppress errors.
+ -- When aspects Abstract_State, Ghost, Initial_Condition
+ -- and Initializes are out of order, ensure that pragma
+ -- SPARK_Mode is always at the top of the declarations to
+ -- properly enabled/suppress errors.
Insert_After_SPARK_Mode
(Prag => Aitem,
Set_Visible_Declarations (Context, Decls);
end if;
- -- When aspects Abstract_State, Initial_Condition and
- -- Initializes are out of order, ensure that pragma
- -- SPARK_Mode is always at the top of the declarative
- -- list to properly enable/suppress errors.
+ -- When aspects Abstract_State, Ghost, Initial_Condition
+ -- and Initializes are out of order, ensure that pragma
+ -- SPARK_Mode is always at the top of the declarations to
+ -- properly enabled/suppress errors.
Insert_After_SPARK_Mode
(Prag => Aitem,
when Aspect_Default_Value =>
T := Entity (ASN);
- -- Depends is a delayed aspect because it mentiones names first
- -- introduced by aspect Global which is already delayed. There is
- -- no action to be taken with respect to the aspect itself as the
- -- analysis is done by the corresponding pragma.
-
- when Aspect_Depends =>
- return;
-
when Aspect_Dispatching_Domain =>
T := RTE (RE_Dispatching_Domain);
when Aspect_External_Name =>
T := Standard_String;
- -- Global is a delayed aspect because it may reference names that
- -- have not been declared yet. There is no action to be taken with
- -- respect to the aspect itself as the reference checking is done
- -- on the corresponding pragma.
-
- when Aspect_Global =>
- return;
-
when Aspect_Link_Name =>
T := Standard_String;
Aspect_Annotate |
Aspect_Contract_Cases |
Aspect_Default_Initial_Condition |
+ Aspect_Depends |
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Extensions_Visible |
+ Aspect_Ghost |
+ Aspect_Global |
Aspect_Implicit_Dereference |
Aspect_Initial_Condition |
Aspect_Initializes |
Set_Analyzed (T);
case Nkind (Def) is
-
when N_Access_To_Subprogram_Definition =>
Access_Subprogram_Declaration (T, Def);
Check_SPARK_05_Restriction ("controlled type is not allowed", N);
end if;
+ -- A type declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Comes_From_Source (T) and then Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (T);
+ end if;
+
-- Some common processing for all types
Set_Depends_On_Private (T, Has_Private_Component (T));
Check_Ops_From_Incomplete_Type;
- -- Both the declared entity, and its anonymous base type if one
- -- was created, need freeze nodes allocated.
+ -- Both the declared entity, and its anonymous base type if one was
+ -- created, need freeze nodes allocated.
declare
B : constant Entity_Id := Base_Type (T);
Set_Is_First_Subtype (T, True);
Set_Etype (T, T);
+ -- An incomplete type declared within a Ghost scope is automatically
+ -- Ghost (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (T);
+ end if;
+
-- Ada 2005 (AI-326): Minimum decoration to give support to tagged
-- incomplete types.
Generate_Definition (Id);
Enter_Name (Id);
+ -- A number declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
-- This is an optimization of a common case of an integer literal
if Nkind (E) = N_Integer_Literal then
Seen : Boolean := False;
begin
+ -- The loop parameter in an element iterator over a formal container
+ -- is declared with an object declaration but no contracts apply.
+
+ if Ekind (Obj_Id) = E_Loop_Parameter then
+ return;
+ end if;
+
if Ekind (Obj_Id) = E_Constant then
-- A constant cannot be effectively volatile. This check is only
Error_Msg_N ("constant cannot be volatile", Obj_Id);
end if;
- -- The loop parameter in an element iterator over a formal container
- -- is declared with an object declaration but no contracts apply.
-
- elsif Ekind (Obj_Id) = E_Loop_Parameter then
- null;
-
else pragma Assert (Ekind (Obj_Id) = E_Variable);
-- The following checks are only relevant when SPARK_Mode is on as
Obj_Id);
end if;
end if;
+
+ if Is_Ghost_Entity (Obj_Id) then
+
+ -- A Ghost object cannot be effectively volatile
+ -- (SPARK RM 6.9(8)).
+
+ if Is_Effectively_Volatile (Obj_Id) then
+ SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+
+ -- A Ghost object cannot be imported or exported
+ -- (SPARK RM 6.9(8)).
+
+ elsif Is_Imported (Obj_Id) then
+ SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+
+ elsif Is_Exported (Obj_Id) then
+ SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
+ end if;
+ end if;
end if;
-- Analyze all external properties
Check_Missing_Part_Of (Obj_Id);
end if;
end if;
+
+ -- A ghost object cannot be imported or exported (SPARK RM 6.9(8))
+
+ if Is_Ghost_Entity (Obj_Id) then
+ if Is_Exported (Obj_Id) then
+ SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
+
+ elsif Is_Imported (Obj_Id) then
+ SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ end if;
+ end if;
end Analyze_Object_Contract;
--------------------------------
-- and must not be unconstrained. (The only exception to this is the
-- acceptance of declarations of constants of type String.)
- if not
- Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
+ if not Nkind_In (Object_Definition (N), N_Expanded_Name, N_Identifier)
then
Check_SPARK_05_Restriction
("subtype mark required", Object_Definition (N));
Set_Ekind (Id, E_Variable);
end if;
+ -- An object declared within a Ghost scope is automatically
+ -- Ghost (SPARK RM 6.9(2)).
+
+ if Comes_From_Source (Id) and then Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+
+ -- The Ghost policy in effect at the point of declaration
+ -- and at the point of completion must match
+ -- (SPARK RM 6.9(14)).
+
+ if Present (Prev_Entity)
+ and then Is_Ghost_Entity (Prev_Entity)
+ then
+ Check_Ghost_Completion (Prev_Entity, Id);
+ end if;
+ end if;
+
Rewrite (N,
Make_Object_Renaming_Declaration (Loc,
Defining_Identifier => Id,
-- true for variables so far (will be reset for a variable if and when
-- we encounter a modification in the source).
- Set_Never_Set_In_Source (Id, True);
+ Set_Never_Set_In_Source (Id);
-- Now establish the proper kind and type of the object
-- the case of exception choice variables, it will already be true).
if Present (E) then
- Set_Has_Initial_Value (Id, True);
+ Set_Has_Initial_Value (Id);
end if;
Set_Contract (Id, Make_Contract (Sloc (Id)));
Init_Esize (Id);
Set_Optimize_Alignment_Flags (Id);
+ -- An object declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)). This property is also inherited when its type
+ -- is Ghost or the previous declaration of the deferred constant is
+ -- Ghost.
+
+ if Comes_From_Source (Id)
+ and then (Is_Ghost_Entity (T)
+ or else (Present (Prev_Entity)
+ and then Is_Ghost_Entity (Prev_Entity))
+ or else Within_Ghost_Scope)
+ then
+ Set_Is_Ghost_Entity (Id);
+
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
+
+ if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
+ Check_Ghost_Completion (Prev_Entity, Id);
+ end if;
+ end if;
+
-- Deal with aliased case
if Aliased_Present (N) then
Derived_Type : Entity_Id;
Derive_Subps : Boolean := True)
is
+ function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ implements at least one Ghost interface
+
+ --------------------------------
+ -- Implements_Ghost_Interface --
+ --------------------------------
+
+ function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
+ Iface_Elmt : Elmt_Id;
+ begin
+ -- Traverse the list of interfaces looking for a Ghost interface
+
+ if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
+ Iface_Elmt := First_Elmt (Interfaces (Typ));
+ while Present (Iface_Elmt) loop
+ if Is_Ghost_Entity (Node (Iface_Elmt)) then
+ return True;
+ end if;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Implements_Ghost_Interface;
+
+ -- Local variables
+
Discriminant_Specs : constant Boolean :=
Present (Discriminant_Specifications (N));
Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type);
-- An empty Discs list means that there were no constraints in the
-- subtype indication or that there was an error processing it.
+ -- Start of processing for Build_Derived_Record_Type
+
begin
if Ekind (Parent_Type) = E_Record_Type_With_Private
and then Present (Full_View (Parent_Type))
declare
Corr_Disc : constant Entity_Id :=
- Corresponding_Discriminant (Discrim);
+ Corresponding_Discriminant (Discrim);
Disc_Type : constant Entity_Id := Etype (Discrim);
Corr_Type : Entity_Id;
if Is_Itype (Derived_Type) then
declare
Def : constant Node_Id :=
- Associated_Node_For_Itype (Derived_Type);
+ Associated_Node_For_Itype (Derived_Type);
begin
if Present (Def)
and then Nkind (Def) = N_Full_Type_Declaration
end if;
end;
end if;
+
+ -- A type extension is automatically Ghost when one of its
+ -- progenitors is Ghost (SPARK RM 6.9(9)). This property is
+ -- also inherited when the parent type is Ghost, but this is
+ -- done in Build_Derived_Type as the mechanism also handles
+ -- untagged derivations.
+
+ if Implements_Ghost_Interface (Derived_Type) then
+ Set_Is_Ghost_Entity (Derived_Type);
+ end if;
end;
end if;
Set_RM_Size (Derived_Type, RM_Size (Parent_Type));
Set_Is_Controlled (Derived_Type, Is_Controlled (Parent_Type));
Set_Is_Tagged_Type (Derived_Type, Is_Tagged_Type (Parent_Type));
+ Set_Is_Volatile (Derived_Type, Is_Volatile (Parent_Type));
if Is_Tagged_Type (Derived_Type) then
Set_No_Tagged_Streams_Pragma
-- type may be set in the private part, and not propagated to the
-- subtype until later, so we obtain the convention from the base type.
- Set_Convention (Derived_Type, Convention (Parent_Base));
+ Set_Convention (Derived_Type, Convention (Parent_Base));
-- Set SSO default for record or array type
Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type);
end if;
+ -- Propagate the attributes related to pragma Ghost from the parent type
+ -- to the derived type or type extension (SPARK RM 6.9(9)).
+
+ if Is_Ghost_Entity (Parent_Type) then
+ Set_Is_Ghost_Entity (Derived_Type);
+ end if;
+
-- Type dependent processing
case Ekind (Parent_Type) is
end if;
end Post_Error;
+ -- Local variables
+
+ Pack_Id : constant Entity_Id := Current_Scope;
+
-- Start of processing for Check_Completion
begin
- E := First_Entity (Current_Scope);
+ E := First_Entity (Pack_Id);
while Present (E) loop
if Is_Intrinsic_Subprogram (E) then
null;
+ -- A Ghost entity declared in a non-Ghost package does not force the
+ -- need for a body (SPARK RM 6.9(11)).
+
+ elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (E) then
+ null;
+
-- The following situation requires special handling: a child unit
-- that appears in the context clause of the body of its parent:
-- this kind is reserved for predefined operators, that are
-- intrinsic and do not need completion.
- elsif Ekind_In (E, E_Function,
- E_Procedure,
- E_Generic_Function,
- E_Generic_Procedure)
+ elsif Ekind_In (E, E_Function,
+ E_Procedure,
+ E_Generic_Function,
+ E_Generic_Procedure)
then
if Has_Completion (E) then
null;
then
Error_Msg_Sloc := Sloc (Prev);
Error_Msg_N
- ("full constant for declaration#"
- & " must be in private part", N);
+ ("full constant for declaration # must be in private part", N);
elsif Ekind (Current_Scope) = E_Package
and then
and then Designated_Type (Etype (New_Subp)) =
Derived_Type
and then not Is_Null_Extension (Derived_Type))
- or else Is_EVF_Procedure (Alias (New_Subp)))
+ or else (Comes_From_Source (Alias (New_Subp))
+ and then Is_EVF_Procedure (Alias (New_Subp))))
and then No (Actual_Subp)
then
if not Is_Tagged_Type (Derived_Type)
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)).
+
+ Check_Ghost_Completion (Priv_T, Full_T);
+
+ -- In the case where the private view of a tagged type lacks a parent
+ -- type and is subject to pragma Ghost, ensure that the parent type
+ -- specified by the full view is also Ghost (SPARK RM 6.9(9)).
+
+ if Is_Derived_Type (Full_T) then
+ Check_Ghost_Derivation (Full_T);
+ end if;
+ end if;
+
-- Propagate invariants to full type
if Has_Invariants (Priv_T) then
-- Flag indicates whether an interpretation of the prefix is a
-- parameterless call that returns an access_to_subprogram.
- procedure Check_Ghost_Subprogram_Call;
- -- Verify the legality of a call to a ghost subprogram. Such calls can
- -- appear only in assertion expressions except subtype predicates or
- -- from within another ghost subprogram.
-
procedure Check_Mixed_Parameter_And_Named_Associations;
-- Check that parameter and named associations are not mixed. This is
-- a restriction in SPARK mode.
procedure No_Interpretation;
-- Output error message when no valid interpretation exists
- ---------------------------------
- -- Check_Ghost_Subprogram_Call --
- ---------------------------------
-
- procedure Check_Ghost_Subprogram_Call is
- S : Entity_Id;
-
- begin
- -- Do not perform the check while preanalyzing the enclosing context
- -- because the call is not in its final place. Premature attempts to
- -- verify the placement lead to bogus errors.
-
- if In_Spec_Expression then
- return;
-
- -- The ghost subprogram appears inside an assertion expression which
- -- is one of the allowed cases.
-
- elsif In_Assertion_Expression_Pragma (N) then
- return;
-
- -- Otherwise see if it inside another ghost subprogram
-
- else
- -- Loop to climb scopes
-
- S := Current_Scope;
- while Present (S) and then S /= Standard_Standard loop
-
- -- The call appears inside another ghost subprogram
-
- if Is_Ghost_Subprogram (S) then
- return;
- end if;
-
- S := Scope (S);
- end loop;
-
- -- If we fall through the loop it was not within another
- -- ghost subprogram, so we have bad placement.
-
- Error_Msg_N
- ("call to ghost subprogram must appear in assertion expression "
- & "or another ghost subprogram", N);
- end if;
- end Check_Ghost_Subprogram_Call;
-
--------------------------------------------------
-- Check_Mixed_Parameter_And_Named_Associations --
--------------------------------------------------
End_Interp_List;
end if;
-
- -- A call to a ghost subprogram is allowed only in assertion expressions
- -- excluding subtype predicates or from within another ghost subprogram.
-
- if Is_Ghost_Subprogram (Get_Subprogram_Entity (N)) then
- Check_Ghost_Subprogram_Call;
- end if;
end Analyze_Call;
-----------------------------
begin
Mark_Coextensions (N, Rhs);
- Analyze (Rhs);
+ -- Analyze the target of the assignment first in case the expression
+ -- contains references to Ghost entities. The checks that verify the
+ -- proper use of a Ghost entity need to know the enclosing context.
+
Analyze (Lhs);
+ Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
-- as Safe_To_Reevaluate.
Set_Categorization_From_Scope (Designator, Scop);
+ -- An abstract subprogram declared within a Ghost scope is automatically
+ -- Ghost (SPARK RM 6.9(2)).
+
+ if Comes_From_Source (Designator) and then Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Designator);
+ end if;
+
if Ekind (Scope (Designator)) = E_Protected_Type then
Error_Msg_N
("abstract subprogram not allowed in protected type", N);
Set_Convention (Body_Id, Convention (Gen_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Scope (Body_Id, Scope (Gen_Id));
+
+ -- Inherit the "ghostness" of the generic spec. Note that this
+ -- property is not directly inherited as the body may be subject
+ -- to a different Ghost assertion policy.
+
+ if Is_Ghost_Entity (Gen_Id) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Body_Id);
+
+ -- The Ghost policy in effect at the point of declaration and at
+ -- the point of completion must match (SPARK RM 6.9(14)).
+
+ Check_Ghost_Completion (Gen_Id, Body_Id);
+ end if;
+
Check_Fully_Conformant (Body_Id, Gen_Id, Body_Id);
if Nkind (N) = N_Subprogram_Body_Stub then
Set_Convention (Body_Id, Convention (Spec_Id));
Set_Has_Completion (Spec_Id);
+ -- Inherit the "ghostness" of the subprogram spec. Note that this
+ -- property is not directly inherited as the body may be subject
+ -- to a different Ghost assertion policy.
+
+ if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Body_Id);
+
+ -- The Ghost policy in effect at the point of declaration and
+ -- at the point of completion must match (SPARK RM 6.9(14)).
+
+ Check_Ghost_Completion (Spec_Id, Body_Id);
+ end if;
+
if Is_Protected_Type (Scope (Spec_Id)) then
Prot_Typ := Scope (Spec_Id);
end if;
Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Designator, True);
+ -- A subprogram declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Comes_From_Source (Designator) and then Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Designator);
+ end if;
+
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
if Old_Type /= Standard_Void_Type
and then New_Type /= Standard_Void_Type
then
-
-- If we are checking interface conformance we omit controlling
-- arguments and result, because we are only checking the conformance
-- of the remaining parameters.
then
Conformance_Error ("\formal subprograms not allowed!");
return;
+
+ -- Pragma Ghost behaves as a convention in the context of subtype
+ -- conformance (SPARK RM 6.9(5)).
+
+ elsif Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id) then
+ Conformance_Error ("\ghost modes do not match!");
+ return;
end if;
end if;
----------------------
procedure Check_Convention (Op : Entity_Id) is
- function Convention_Of (Id : Entity_Id) return Convention_Id;
- -- Given an entity, return its convention. The function treats Ghost
- -- as convention Ada because the two have the same dynamic semantics.
-
- -------------------
- -- Convention_Of --
- -------------------
-
- function Convention_Of (Id : Entity_Id) return Convention_Id is
- Conv : constant Convention_Id := Convention (Id);
- begin
- if Conv = Convention_Ghost then
- return Convention_Ada;
- else
- return Conv;
- end if;
- end Convention_Of;
-
- -- Local variables
-
- Op_Conv : constant Convention_Id := Convention_Of (Op);
+ Op_Conv : constant Convention_Id := Convention (Op);
Iface_Conv : Convention_Id;
Iface_Elmt : Elmt_Id;
Iface_Prim_Elmt : Elmt_Id;
Iface_Prim : Entity_Id;
- -- Start of processing for Check_Convention
-
begin
Iface_Elmt := First_Elmt (Ifaces_List);
while Present (Iface_Elmt) loop
First_Elmt (Primitive_Operations (Node (Iface_Elmt)));
while Present (Iface_Prim_Elmt) loop
Iface_Prim := Node (Iface_Prim_Elmt);
- Iface_Conv := Convention_Of (Iface_Prim);
+ Iface_Conv := Convention (Iface_Prim);
if Is_Interface_Conformant (Typ, Iface_Prim, Op)
and then Iface_Conv /= Op_Conv
-- created at the beginning of the corresponding package body and inserted
-- before other body declarations.
- procedure Install_Package_Entity (Id : Entity_Id);
- -- Supporting procedure for Install_{Visible,Private}_Declarations. Places
- -- one entity on its visibility chain, and recurses on the visible part if
- -- the entity is an inner package.
-
- function Is_Private_Base_Type (E : Entity_Id) return Boolean;
- -- True for a private type that is not a subtype
-
- function Is_Visible_Dependent (Dep : Entity_Id) return Boolean;
- -- If the private dependent is a private type whose full view is derived
- -- from the parent type, its full properties are revealed only if we are in
- -- the immediate scope of the private dependent. Should this predicate be
- -- tightened further???
-
procedure Declare_Inherited_Private_Subprograms (Id : Entity_Id);
-- Called upon entering the private part of a public child package and the
-- body of a nested package, to potentially declare certain inherited
-- inherited private operation has been overridden, then it's replaced by
-- the overriding operation.
- procedure Unit_Requires_Body_Info (P : Entity_Id);
- -- Outputs info messages showing why package specification P requires a
- -- body. Caller has checked that the switch requesting this information
- -- is set, and that the package does indeed require a body.
+ procedure Install_Package_Entity (Id : Entity_Id);
+ -- Supporting procedure for Install_{Visible,Private}_Declarations. Places
+ -- one entity on its visibility chain, and recurses on the visible part if
+ -- the entity is an inner package.
+
+ function Is_Private_Base_Type (E : Entity_Id) return Boolean;
+ -- True for a private type that is not a subtype
+
+ function Is_Visible_Dependent (Dep : Entity_Id) return Boolean;
+ -- If the private dependent is a private type whose full view is derived
+ -- from the parent type, its full properties are revealed only if we are in
+ -- the immediate scope of the private dependent. Should this predicate be
+ -- tightened further???
+
+ function Requires_Completion_In_Body
+ (Id : Entity_Id;
+ Pack_Id : Entity_Id) return Boolean;
+ -- Subsidiary to routines Unit_Requires_Body and Unit_Requires_Body_Info.
+ -- Determine whether entity Id declared in package spec Pack_Id requires
+ -- completion in a package body.
+
+ procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id);
+ -- Outputs info messages showing why package Pack_Id requires a body. The
+ -- caller has checked that the switch requesting this information is set,
+ -- and that the package does indeed require a body.
--------------------------
-- Analyze_Package_Body --
-- been set.
if Present (Corresponding_Spec (N)) then
- Spec_Id := Corresponding_Spec (N);
+ Spec_Id := Corresponding_Spec (N);
Pack_Decl := Unit_Declaration_Node (Spec_Id);
else
Spec_Id := Current_Entity_In_Scope (Defining_Entity (N));
- if Present (Spec_Id) and then Is_Package_Or_Generic_Package (Spec_Id)
+ if Present (Spec_Id)
+ and then Is_Package_Or_Generic_Package (Spec_Id)
then
Pack_Decl := Unit_Declaration_Node (Spec_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
end if;
+ -- Inherit the "ghostness" of the subprogram spec. Note that this
+ -- property is not directly inherited as the body may be subject to a
+ -- different Ghost assertion policy.
+
+ if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Body_Id);
+
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
+
+ Check_Ghost_Completion (Spec_Id, Body_Id);
+ end if;
+
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
New_Private_Type (N, Id, N);
Set_Depends_On_Private (Id);
+ -- A type declared within a Ghost scope is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
end if;
end New_Private_Type;
+ ---------------------------------
+ -- Requires_Completion_In_Body --
+ ---------------------------------
+
+ function Requires_Completion_In_Body
+ (Id : Entity_Id;
+ Pack_Id : Entity_Id) return Boolean is
+ begin
+ -- Always ignore child units. Child units get added to the entity list
+ -- of a parent unit, but are not original entities of the parent, and
+ -- so do not affect whether the parent needs a body.
+
+ if Is_Child_Unit (Id) then
+ return False;
+
+ -- Ignore formal packages and their renamings
+
+ elsif Ekind (Id) = E_Package
+ and then Nkind (Original_Node (Unit_Declaration_Node (Id))) =
+ N_Formal_Package_Declaration
+ then
+ return False;
+
+ -- A Ghost entity declared in a non-Ghost package does not force the
+ -- need for a body (SPARK RM 6.9(11)).
+
+ elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (Id) then
+ return False;
+
+ -- Otherwise test to see if entity requires a completion. Note that
+ -- subprogram entities whose declaration does not come from source are
+ -- ignored here on the basis that we assume the expander will provide an
+ -- implicit completion at some point.
+
+ elsif (Is_Overloadable (Id)
+ and then Ekind (Id) /= E_Enumeration_Literal
+ and then Ekind (Id) /= E_Operator
+ and then not Is_Abstract_Subprogram (Id)
+ and then not Has_Completion (Id)
+ and then Comes_From_Source (Parent (Id)))
+
+ or else
+ (Ekind (Id) = E_Package
+ and then Id /= Pack_Id
+ and then not Has_Completion (Id)
+ and then Unit_Requires_Body (Id))
+
+ or else
+ (Ekind (Id) = E_Incomplete_Type
+ and then No (Full_View (Id))
+ and then not Is_Generic_Type (Id))
+
+ or else
+ (Ekind_In (Id, E_Task_Type, E_Protected_Type)
+ and then not Has_Completion (Id))
+
+ or else
+ (Ekind (Id) = E_Generic_Package
+ and then Id /= Pack_Id
+ and then not Has_Completion (Id)
+ and then Unit_Requires_Body (Id))
+
+ or else
+ (Is_Generic_Subprogram (Id)
+ and then not Has_Completion (Id))
+
+ then
+ return True;
+
+ -- Otherwise the entity does not require completion in a package body
+
+ else
+ return False;
+ end if;
+ end Requires_Completion_In_Body;
+
----------------------------
-- Uninstall_Declarations --
----------------------------
------------------------
function Unit_Requires_Body
- (P : Entity_Id;
+ (Pack_Id : Entity_Id;
Ignore_Abstract_State : Boolean := False) return Boolean
is
E : Entity_Id;
-- be imported, but perhaps in the future we will allow import of
-- packages.
- if Is_Imported (P) then
+ if Is_Imported (Pack_Id) then
return False;
-- Body required if library package with pragma Elaborate_Body
- elsif Has_Pragma_Elaborate_Body (P) then
+ elsif Has_Pragma_Elaborate_Body (Pack_Id) then
return True;
-- Body required if subprogram
- elsif Is_Subprogram_Or_Generic_Subprogram (P) then
+ elsif Is_Subprogram_Or_Generic_Subprogram (Pack_Id) then
return True;
-- Treat a block as requiring a body
- elsif Ekind (P) = E_Block then
+ elsif Ekind (Pack_Id) = E_Block then
return True;
- elsif Ekind (P) = E_Package
- and then Nkind (Parent (P)) = N_Package_Specification
- and then Present (Generic_Parent (Parent (P)))
+ elsif Ekind (Pack_Id) = E_Package
+ and then Nkind (Parent (Pack_Id)) = N_Package_Specification
+ and then Present (Generic_Parent (Parent (Pack_Id)))
then
declare
- G_P : constant Entity_Id := Generic_Parent (Parent (P));
+ G_P : constant Entity_Id := Generic_Parent (Parent (Pack_Id));
begin
if Has_Pragma_Elaborate_Body (G_P) then
return True;
-- provided). If Ignore_Abstract_State is True, we don't do this check
-- (so we can use Unit_Requires_Body to check for some other reason).
- elsif Ekind_In (P, E_Generic_Package, E_Package)
+ elsif Ekind_In (Pack_Id, E_Generic_Package, E_Package)
and then not Ignore_Abstract_State
- and then Present (Abstract_States (P))
- and then not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
+ and then Present (Abstract_States (Pack_Id))
+ and then not Is_Null_State
+ (Node (First_Elmt (Abstract_States (Pack_Id))))
then
return True;
end if;
-- Otherwise search entity chain for entity requiring completion
- E := First_Entity (P);
+ E := First_Entity (Pack_Id);
while Present (E) loop
-
- -- Always ignore child units. Child units get added to the entity
- -- list of a parent unit, but are not original entities of the
- -- parent, and so do not affect whether the parent needs a body.
-
- if Is_Child_Unit (E) then
- null;
-
- -- Ignore formal packages and their renamings
-
- elsif Ekind (E) = E_Package
- and then Nkind (Original_Node (Unit_Declaration_Node (E))) =
- N_Formal_Package_Declaration
- then
- null;
-
- -- Otherwise test to see if entity requires a completion.
- -- Note that subprogram entities whose declaration does not come
- -- from source are ignored here on the basis that we assume the
- -- expander will provide an implicit completion at some point.
-
- elsif (Is_Overloadable (E)
- and then Ekind (E) /= E_Enumeration_Literal
- and then Ekind (E) /= E_Operator
- and then not Is_Abstract_Subprogram (E)
- and then not Has_Completion (E)
- and then Comes_From_Source (Parent (E)))
-
- or else
- (Ekind (E) = E_Package
- and then E /= P
- and then not Has_Completion (E)
- and then Unit_Requires_Body (E))
-
- or else
- (Ekind (E) = E_Incomplete_Type
- and then No (Full_View (E))
- and then not Is_Generic_Type (E))
-
- or else
- (Ekind_In (E, E_Task_Type, E_Protected_Type)
- and then not Has_Completion (E))
-
- or else
- (Ekind (E) = E_Generic_Package
- and then E /= P
- and then not Has_Completion (E)
- and then Unit_Requires_Body (E))
-
- or else
- (Is_Generic_Subprogram (E)
- and then not Has_Completion (E))
-
- then
+ if Requires_Completion_In_Body (E, Pack_Id) then
return True;
-
- -- Entity that does not require completion
-
- else
- null;
end if;
Next_Entity (E);
-- Unit_Requires_Body_Info --
-----------------------------
- procedure Unit_Requires_Body_Info (P : Entity_Id) is
+ procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id) is
E : Entity_Id;
begin
- -- Imported entity never requires body. Right now, only subprograms can
- -- be imported, but perhaps in the future we will allow import of
+ -- An imported entity never requires body. Right now, only subprograms
+ -- can be imported, but perhaps in the future we will allow import of
-- packages.
- if Is_Imported (P) then
+ if Is_Imported (Pack_Id) then
return;
-- Body required if library package with pragma Elaborate_Body
- elsif Has_Pragma_Elaborate_Body (P) then
- Error_Msg_N ("info: & requires body (Elaborate_Body)?Y?", P);
+ elsif Has_Pragma_Elaborate_Body (Pack_Id) then
+ Error_Msg_N ("info: & requires body (Elaborate_Body)?Y?", Pack_Id);
-- Body required if subprogram
- elsif Is_Subprogram_Or_Generic_Subprogram (P) then
- Error_Msg_N ("info: & requires body (subprogram case)?Y?", P);
+ elsif Is_Subprogram_Or_Generic_Subprogram (Pack_Id) then
+ Error_Msg_N ("info: & requires body (subprogram case)?Y?", Pack_Id);
-- Body required if generic parent has Elaborate_Body
- elsif Ekind (P) = E_Package
- and then Nkind (Parent (P)) = N_Package_Specification
- and then Present (Generic_Parent (Parent (P)))
+ elsif Ekind (Pack_Id) = E_Package
+ and then Nkind (Parent (Pack_Id)) = N_Package_Specification
+ and then Present (Generic_Parent (Parent (Pack_Id)))
then
declare
- G_P : constant Entity_Id := Generic_Parent (Parent (P));
+ G_P : constant Entity_Id := Generic_Parent (Parent (Pack_Id));
begin
if Has_Pragma_Elaborate_Body (G_P) then
Error_Msg_N
("info: & requires body (generic parent Elaborate_Body)?Y?",
- P);
+ Pack_Id);
end if;
end;
-- provided). If Ignore_Abstract_State is True, we don't do this check
-- (so we can use Unit_Requires_Body to check for some other reason).
- elsif Ekind_In (P, E_Generic_Package, E_Package)
- and then Present (Abstract_States (P))
- and then not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
+ elsif Ekind_In (Pack_Id, E_Generic_Package, E_Package)
+ and then Present (Abstract_States (Pack_Id))
+ and then not Is_Null_State
+ (Node (First_Elmt (Abstract_States (Pack_Id))))
then
Error_Msg_N
- ("info: & requires body (non-null abstract state aspect)?Y?", P);
+ ("info: & requires body (non-null abstract state aspect)?Y?",
+ Pack_Id);
end if;
-- Otherwise search entity chain for entity requiring completion
- E := First_Entity (P);
+ E := First_Entity (Pack_Id);
while Present (E) loop
-
- -- Always ignore child units. Child units get added to the entity
- -- list of a parent unit, but are not original entities of the
- -- parent, and so do not affect whether the parent needs a body.
-
- if Is_Child_Unit (E) then
- null;
-
- -- Ignore formal packages and their renamings
-
- elsif Ekind (E) = E_Package
- and then Nkind (Original_Node (Unit_Declaration_Node (E))) =
- N_Formal_Package_Declaration
- then
- null;
-
- -- Otherwise test to see if entity requires a completion.
- -- Note that subprogram entities whose declaration does not come
- -- from source are ignored here on the basis that we assume the
- -- expander will provide an implicit completion at some point.
-
- elsif (Is_Overloadable (E)
- and then Ekind (E) /= E_Enumeration_Literal
- and then Ekind (E) /= E_Operator
- and then not Is_Abstract_Subprogram (E)
- and then not Has_Completion (E)
- and then Comes_From_Source (Parent (E)))
-
- or else
- (Ekind (E) = E_Package
- and then E /= P
- and then not Has_Completion (E)
- and then Unit_Requires_Body (E))
-
- or else
- (Ekind (E) = E_Incomplete_Type
- and then No (Full_View (E))
- and then not Is_Generic_Type (E))
-
- or else
- (Ekind_In (E, E_Task_Type, E_Protected_Type)
- and then not Has_Completion (E))
-
- or else
- (Ekind (E) = E_Generic_Package
- and then E /= P
- and then not Has_Completion (E)
- and then Unit_Requires_Body (E))
-
- or else
- (Is_Generic_Subprogram (E)
- and then not Has_Completion (E))
- then
+ if Requires_Completion_In_Body (E, Pack_Id) then
Error_Msg_Node_2 := E;
Error_Msg_NE
- ("info: & requires body (& requires completion)?Y?", E, P);
-
- -- Entity that does not require completion
-
- else
- null;
+ ("info: & requires body (& requires completion)?Y?", E, Pack_Id);
end if;
Next_Entity (E);
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, 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- --
-- child for public child packages.
function Unit_Requires_Body
- (P : Entity_Id;
+ (Pack_Id : Entity_Id;
Ignore_Abstract_State : Boolean := False) return Boolean;
- -- Check if a unit requires a body. A specification requires a body if it
- -- contains declarations that require completion in a body. If the flag
- -- Ignore_Abstract_State is set True, then the test for a non-null abstract
- -- state (which normally requires a body) is not carried out. This allows
- -- the use of this routine to tell if there is some other reason that a
- -- body is required (as is required for analyzing Abstract_State). This
- -- is not currently used, but may be useful in future if we implement a
- -- compatibility mode which warns about possible incompatibilities if a
- -- SPARK 2014 program is compiled with a SPARK-unaware compiler.
+ -- Determine whether package Pack_Id requires a body. A specification needs
+ -- a body if it contains declarations that require completion in the body.
+ -- A non-Ghost [generic] package does not require a body when it declares
+ -- Ghost entities exclusively. If flag Ignore_Abstract_State is True, then
+ -- the test for a non-null abstract state (which normally requires a body)
+ -- is not carried out. The flag is not currently used, but may be useful
+ -- in the future if we implement a compatibility mode which warns about
+ -- possible incompatibilities if a SPARK 2014 program is compiled with a
+ -- SPARK-unaware compiler.
procedure May_Need_Implicit_Body (E : Entity_Id);
-- If a package declaration contains tasks or RACWs and does not require
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 not Is_Entity_Name (Nam)
+ or else Ekind (Entity (Nam)) /= E_Exception
then
Error_Msg_N ("invalid exception name in renaming", Nam);
else
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.
+
+ if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (Id);
+ end if;
end if;
-- Implementation-defined aspect specifications can appear in a renaming
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.
+
+ if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (New_P);
+ end if;
+
if In_Open_Scopes (Old_P) then
Error_Msg_N ("within its scope, generic denotes its instance", N);
end if;
if Nkind (Nam) = N_Selected_Component and then Analyzed (Nam) then
T := Etype (Nam);
- Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam);
+ Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam);
if Present (Dec) then
Insert_Action (N, Dec);
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.
+
+ if (Is_Entity_Name (Nam)
+ and then Is_Ghost_Entity (Entity (Nam)))
+ or else Within_Ghost_Scope
+ then
+ Set_Is_Ghost_Entity (Id);
+ end if;
+
-- The entity of the renaming declaration needs to reflect whether the
-- renamed object is volatile. Is_Volatile is set if the renamed object
-- is volatile in the RM legality sense.
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.
+
+ if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (New_P);
+ end if;
+
-- If the renaming is in the visible part of a package, then we set
-- Renamed_In_Spec for the renamed package, to prevent giving
-- warnings about no entities referenced. Such a warning would be
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.
+
+ if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (New_S);
+ end if;
+
-- Ada 2005 (AI-423): Check the consistency of null exclusions
-- between a subprogram and its correct renaming.
when Convention_Ada |
Convention_Intrinsic |
Convention_Entry |
- Convention_Ghost |
Convention_Protected |
Convention_Stubbed =>
(C : out Convention_Id;
Ent : out Entity_Id)
is
- Id : Node_Id;
- E : Entity_Id;
- E1 : Entity_Id;
- Cname : Name_Id;
- Comp_Unit : Unit_Number_Type;
+ Cname : Name_Id;
procedure Diagnose_Multiple_Pragmas (S : Entity_Id);
-- Called if we have more than one Export/Import/Convention pragma.
procedure Set_Convention_From_Pragma (E : Entity_Id) is
begin
- -- Ghost convention is allowed only for functions
-
- if Ekind (E) /= E_Function and then C = Convention_Ghost then
- Error_Msg_N
- ("& may not have Ghost convention", E);
- Error_Msg_N
- ("\only functions are permitted to have Ghost convention",
- E);
- return;
- end if;
-
-- Ada 2005 (AI-430): Check invalid attempt to change convention
-- for an overridden dispatching operation. Technically this is
-- an amendment and should only be done in Ada 2005 mode. However,
and then Present (Overridden_Operation (E))
and then C /= Convention (Overridden_Operation (E))
then
- -- An attempt to override a function with a ghost function
- -- appears as a mismatch in conventions.
-
- if C = Convention_Ghost then
- Error_Msg_N ("ghost function & cannot be overriding", E);
- else
- Error_Pragma_Arg
- ("cannot change convention for overridden dispatching "
- & "operation", Arg1);
- end if;
+ Error_Pragma_Arg
+ ("cannot change convention for overridden dispatching "
+ & "operation", Arg1);
end if;
-- Special checks for Convention_Stdcall
end if;
end Set_Convention_From_Pragma;
+ -- Local variables
+
+ Comp_Unit : Unit_Number_Type;
+ E : Entity_Id;
+ E1 : Entity_Id;
+ Id : Node_Id;
+
-- Start of processing for Process_Convention
begin
("convention `Ada_Pass_By_Copy` not allowed for by-reference "
& "type", Arg1);
end if;
- end if;
-- Ada_Pass_By_Reference special checking
- if C = Convention_Ada_Pass_By_Reference then
+ elsif C = Convention_Ada_Pass_By_Reference then
if not Is_First_Subtype (E) then
Error_Pragma_Arg
("convention `Ada_Pass_By_Reference` only allowed for types",
end if;
end if;
- -- Ghost special checking
-
- if Is_Ghost_Subprogram (E)
- and then Present (Overridden_Operation (E))
- then
- Error_Msg_N ("ghost function & cannot be overriding", E);
- end if;
-
-- Go to renamed subprogram if present, since convention applies to
-- the actual renamed entity, not to the renaming entity. If the
-- subprogram is inherited, go to parent subprogram.
end if;
end if;
- -- Check that we are not applying this to a specless body
- -- Relax this check if Relaxed_RM_Semantics to accomodate other Ada
- -- compilers.
+ -- Check that we are not applying this to a specless body. Relax this
+ -- check if Relaxed_RM_Semantics to accomodate other Ada compilers.
if Is_Subprogram (E)
and then Nkind (Parent (Declaration_Node (E))) = N_Subprogram_Body
-- SIMPLE_OPTION
-- | NAME_VALUE_OPTION
- -- SIMPLE_OPTION ::= identifier
+ -- SIMPLE_OPTION ::= Ghost
-- NAME_VALUE_OPTION ::=
-- Part_Of => ABSTRACT_STATE
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
- Pack_Id : Entity_Id;
- -- Entity of related package when pragma Abstract_State appears
-
- procedure Analyze_Abstract_State (State : Node_Id);
+ procedure Analyze_Abstract_State
+ (State : Node_Id;
+ Pack_Id : Entity_Id);
-- Verify the legality of a single state declaration. Create and
-- decorate a state abstraction entity and introduce it into the
- -- visibility chain.
+ -- visibility chain. Pack_Id denotes the entity or the related
+ -- package where pragma Abstract_State appears.
----------------------------
-- Analyze_Abstract_State --
----------------------------
- procedure Analyze_Abstract_State (State : Node_Id) is
-
+ procedure Analyze_Abstract_State
+ (State : Node_Id;
+ Pack_Id : Entity_Id)
+ is
-- Flags used to verify the consistency of options
AR_Seen : Boolean := False;
Set_Refinement_Constituents (State_Id, New_Elmt_List);
Set_Part_Of_Constituents (State_Id, New_Elmt_List);
+ -- An abstract state declared within a Ghost scope becomes
+ -- Ghost (SPARK RM 6.9(2)).
+
+ if Within_Ghost_Scope then
+ Set_Is_Ghost_Entity (State_Id);
+ end if;
+
-- Establish a link between the state declaration and the
-- abstract state entity. Note that a null state remains as
-- N_Null and does not carry any linkages.
Ancestor_Part (State));
end if;
- -- Catch an attempt to introduce a simple option which is
- -- currently not allowed. An exception to this is External
- -- defined without any properties.
+ -- Options External and Ghost appear as expressions
Opt := First (Expressions (State));
while Present (Opt) loop
if Chars (Opt) = Name_External then
Analyze_External_Option (Opt);
+ elsif Chars (Opt) = Name_Ghost then
+ if Present (State_Id) then
+ Set_Is_Ghost_Entity (State_Id);
+ end if;
+
-- Option Part_Of without an encapsulating state is
-- illegal. (SPARK RM 7.1.4(9)).
-- Local variables
Context : constant Node_Id := Parent (Parent (N));
+ Pack_Id : Entity_Id;
State : Node_Id;
-- Start of processing for Abstract_State
State := Expression (Arg1);
Pack_Id := Defining_Entity (Context);
+ -- Mark the associated package as Ghost if it is subject to aspect
+ -- or pragma Ghost as this affects the declaration of an abstract
+ -- state.
+
+ if Is_Subject_To_Ghost (Unit_Declaration_Node (Pack_Id)) then
+ Set_Is_Ghost_Entity (Pack_Id);
+ end if;
+
-- Multiple non-null abstract states appear as an aggregate
if Nkind (State) = N_Aggregate then
State := First (Expressions (State));
while Present (State) loop
- Analyze_Abstract_State (State);
+ Analyze_Abstract_State (State, Pack_Id);
Next (State);
end loop;
-- include malformed state declarations.
else
- Analyze_Abstract_State (State);
+ Analyze_Abstract_State (State, Pack_Id);
end if;
-- Save the pragma for retrieval by other tools
-- Contract_Cases |
-- Debug |
-- Default_Initial_Condition |
+ -- Ghost |
-- Initial_Condition |
-- Loop_Invariant |
-- Loop_Variant |
-- new form syntax.
when Pragma_Check_Policy => Check_Policy : declare
- Kind : Node_Id;
+ Ident : Node_Id;
+ Kind : Node_Id;
begin
GNAT_Pragma;
-- identifier is Name.
if Nkind (Arg1) /= N_Pragma_Argument_Association
- or else Nam_In (Chars (Arg1), No_Name, Name_Name)
+ or else Nam_In (Chars (Arg1), No_Name, Name_Name)
then
-- Old syntax
if Nam_In (Chars (Kind), Name_Name, Name_Policy) then
Error_Msg_Name_2 := Chars (Kind);
- Error_Pragma_Arg
- ("pragma% does not allow% as check name", Arg1);
+ Error_Pragma_Arg
+ ("pragma% does not allow% as check name", Arg1);
end if;
-- Check policy
Check_Arg_Is_One_Of
(Arg2,
Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+ Ident := Get_Pragma_Arg (Arg2);
+
+ if Chars (Kind) = Name_Ghost then
+
+ -- Pragma Check_Policy specifying a Ghost policy cannot
+ -- occur within a ghost subprogram or package.
+
+ if Within_Ghost_Scope then
+ Error_Pragma
+ ("pragma % cannot appear within ghost subprogram or "
+ & "package");
+
+ -- The policy identifier of pragma Ghost must be either
+ -- Check or Ignore (SPARK RM 6.9(7)).
+
+ elsif not Nam_In (Chars (Ident), Name_Check,
+ Name_Ignore)
+ then
+ Error_Pragma_Arg
+ ("argument of pragma % Ghost must be Check or Ignore",
+ Arg2);
+ end if;
+ end if;
-- And chain pragma on the Check_Policy_List for search
begin
GNAT_Pragma;
Check_No_Identifiers;
- Check_At_Most_N_Arguments (1);
+ Check_At_Most_N_Arguments (1);
Subp := Empty;
Stmt := Prev (N);
-- enclosing construct is the proper context. This check is done
-- after the traversal above to allow for duplicate detection.
- if Nkind (Context) = N_Subprogram_Body
+ if No (Subp)
+ and then Nkind (Context) = N_Subprogram_Body
and then No (Corresponding_Spec (Context))
then
Subp := Defining_Entity (Context);
end if;
end Finalize_Storage;
+ -----------
+ -- Ghost --
+ -----------
+
+ -- pragma Ghost [ (boolean_EXPRESSION) ];
+
+ when Pragma_Ghost => Ghost : declare
+ Context : constant Node_Id := Parent (N);
+ Expr : Node_Id;
+ Id : Entity_Id;
+ Orig_Stmt : Node_Id;
+ Prev_Id : Entity_Id;
+ Stmt : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_At_Most_N_Arguments (1);
+
+ Id := Empty;
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N ("pragma % duplicates pragma declared#", N);
+ end if;
+
+ -- Protected and task types cannot be subject to pragma Ghost
+
+ elsif Nkind (Stmt) = N_Protected_Type_Declaration then
+ Error_Pragma ("pragma % cannot apply to a protected type");
+ return;
+
+ elsif Nkind (Stmt) = N_Task_Type_Declaration then
+ Error_Pragma ("pragma % cannot apply to a task type");
+ return;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ Orig_Stmt := Original_Node (Stmt);
+
+ -- When pragma Ghost applies to an untagged derivation, the
+ -- derivation is transformed into a [sub]type declaration.
+
+ if Nkind_In (Stmt, N_Full_Type_Declaration,
+ N_Subtype_Declaration)
+ and then Comes_From_Source (Orig_Stmt)
+ and then Nkind (Orig_Stmt) = N_Full_Type_Declaration
+ and then Nkind (Type_Definition (Orig_Stmt)) =
+ N_Derived_Type_Definition
+ then
+ Id := Defining_Entity (Stmt);
+ exit;
+
+ -- When pragma Ghost applies to an expression function, the
+ -- expression function is transformed into a subprogram.
+
+ elsif Nkind (Stmt) = N_Subprogram_Declaration
+ and then Comes_From_Source (Orig_Stmt)
+ and then Nkind (Orig_Stmt) = N_Expression_Function
+ then
+ Id := Defining_Entity (Stmt);
+ exit;
+ end if;
+
+ -- The pragma applies to a legal construct, stop the traversal
+
+ elsif Nkind_In (Stmt, N_Abstract_Subprogram_Declaration,
+ N_Full_Type_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Object_Declaration,
+ N_Private_Extension_Declaration,
+ N_Private_Type_Declaration,
+ N_Subprogram_Declaration,
+ N_Subtype_Declaration)
+ then
+ Id := Defining_Entity (Stmt);
+ exit;
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
+
+ else
+ Error_Pragma
+ ("pragma % must apply to an object, package, subprogram "
+ & "or type");
+ return;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
+ if No (Id) then
+
+ -- When pragma Ghost is associated with a [generic] package, it
+ -- appears in the visible declarations.
+
+ if Nkind (Context) = N_Package_Specification
+ and then Present (Visible_Declarations (Context))
+ and then List_Containing (N) = Visible_Declarations (Context)
+ then
+ Id := Defining_Entity (Context);
+
+ -- Pragma Ghost applies to a stand alone subprogram body
+
+ elsif Nkind (Context) = N_Subprogram_Body
+ and then No (Corresponding_Spec (Context))
+ then
+ Id := Defining_Entity (Context);
+ end if;
+ end if;
+
+ if No (Id) then
+ Error_Pragma
+ ("pragma % must apply to an object, package, subprogram or "
+ & "type");
+ return;
+ end if;
+
+ -- A derived type or type extension cannot be subject to pragma
+ -- Ghost if either the parent type or one of the progenitor types
+ -- is not Ghost (SPARK RM 6.9(9)).
+
+ if Is_Derived_Type (Id) then
+ Check_Ghost_Derivation (Id);
+ end if;
+
+ -- Handle completions of types and constants that are subject to
+ -- pragma Ghost.
+
+ if Is_Record_Type (Id) or else Ekind (Id) = E_Constant then
+ Prev_Id := Incomplete_Or_Partial_View (Id);
+
+ if Present (Prev_Id) and then not Is_Ghost_Entity (Prev_Id) then
+ Error_Msg_Name_1 := Pname;
+
+ -- The full declaration of a deferred constant cannot be
+ -- subject to pragma Ghost unless the deferred declaration
+ -- is also Ghost (SPARK RM 6.9(10)).
+
+ if Ekind (Prev_Id) = E_Constant then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_NE (Fix_Error
+ ("pragma % must apply to declaration of deferred "
+ & "constant &"), N, Id);
+ return;
+
+ -- Pragma Ghost may appear on the full view of an incomplete
+ -- type because the incomplete declaration lacks aspects and
+ -- cannot be subject to pragma Ghost.
+
+ elsif Ekind (Prev_Id) = E_Incomplete_Type then
+ null;
+
+ -- The full declaration of a type cannot be subject to
+ -- pragma Ghost unless the partial view is also Ghost
+ -- (SPARK RM 6.9(10)).
+
+ else
+ Error_Msg_NE (Fix_Error
+ ("pragma % must apply to partial view of type &"),
+ N, Id);
+ return;
+ end if;
+ end if;
+ end if;
+
+ -- Analyze the Boolean expression (if any)
+
+ if Present (Arg1) then
+ Expr := Get_Pragma_Arg (Arg1);
+
+ Analyze_And_Resolve (Expr, Standard_Boolean);
+
+ if Is_OK_Static_Expression (Expr) then
+
+ -- "Ghostness" cannot be turned off once enabled within a
+ -- region (SPARK RM 6.9(7)).
+
+ if Is_False (Expr_Value (Expr))
+ and then Within_Ghost_Scope
+ then
+ Error_Pragma
+ ("pragma % with value False cannot appear in enabled "
+ & "ghost region");
+ return;
+ end if;
+
+ -- Otherwie the expression is not static
+
+ else
+ Error_Pragma_Arg
+ ("expression of pragma % must be static", Expr);
+ return;
+ end if;
+ end if;
+
+ Set_Is_Ghost_Entity (Id);
+ end Ghost;
+
------------
-- Global --
------------
-------------------------
procedure Analyze_Constituent (Constit : Node_Id) is
+ procedure Check_Ghost_Constituent (Constit_Id : Entity_Id);
+ -- Verify that the constituent Constit_Id is a Ghost entity if the
+ -- abstract state being refined is also Ghost. If this is the case
+ -- verify that the Ghost policy in effect at the point of state
+ -- and constituent declaration is the same.
+
procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
-- Determine whether constituent Constit denoted by its entity
-- Constit_Id appears in Hidden_States. Emit an error when the
if Present (Encapsulating_State (Constit_Id)) then
if Encapsulating_State (Constit_Id) = State_Id then
+ Check_Ghost_Constituent (Constit_Id);
Remove (Part_Of_Constits, Constit_Id);
Collect_Constituent;
-- been encountered.
if Node (State_Elmt) = Constit_Id then
+ Check_Ghost_Constituent (Constit_Id);
+
Remove_Elmt (Body_States, State_Elmt);
Collect_Constituent;
return;
end if;
end Check_Matching_Constituent;
+ -----------------------------
+ -- Check_Ghost_Constituent --
+ -----------------------------
+
+ procedure Check_Ghost_Constituent (Constit_Id : Entity_Id) is
+ begin
+ if Is_Ghost_Entity (State_Id) then
+ if Is_Ghost_Entity (Constit_Id) then
+
+ -- The Ghost policy in effect at the point of abstract
+ -- state declaration and constituent must match
+ -- (SPARK RM 6.9(15)).
+
+ if Is_Checked_Ghost_Entity (State_Id)
+ and then Is_Ignored_Ghost_Entity (Constit_Id)
+ then
+ Error_Msg_Sloc := Sloc (Constit);
+
+ SPARK_Msg_N
+ ("incompatible ghost policies in effect", State);
+ SPARK_Msg_NE
+ ("\abstract state & declared with ghost policy "
+ & "Check", State, State_Id);
+ SPARK_Msg_NE
+ ("\constituent & declared # with ghost policy "
+ & "Ignore", State, Constit_Id);
+
+ elsif Is_Ignored_Ghost_Entity (State_Id)
+ and then Is_Checked_Ghost_Entity (Constit_Id)
+ then
+ Error_Msg_Sloc := Sloc (Constit);
+
+ SPARK_Msg_N
+ ("incompatible ghost policies in effect", State);
+ SPARK_Msg_NE
+ ("\abstract state & declared with ghost policy "
+ & "Ignore", State, State_Id);
+ SPARK_Msg_NE
+ ("\constituent & declared # with ghost policy "
+ & "Check", State, Constit_Id);
+ end if;
+
+ -- A constituent of a Ghost abstract state must be a Ghost
+ -- entity (SPARK RM 7.2.2(12)).
+
+ else
+ SPARK_Msg_NE
+ ("constituent of ghost state & must be ghost",
+ Constit, State_Id);
+ end if;
+ end if;
+ end Check_Ghost_Constituent;
+
-- Local variables
Constit_Id : Entity_Id;
Pragma_External_Name_Casing => 0,
Pragma_Fast_Math => 0,
Pragma_Finalize_Storage_Only => 0,
+ Pragma_Ghost => 0,
Pragma_Global => -1,
Pragma_Ident => -1,
Pragma_Implementation_Defined => -1,
Name_Contract_Cases |
Name_Debug |
Name_Default_Initial_Condition |
+ Name_Ghost |
Name_Initial_Condition |
Name_Invariant |
Name_uInvariant |
Pref : Node_Id);
-- Check that the type of the prefix of a dereference is not incomplete
+ procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
+ -- Determine whether node Ghost_Ref appears within a Ghost-friendly context
+ -- where Ghost entity Ghost_Id can safely reside.
+
function Check_Infinite_Recursion (N : Node_Id) return Boolean;
-- Given a call node, N, which is known to occur immediately within the
-- subprogram being called, determines whether it is a detectable case of
end if;
end Check_Fully_Declared_Prefix;
+ -------------------------
+ -- Check_Ghost_Context --
+ -------------------------
+
+ procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
+ procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
+ -- Verify that the Ghost policy at the point of declaration of entity Id
+ -- matches the policy at the point of reference. If this is not the case
+ -- emit an error at Err_N.
+
+ function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
+ -- Determine whether node Context denotes a Ghost-friendly context where
+ -- a Ghost entity can safely reside.
+
+ -------------------------
+ -- Is_OK_Ghost_Context --
+ -------------------------
+
+ 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.
+
+ --------------------------
+ -- Is_Ghost_Declaration --
+ --------------------------
+
+ function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
+ Par : Node_Id;
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ begin
+ -- Climb the parent chain looking for an object declaration
+
+ Par := Decl;
+ while Present (Par) loop
+ case Nkind (Par) is
+ when N_Abstract_Subprogram_Declaration |
+ N_Exception_Declaration |
+ N_Exception_Renaming_Declaration |
+ N_Full_Type_Declaration |
+ N_Generic_Function_Renaming_Declaration |
+ N_Generic_Package_Declaration |
+ N_Generic_Package_Renaming_Declaration |
+ N_Generic_Procedure_Renaming_Declaration |
+ N_Generic_Subprogram_Declaration |
+ N_Number_Declaration |
+ N_Object_Declaration |
+ N_Object_Renaming_Declaration |
+ N_Package_Declaration |
+ N_Package_Renaming_Declaration |
+ N_Private_Extension_Declaration |
+ N_Private_Type_Declaration |
+ N_Subprogram_Declaration |
+ N_Subprogram_Renaming_Declaration |
+ N_Subtype_Declaration =>
+ return Is_Subject_To_Ghost (Par);
+
+ when others =>
+ null;
+ end case;
+
+ -- Special cases
+
+ -- 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.
+
+ if Nkind (Par) = N_Parameter_Specification
+ and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
+ then
+ return True;
+
+ -- References to Ghost entities may be relocated in internally
+ -- generated bodies.
+
+ elsif Nkind (Par) = N_Subprogram_Body
+ and then not Comes_From_Source (Par)
+ then
+ Subp_Id := Corresponding_Spec (Par);
+
+ -- 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.
+
+ 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;
+ 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.
+
+ 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;
+
+ return False;
+ end Is_Ghost_Declaration;
+
+ -- Start of processing for Is_OK_Ghost_Context
+
+ begin
+ -- The Ghost entity appears within an assertion expression
+
+ if In_Assertion_Expr > 0 then
+ return True;
+
+ -- The Ghost entity is part of a declaration or its completion
+
+ elsif Is_Ghost_Declaration (Context) then
+ return True;
+
+ -- The Ghost entity is referenced within a Ghost statement
+
+ elsif Is_Ghost_Statement_Or_Pragma (Context) then
+ return True;
+
+ else
+ return False;
+ end if;
+ end Is_OK_Ghost_Context;
+
+ ------------------------
+ -- Check_Ghost_Policy --
+ ------------------------
+
+ procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ -- The Ghost policy in effect a the point of declaration and at the
+ -- point of use must match (SPARK RM 6.9(13)).
+
+ if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
+ Error_Msg_Sloc := Sloc (Err_N);
+
+ SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
+ SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
+ SPARK_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);
+
+ SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
+ SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
+ SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+ end if;
+ end Check_Ghost_Policy;
+
+ -- Start of processing for Check_Ghost_Context
+
+ begin
+ -- Once it has been established that the reference to the Ghost entity
+ -- is within a suitable context, ensure that the policy at the point of
+ -- declaration and at the point of use match.
+
+ if Is_OK_Ghost_Context (Ghost_Ref) then
+ Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+
+ -- Otherwise the Ghost entity appears in a non-Ghost context and affects
+ -- its behavior or value.
+
+ else
+ SPARK_Msg_N
+ ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
+ Ghost_Ref);
+ end if;
+ end Check_Ghost_Context;
+
------------------------------
-- Check_Infinite_Recursion --
------------------------------
end if;
if Is_Access_Subprogram_Type (Base_Type (Etype (Nam)))
- and then not Is_Access_Subprogram_Type (Base_Type (Typ))
- and then Nkind (Subp) /= N_Explicit_Dereference
- and then Present (Parameter_Associations (N))
+ and then not Is_Access_Subprogram_Type (Base_Type (Typ))
+ and then Nkind (Subp) /= N_Explicit_Dereference
+ and then Present (Parameter_Associations (N))
then
-- The prefix is a parameterless function call that returns an access
-- to subprogram. If parameters are present in the current call, add
Set_Is_Overloaded (Subp, False);
Set_Is_Overloaded (N, False);
+ -- A Ghost entity must appear in a specific context
+
+ if Is_Ghost_Entity (Nam) and then Comes_From_Source (N) then
+ Check_Ghost_Context (Nam, N);
+ end if;
+
-- If we are calling the current subprogram from immediately within its
-- body, then that is the case where we can sometimes detect cases of
-- infinite recursion statically. Do not try this in case restriction
Par := Parent (Par);
end if;
- -- An effectively volatile object subject to enabled properties
- -- Async_Writers or Effective_Reads must appear in a specific context.
-- The following checks are only relevant when SPARK_Mode is on as they
-- are not standard Ada legality rules.
- if SPARK_Mode = On
- and then Is_Object (E)
- and then Is_Effectively_Volatile (E)
- and then Comes_From_Source (E)
- and then
- (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
- then
- -- The effectively volatile objects appears in a "non-interfering
- -- context" as defined in SPARK RM 7.1.3(13).
+ if SPARK_Mode = On then
- if Is_OK_Volatile_Context (Par, N) then
- null;
+ -- An effectively volatile object subject to enabled properties
+ -- Async_Writers or Effective_Reads must appear in a specific
+ -- context.
+
+ if Is_Object (E)
+ and then Is_Effectively_Volatile (E)
+ and then
+ (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
+ and then Comes_From_Source (N)
+ then
+ -- The effectively volatile objects appears in a "non-interfering
+ -- context" as defined in SPARK RM 7.1.3(13).
- -- Assume that references to effectively volatile objects that appear
- -- as actual parameters in a procedure call are always legal. A full
- -- legality check is done when the actuals are resolved.
+ if Is_OK_Volatile_Context (Par, N) then
+ null;
- elsif Nkind (Par) = N_Procedure_Call_Statement then
- null;
+ -- Assume that references to effectively volatile objects that
+ -- appear as actual parameters in a procedure call are always
+ -- legal. A full legality check is done when the actuals are
+ -- resolved.
- -- Otherwise the context causes a side effect with respect to the
- -- effectively volatile object.
+ elsif Nkind (Par) = N_Procedure_Call_Statement then
+ null;
- else
- Error_Msg_N
- ("volatile object cannot appear in this context "
- & "(SPARK RM 7.1.3(13))", N);
+ -- Otherwise the context causes a side effect with respect to the
+ -- effectively volatile object.
+
+ else
+ SPARK_Msg_N
+ ("volatile object cannot appear in this context "
+ & "(SPARK RM 7.1.3(13))", N);
+ end if;
+
+ -- A Ghost entity must appear in a specific context
+
+ elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then
+ Check_Ghost_Context (E, N);
end if;
end if;
end Resolve_Entity_Name;
end if;
end Check_Function_Writable_Actuals;
+ ----------------------------
+ -- Check_Ghost_Completion --
+ ----------------------------
+
+ procedure Check_Ghost_Completion
+ (Partial_View : Entity_Id;
+ Full_View : Entity_Id)
+ is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
+
+ if Is_Checked_Ghost_Entity (Partial_View)
+ and then Policy = Name_Ignore
+ then
+ Error_Msg_Sloc := Sloc (Full_View);
+
+ SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View);
+ SPARK_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);
+
+ SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
+ SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View);
+ end if;
+ end Check_Ghost_Completion;
+
+ ----------------------------
+ -- Check_Ghost_Derivation --
+ ----------------------------
+
+ procedure Check_Ghost_Derivation (Typ : Entity_Id) is
+ Parent_Typ : constant Entity_Id := Etype (Typ);
+ Iface : Entity_Id;
+ Iface_Elmt : Elmt_Id;
+
+ begin
+ -- Allow untagged derivations from predefined types such as Integer as
+ -- those are not Ghost by definition.
+
+ if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
+ null;
+
+ -- The parent type of a Ghost type extension must be Ghost
+
+ elsif not Is_Ghost_Entity (Parent_Typ) then
+ SPARK_Msg_N ("type extension & cannot be ghost", Typ);
+ SPARK_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
+ return;
+ end if;
+
+ -- All progenitors (if any) must be Ghost as well
+
+ if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
+ Iface_Elmt := First_Elmt (Interfaces (Typ));
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
+
+ if not Is_Ghost_Entity (Iface) then
+ SPARK_Msg_N ("type extension & cannot be ghost", Typ);
+ SPARK_Msg_NE ("\interface type & is not ghost", Typ, Iface);
+ return;
+ end if;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end if;
+ end Check_Ghost_Derivation;
+
--------------------------------
-- Check_Implicit_Dereference --
--------------------------------
end In_Visible_Part;
--------------------------------
- -- Incomplete_Or_Private_View --
+ -- Incomplete_Or_Partial_View --
--------------------------------
- function Incomplete_Or_Private_View (Typ : Entity_Id) return Entity_Id is
+ function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id is
function Inspect_Decls
(Decls : List_Id;
Taft : Boolean := False) return Entity_Id;
- -- Check whether a declarative region contains the incomplete or private
- -- view of Typ.
+ -- Check whether a declarative region contains the incomplete or partial
+ -- view of Id.
-------------------
-- Inspect_Decls --
if Present (Match)
and then Present (Full_View (Match))
- and then Full_View (Match) = Typ
+ and then Full_View (Match) = Id
then
return Match;
end if;
-- Start of processing for Incomplete_Or_Partial_View
begin
- -- Incomplete type case
+ -- Deferred constant or incomplete type case
- Prev := Current_Entity_In_Scope (Typ);
+ Prev := Current_Entity_In_Scope (Id);
if Present (Prev)
- and then Is_Incomplete_Type (Prev)
+ and then (Is_Incomplete_Type (Prev) or else Ekind (Prev) = E_Constant)
and then Present (Full_View (Prev))
- and then Full_View (Prev) = Typ
+ and then Full_View (Prev) = Id
then
return Prev;
end if;
-- Private or Taft amendment type case
declare
- Pkg : constant Entity_Id := Scope (Typ);
+ Pkg : constant Entity_Id := Scope (Id);
Pkg_Decl : Node_Id := Pkg;
begin
-- of this is when the two views have been exchanged - the full
-- appears earlier than the private.
- if Has_Private_Declaration (Typ) then
+ if Has_Private_Declaration (Id) then
Prev := Inspect_Decls (Visible_Declarations (Pkg_Decl));
-- Exchanged view case, look in the private declarations
-- The type has no incomplete or private view
return Empty;
- end Incomplete_Or_Private_View;
+ end Incomplete_Or_Partial_View;
-----------------------------------------
-- Inherit_Default_Init_Cond_Procedure --
end if;
end Is_Fully_Initialized_Variant;
+ ---------------------
+ -- Is_Ghost_Entity --
+ ---------------------
+
+ function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
+ begin
+ return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
+ end Is_Ghost_Entity;
+
+ ----------------------------------
+ -- Is_Ghost_Statement_Or_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.
+
+ -------------------------------
+ -- Is_Ghost_Entity_Reference --
+ -------------------------------
+
+ function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
+ Ref : Node_Id;
+
+ begin
+ Ref := N;
+
+ -- When the reference extracts a subcomponent, recover the related
+ -- object (SPARK RM 6.9(1)).
+
+ 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;
+
+ -- Local variables
+
+ Arg : Node_Id;
+ Stmt : Node_Id;
+
+ -- Start of processing for Is_Ghost_Statement_Or_Pragma
+
+ begin
+ if Nkind (N) = N_Pragma then
+
+ -- A pragma is Ghost when it appears within a Ghost package or
+ -- subprogram.
+
+ if Within_Ghost_Scope then
+ return True;
+ end if;
+
+ -- A pragma is Ghost when it mentions a Ghost entity
+
+ Arg := First (Pragma_Argument_Associations (N));
+ while Present (Arg) loop
+ if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
+ return True;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+
+ Stmt := N;
+ while Present (Stmt) loop
+
+ -- A statement is Ghost when it appears within a Ghost package or
+ -- subprogram.
+
+ if Is_Statement (Stmt) and then Within_Ghost_Scope then
+ return True;
+
+ -- An assignment statement is Ghost when the target is a Ghost
+ -- variable. A procedure call is Ghost when the invoked procedure
+ -- is Ghost.
+
+ elsif Nkind_In (Stmt, N_Assignment_Statement,
+ N_Procedure_Call_Statement)
+ then
+ return Is_Ghost_Entity_Reference (Name (Stmt));
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
+ return False;
+ end if;
+
+ Stmt := Parent (Stmt);
+ end loop;
+
+ return False;
+ end Is_Ghost_Statement_Or_Pragma;
+
----------------------------
-- Is_Inherited_Operation --
----------------------------
or else Nkind (N) = N_Procedure_Call_Statement;
end Is_Statement;
+ -------------------------
+ -- Is_Subject_To_Ghost --
+ -------------------------
+
+ function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
+ function Enables_Ghostness (Arg : Node_Id) return Boolean;
+ -- Determine whether aspect or pragma argument Arg enables "ghostness"
+
+ -----------------------
+ -- Enables_Ghostness --
+ -----------------------
+
+ function Enables_Ghostness (Arg : Node_Id) return Boolean is
+ Expr : Node_Id;
+
+ begin
+ Expr := Arg;
+
+ if Nkind (Expr) = N_Pragma_Argument_Association then
+ Expr := Get_Pragma_Arg (Expr);
+ end if;
+
+ -- Determine whether the expression of the aspect is static and
+ -- denotes True.
+
+ if Present (Expr) then
+ Preanalyze_And_Resolve (Expr);
+
+ return
+ Is_OK_Static_Expression (Expr)
+ and then Is_True (Expr_Value (Expr));
+
+ -- Otherwise Ghost defaults to True
+
+ else
+ return True;
+ end if;
+ end Enables_Ghostness;
+
+ -- Local variables
+
+ Id : constant Entity_Id := Defining_Entity (N);
+ Asp : Node_Id;
+ Decl : Node_Id;
+ Prev_Id : Entity_Id;
+
+ -- Start of processing for Is_Subject_To_Ghost
+
+ begin
+ if Is_Ghost_Entity (Id) then
+ return True;
+
+ -- The completion of a type or a constant is not fully analyzed when the
+ -- reference to the Ghost entity is resolved. Because the completion is
+ -- not marked as Ghost yet, inspect the partial view.
+
+ elsif Is_Record_Type (Id)
+ or else Ekind (Id) = E_Constant
+ or else (Nkind (N) = N_Object_Declaration
+ and then Constant_Present (N))
+ then
+ Prev_Id := Incomplete_Or_Partial_View (Id);
+
+ if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
+ return True;
+ end if;
+ end if;
+
+ -- Examine the aspect specifications (if any) looking for aspect Ghost
+
+ if Permits_Aspect_Specifications (N) then
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ if Chars (Identifier (Asp)) = Name_Ghost then
+ return Enables_Ghostness (Expression (Asp));
+ end if;
+
+ Next (Asp);
+ end loop;
+ end if;
+
+ Decl := Empty;
+
+ -- When the context is a [generic] package declaration, pragma Ghost
+ -- resides in the visible declarations.
+
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decl := First (Visible_Declarations (Specification (N)));
+
+ -- Otherwise pragma Ghost appears in the declarations following N
+
+ elsif Is_List_Member (N) then
+ Decl := Next (N);
+ end if;
+
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma
+ and then Pragma_Name (Decl) = Name_Ghost
+ then
+ return
+ Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
+
+ -- A source construct ends the region where pragma Ghost may appear,
+ -- stop the traversal.
+
+ elsif Comes_From_Source (Decl) then
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ return False;
+ end Is_Subject_To_Ghost;
+
--------------------------------------------------
-- Is_Subprogram_Stub_Without_Prior_Declaration --
--------------------------------------------------
end if;
end Original_Corresponding_Operation;
+ ----------------------
+ -- Policy_In_Effect --
+ ----------------------
+
+ function Policy_In_Effect (Policy : Name_Id) return Name_Id is
+ function Policy_In_List (List : Node_Id) return Name_Id;
+ -- Determine the the mode of a policy in a N_Pragma list
+
+ --------------------
+ -- Policy_In_List --
+ --------------------
+
+ function Policy_In_List (List : Node_Id) return Name_Id is
+ Arg : Node_Id;
+ Expr : Node_Id;
+ Prag : Node_Id;
+
+ begin
+ Prag := List;
+ while Present (Prag) loop
+ Arg := First (Pragma_Argument_Associations (Prag));
+ Expr := Get_Pragma_Arg (Arg);
+
+ -- The current Check_Policy pragma matches the requested policy,
+ -- return the second argument which denotes the policy identifier.
+
+ if Chars (Expr) = Policy then
+ return Chars (Get_Pragma_Arg (Next (Arg)));
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ return No_Name;
+ end Policy_In_List;
+
+ -- Local variables
+
+ Kind : Name_Id;
+
+ -- Start of processing for Policy_In_Effect
+
+ begin
+ if not Is_Valid_Assertion_Kind (Policy) then
+ raise Program_Error;
+ end if;
+
+ -- Inspect all policy pragmas that appear within scopes (if any)
+
+ Kind := Policy_In_List (Check_Policy_List);
+
+ -- Inspect all configuration policy pragmas (if any)
+
+ if Kind = No_Name then
+ Kind := Policy_In_List (Check_Policy_List_Config);
+ end if;
+
+ -- The context lacks policy pragmas, determine the mode based on whether
+ -- assertions are enabled.
+
+ if Kind = No_Name then
+ if Assertions_Enabled then
+ Kind := Name_Check;
+ else
+ Kind := Name_Ignore;
+ end if;
+ end if;
+
+ return Kind;
+ end Policy_In_Effect;
+
----------------------------------
-- Predicate_Tests_On_Arguments --
----------------------------------
Set_Entity (N, Val);
end Set_Entity_With_Checks;
+ -------------------------
+ -- Set_Is_Ghost_Entity --
+ -------------------------
+
+ procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ if Policy = Name_Check then
+ Set_Is_Checked_Ghost_Entity (Id);
+
+ elsif Policy = Name_Ignore then
+ Set_Is_Ignored_Ghost_Entity (Id);
+ end if;
+ end Set_Is_Ghost_Entity;
+
------------------------
-- Set_Name_Entity_Id --
------------------------
return List_1;
end Visible_Ancestors;
+ ------------------------
+ -- Within_Ghost_Scope --
+ ------------------------
+
+ function Within_Ghost_Scope
+ (Id : Entity_Id := Current_Scope) return Boolean
+ is
+ S : Entity_Id;
+
+ begin
+ -- Climb the scope stack looking for a Ghost scope
+
+ S := Id;
+ while Present (S) and then S /= Standard_Standard loop
+ if Is_Ghost_Entity (S) then
+ return True;
+ end if;
+
+ S := Scope (S);
+ end loop;
+
+ return False;
+ end Within_Ghost_Scope;
+
----------------------
-- Within_Init_Proc --
----------------------
-- the one containing C2, that is known to refer to the same object (RM
-- 6.4.1(6.17/3)).
+ procedure Check_Ghost_Completion
+ (Partial_View : Entity_Id;
+ Full_View : Entity_Id);
+ -- Verify that the Ghost policy of a full view or a completion is the same
+ -- as the Ghost policy of the partial view. Emit an error if this is not
+ -- the case.
+
+ procedure Check_Ghost_Derivation (Typ : Entity_Id);
+ -- 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_Implicit_Dereference (N : Node_Id; Typ : Entity_Id);
-- AI05-139-2: Accessors and iterators for containers. This procedure
-- checks whether T is a reference type, and if so it adds an interprettion
-- package specification. The package must be on the scope stack, and the
-- corresponding private part must not.
- function Incomplete_Or_Private_View (Typ : Entity_Id) return Entity_Id;
- -- Given the entity of a type, retrieve the incomplete or private view of
- -- the same type. Note that Typ may not have a partial view to begin with,
- -- in that case the function returns Empty.
+ function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id;
+ -- Given the entity of a constant or a type, retrieve the incomplete or
+ -- partial view of the same entity. Note that Id may not have a partial
+ -- view in which case the function returns Empty.
procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id);
-- Inherit the default initial condition procedure from the parent type of
-- means that the result returned is not crucial, but should err on the
-- side of thinking things are fully initialized if it does not know.
+ function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id is Ghost. To qualify as such, the entity
+ -- must be subject to Convention Ghost.
+
+ function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
+ -- Determine whether statement or pragma N is ghost. 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
+
function Is_Inherited_Operation (E : Entity_Id) return Boolean;
-- E is a subprogram. Return True is E is an implicit operation inherited
-- by a derived type declaration.
-- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo).
-- Note that a label is *not* a statement, and will return False.
+ function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
+ -- Determine whether declarative node N is subject to aspect or pragma
+ -- Ghost. Use this routine in cases where [source] pragma Ghost has not
+ -- been analyzed yet, but the context needs to establish the "ghostness"
+ -- of N.
+
function Is_Subprogram_Stub_Without_Prior_Declaration
(N : Node_Id) return Boolean;
-- Return True if N is a subprogram stub with no prior subprogram
-- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being
-- returned to represent the corresponding aspects with x'Class names.
+ function Policy_In_Effect (Policy : Name_Id) return Name_Id;
+ -- Given a policy, return the policy identifier associated with it. If no
+ -- such policy is in effect, the value returned is No_Name.
+
function Predicate_Tests_On_Arguments (Subp : Entity_Id) return Boolean;
-- Subp is the entity for a subprogram call. This function returns True if
-- predicate tests are required for the arguments in this call (this is the
-- If restriction No_Implementation_Identifiers is set, then it checks
-- that the entity is not implementation defined.
+ procedure Set_Is_Ghost_Entity (Id : Entity_Id);
+ -- Set the relevant ghost attribute of entity Id depending on the current
+ -- Ghost assertion policy in effect.
+
procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
pragma Inline (Set_Name_Entity_Id);
-- Sets the Entity_Id value associated with the given name, which is the
-- generate the list of visible ancestors; otherwise their partial
-- view is added to the resulting list.
+ function Within_Ghost_Scope
+ (Id : Entity_Id := Current_Scope) return Boolean;
+ -- Determine whether an arbitrary entity is either a scope or within a
+ -- scope subject to convention Ghost or one that inherits "ghostness" from
+ -- an enclosing construct.
+
function Within_Init_Proc return Boolean;
-- Determines if Current_Scope is within an init proc
when Name_COBOL => return Convention_COBOL;
when Name_CPP => return Convention_CPP;
when Name_Fortran => return Convention_Fortran;
- when Name_Ghost => return Convention_Ghost;
when Name_Intrinsic => return Convention_Intrinsic;
when Name_Java => return Convention_Java;
when Name_Stdcall => return Convention_Stdcall;
when Convention_CPP => return Name_CPP;
when Convention_Entry => return Name_Entry;
when Convention_Fortran => return Name_Fortran;
- when Convention_Ghost => return Name_Ghost;
when Convention_Intrinsic => return Name_Intrinsic;
when Convention_Java => return Name_Java;
when Convention_Protected => return Name_Protected;
Name_Extensions_Visible : constant Name_Id := N + $; -- GNAT
Name_External : constant Name_Id := N + $; -- GNAT
Name_Finalize_Storage_Only : constant Name_Id := N + $; -- GNAT
+ Name_Ghost : constant Name_Id := N + $; -- GNAT
Name_Global : constant Name_Id := N + $; -- GNAT
Name_Ident : constant Name_Id := N + $; -- GNAT
Name_Implementation_Defined : constant Name_Id := N + $; -- GNAT
Name_COBOL : constant Name_Id := N + $;
Name_CPP : constant Name_Id := N + $;
Name_Fortran : constant Name_Id := N + $;
- Name_Ghost : constant Name_Id := N + $;
Name_Intrinsic : constant Name_Id := N + $;
Name_Java : constant Name_Id := N + $;
Name_Stdcall : constant Name_Id := N + $;
type Convention_Id is (
-- The native-to-Ada (non-foreign) conventions come first. These include
- -- the ones defined in the RM, plus Ghost and Stubbed.
+ -- the ones defined in the RM, plus Stubbed.
Convention_Ada,
Convention_Intrinsic,
Convention_Entry,
- Convention_Ghost,
Convention_Protected,
Convention_Stubbed,
Pragma_Extensions_Visible,
Pragma_External,
Pragma_Finalize_Storage_Only,
+ Pragma_Ghost,
Pragma_Global,
Pragma_Ident,
Pragma_Implementation_Defined,
projects / gcc.git / commitdiff