This patch provides the initial implementation of aspect Ghost. This construct
is intended for formal verification proofs.
Aspect Ghost is a boolean aspect with the following semantics:
A function with a Ghost aspect_mark in the aspect_specification of its
declaration may only be called from within an assertion expression, excluding
subtype predicates, or from within another ghost function.
The patch also corrects several issues found in aspect/pragma Loop_Invariant
and Loop_Variant.
------------
-- Source --
------------
-- gen.ads
generic
type Element is private;
with function Formal_Func (Val : Element) return Element;
package Gen is
end Gen;
-- illegal usage.ads
with Gen;
package Illegal_Usage is
function Ghost_Func (Val : Integer) return Integer
with Ghost;
function Ren_GF_1 (Val : Integer) return Integer renames Ghost_Func;
function Ren_GF_2 (Val : Integer) return Integer renames Ren_GF_1;
subtype Nat_Subtype_1 is Natural
with Dynamic_Predicate => Ghost_Func (Nat_Subtype_1) > 1;
subtype Nat_Subtype_2 is Natural
with Dynamic_Predicate => Ren_GF_1 (Nat_Subtype_2) > 1;
subtype Nat_Subtype_3 is Natural
with Dynamic_Predicate => Ren_GF_2 (Nat_Subtype_3) > 1;
package Inst is new Gen (Integer, Ghost_Func);
type Iface is interface;
function Func_1 return Iface is abstract;
function Func_2 return Iface is abstract;
type Impl_Type is new Iface with null record;
overriding function Func_1 return Impl_Type
with Ghost;
function Func_2 return Impl_Type
with Ghost;
procedure Proc;
end Illegal_Usage;
-- illegal_usage.adb
package body Illegal_Usage is
overriding function Func_1 return Impl_Type is
Result : Impl_Type;
begin
return Result;
end Func_1;
function Func_2 return Impl_Type is
begin
return Func_1;
end Func_2;
function Ghost_Func (Val : Integer) return Integer is
begin
return Val + 1;
end Ghost_Func;
procedure Proc is
type Ghost_Func_Ptr is access function (Val : Integer) return Integer;
Ptr : constant Ghost_Func_Ptr := Ghost_Func'Access;
Var : Integer;
begin
Var := Ghost_Func (1);
Var := Ren_GF_1 (2);
Var := Ren_GF_2 (3);
end Proc;
end Illegal_Usage;
-------------------------------------
-- Compilation and expected output --
-------------------------------------
$ gcc -c -gnat12 -gnata -gnatd.V illegal_usage.adb
illegal_usage.adb:20:40: prefix of "Access" attribute cannot be a ghost
function
illegal_usage.adb:23:14: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.adb:24:14: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.adb:25:14: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.ads:11:32: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.ads:13:32: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.ads:15:32: call to ghost function must appear in assertion
expression or another ghost function
illegal_usage.ads:17:38: ghost function "Ghost_Func" cannot act as generic
actual
illegal_usage.ads:17:38: instantiation abandoned
illegal_usage.ads:24:24: ghost function "Func_1" cannot be overriding
illegal_usage.ads:26:13: ghost function "Func_2" cannot be overriding
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-04-12 Hristian Kirtchev <kirtc...@adacore.com>
* aspects.adb: Alphabetize subprogram bodies in this unit. Add
an entry for Aspect_Ghost in the table of canonical aspects.
(Has_Aspect): New routine.
* aspects.ads: Add Aspect_Ghost to all relevant
tables. Alphabetize subprograms in this unit.
(Has_Aspect): New routine.
* einfo.adb: Add with and use clauses for Aspects.
(Is_Ghost_Function): New routine.
* einfo.ads: Add new synthesized attribute Is_Ghost_Function and
update the structure of the related nodes.
(Is_Ghost_Function): New routine.
* exp_ch4.adb (Find_Enclosing_Context): Use routine
Is_Body_Or_Package_Declaration to terminate a search.
(Is_Body_Or_Unit): Removed.
* exp_util.adb (Within_Case_Or_If_Expression): Use routine
Is_Body_Or_Package_Declaration to terminate a search.
* par-prag.adb: Add pragma Ghost to the list of pragmas that do
not need special processing by the parser.
* sem_attr.adb (Analyze_Access_Attribute): Detect an
illegal use of 'Access where the prefix is a ghost function.
(Analyze_Attribute): Use routine Is_Body_Or_Package_Declaration
to terminate a search. (Check_References_In_Prefix): Use routine
Is_Body_Or_Package_Declaration to terminate a search.
* sem_ch4.adb (Analyze_Call): Mark a function when it appears
inside an assertion expression. Verify the legality of a call
to a ghost function.
(Check_Ghost_Function_Call): New routine.
* sem_ch6.adb (Analyze_Function_Call): Code reformatting. Move
the setting of attribute In_Assertion_Expression to Analyze_Call.
(Check_Overriding_Indicator): Detect an illegal attempt to
override a function with a ghost function.
* sem_ch12.adb (Preanalyze_Actuals): Detect an illegal use of
a ghost function as a generic actual.
* sem_elab.adb (Check_Internal_Call_Continue): Update the call
to In_Assertion.
* sem_prag.adb: Add an entry for pragma Ghost in the table
of significant arguments.
(Analyze_Pragma): Do not analyze
an "others" case guard. Add processing for pragma Ghost. Use
Preanalyze_Assert_Expression when analyzing the expression of
pragmas Loop_Invariant and Loop_Variant.
* sem_util.adb (Get_Subprogram_Entity): Reimplemented.
(Is_Body_Or_Package_Declaration): New routine.
* sem_util.ads: Alphabetize subprotrams in this unit.
(Is_Body_Or_Package_Declaration): New routine.
* sinfo.adb (In_Assertion): Rename to In_Assertion_Expression.
(Set_In_Assertion): Rename to Set_In_Assertion_Expression.
* sinfo.ads: Rename flag In_Assertion to In_Assertion_Expression
to better reflect its use. Update all places that mention the flag.
(In_Assertion): Rename to In_Assertion_Expression. Update
related pragma Inline. (Set_In_Assertion): Rename to
Set_In_Assertion_Expression. Update related pragma Inline.
* snames.ads-tmpl: Add new predefined name Ghost. Add new pragma
id Pragma_Ghost.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 197899)
+++ exp_util.adb (working copy)
@@ -8013,13 +8013,7 @@
-- Prevent the search from going too far
- elsif Nkind_In (Par, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Index: sinfo.adb
===================================================================
--- sinfo.adb (revision 197899)
+++ sinfo.adb (working copy)
@@ -1640,13 +1640,13 @@
return Flag16 (N);
end Import_Interface_Present;
- function In_Assertion
+ function In_Assertion_Expression
(N : Node_Id) return Boolean is
begin
pragma Assert (False
or else NT (N).Nkind = N_Function_Call);
return Flag4 (N);
- end In_Assertion;
+ end In_Assertion_Expression;
function In_Present
(N : Node_Id) return Boolean is
@@ -4722,13 +4722,13 @@
Set_Flag16 (N, Val);
end Set_Import_Interface_Present;
- procedure Set_In_Assertion
+ procedure Set_In_Assertion_Expression
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
or else NT (N).Nkind = N_Function_Call);
Set_Flag4 (N, Val);
- end Set_In_Assertion;
+ end Set_In_Assertion_Expression;
procedure Set_In_Present
(N : Node_Id; Val : Boolean := True) is
Index: sinfo.ads
===================================================================
--- sinfo.ads (revision 197899)
+++ sinfo.ads (working copy)
@@ -1227,7 +1227,7 @@
-- pragma of the other kind is also present. This is used to avoid
-- generating some unwanted error messages.
- -- In_Assertion (Flag4-Sem)
+ -- In_Assertion_Expression (Flag4-Sem)
-- This flag is present in N_Function_Call nodes. It is set if the
-- function is called from within an assertion expression. This is
-- used to avoid some bogus warnings about early elaboration.
@@ -4772,7 +4772,7 @@
-- actual parameter part)
-- First_Named_Actual (Node4-Sem)
-- Controlling_Argument (Node1-Sem) (set to Empty if not dispatching)
- -- In_Assertion (Flag4-Sem)
+ -- In_Assertion_Expression (Flag4-Sem)
-- Is_Expanded_Build_In_Place_Call (Flag11-Sem)
-- Do_Tag_Check (Flag13-Sem)
-- No_Elaboration_Check (Flag14-Sem)
@@ -8628,7 +8628,7 @@
function Import_Interface_Present
(N : Node_Id) return Boolean; -- Flag16
- function In_Assertion
+ function In_Assertion_Expression
(N : Node_Id) return Boolean; -- Flag4
function In_Present
@@ -9609,7 +9609,7 @@
procedure Set_Import_Interface_Present
(N : Node_Id; Val : Boolean := True); -- Flag16
- procedure Set_In_Assertion
+ procedure Set_In_Assertion_Expression
(N : Node_Id; Val : Boolean := True); -- Flag4
procedure Set_In_Present
@@ -12007,7 +12007,7 @@
pragma Inline (Interface_Present);
pragma Inline (Includes_Infinities);
pragma Inline (Import_Interface_Present);
- pragma Inline (In_Assertion);
+ pragma Inline (In_Assertion_Expression);
pragma Inline (In_Present);
pragma Inline (Inherited_Discriminant);
pragma Inline (Instance_Spec);
@@ -12329,7 +12329,7 @@
pragma Inline (Set_Interface_List);
pragma Inline (Set_Interface_Present);
pragma Inline (Set_Import_Interface_Present);
- pragma Inline (Set_In_Assertion);
+ pragma Inline (Set_In_Assertion_Expression);
pragma Inline (Set_In_Present);
pragma Inline (Set_Inherited_Discriminant);
pragma Inline (Set_Instance_Spec);
Index: einfo.adb
===================================================================
--- einfo.adb (revision 197899)
+++ einfo.adb (working copy)
@@ -32,12 +32,13 @@
pragma Style_Checks (All_Checks);
-- Turn off subprogram ordering, not used for this unit
-with Atree; use Atree;
-with Namet; use Namet;
-with Nlists; use Nlists;
-with Output; use Output;
-with Sinfo; use Sinfo;
-with Stand; use Stand;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Output; use Output;
+with Sinfo; use Sinfo;
+with Stand; use Stand;
package body Einfo is
@@ -6549,10 +6550,31 @@
function Is_Finalizer (Id : E) return B is
begin
- return Ekind (Id) = E_Procedure
- and then Chars (Id) = Name_uFinalizer;
+ return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer;
end Is_Finalizer;
+ -----------------------
+ -- Is_Ghost_Function --
+ -----------------------
+
+ function Is_Ghost_Function (Id : E) return B is
+ Subp_Id : Entity_Id := Id;
+
+ begin
+ if Present (Subp_Id) and then Ekind (Subp_Id) = E_Function then
+
+ -- Handle renamings of functions
+
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Alias (Subp_Id);
+ end if;
+
+ return Has_Aspect (Subp_Id, Aspect_Ghost);
+ end if;
+
+ return False;
+ end Is_Ghost_Function;
+
--------------------
-- Is_Input_State --
--------------------
@@ -6570,8 +6592,7 @@
function Is_Null_State (Id : E) return B is
begin
return
- Ekind (Id) = E_Abstract_State
- and then Nkind (Parent (Id)) = N_Null;
+ Ekind (Id) = E_Abstract_State and then Nkind (Parent (Id)) = N_Null;
end Is_Null_State;
---------------------
@@ -6590,10 +6611,7 @@
function Is_Package_Or_Generic_Package (Id : E) return B is
begin
- return
- Ekind (Id) = E_Package
- or else
- Ekind (Id) = E_Generic_Package;
+ return Ekind_In (Id, E_Generic_Package, E_Package);
end Is_Package_Or_Generic_Package;
---------------
@@ -6612,8 +6630,7 @@
function Is_Protected_Component (Id : E) return B is
begin
- return Ekind (Id) = E_Component
- and then Is_Protected_Type (Scope (Id));
+ return Ekind (Id) = E_Component and then Is_Protected_Type (Scope (Id));
end Is_Protected_Component;
----------------------------
Index: einfo.ads
===================================================================
--- einfo.ads (revision 197899)
+++ einfo.ads (working copy)
@@ -1230,7 +1230,7 @@
-- the same structure for constrained and unconstrained arrays, subtype
-- marks and discrete ranges are both represented by a subtype. This
-- function returns the tree node corresponding to an occurrence of the
--- first index (NOT the entity for the type). Subsequent indexes are
+-- first index (NOT the entity for the type). Subsequent indices are
-- obtained using Next_Index. Note that this field is defined for the
-- case of string literal subtypes, but is always Empty.
@@ -2292,6 +2292,10 @@
-- package, generic function, generic procedure), and False for all
-- other entities.
+-- Is_Ghost_Function (synthesized)
+-- Applies to all entities. Yields True for a function marked by aspect
+-- Ghost.
+
-- Is_Hidden (Flag57)
-- Defined in all entities. Set true for all entities declared in the
-- private part or body of a package. Also marks generic formals of a
@@ -5404,6 +5408,7 @@
-- Address_Clause (synth)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
+ -- Is_Ghost_Function (synth) (non-generic case only)
-- Last_Formal (synth)
-- Number_Formals (synth)
-- Scope_Depth (synth)
@@ -6611,6 +6616,7 @@
function Is_Discriminal (Id : E) return B;
function Is_Dynamic_Scope (Id : E) return B;
function Is_Finalizer (Id : E) return B;
+ function Is_Ghost_Function (Id : E) return B;
function Is_Input_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Output_State (Id : E) return B;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 197908)
+++ sem_prag.adb (working copy)
@@ -253,10 +253,15 @@
-- Pre-analyze the guard and consequence expressions of a Contract_Cases
-- pragma/aspect aggregate expression.
+ ----------------------------
+ -- Analyze_Contract_Cases --
+ ----------------------------
+
procedure Analyze_Contract_Cases (Aggr : Node_Id) is
Case_Guard : Node_Id;
Conseq : Node_Id;
Post_Case : Node_Id;
+
begin
Post_Case := First (Component_Associations (Aggr));
while Present (Post_Case) loop
@@ -266,19 +271,24 @@
-- Preanalyze the boolean expression, we treat this as a spec
-- expression (i.e. similar to a default expression).
- Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+ if Nkind (Case_Guard) /= N_Others_Choice then
+ Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+ end if;
+
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
Next (Post_Case);
end loop;
end Analyze_Contract_Cases;
+ -- Start of processing for Analyze_CTC_In_Decl_Part
+
begin
-- Install formals and push subprogram spec onto scope stack so that we
-- can see the formals from the pragma.
+ Push_Scope (S);
Install_Formals (S);
- Push_Scope (S);
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
@@ -11194,6 +11204,39 @@
end if;
end Float_Representation;
+ -----------
+ -- Ghost --
+ -----------
+
+ -- pragma GHOST (function_LOCAL_NAME);
+
+ when Pragma_Ghost => Ghost : declare
+ Subp : Node_Id;
+ Subp_Id : Entity_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+ Check_Arg_Is_Local_Name (Arg1);
+
+ -- Ensure the proper placement of the pragma. Ghost must be
+ -- associated with a subprogram declaration.
+
+ Subp := Parent (Corresponding_Aspect (N));
+
+ if Nkind (Subp) /= N_Subprogram_Declaration then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Id := Defining_Unit_Name (Specification (Subp));
+
+ if Ekind (Subp_Id) /= E_Function then
+ Error_Pragma ("pragma % must be applied to a function");
+ end if;
+ end Ghost;
+
------------
-- Global --
------------
@@ -13542,14 +13585,12 @@
return;
end if;
- Preanalyze_And_Resolve (Expression (Arg1), Any_Boolean);
+ Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
-- Transform pragma Loop_Invariant into equivalent pragma Check
-- Generate:
-- pragma Check (Loop_Invaraint, Arg1);
- -- Seems completely wrong to hijack pragma Check this way ???
-
Rewrite (N,
Make_Pragma (Loc,
Chars => Name_Check,
@@ -13625,7 +13666,8 @@
Error_Pragma_Arg ("wrong change modifier", Variant);
end if;
- Preanalyze_And_Resolve (Expression (Variant), Any_Discrete);
+ Preanalyze_Assert_Expression
+ (Expression (Variant), Any_Discrete);
Next (Variant);
end loop;
@@ -17762,6 +17804,7 @@
Pragma_Fast_Math => -1,
Pragma_Finalize_Storage_Only => 0,
Pragma_Float_Representation => 0,
+ Pragma_Ghost => 0,
Pragma_Global => -1,
Pragma_Ident => -1,
Pragma_Implementation_Defined => -1,
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 197899)
+++ sem_ch12.adb (working copy)
@@ -12402,8 +12402,17 @@
Analyze (Act);
end if;
- if Errs /= Serious_Errors_Detected then
+ -- Ensure that a ghost function does not act as generic actual
+ if Is_Entity_Name (Act)
+ and then Is_Ghost_Function (Entity (Act))
+ then
+ Error_Msg_N
+ ("ghost function & cannot act as generic actual", Act);
+ Abandon_Instantiation (Act);
+
+ elsif Errs /= Serious_Errors_Detected then
+
-- Do a minimal analysis of the generic, to prevent spurious
-- warnings complaining about the generic being unreferenced,
-- before abandoning the instantiation.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 197899)
+++ sem_util.adb (working copy)
@@ -5612,49 +5612,58 @@
---------------------------
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id is
- Nam : Node_Id;
- Proc : Entity_Id;
+ Subp : Node_Id;
+ Subp_Id : Entity_Id;
begin
if Nkind (Nod) = N_Accept_Statement then
- Nam := Entry_Direct_Name (Nod);
+ Subp := Entry_Direct_Name (Nod);
- -- For an entry call, the prefix of the call is a selected component.
- -- Need additional code for internal calls ???
+ elsif Nkind (Nod) = N_Slice then
+ Subp := Prefix (Nod);
- elsif Nkind (Nod) = N_Entry_Call_Statement then
- if Nkind (Name (Nod)) = N_Selected_Component then
- Nam := Entity (Selector_Name (Name (Nod)));
+ else
+ Subp := Name (Nod);
+ end if;
+
+ -- Strip the subprogram call
+
+ loop
+ if Nkind_In (Subp, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component)
+ then
+ Subp := Prefix (Subp);
+
+ elsif Nkind_In (Subp, N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ then
+ Subp := Expression (Subp);
+
else
- Nam := Empty;
+ exit;
end if;
+ end loop;
- else
- Nam := Name (Nod);
- end if;
+ -- Extract the entity of the subprogram call
- if Nkind (Nam) = N_Explicit_Dereference then
- Proc := Etype (Prefix (Nam));
- elsif Is_Entity_Name (Nam) then
- Proc := Entity (Nam);
- else
- return Empty;
- end if;
+ if Is_Entity_Name (Subp) then
+ Subp_Id := Entity (Subp);
- if Is_Object (Proc) then
- Proc := Etype (Proc);
- end if;
+ if Ekind (Subp_Id) = E_Access_Subprogram_Type then
+ Subp_Id := Directly_Designated_Type (Subp_Id);
+ end if;
- if Ekind (Proc) = E_Access_Subprogram_Type then
- Proc := Directly_Designated_Type (Proc);
- end if;
+ if Is_Subprogram (Subp_Id) then
+ return Subp_Id;
+ else
+ return Empty;
+ end if;
- if not Is_Subprogram (Proc)
- and then Ekind (Proc) /= E_Subprogram_Type
- then
+ -- The search did not find a construct that denotes a subprogram
+
+ else
return Empty;
- else
- return Proc;
end if;
end Get_Subprogram_Entity;
@@ -7714,6 +7723,20 @@
end if;
end Is_Atomic_Object;
+ ------------------------------------
+ -- Is_Body_Or_Package_Declaration --
+ ------------------------------------
+
+ function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean is
+ begin
+ return Nkind_In (N, N_Entry_Body,
+ N_Package_Body,
+ N_Package_Declaration,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body);
+ end Is_Body_Or_Package_Declaration;
+
-----------------------
-- Is_Bounded_String --
-----------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 197901)
+++ sem_util.ads (working copy)
@@ -178,6 +178,17 @@
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
+ procedure Check_Dynamically_Tagged_Expression
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Related_Nod : Node_Id);
+ -- Check wrong use of dynamically tagged expression
+
+ procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
+ -- Verify that the full declaration of type T has been seen. If not, place
+ -- error message on node N. Used in object declarations, type conversions
+ -- and qualified expressions.
+
procedure Check_Function_Writable_Actuals (N : Node_Id);
-- (Ada 2012): If the construct N has two or more direct constituents that
-- are names or expressions whose evaluation may occur in an arbitrary
@@ -210,17 +221,6 @@
-- remains in the Examiner (JB01-005). Note that the Examiner does not
-- count package declarations in later declarative items.
- procedure Check_Dynamically_Tagged_Expression
- (Expr : Node_Id;
- Typ : Entity_Id;
- Related_Nod : Node_Id);
- -- Check wrong use of dynamically tagged expression
-
- procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
- -- Verify that the full declaration of type T has been seen. If not, place
- -- error message on node N. Used in object declarations, type conversions
- -- and qualified expressions.
-
procedure Check_Nested_Access (Ent : Entity_Id);
-- Check whether Ent denotes an entity declared in an uplevel scope, which
-- is accessed inside a nested procedure, and set Has_Up_Level_Access flag
@@ -470,7 +470,7 @@
-- discriminant at the same position in this new type.
procedure Find_Overlaid_Entity
- (N : Node_Id;
+ (N : Node_Id;
Ent : out Entity_Id;
Off : out Boolean);
-- The node N should be an address representation clause. Determines if
@@ -849,6 +849,9 @@
-- Determines if the given node denotes an atomic object in the sense of
-- the legality checks described in RM C.6(12).
+ function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether node N denotes a body or a package declaration
+
function Is_Bounded_String (T : Entity_Id) return Boolean;
-- True if T is a bounded string type. Used to make sure "=" composes
-- properly for bounded string types.
@@ -1304,9 +1307,9 @@
-- S2. Otherwise, it is S itself.
function Object_Access_Level (Obj : Node_Id) return Uint;
- -- Return the accessibility level of the view of the object Obj.
- -- For convenience, qualified expressions applied to object names
- -- are also allowed as actuals for this function.
+ -- Return the accessibility level of the view of the object Obj. For
+ -- convenience, qualified expressions applied to object names are also
+ -- allowed as actuals for this function.
function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean;
-- Returns True if the names of both entities correspond with matching
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 197906)
+++ sem_attr.adb (working copy)
@@ -602,10 +602,13 @@
if Has_Pragma_Inline_Always (Entity (P)) then
Error_Attr_P
("prefix of % attribute cannot be Inline_Always subprogram");
- end if;
- if Aname = Name_Unchecked_Access then
+ elsif Aname = Name_Unchecked_Access then
Error_Attr ("attribute% cannot be applied to a subprogram", P);
+
+ elsif Is_Ghost_Function (Entity (P)) then
+ Error_Attr_P
+ ("prefix of % attribute cannot be a ghost function");
end if;
-- Issue an error if the prefix denotes an eliminated subprogram
@@ -3694,13 +3697,7 @@
-- Prevent the search from going too far
- elsif Nkind_In (Stmt, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
@@ -3845,13 +3842,7 @@
-- Prevent the search from going too far
- elsif Nkind_In (Stmt, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
@@ -9193,7 +9184,6 @@
and then
(Ekind (Btyp) = E_Access_Subprogram_Type
or else Is_Local_Anonymous_Access (Btyp))
-
and then Subprogram_Access_Level (Entity (P)) >
Type_Access_Level (Btyp)
then
@@ -9595,9 +9585,9 @@
-- in such a context.
if Attr_Id /= Attribute_Unchecked_Access
+ and then Ekind (Btyp) = E_General_Access_Type
and then
Object_Access_Level (P) > Deepest_Type_Access_Level (Btyp)
- and then Ekind (Btyp) = E_General_Access_Type
then
Accessibility_Message;
return;
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 197906)
+++ sem_elab.adb (working copy)
@@ -2258,7 +2258,7 @@
-- in this case, due to the out of order handling in this case.
and then (Nkind (Original_Node (N)) /= N_Function_Call
- or else not In_Assertion (Original_Node (N)))
+ or else not In_Assertion_Expression (Original_Node (N)))
then
if Inst_Case then
Error_Msg_NE
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb (revision 197899)
+++ exp_ch4.adb (working copy)
@@ -5033,30 +5033,9 @@
----------------------------
function Find_Enclosing_Context return Node_Id is
- function Is_Body_Or_Unit (N : Node_Id) return Boolean;
- -- Determine whether N denotes a body or unit declaration
-
- ---------------------
- -- Is_Body_Or_Unit --
- ---------------------
-
- function Is_Body_Or_Unit (N : Node_Id) return Boolean is
- begin
- return Nkind_In (N, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body);
- end Is_Body_Or_Unit;
-
- -- Local variables
-
Par : Node_Id;
Top : Node_Id;
- -- Start of processing for Find_Enclosing_Context
-
begin
-- The expression_with_actions is in a case/if expression and
-- the lifetime of any temporary controlled object is therefore
@@ -5074,7 +5053,7 @@
-- Prevent the search from going too far
- elsif Is_Body_Or_Unit (Par) then
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
@@ -5099,7 +5078,7 @@
-- Prevent the search from going too far
- elsif Is_Body_Or_Unit (Par) then
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
@@ -5171,7 +5150,9 @@
then
return Par;
- elsif Is_Body_Or_Unit (Par) then
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 197907)
+++ sem_ch4.adb (working copy)
@@ -868,6 +868,11 @@
-- Flag indicates whether an interpretation of the prefix is a
-- parameterless call that returns an access_to_subprogram.
+ procedure Check_Ghost_Function_Call;
+ -- Verify the legality of a call to a ghost function. Such calls can
+ -- appear only in assertion expressions except subtype predicates or
+ -- from within another ghost function.
+
procedure Check_Mixed_Parameter_And_Named_Associations;
-- Check that parameter and named associations are not mixed. This is
-- a restriction in SPARK mode.
@@ -882,6 +887,38 @@
procedure No_Interpretation;
-- Output error message when no valid interpretation exists
+ -------------------------------
+ -- Check_Ghost_Function_Call --
+ -------------------------------
+
+ procedure Check_Ghost_Function_Call is
+ S : Entity_Id;
+
+ begin
+ -- The ghost function appears inside an assertion expression
+
+ if In_Assertion_Expression (N) then
+ return;
+
+ else
+ S := Current_Scope;
+ while Present (S) and then S /= Standard_Standard loop
+
+ -- The call appears inside another ghost function
+
+ if Is_Ghost_Function (S) then
+ return;
+ end if;
+
+ S := Scope (S);
+ end loop;
+ end if;
+
+ Error_Msg_N
+ ("call to ghost function must appear in assertion expression or "
+ & "another ghost function", N);
+ end Check_Ghost_Function_Call;
+
--------------------------------------------------
-- Check_Mixed_Parameter_And_Named_Associations --
--------------------------------------------------
@@ -972,6 +1009,12 @@
Check_Mixed_Parameter_And_Named_Associations;
end if;
+ -- Mark a function that appears inside an assertion expression
+
+ if Nkind (N) = N_Function_Call and then In_Assertion_Expr > 0 then
+ Set_In_Assertion_Expression (N);
+ end if;
+
-- Initialize the type of the result of the call to the error type,
-- which will be reset if the type is successfully resolved.
@@ -1078,6 +1121,8 @@
Set_Etype (Nam_Ent, Etype (N));
end if;
+ -- Overloaded call
+
else
-- An overloaded selected component must denote overloaded operations
-- of a concurrent type. The interpretations are attached to the
@@ -1162,9 +1207,9 @@
Get_Next_Interp (X, It);
end loop;
- -- If the name is the result of a function call, it can only
- -- be a call to a function returning an access to subprogram.
- -- Insert explicit dereference.
+ -- If the name is the result of a function call, it can only be a
+ -- call to a function returning an access to subprogram. Insert
+ -- explicit dereference.
if Nkind (Nam) = N_Function_Call then
Insert_Explicit_Dereference (Nam);
@@ -1243,6 +1288,13 @@
End_Interp_List;
end if;
+
+ -- A call to a ghost function is allowed only in assertion expressions,
+ -- excluding subtype predicates, or from within another ghost function.
+
+ if Is_Ghost_Function (Get_Subprogram_Entity (N)) then
+ Check_Ghost_Function_Call;
+ end if;
end Analyze_Call;
-----------------------------
Index: aspects.adb
===================================================================
--- aspects.adb (revision 197899)
+++ aspects.adb (working copy)
@@ -110,15 +110,6 @@
end if;
end Aspect_Specifications;
- -------------------
- -- Get_Aspect_Id --
- -------------------
-
- function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
- begin
- return Aspect_Id_Hash_Table.Get (Name);
- end Get_Aspect_Id;
-
-----------------
-- Find_Aspect --
-----------------
@@ -169,6 +160,38 @@
return Empty;
end Find_Aspect;
+ -------------------
+ -- Get_Aspect_Id --
+ -------------------
+
+ function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
+ begin
+ return Aspect_Id_Hash_Table.Get (Name);
+ end Get_Aspect_Id;
+
+ ----------------
+ -- Has_Aspect --
+ ----------------
+
+ function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean is
+ Decl : constant Node_Id := Parent (Parent (Id));
+ Aspect : Node_Id;
+
+ begin
+ if Has_Aspects (Decl) then
+ Aspect := First (Aspect_Specifications (Decl));
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Chars (Identifier (Aspect))) = A then
+ return True;
+ end if;
+
+ Next (Aspect);
+ end loop;
+ end if;
+
+ return False;
+ end Has_Aspect;
+
------------------
-- Move_Aspects --
------------------
@@ -271,6 +294,7 @@
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,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 197899)
+++ aspects.ads (working copy)
@@ -161,6 +161,7 @@
Aspect_Discard_Names,
Aspect_Export,
Aspect_Favor_Top_Level, -- GNAT
+ Aspect_Ghost, -- GNAT
Aspect_Independent,
Aspect_Independent_Components,
Aspect_Import,
@@ -234,6 +235,7 @@
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
+ Aspect_Ghost => True,
Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Invariant => True,
@@ -413,6 +415,7 @@
Aspect_External_Tag => Name_External_Tag,
Aspect_Export => Name_Export,
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,
@@ -500,11 +503,6 @@
-- implemented internally with a hash table in the body, that provides
-- access to aspect specifications.
- function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
- -- Returns True if the node N is a declaration node that permits aspect
- -- specifications in the grammar. It is possible for other nodes to have
- -- aspect specifications as a result of Rewrite or Replace calls.
-
function Aspect_Specifications (N : Node_Id) return List_Id;
-- Given a node N, returns the list of N_Aspect_Specification nodes that
-- are attached to this declaration node. If the node is in the class of
@@ -519,34 +517,42 @@
-- Replace calls, and this function may be used to retrieve the aspect
-- specifications for the original rewritten node in such cases.
- procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
- -- The node N must be in the class of declaration nodes that permit aspect
- -- specifications and the Has_Aspects flag must be False on entry. L must
- -- be a non-empty list of N_Aspect_Specification nodes. This procedure sets
- -- the Has_Aspects flag to True, and makes an entry that can be retrieved
- -- by a subsequent Aspect_Specifications call. It is an error to call this
- -- procedure with a node that does not permit aspect specifications, or a
- -- node that has its Has_Aspects flag set True on entry, or with L being an
- -- empty list or No_List.
-
function Find_Aspect (Ent : Entity_Id; A : Aspect_Id) return Node_Id;
-- Find value of a given aspect from aspect list of entity
+ function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean;
+ -- Determine whether entity Id has aspect A
+
procedure Move_Aspects (From : Node_Id; To : Node_Id);
-- Moves aspects from 'From' node to 'To' node. Has_Aspects (To) must be
-- False on entry. If Has_Aspects (From) is False, the call has no effect.
-- Otherwise the aspects are moved and on return Has_Aspects (To) is True,
-- and Has_Aspects (From) is False.
+ function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
+ -- Returns True if the node N is a declaration node that permits aspect
+ -- specifications in the grammar. It is possible for other nodes to have
+ -- aspect specifications as a result of Rewrite or Replace calls.
+
function Same_Aspect (A1 : Aspect_Id; A2 : Aspect_Id) return Boolean;
-- Returns True if A1 and A2 are (essentially) the same aspect. This is not
-- a simple equality test because e.g. Post and Postcondition are the same.
-- This is used for detecting duplicate aspects.
- procedure Tree_Write;
- -- Writes contents of Aspect_Specifications hash table to the tree file
+ procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
+ -- The node N must be in the class of declaration nodes that permit aspect
+ -- specifications and the Has_Aspects flag must be False on entry. L must
+ -- be a non-empty list of N_Aspect_Specification nodes. This procedure sets
+ -- the Has_Aspects flag to True, and makes an entry that can be retrieved
+ -- by a subsequent Aspect_Specifications call. It is an error to call this
+ -- procedure with a node that does not permit aspect specifications, or a
+ -- node that has its Has_Aspects flag set True on entry, or with L being an
+ -- empty list or No_List.
procedure Tree_Read;
-- Reads contents of Aspect_Specifications hash table from the tree file
+ procedure Tree_Write;
+ -- Writes contents of Aspect_Specifications hash table to the tree file
+
end Aspects;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 197906)
+++ sem_ch6.adb (working copy)
@@ -486,19 +486,21 @@
----------------------------
procedure Analyze_Function_Call (N : Node_Id) is
- P : constant Node_Id := Name (N);
- Actuals : constant List_Id := Parameter_Associations (N);
- Actual : Node_Id;
+ Actuals : constant List_Id := Parameter_Associations (N);
+ Func_Nam : constant Node_Id := Name (N);
+ Actual : Node_Id;
+ -- Start of processing for Analyze_Function_Call
+
begin
- Analyze (P);
+ Analyze (Func_Nam);
-- A call of the form A.B (X) may be an Ada 2005 call, which is
-- rewritten as B (A, X). If the rewriting is successful, the call
-- has been analyzed and we just return.
- if Nkind (P) = N_Selected_Component
- and then Name (N) /= P
+ if Nkind (Func_Nam) = N_Selected_Component
+ and then Name (N) /= Func_Nam
and then Is_Rewrite_Substitution (N)
and then Present (Etype (N))
then
@@ -507,7 +509,7 @@
-- If error analyzing name, then set Any_Type as result type and return
- if Etype (P) = Any_Type then
+ if Etype (Func_Nam) = Any_Type then
Set_Etype (N, Any_Type);
return;
end if;
@@ -524,12 +526,6 @@
end if;
Analyze_Call (N);
-
- -- Mark function call if within assertion
-
- if In_Assertion_Expr /= 0 then
- Set_In_Assertion (N);
- end if;
end Analyze_Function_Call;
-----------------------------
@@ -537,9 +533,9 @@
-----------------------------
procedure Analyze_Function_Return (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Stm_Entity : constant Entity_Id := Return_Statement_Entity (N);
- Scope_Id : constant Entity_Id := Return_Applies_To (Stm_Entity);
+ Loc : constant Source_Ptr := Sloc (N);
+ Stm_Entity : constant Entity_Id := Return_Statement_Entity (N);
+ Scope_Id : constant Entity_Id := Return_Applies_To (Stm_Entity);
R_Type : constant Entity_Id := Etype (Scope_Id);
-- Function result subtype
@@ -6562,6 +6558,11 @@
else
Set_Overridden_Operation (Subp, Overridden_Subp);
end if;
+
+ -- Ensure that a ghost function is not overriding another routine
+
+ elsif Is_Ghost_Function (Subp) then
+ Error_Msg_N ("ghost function & cannot be overriding", Subp);
end if;
end if;
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 197899)
+++ par-prag.adb (working copy)
@@ -1166,6 +1166,7 @@
Pragma_Fast_Math |
Pragma_Finalize_Storage_Only |
Pragma_Float_Representation |
+ Pragma_Ghost |
Pragma_Global |
Pragma_Ident |
Pragma_Implementation_Defined |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 197907)
+++ snames.ads-tmpl (working copy)
@@ -498,6 +498,7 @@
Name_Export_Valued_Procedure : 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 + $; -- VMS
Name_Implementation_Defined : constant Name_Id := N + $; -- GNAT
@@ -1792,6 +1793,7 @@
Pragma_Export_Valued_Procedure,
Pragma_External,
Pragma_Finalize_Storage_Only,
+ Pragma_Ghost,
Pragma_Global,
Pragma_Ident,
Pragma_Implementation_Defined,
