From 4179af278f73fc12431fc749bda65fbbf4752602 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Mon, 18 Apr 2016 10:22:13 +0000 Subject: [PATCH] contracts.adb (Analyze_Object_Contract): Update references to SPARK RM. 2016-04-18 Hristian Kirtchev * 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. From-SVN: r235115 --- gcc/ada/ChangeLog | 32 +++++ gcc/ada/contracts.adb | 4 +- gcc/ada/freeze.adb | 6 +- gcc/ada/ghost.adb | 290 +++++++++++++++++++++++++++++++----------- gcc/ada/ghost.ads | 25 ++-- gcc/ada/sem_ch3.adb | 12 +- gcc/ada/sem_ch6.adb | 30 +++-- gcc/ada/sem_prag.adb | 117 +++++------------ gcc/ada/sem_res.adb | 2 +- 9 files changed, 326 insertions(+), 192 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e59b0672df3..969143318ba 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,35 @@ +2016-04-18 Hristian Kirtchev + + * 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 * layout.adb: Fix more minor typos in comments. diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 4eb6d26adba..35a9fd0d1fc 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -907,13 +907,13 @@ package body Contracts is 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. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 736535eafaf..556c23adbd4 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -3466,8 +3466,8 @@ package body Freeze is 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 @@ -5213,7 +5213,7 @@ package body Freeze is 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); diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index f2ac16b5421..9d01b6dce14 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -36,6 +36,7 @@ with Nmake; use Nmake; 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; @@ -154,7 +155,7 @@ package body Ghost is 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 -- @@ -334,30 +335,19 @@ package body Ghost is 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, @@ -455,7 +445,7 @@ package body Ghost is 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; @@ -504,7 +494,7 @@ package body Ghost is 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); @@ -540,48 +530,6 @@ package body Ghost is 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 -- ---------------------------- @@ -590,40 +538,234 @@ package body Ghost is (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 -- ------------------ diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 3dbe5026aea..7a0aec3906c 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -45,16 +45,25 @@ 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_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 @@ -85,7 +94,7 @@ package Ghost is 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. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index a010b54cb61..d401bd181a3 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -14649,8 +14649,8 @@ package body Sem_Ch3 is 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')); @@ -19956,14 +19956,6 @@ package body Sem_Ch3 is 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. diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 437ca141954..17c26238fca 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4701,18 +4701,6 @@ package body Sem_Ch6 is 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; @@ -9014,6 +9002,12 @@ package body Sem_Ch6 is 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; @@ -9041,6 +9035,12 @@ package body Sem_Ch6 is 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); @@ -9068,6 +9068,12 @@ package body Sem_Ch6 is 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; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 46a30390c86..e951804cd62 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -11585,7 +11585,8 @@ package body Sem_Prag is -- 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 @@ -11595,6 +11596,30 @@ package body Sem_Prag is 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: @@ -11612,7 +11637,7 @@ package body Sem_Prag is 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; @@ -12371,8 +12396,7 @@ package body Sem_Prag is -- new form syntax. when Pragma_Check_Policy => Check_Policy : declare - Ident : Node_Id; - Kind : Node_Id; + Kind : Node_Id; begin GNAT_Pragma; @@ -12416,29 +12440,6 @@ package body Sem_Prag is 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 @@ -15021,14 +15022,6 @@ package body Sem_Prag is 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. @@ -15040,7 +15033,7 @@ package body Sem_Prag is -- 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; @@ -15058,7 +15051,7 @@ package body Sem_Prag is -- 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 @@ -15092,7 +15085,7 @@ package body Sem_Prag is 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 @@ -25230,51 +25223,11 @@ package body Sem_Prag is 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). diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index bd4b562f09b..18794c83a50 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4528,7 +4528,7 @@ package body Sem_Res is 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) -- 2.30.2