@@ -472,6 +472,13 @@ package body Ghost is
if Is_Ignored_Ghost_Node (Par) then
return True;
+ -- It is not possible to check correct use of Ghost entities
+ -- in generic instantiations until after the generic has been
+ -- resolved. Postpone that verification to after resolution.
+
+ elsif Nkind (Par) = N_Generic_Association then
+ return True;
+
-- A reference to a Ghost entity can appear within an aspect
-- specification (SPARK RM 6.9(10)). The precise checking will
-- occur when analyzing the corresponding pragma. We make an
@@ -521,19 +528,6 @@ package body Ghost is
then
return True;
- -- In the context of an instantiation, accept currently Ghost
- -- arguments for formal subprograms, as SPARK does not provide
- -- a way to distinguish Ghost formal parameters from non-Ghost
- -- ones. Illegal use of such arguments in a non-Ghost context
- -- will lead to errors inside the instantiation.
-
- elsif Nkind (Parent (Par)) = N_Generic_Association
- and then (Nkind (Par) in N_Has_Entity
- and then Present (Entity (Par))
- and then Is_Subprogram (Entity (Par)))
- then
- return True;
-
elsif Is_OK_Declaration (Par) then
return True;
@@ -680,6 +674,128 @@ package body Ghost is
end if;
end Check_Ghost_Context;
+ ------------------------------------------------
+ -- Check_Ghost_Context_In_Generic_Association --
+ ------------------------------------------------
+
+ procedure Check_Ghost_Context_In_Generic_Association
+ (Actual : Node_Id;
+ Formal : Entity_Id)
+ is
+ function Emit_Error_On_Ghost_Reference
+ (N : Node_Id)
+ return Traverse_Result;
+ -- Determine wether N denotes a reference to a ghost entity, and if so
+ -- issue an error.
+
+ -----------------------------------
+ -- Emit_Error_On_Ghost_Reference --
+ -----------------------------------
+
+ function Emit_Error_On_Ghost_Reference
+ (N : Node_Id)
+ return Traverse_Result
+ is
+ begin
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ and then Is_Ghost_Entity (Entity (N))
+ then
+ Error_Msg_N ("ghost entity cannot appear in this context", N);
+ Error_Msg_Sloc := Sloc (Formal);
+ Error_Msg_NE ("\formal & was not declared as ghost #", N, Formal);
+ return Abandon;
+ end if;
+
+ return OK;
+ end Emit_Error_On_Ghost_Reference;
+
+ procedure Check_Ghost_References is
+ new Traverse_Proc (Emit_Error_On_Ghost_Reference);
+
+ -- Start of processing for Check_Ghost_Context_In_Generic_Association
+
+ begin
+ -- The context is ghost when it appears within a Ghost package or
+ -- subprogram.
+
+ if Ghost_Mode > None then
+ return;
+
+ -- The context is ghost if Formal is explicitly marked as ghost
+
+ elsif Is_Ghost_Entity (Formal) then
+ return;
+
+ else
+ Check_Ghost_References (Actual);
+ end if;
+ end Check_Ghost_Context_In_Generic_Association;
+
+ ---------------------------------------------
+ -- Check_Ghost_Formal_Procedure_Or_Package --
+ ---------------------------------------------
+
+ procedure Check_Ghost_Formal_Procedure_Or_Package
+ (N : Node_Id;
+ Actual : Entity_Id;
+ Formal : Entity_Id;
+ Is_Default : Boolean := False)
+ is
+ begin
+ if not Is_Ghost_Entity (Formal) then
+ return;
+ end if;
+
+ if Present (Actual) and then Is_Ghost_Entity (Actual) then
+ return;
+ end if;
+
+ if Is_Default then
+ Error_Msg_N ("ghost procedure expected as default", N);
+ Error_Msg_NE ("\formal & is declared as ghost", N, Formal);
+
+ else
+ if Ekind (Formal) = E_Procedure then
+ Error_Msg_N ("ghost procedure expected for actual", N);
+ else
+ Error_Msg_N ("ghost package expected for actual", N);
+ end if;
+
+ Error_Msg_Sloc := Sloc (Formal);
+ Error_Msg_NE ("\formal & was declared as ghost #", N, Formal);
+ end if;
+ end Check_Ghost_Formal_Procedure_Or_Package;
+
+ ---------------------------------
+ -- Check_Ghost_Formal_Variable --
+ ---------------------------------
+
+ procedure Check_Ghost_Formal_Variable
+ (Actual : Node_Id;
+ Formal : Entity_Id;
+ Is_Default : Boolean := False)
+ is
+ Actual_Obj : constant Entity_Id := Get_Enclosing_Deep_Object (Actual);
+ begin
+ if not Is_Ghost_Entity (Formal) then
+ return;
+ end if;
+
+ if No (Actual_Obj)
+ or else not Is_Ghost_Entity (Actual_Obj)
+ then
+ if Is_Default then
+ Error_Msg_N ("ghost object expected as default", Actual);
+ Error_Msg_NE ("\formal & is declared as ghost", Actual, Formal);
+ else
+ Error_Msg_N ("ghost object expected for mutable actual", Actual);
+ Error_Msg_Sloc := Sloc (Formal);
+ Error_Msg_NE ("\formal & was declared as ghost #", Actual, Formal);
+ end if;
+ end if;
+ end Check_Ghost_Formal_Variable;
+
----------------------------
-- Check_Ghost_Overriding --
----------------------------
@@ -44,6 +44,33 @@ package Ghost is
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
+ procedure Check_Ghost_Context_In_Generic_Association
+ (Actual : Node_Id;
+ Formal : Entity_Id);
+ -- Check that if Actual contains references to ghost entities, generic
+ -- formal parameter Formal is ghost (SPARK RM 6.9(10)).
+
+ procedure Check_Ghost_Formal_Procedure_Or_Package
+ (N : Node_Id;
+ Actual : Entity_Id;
+ Formal : Entity_Id;
+ Is_Default : Boolean := False);
+ -- Verify that if generic formal procedure (resp. package) Formal is ghost,
+ -- then Actual is not Empty and also a ghost procedure (resp. package)
+ -- (SPARK RM 6.9(13-14)). The error if any is located on N. If
+ -- Is_Default is False, N and Actual represent the actual parameter in an
+ -- instantiation. Otherwise, they represent the default subprogram of a
+ -- formal subprogram declaration.
+
+ procedure Check_Ghost_Formal_Variable
+ (Actual : Node_Id;
+ Formal : Entity_Id;
+ Is_Default : Boolean := False);
+ -- Verify that if Formal (either an IN OUT generic formal parameter, or an
+ -- IN generic formal parameter of access-to-variable type) is ghost, then
+ -- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
+ -- Actual is the default expression of the formal object declaration.
+
procedure Check_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id);
@@ -54,27 +54,34 @@ generic
Unsigned_Width_Ghost : Natural;
- with function Wrap_Option (Value : Uns) return Uns_Option;
+ with function Wrap_Option (Value : Uns) return Uns_Option
+ with Ghost;
with function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
- return Boolean;
- with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+ return Boolean
+ with Ghost;
+ with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+ with Ghost;
with function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
- Acc : Uns := 0) return Uns_Option;
- with function Is_Unsigned_Ghost (Str : String) return Boolean;
+ Acc : Uns := 0) return Uns_Option
+ with Ghost;
+ with function Is_Unsigned_Ghost (Str : String) return Boolean
+ with Ghost;
with function Value_Unsigned (Str : String) return Uns;
with procedure Prove_Iter_Scan_Based_Number_Ghost
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
- Acc : Uns := 0);
+ Acc : Uns := 0)
+ with Ghost;
with procedure Prove_Scan_Only_Decimal_Ghost
(Str : String;
- Val : Uns);
+ Val : Uns)
+ with Ghost;
package System.Image_U is
@@ -55,30 +55,37 @@ generic
-- Additional parameters for ghost subprograms used inside contracts
type Uns_Option is private;
- with function Wrap_Option (Value : Uns) return Uns_Option;
- with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
+ with function Wrap_Option (Value : Uns) return Uns_Option
+ with Ghost;
+ with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean
+ with Ghost;
with function Raw_Unsigned_Overflows_Ghost
(Str : String;
From, To : Integer)
- return Boolean;
+ return Boolean
+ with Ghost;
with function Scan_Raw_Unsigned_Ghost
(Str : String;
From, To : Integer)
- return Uns;
+ return Uns
+ with Ghost;
with function Raw_Unsigned_Last_Ghost
(Str : String;
From, To : Integer)
- return Positive;
+ return Positive
+ with Ghost;
with function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
- return Boolean;
+ return Boolean
+ with Ghost;
with function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
- return Uns_Option;
+ return Uns_Option
+ with Ghost;
package System.Value_I is
pragma Preelaborate;
@@ -384,27 +384,36 @@ is
Unsigned_Width_Ghost : Natural;
- with function Wrap_Option (Value : Uns) return Uns_Option;
+ with function Wrap_Option (Value : Uns) return Uns_Option
+ with Ghost;
with function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
- return Boolean;
- with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+ return Boolean
+ with Ghost;
+ with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+ with Ghost;
with function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
- return Uns_Option;
- with function Is_Integer_Ghost (Str : String) return Boolean;
+ return Uns_Option
+ with Ghost;
+ with function Is_Integer_Ghost (Str : String) return Boolean
+ with Ghost;
with procedure Prove_Iter_Scan_Based_Number_Ghost
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
- Acc : Uns := 0);
- with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int);
- with function Abs_Uns_Of_Int (Val : Int) return Uns;
- with function Value_Integer (Str : String) return Int;
+ Acc : Uns := 0)
+ with Ghost;
+ with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+ with Ghost;
+ with function Abs_Uns_Of_Int (Val : Int) return Uns
+ with Ghost;
+ with function Value_Integer (Str : String) return Int
+ with Ghost;
package Int_Params is
end Int_Params;
@@ -2204,6 +2204,19 @@ package body Sem_Ch12 is
raise Program_Error;
end case;
+ -- Check here the correct use of Ghost entities in generic
+ -- instantiations, as now the generic has been resolved and
+ -- we know which formal generic parameters are ghost (SPARK
+ -- RM 6.9(10)).
+
+ if Nkind (Formal) not in N_Use_Package_Clause
+ | N_Use_Type_Clause
+ then
+ Check_Ghost_Context_In_Generic_Association
+ (Actual => Match,
+ Formal => Defining_Entity (Analyzed_Formal));
+ end if;
+
Formal := Saved_Formal;
Next_Non_Pragma (Analyzed_Formal);
end loop;
@@ -2715,6 +2728,17 @@ package body Sem_Ch12 is
if Present (E) then
Preanalyze_Spec_Expression (E, T);
+ -- The default for a ghost generic formal IN parameter of
+ -- access-to-variable type should be a ghost object (SPARK
+ -- RM 6.9(13)).
+
+ if Is_Access_Variable (T) then
+ Check_Ghost_Formal_Variable
+ (Actual => E,
+ Formal => Id,
+ Is_Default => True);
+ end if;
+
if Is_Limited_Type (T) and then not OK_For_Limited_Init (T, E) then
Error_Msg_N
("initialization not allowed for limited types", E);
@@ -3398,6 +3422,25 @@ package body Sem_Ch12 is
goto Leave;
end if;
+ -- The default for a ghost generic formal procedure should be a ghost
+ -- procedure (SPARK RM 6.9(13)).
+
+ if Ekind (Nam) = E_Procedure then
+ declare
+ Def_E : Entity_Id := Empty;
+ begin
+ if Nkind (Def) in N_Has_Entity then
+ Def_E := Entity (Def);
+ end if;
+
+ Check_Ghost_Formal_Procedure_Or_Package
+ (N => Def,
+ Actual => Def_E,
+ Formal => Nam,
+ Is_Default => True);
+ end;
+ end if;
+
-- Default name may be overloaded, in which case the interpretation
-- with the correct profile must be selected, as for a renaming.
-- If the definition is an indexed component, it must denote a
@@ -10594,6 +10637,14 @@ package body Sem_Ch12 is
Gen_Parent := Generic_Parent (Specification (Analyzed_Formal));
Formal_Pack := Defining_Unit_Name (Specification (Analyzed_Formal));
+ -- The actual for a ghost generic formal package should be a ghost
+ -- package (SPARK RM 6.9(14)).
+
+ Check_Ghost_Formal_Procedure_Or_Package
+ (N => Actual,
+ Actual => Actual_Pack,
+ Formal => Formal_Pack);
+
if Nkind (Parent (Actual_Pack)) = N_Defining_Program_Unit_Name then
Parent_Spec := Package_Specification (Actual_Pack);
else
@@ -10881,6 +10932,18 @@ package body Sem_Ch12 is
Act_E := Empty;
end if;
+ -- The actual for a ghost generic formal procedure should be a ghost
+ -- procedure (SPARK RM 6.9(14)).
+
+ if Present (Act_E)
+ and then Ekind (Act_E) = E_Procedure
+ then
+ Check_Ghost_Formal_Procedure_Or_Package
+ (N => Act,
+ Actual => Act_E,
+ Formal => Analyzed_S);
+ end if;
+
if (Present (Act_E) and then Is_Overloadable (Act_E))
or else Nkind (Act) in N_Attribute_Reference
| N_Indexed_Component
@@ -11400,40 +11463,22 @@ package body Sem_Ch12 is
-- volatility refinement aspects.
declare
- Actual_Obj : Entity_Id;
- N : Node_Id := Actual;
+ Actual_Obj : constant Entity_Id :=
+ Get_Enclosing_Deep_Object (Actual);
begin
- -- Similar to Sem_Util.Get_Enclosing_Object, but treat
- -- pointer dereference like component selection.
- loop
- if Is_Entity_Name (N) then
- Actual_Obj := Entity (N);
- exit;
- end if;
-
- case Nkind (N) is
- when N_Indexed_Component
- | N_Selected_Component
- | N_Slice
- | N_Explicit_Dereference
- =>
- N := Prefix (N);
-
- when N_Type_Conversion =>
- N := Expression (N);
-
- when others =>
- Actual_Obj := Etype (N);
- exit;
- end case;
- end loop;
-
Check_Volatility_Compatibility
(Actual_Obj, A_Gen_Obj, "actual object",
"its corresponding formal object of mode in out",
Srcpos_Bearer => Actual);
end;
+ -- The actual for a ghost generic formal IN OUT parameter should be a
+ -- ghost object (SPARK RM 6.9(14)).
+
+ Check_Ghost_Formal_Variable
+ (Actual => Actual,
+ Formal => A_Gen_Obj);
+
-- Formal in-parameter
else
@@ -11459,6 +11504,7 @@ package body Sem_Ch12 is
Object_Definition => Def,
Expression => Actual);
+ Copy_Ghost_Aspect (Formal, To => Decl_Node);
Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc);
-- A generic formal object of a tagged type is defined to be
@@ -11470,6 +11516,16 @@ package body Sem_Ch12 is
Append (Decl_Node, List);
+ -- The actual for a ghost generic formal IN parameter of
+ -- access-to-variable type should be a ghost object (SPARK
+ -- RM 6.9(14)).
+
+ if Is_Access_Variable (Etype (A_Gen_Obj)) then
+ Check_Ghost_Formal_Variable
+ (Actual => Actual,
+ Formal => A_Gen_Obj);
+ end if;
+
-- No need to repeat (pre-)analysis of some expression nodes
-- already handled in Preanalyze_Actuals.
@@ -11543,6 +11599,7 @@ package body Sem_Ch12 is
Expression => New_Copy_Tree
(Default_Expression (Formal)));
+ Copy_Ghost_Aspect (Formal, To => Decl_Node);
Set_Corresponding_Generic_Association
(Decl_Node, Expression (Decl_Node));
@@ -14199,6 +14256,8 @@ package body Sem_Ch12 is
Defining_Identifier => Subt,
Subtype_Indication => New_Occurrence_Of (Act_T, Loc));
+ Copy_Ghost_Aspect (Formal, To => Decl_Node);
+
-- Record whether the actual is private at this point, so that
-- Check_Generic_Actuals can restore its proper view before the
-- semantic analysis of the instance.
@@ -17002,6 +17002,9 @@ package body Sem_Prag is
-- The pragma applies to a legal construct, stop the traversal
elsif Nkind (Stmt) in N_Abstract_Subprogram_Declaration
+ | N_Formal_Object_Declaration
+ | N_Formal_Subprogram_Declaration
+ | N_Formal_Type_Declaration
| N_Full_Type_Declaration
| N_Generic_Subprogram_Declaration
| N_Object_Declaration
@@ -7024,6 +7024,25 @@ package body Sem_Util is
return Comps;
end Copy_Component_List;
+ -----------------------
+ -- Copy_Ghost_Aspect --
+ -----------------------
+
+ procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id) is
+ pragma Assert (not Has_Aspects (To));
+ Asp : Node_Id;
+
+ begin
+ if Has_Aspects (From) then
+ Asp := Find_Aspect (Defining_Entity (From), Aspect_Ghost);
+
+ if Present (Asp) then
+ Set_Aspect_Specifications (To, New_List (New_Copy_Tree (Asp)));
+ Set_Has_Aspects (To, True);
+ end if;
+ end if;
+ end Copy_Ghost_Aspect;
+
-------------------------
-- Copy_Parameter_List --
-------------------------
@@ -11004,6 +11023,32 @@ package body Sem_Util is
end if;
end Get_Enclosing_Object;
+ -------------------------------
+ -- Get_Enclosing_Deep_Object --
+ -------------------------------
+
+ function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id is
+ begin
+ if Is_Entity_Name (N) then
+ return Entity (N);
+ else
+ case Nkind (N) is
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ return Get_Enclosing_Deep_Object (Prefix (N));
+
+ when N_Type_Conversion =>
+ return Get_Enclosing_Deep_Object (Expression (N));
+
+ when others =>
+ return Empty;
+ end case;
+ end if;
+ end Get_Enclosing_Deep_Object;
+
---------------------------
-- Get_Enum_Lit_From_Pos --
---------------------------
@@ -625,6 +625,11 @@ package Sem_Util is
-- create a new compatible record type. Loc is the source location assigned
-- to the created nodes.
+ procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id);
+ -- Copy the Ghost aspect if present in the aspect specifications of node
+ -- From to node To. On entry it is assumed that To does not have aspect
+ -- specifications. If From has no aspects, the routine has no effect.
+
function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
-- Utility to create a parameter profile for a new subprogram spec, when
-- the subprogram has a body that acts as spec. This is done for some cases
@@ -1183,6 +1188,12 @@ package Sem_Util is
-- If expression N references a part of an object, return this object.
-- Otherwise return Empty. Expression N should have been resolved already.
+ function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id;
+ -- If expression N references a reachable part of an object (as defined in
+ -- SPARK RM 6.9), return this object. Otherwise return Empty. It is similar
+ -- to Get_Enclosing_Object, but treats pointer dereference like component
+ -- selection. Expression N should have been resolved already.
+
function Get_Generic_Entity (N : Node_Id) return Entity_Id;
-- Returns the true generic entity in an instantiation. If the name in the
-- instantiation is a renaming, the function returns the renamed generic.