+2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * contracts.adb (Analyze_Object_Contract): Update references to
+ SPARK RM.
+ * freeze.adb (Freeze_Entity): Update references to SPARK RM.
+ * ghost.adb Add with and use clauses for Sem_Disp.
+ (Check_Ghost_Derivation): Removed.
+ (Check_Ghost_Overriding):
+ Reimplemented. (Check_Ghost_Policy): Update references to SPARK RM.
+ (Check_Ghost_Primitive): New routine.
+ (Check_Ghost_Refinement): New routine. (Is_OK_Ghost_Context):
+ Update references to SPARK RM. (Is_OK_Pragma): Update references
+ to SPARK RM. Predicates are now a valid context for references
+ to Ghost entities.
+ * ghost.ads (Check_Ghost_Derivation): Removed.
+ (Check_Ghost_Overriding): Update the comment on usage.
+ (Check_Ghost_Primitive): New routine.
+ (Check_Ghost_Refinement): New routine.
+ (Remove_Ignored_Ghost_Code): Update references to SPARK RM.
+ * sem_ch3.adb (Process_Full_View): Remove the now obsolete check
+ related to Ghost derivations
+ * sem_ch6.adb (Check_Conformance): Remove now obsolete check
+ related to the convention-like behavior of pragma Ghost.
+ (Check_For_Primitive_Subprogram): Verify that the Ghost policy
+ of a tagged type and its primitive agree.
+ * sem_prag.adb (Analyze_Pragma): Update references to SPARK
+ RM. Move the verification of pragma Assertion_Policy Ghost
+ to the proper place. Remove the now obsolete check related
+ to Ghost derivations.
+ (Collect_Constituent): Add a call to Check_Ghost_Refinement.
+ * sem_res.adb (Resolve_Actuals): Update references to SPARK RM.
+
2016-04-18 Eric Botcazou <ebotcazou@adacore.com>
* layout.adb: Fix more minor typos in comments.
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
- -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
+ -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
-- SPARK RM 6.9(19)).
elsif Is_Effectively_Volatile (Obj_Id) then
Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
- -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)).
+ -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
-- One exception to this is the object that represents the dispatch
-- table of a Ghost tagged type, as the symbol needs to be exported.
and then Convention (E) /= Convention_Intrinsic
- -- Assume that ASM interface knows what it is doing. This deals
- -- with unsigned.ads in the AAMP back end.
+ -- Assume that ASM interface knows what it is doing. This deals
+ -- with unsigned.ads in the AAMP back end.
and then Convention (E) /= Convention_Assembler
then
if Is_Concurrent_Type (E) then
Error_Msg_N ("ghost type & cannot be concurrent", E);
- -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
+ -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
elsif Is_Effectively_Volatile (E) then
Error_Msg_N ("ghost type & cannot be volatile", E);
with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
+with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
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.
+ -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
-------------------------
-- Is_OK_Ghost_Context --
return True;
-- An assertion expression pragma is Ghost when it contains a
- -- reference to a Ghost entity (SPARK RM 6.9(11)).
+ -- reference to a Ghost entity (SPARK RM 6.9(10)).
elsif Assertion_Expression_Pragma (Prag_Id) then
- -- Predicates are excluded from this category when they do
- -- not apply to a Ghost subtype (SPARK RM 6.9(11)).
+ -- Ensure that the assertion policy and the Ghost policy are
+ -- compatible (SPARK RM 6.9(18)).
- if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
- Name_Predicate,
- Name_Static_Predicate)
- then
- return False;
-
- -- Otherwise ensure that the assertion policy and the Ghost
- -- policy are compatible (SPARK RM 6.9(18)).
-
- else
- Check_Policies (Prag_Nam);
- return True;
- end if;
+ Check_Policies (Prag_Nam);
+ return True;
-- Several pragmas that may apply to a non-Ghost entity are
-- treated as Ghost when they contain a reference to a Ghost
- -- entity (SPARK RM 6.9(12)).
+ -- entity (SPARK RM 6.9(11)).
elsif Nam_In (Prag_Nam, Name_Global,
Name_Depends,
return True;
-- A reference to a Ghost entity can appear within an aspect
- -- specification (SPARK RM 6.9(11)).
+ -- specification (SPARK RM 6.9(10)).
elsif Nkind (Par) = N_Aspect_Specification then
return True;
begin
-- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(14)).
+ -- 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);
end if;
end Check_Ghost_Context;
- ----------------------------
- -- 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
- Error_Msg_N ("type extension & cannot be ghost", Typ);
- Error_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
- Error_Msg_N ("type extension & cannot be ghost", Typ);
- Error_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_Ghost_Overriding --
----------------------------
(Subp : Entity_Id;
Overridden_Subp : Entity_Id)
is
+ Deriv_Typ : Entity_Id;
Over_Subp : Entity_Id;
begin
if Present (Subp) and then Present (Overridden_Subp) then
Over_Subp := Ultimate_Alias (Overridden_Subp);
+ Deriv_Typ := Find_Dispatching_Type (Subp);
- -- The Ghost policy in effect at the point of declaration of a parent
- -- and an overriding subprogram must match (SPARK RM 6.9(17)).
+ -- A Ghost primitive of a non-Ghost type extension cannot override an
+ -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
- if Is_Checked_Ghost_Entity (Over_Subp)
- and then Is_Ignored_Ghost_Entity (Subp)
+ if Is_Ghost_Entity (Subp)
+ and then Present (Deriv_Typ)
+ and then not Is_Ghost_Entity (Deriv_Typ)
+ and then not Is_Ghost_Entity (Over_Subp)
then
- Error_Msg_N ("incompatible ghost policies in effect", Subp);
+ Error_Msg_N ("incompatible overriding in effect", Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N ("\& declared # with ghost policy `Check`", Subp);
+ Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
+ Error_Msg_N ("\overridden # with ghost subprogram", Subp);
+ end if;
+
+ -- A non-Ghost primitive of a type extension cannot override an
+ -- inherited Ghost primitive (SPARK RM 6.9(8)).
- elsif Is_Ignored_Ghost_Entity (Over_Subp)
- and then Is_Checked_Ghost_Entity (Subp)
+ if not Is_Ghost_Entity (Subp)
+ and then Is_Ghost_Entity (Over_Subp)
then
- Error_Msg_N ("incompatible ghost policies in effect", Subp);
+ Error_Msg_N ("incompatible overriding in effect", Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
+ Error_Msg_N ("\& declared # as ghost subprogram", Subp);
Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N ("\overridden # with ghost policy `Check`", Subp);
+ Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
+ end if;
+
+ if Present (Deriv_Typ)
+ and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
+ then
+ -- When a tagged type is either non-Ghost or checked Ghost and
+ -- one of its primitives overrides an inherited operation, the
+ -- overridden operation of the ancestor type must be ignored Ghost
+ -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
+
+ if Is_Ignored_Ghost_Entity (Subp) then
+
+ -- Both the parent subprogram and overriding subprogram are
+ -- ignored Ghost.
+
+ if Is_Ignored_Ghost_Entity (Over_Subp) then
+ null;
+
+ -- The parent subprogram carries policy Check
+
+ elsif Is_Checked_Ghost_Entity (Over_Subp) then
+ Error_Msg_N
+ ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Check`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with ghost policy `Ignore`", Subp);
+
+ -- The parent subprogram is non-Ghost
+
+ else
+ Error_Msg_N
+ ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with ghost policy `Ignore`", Subp);
+ end if;
+
+ -- When a tagged type is either non-Ghost or checked Ghost and
+ -- one of its primitives overrides an inherited operation, the
+ -- the primitive of the tagged type must be ignored Ghost if the
+ -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
+
+ elsif Is_Ignored_Ghost_Entity (Over_Subp) then
+
+ -- Both the parent subprogram and the overriding subprogram are
+ -- ignored Ghost.
+
+ if Is_Ignored_Ghost_Entity (Subp) then
+ null;
+
+ -- The overriding subprogram carries policy Check
+
+ elsif Is_Checked_Ghost_Entity (Subp) then
+ Error_Msg_N
+ ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Ignore`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with Ghost policy `Check`", Subp);
+
+ -- The overriding subprogram is non-Ghost
+
+ else
+ Error_Msg_N
+ ("incompatible ghost policies in effect", Subp);
+
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Ignore`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with non-ghost subprogram", Subp);
+ end if;
+ end if;
end if;
end if;
end Check_Ghost_Overriding;
+ ---------------------------
+ -- Check_Ghost_Primitive --
+ ---------------------------
+
+ procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
+ begin
+ -- The Ghost policy in effect at the point of declaration of a primitive
+ -- operation and a tagged type must match (SPARK RM 6.9(16)).
+
+ if Is_Tagged_Type (Typ) then
+ if Is_Checked_Ghost_Entity (Prim)
+ and then Is_Ignored_Ghost_Entity (Typ)
+ then
+ Error_Msg_N ("incompatible ghost policies in effect", Prim);
+
+ Error_Msg_Sloc := Sloc (Typ);
+ Error_Msg_NE
+ ("\tagged type & declared # with ghost policy `Ignore`",
+ Prim, Typ);
+
+ Error_Msg_Sloc := Sloc (Prim);
+ Error_Msg_N
+ ("\primitive subprogram & declared # with ghost policy `Check`",
+ Prim);
+
+ elsif Is_Ignored_Ghost_Entity (Prim)
+ and then Is_Checked_Ghost_Entity (Typ)
+ then
+ Error_Msg_N ("incompatible ghost policies in effect", Prim);
+
+ Error_Msg_Sloc := Sloc (Typ);
+ Error_Msg_NE
+ ("\tagged type & declared # with ghost policy `Check`",
+ Prim, Typ);
+
+ Error_Msg_Sloc := Sloc (Prim);
+ Error_Msg_N
+ ("\primitive subprogram & declared # with ghost policy `Ignore`",
+ Prim);
+ end if;
+ end if;
+ end Check_Ghost_Primitive;
+
+ ----------------------------
+ -- Check_Ghost_Refinement --
+ ----------------------------
+
+ procedure Check_Ghost_Refinement
+ (State : Node_Id;
+ State_Id : Entity_Id;
+ Constit : Node_Id;
+ 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_Refinement;
+
------------------
-- Ghost_Entity --
------------------
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
- 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_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id);
- -- Verify that the Ghost policy of parent subprogram Overridden_Subp is the
- -- same as the Ghost policy of overriding subprogram Subp. Emit an error if
- -- this is not the case.
+ -- Verify that the Ghost policy of parent subprogram Overridden_Subp is
+ -- compatible with the Ghost policy of overriding subprogram Subp. Emit
+ -- an error if this is not the case.
+
+ procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
+ -- Verify that the Ghost policy of primitive operation Prim is the same as
+ -- the Ghost policy of tagged type Typ. Emit an error if this is not the
+ -- case.
+
+ procedure Check_Ghost_Refinement
+ (State : Node_Id;
+ State_Id : Entity_Id;
+ Constit : Node_Id;
+ Constit_Id : Entity_Id);
+ -- Verify that the Ghost policy of constituent Constit_Id is compatible
+ -- with the Ghost policy of abstract state State_I.
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
- -- units.
+ -- units (SPARK RM 6.9(4)).
--
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
then
Set_Derived_Name;
- -- Otherwise, the type is inheriting a private operation, so enter
- -- it with a special name so it can't be overridden.
+ -- Otherwise, the type is inheriting a private operation, so enter it
+ -- with a special name so it can't be overridden.
else
Set_Chars (New_Subp, New_External_Name (Chars (Parent_Subp), 'P'));
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;
-
-- Propagate the attributes related to pragma Ghost from the private
-- to the full view.
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)). Do not check internally generated
- -- subprograms as their spec may reside in a Ghost region and their
- -- body not, or vice versa.
-
- elsif Comes_From_Source (Old_Id)
- and then Comes_From_Source (New_Id)
- and then Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id)
- then
- Conformance_Error ("\ghost modes do not match!");
- return;
end if;
end if;
Set_Has_Primitive_Operations (B_Typ);
Set_Is_Primitive (S);
Check_Private_Overriding (B_Typ);
+
+ -- The Ghost policy in effect at the point of declaration of
+ -- a tagged type and a primitive operation must match
+ -- (SPARK RM 6.9(16)).
+
+ Check_Ghost_Primitive (S, B_Typ);
end if;
end if;
Set_Is_Primitive (S);
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
+
+ -- The Ghost policy in effect at the point of declaration of
+ -- a tagged type and a primitive operation must match
+ -- (SPARK RM 6.9(16)).
+
+ Check_Ghost_Primitive (S, B_Typ);
end if;
Next_Formal (Formal);
Set_Is_Primitive (S);
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
+
+ -- The Ghost policy in effect at the point of declaration of a
+ -- tagged type and a primitive operation must match
+ -- (SPARK RM 6.9(16)).
+
+ Check_Ghost_Primitive (S, B_Typ);
end if;
end if;
end Check_For_Primitive_Subprogram;
-- Check Kind and Policy have allowed forms
- Kind := Chars (Arg);
+ Kind := Chars (Arg);
+ Policy := Get_Pragma_Arg (Arg);
if not Is_Valid_Assertion_Kind (Kind) then
Error_Pragma_Arg
Check_Arg_Is_One_Of
(Arg, Name_Check, Name_Disable, Name_Ignore);
+ if Kind = Name_Ghost then
+
+ -- The Ghost policy must be either Check or Ignore
+ -- (SPARK RM 6.9(6)).
+
+ if not Nam_In (Chars (Policy), Name_Check,
+ Name_Ignore)
+ then
+ Error_Pragma_Arg
+ ("argument of pragma % Ghost must be Check or "
+ & "Ignore", Policy);
+ end if;
+
+ -- Pragma Assertion_Policy specifying a Ghost policy
+ -- cannot occur within a Ghost subprogram or package
+ -- (SPARK RM 6.9(14)).
+
+ if Ghost_Mode > None then
+ Error_Pragma
+ ("pragma % cannot appear within ghost subprogram or "
+ & "package");
+ end if;
+ end if;
+
-- Rewrite the Assertion_Policy pragma as a series of
-- Check_Policy pragmas of the form:
Make_Pragma_Argument_Association (LocP,
Expression => Make_Identifier (LocP, Kind)),
Make_Pragma_Argument_Association (LocP,
- Expression => Get_Pragma_Arg (Arg)))));
+ Expression => Policy))));
Arg := Next (Arg);
end loop;
-- new form syntax.
when Pragma_Check_Policy => Check_Policy : declare
- Ident : Node_Id;
- Kind : Node_Id;
+ Kind : Node_Id;
begin
GNAT_Pragma;
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 Ghost_Mode > None 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
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.
-- 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)).
+ -- is also Ghost (SPARK RM 6.9(9)).
if Ekind (Prev_Id) = E_Constant then
Error_Msg_Name_1 := Pname;
-- The full declaration of a type cannot be subject to
-- pragma Ghost unless the partial view is also Ghost
- -- (SPARK RM 6.9(10)).
+ -- (SPARK RM 6.9(9)).
else
Error_Msg_NE (Fix_Error
if Is_OK_Static_Expression (Expr) then
-- "Ghostness" cannot be turned off once enabled within a
- -- region (SPARK RM 6.9(7)).
+ -- region (SPARK RM 6.9(6)).
if Is_False (Expr_Value (Expr))
and then Ghost_Mode > None
procedure Collect_Constituent 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(16)).
-
- 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;
+ -- The Ghost policy in effect at the point of abstract state
+ -- declaration and constituent must match (SPARK RM 6.9(15))
- -- 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;
+ Check_Ghost_Refinement
+ (State, State_Id, Constit, Constit_Id);
-- A synchronized state must be refined by a synchronized
-- object or another synchronized state (SPARK RM 9.6).
end if;
-- The actual parameter of a Ghost subprogram whose formal is of
- -- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(13)).
+ -- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(12)).
if Comes_From_Source (Nam)
and then Is_Ghost_Entity (Nam)
projects / gcc.git / commitdiff