From patchwork Mon Oct 14 12:42:14 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 283190 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client did not present a certificate) by ozlabs.org (Postfix) with ESMTPS id 378672C0359 for ; Mon, 14 Oct 2013 23:42:26 +1100 (EST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=P2msrBa/NfoX7urb7UijIzJXlp7qWUob1tG72xUZqsrwqzjQ+G egNLJ0F9y+6Sd3gk7F2ghN5w6QcEHcbfSGJHA44PWopjUM3Jy2xd1xqL9mALB1lG 9Ut2fg7HBY354uOGUaDe+IfKAxNEG4PzSGqLJT8boyWzJ+/FCvWDSe3fs= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=AqBNzZr4V97hZAXMICwR4Z7RPTE=; b=wp0lBfmkt72/xsLn69tn LMlhkszR8es52bgiG3Z5IPZOdBv8YtxiAx1JJwusSE4H+WEMHcD+PYO91b2PBiiK Jm01153qRZlru6x3QpfRBgxXbhTUKtoLAaYqSqkfa+gSuvH2DeKnHvEHNhj0nQcO MRpjMsqIo1UhRQ9hXOOn1tA= Received: (qmail 5063 invoked by alias); 14 Oct 2013 12:42:19 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 5051 invoked by uid 89); 14 Oct 2013 12:42:19 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Mon, 14 Oct 2013 12:42:17 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 34D7D116537; Mon, 14 Oct 2013 08:42:37 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id O2LaIrAq5sg4; Mon, 14 Oct 2013 08:42:37 -0400 (EDT) Received: from kwai.gnat.com (unknown [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 21D38116518; Mon, 14 Oct 2013 08:42:37 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id BA4763FB31; Mon, 14 Oct 2013 08:42:14 -0400 (EDT) Date: Mon, 14 Oct 2013 08:42:14 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Handling of null refinements in aspect/pragma Refined_Global Message-ID: <20131014124214.GA21217@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) This patch updates the analysis of aspect/pragma Refined_Global to accept legal global refinements of states with null visible refinements. ------------ -- Source -- ------------ -- global_null.ads package Global_Null with Abstract_State => ((In_State with External, Input_Only), (In_Error with External, Input_Only), In_Out_State, In_Out_Error, (Out_State with External, Output_Only), (Out_Error with External, Output_Only)) is In_Var : Integer; In_Out_Var : Integer; Out_Var : Integer; procedure OK_1 with Global => (Input => In_State, In_Out => In_Out_State, Output => Out_State); procedure OK_2 with Global => (Input => In_State, In_Out => In_Out_State, Output => Out_State); procedure OK_3 with Global => (Input => (In_State, In_Var), In_Out => (In_Out_State, In_Out_Var), Output => (Out_State, Out_Var)); procedure Error_1 with Global => (Input => In_Error, In_Out => In_Out_Error, Output => Out_Error); procedure Error_2 with Global => (Input => In_Error, In_Out => In_Out_Error, Output => Out_Error); procedure Error_3 with Global => (Input => (In_Error, In_Var), In_Out => (In_Out_Error, In_Out_Var), Output => (Out_Error, Out_Var)); end Global_Null; -- global_null.adb package body Global_Null with Refined_State => (In_State => null, In_Error => Var_1, In_Out_State => null, In_Out_Error => Var_2, Out_State => null, Out_Error => Var_3) is procedure OK_1 with Refined_Global => null is begin null; end OK_1; procedure OK_2 with Refined_Global => (Input => null, In_Out => null, Output => null) is begin null; end OK_2; procedure OK_3 with Refined_Global => (Input => In_Var, In_Out => In_Out_Var, Output => Out_Var) is begin null; end OK_3; procedure Error_1 with Refined_Global => null is begin null; end Error_1; procedure Error_2 with Refined_Global => (Input => null, In_Out => null, Output => null) is begin null; end Error_2; procedure Error_3 with Refined_Global => (Input => In_Var, In_Out => In_Out_Var, Output => Out_Var) is begin null; end Error_3; Var_1 : Integer; Var_2 : Integer; Var_3 : Integer; end Global_Null; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnatd.V global_null.adb global_null.adb:29:11: refinement cannot be null, subprogram "Error_1" has global items global_null.adb:33:11: global refinement of state "In_Error" must include at least one constituent of mode Input global_null.adb:40:11: global refinement of state "In_Error" must include at least one constituent of mode Input Tested on x86_64-pc-linux-gnu, committed on trunk 2013-10-14 Hristian Kirtchev * einfo.adb: Flag263 is now known as Has_Null_Refinement. (Has_Null_Refinement): New routine. (Set_Has_Null_Refinement): New routine. (Write_Entity_Flags): Output the status of flag Has_Null_Refinement. * einfo.ads: Add new flag Has_Null_Refinement along with comment on usage and update all nodes subject to the flag. (Has_Null_Refinement): New routine along with pragma Inline. (Set_Has_Null_Refinement): New rouitine along with pragma Inline. * sem_prag.adb (Analyze_Constituent): Mark a state as having a null refinement when the sole constituent is "null". (Analyze_Global_List): Handle null input/output items. (Analyze_Refined_Global_In_Decl_Part): Add local variable Has_Null_State. Add logic to handle combinations of states with null refinements and null global lists and/or items. (Check_In_Out_States, Check_Input_States, Check_Output_States): Use attribute Has_Null_Refinement to detect states with constituents. (Check_Refined_Global_List): Handle null input/output items. (Process_Global_Item): Handle states with null refinements. (Process_Global_List): Handle null input/output items. Index: einfo.adb =================================================================== --- einfo.adb (revision 203523) +++ einfo.adb (working copy) @@ -551,8 +551,8 @@ -- Has_Delayed_Rep_Aspects Flag261 -- May_Inherit_Delayed_Rep_Aspects Flag262 + -- Has_Null_Refinement Flag263 - -- (unused) Flag263 -- (unused) Flag264 -- (unused) Flag265 -- (unused) Flag266 @@ -1483,6 +1483,12 @@ return Flag75 (Implementation_Base_Type (Id)); end Has_Non_Standard_Rep; + function Has_Null_Refinement (Id : E) return B is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + return Flag263 (Id); + end Has_Null_Refinement; + function Has_Object_Size_Clause (Id : E) return B is begin pragma Assert (Is_Type (Id)); @@ -4104,6 +4110,12 @@ Set_Flag75 (Id, V); end Set_Has_Non_Standard_Rep; + procedure Set_Has_Null_Refinement (Id : E; V : B := True) is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + Set_Flag263 (Id, V); + end Set_Has_Null_Refinement; + procedure Set_Has_Object_Size_Clause (Id : E; V : B := True) is begin pragma Assert (Is_Type (Id)); @@ -7957,6 +7969,7 @@ W ("Has_Missing_Return", Flag142 (Id)); W ("Has_Nested_Block_With_Handler", Flag101 (Id)); W ("Has_Non_Standard_Rep", Flag75 (Id)); + W ("Has_Null_Refinement", Flag263 (Id)); W ("Has_Object_Size_Clause", Flag172 (Id)); W ("Has_Per_Object_Constraint", Flag154 (Id)); W ("Has_Postconditions", Flag240 (Id)); Index: einfo.ads =================================================================== --- einfo.ads (revision 203522) +++ einfo.ads (working copy) @@ -505,10 +505,10 @@ -- Can_Never_Be_Null (Flag38) -- This flag is defined in all entities, but can only be set in an object --- which can never have a null value. This is set True for constant --- access values initialized to a non-null value. This is also True for --- all access parameters in Ada 83 and Ada 95 modes, and for access --- parameters that explicitly exclude null in Ada 2005. +-- which can never have a null value. Set for constant access values +-- initialized to a non-null value. This is also set for all access +-- parameters in Ada 83 and Ada 95 modes, and for access parameters +-- that explicitly exclude null in Ada 2005. -- -- This is used to avoid unnecessary resetting of the Is_Known_Non_Null -- flag for such entities. In Ada 2005 mode, this is also used when @@ -651,7 +651,7 @@ -- Corresponding_Concurrent_Type (Node18) -- Defined in record types that are constructed by the expander to -- represent task and protected types (Is_Concurrent_Record_Type flag --- set True). Points to the entity for the corresponding task type or +-- set). Points to the entity for the corresponding task type or the -- protected type. -- Corresponding_Discriminant (Node19) @@ -1361,14 +1361,14 @@ -- of derived type declarations). -- Has_All_Calls_Remote (Flag79) --- Defined in all library unit entities. Set true if the library unit --- has an All_Calls_Remote pragma. Note that such entities must also --- be RCI entities, so the flag Is_Remote_Call_Interface will always --- be set if this flag is set. +-- Defined in all library unit entities. Set if the library unit has an +-- All_Calls_Remote pragma. Note that such entities must also be RCI +-- entities, so the flag Is_Remote_Call_Interface will always be set if +-- this flag is set. -- Has_Anonymous_Master (Flag253) -- Defined in units (top-level functions and procedures, library-level --- packages). Set to True if the associated unit contains a heterogeneous +-- packages). Set if the associated unit contains a heterogeneous -- finalization master. The master's name is of the form AM and it -- services anonymous access-to-controlled types with an undetermined -- lifetime. @@ -1438,11 +1438,11 @@ -- in sem_aux is used to test for this case. -- Has_Contiguous_Rep (Flag181) --- Defined in enumeration types. True if the type as a representation +-- Defined in enumeration types. Set if the type as a representation -- clause whose entries are successive integers. -- Has_Controlling_Result (Flag98) --- Defined in E_Function entities. True if the function is a primitive +-- Defined in E_Function entities. Set if the function is a primitive -- function of a tagged type which can dispatch on result. -- Has_Controlled_Component (Flag43) [base type only] @@ -1452,13 +1452,13 @@ -- Has_Controlled_Component is set for at least one component). -- Has_Convention_Pragma (Flag119) --- Defined in all entities. Set true for an entity for which a valid --- Convention, Import, or Export pragma has been given. Used to prevent --- more than one such pragma appearing for a given entity (RM B.1(45)). +-- Defined in all entities. Set for an entity for which a valid pragma +-- Convention, Import, or Export has been given. Used to prevent more +-- than one such pragma appearing for a given entity (RM B.1(45)). -- Has_Delayed_Aspects (Flag200) --- Defined in all entities. Set true if the Rep_Item chain for the entity --- has one or more N_Aspect_Definition nodes chained which are not to be +-- Defined in all entities. Set if the Rep_Item chain for the entity has +-- one or more N_Aspect_Definition nodes chained which are not to be -- evaluated till the freeze point. The aspect definition expression -- clause has been preanalyzed to get visibility at the point of use, -- but no other action has been taken. @@ -1531,18 +1531,18 @@ -- Convention_Intrinsic, Convention_Entry or Convention_Protected). -- Has_Forward_Instantiation (Flag175) --- Defined in package entities. Set true for packages that contain --- instantiations of local generic entities, before the corresponding --- generic body has been seen. If a package has a forward instantiation, --- we cannot inline subprograms appearing in the same package because --- the placement requirements of the instance will conflict with the --- linear elaboration of front-end inlining. +-- Defined in package entities. Set for packages that instantiate local +-- generic entities before the corresponding generic body has been seen. +-- If a package has a forward instantiation, we cannot inline subprograms +-- appearing in the same package because the placement requirements of +-- the instance will conflict with the linear elaboration of front-end +-- inlining. -- Has_Fully_Qualified_Name (Flag173) --- Defined in all entities. Set True if the name in the Chars field has --- been replaced by the fully qualified name, as used for debug output. --- See Exp_Dbug for a full description of the use of this flag and also --- the related flag Has_Qualified_Name. +-- Defined in all entities. Set if the name in the Chars field has been +-- replaced by the fully qualified name, as used for debug output. See +-- Exp_Dbug for a full description of the use of this flag and also the +-- related flag Has_Qualified_Name. -- Has_Gigi_Rep_Item (Flag82) -- Defined in all entities. Set if the rep item chain (referenced by @@ -1576,7 +1576,7 @@ -- applies (as set by coresponding pragma or aspect specification). -- Has_Inheritable_Invariants (Flag248) --- Defined in all type entities. Set True in private types from which one +-- Defined in all type entities. Set in private types from which one -- or more Invariant'Class aspects will be inherited if a another type is -- derived from the type (i.e. those types which have an Invariant'Class -- aspect, or which inherit one or more Invariant'Class aspects). Also @@ -1599,7 +1599,7 @@ -- Interrupt_Handler applies. -- Has_Invariants (Flag232) --- Defined in all type entities and in subprogram entities. Set True in +-- Defined in all type entities and in subprogram entities. Set in -- private types if an Invariant or Invariant'Class aspect applies to the -- type, or if the type inherits one or more Invariant'Class aspects. -- Also set in the corresponding full type. Note: if this flag is set @@ -1650,15 +1650,19 @@ -- Defined in package entities. True if the package is subject to a null -- Abstract_State aspect/pragma. +-- Has_Null_Refinement (Flag263) +-- Defined in E_Abstract_State entities. Set if the state has a null +-- refinement in aspect/pragma Refined_State. + -- Has_Object_Size_Clause (Flag172) -- Defined in entities for types and subtypes. Set if an Object_Size -- clause has been processed for the type Used to prevent multiple -- Object_Size clauses for a given entity. -- Has_Per_Object_Constraint (Flag154) --- Defined in E_Component entities, true if the subtype of the --- component has a per object constraint. Per object constraints result --- from the following situations: +-- Defined in E_Component entities. Set if the subtype of the component +-- has a per object constraint. Per object constraints result from the +-- following situations : -- -- 1. N_Attribute_Reference - when the prefix is the enclosing type and -- the attribute is Access. @@ -1770,27 +1774,27 @@ -- some ancestor is derived from a private type, making some components -- invisible and aggregates illegal. Used to check the legality of -- selected components and aggregates. The flag is set at the point of --- derivation. --- The legality of an aggregate of a type with a private ancestor must --- be checked because it also depends on the visibility at the point the --- aggregate is resolved. See sem_aggr.adb. This is part of AI05-0115. +-- derivation. The legality of an aggregate of a type with a private +-- ancestor must be checked because it also depends on the visibility +-- at the point the aggregate is resolved. See sem_aggr.adb. This is +-- part of AI05-0115. -- Has_Private_Declaration (Flag155) --- Defined in all entities. Returns True if it is the defining entity --- of a private type declaration or its corresponding full declaration. --- This flag is thus preserved when the full and the partial views are --- exchanged, to indicate if a full type declaration is a completion. --- Used for semantic checks in E.4(18) and elsewhere. +-- Defined in all entities. Set if it is the defining entity of a private +-- type declaration or its corresponding full declaration. This flag is +-- thus preserved when the full and the partial views are exchanged, to +-- indicate if a full type declaration is a completion. Used for semantic +-- checks in E.4(18) and elsewhere. -- Has_Qualified_Name (Flag161) --- Defined in all entities. Set True if the name in the Chars field --- has been replaced by its qualified name, as used for debug output. --- See Exp_Dbug for a full description of qualification requirements. --- For some entities, the name is the fully qualified name, but there --- are exceptions. In particular, for local variables in procedures, --- we do not include the procedure itself or higher scopes. See also --- the flag Has_Fully_Qualified_Name, which is set if the name does --- indeed include the fully qualified name. +-- Defined in all entities. Set if the name in the Chars field has +-- been replaced by its qualified name, as used for debug output. See +-- Exp_Dbug for a full description of qualification requirements. For +-- some entities, the name is the fully qualified name, but there are +-- exceptions. In particular, for local variables in procedures, we +-- do not include the procedure itself or higher scopes. See also the +-- flag Has_Fully_Qualified_Name, which is set if the name does indeed +-- include the fully qualified name. -- Has_RACW (Flag214) -- Defined in package spec entities. Set if the spec contains the @@ -2168,7 +2172,7 @@ -- Set if the type or subtype is constrained. -- Is_Constr_Subt_For_U_Nominal (Flag80) --- Defined in all types and subtypes. Set true only for the constructed +-- Defined in all types and subtypes. Set only for the constructed -- subtype of an object whose nominal subtype is unconstrained. Note -- that the constructed subtype itself will be constrained. @@ -2225,9 +2229,9 @@ -- entity is associated with a dispatch table. -- Is_Dispatching_Operation (Flag6) --- Defined in all entities. Set true for procedures, functions, --- generic procedures and generic functions if the corresponding --- operation is dispatching. +-- Defined in all entities. Set for procedures, functions, generic +-- procedures, and generic functions if the corresponding operation +-- is dispatching. -- Is_Dynamic_Scope (synthesized) -- Applies to all Entities. Returns True if the entity is a dynamic @@ -2253,9 +2257,9 @@ -- entities and False for all other entity kinds. -- Is_Entry_Formal (Flag52) --- Defined in all entities. Set only for entry formals (which can --- only be in, in-out or out parameters). This flag is used to speed --- up the test for the need to replace references in Exp_Ch2. +-- Defined in all entities. Set only for entry formals (which can only +-- be in, in-out or out parameters). This flag is used to speed up the +-- test for the need to replace references in Exp_Ch2. -- Is_Exported (Flag99) -- Defined in all entities. Set if the entity is exported. For now we @@ -2338,7 +2342,7 @@ -- convention. -- Is_Hidden (Flag57) --- Defined in all entities. Set true for all entities declared in the +-- Defined in all entities. Set for all entities declared in the -- private part or body of a package. Also marks generic formals of a -- formal package declared without a box. For library level entities, -- this flag is set if the entity is not publicly visible. This flag @@ -2348,7 +2352,7 @@ -- Private_Declaration in sem_ch7). -- Is_Hidden_Open_Scope (Flag171) --- Defined in all entities. Set true for a scope that contains the +-- Defined in all entities. Set for a scope that contains the -- instantiation of a child unit, and whose entities are not visible -- during analysis of the instance. @@ -2462,20 +2466,20 @@ -- to be defined) must be in the same scope as the type. -- Is_Known_Non_Null (Flag37) --- Defined in all entities. Relevant (and can be set True) only for +-- Defined in all entities. Relevant (and can be set) only for -- objects of an access type. It is set if the object is currently -- known to have a non-null value (meaning that no access checks -- are needed). The indication can for example come from assignment -- of an access parameter or an allocator whose value is known non-null. -- -- Note: this flag is set according to the sequential flow of the --- program, watching the current value of the variable. However, --- this processing can miss cases of changing the value of an aliased --- or constant object, so even if this flag is set, it should not --- be believed if the variable is aliased or volatile. It would --- be a little neater to avoid the flag being set in the first --- place in such cases, but that's trickier, and there is only --- one place that tests the value anyway. +-- program, watching the current value of the variable. However, this +-- processing can miss cases of changing the value of an aliased or +-- constant object, so even if this flag is set, it should not be +-- believed if the variable is aliased or volatile. It would be a +-- little neater to avoid the flag being set in the first place in +-- such cases, but that's trickier, and there is only one place that +-- tests the value anyway. -- -- The flag is dynamically set and reset as semantic analysis and -- expansion proceeds. Its value is meaningless once the tree is @@ -2483,7 +2487,7 @@ -- Thus this flag has no meaning to the back end. -- Is_Known_Null (Flag204) --- Defined in all entities. Relevant (and can be set True) only for +-- Defined in all entities. Relevant (and can be set ) only for -- objects of an access type. It is set if the object is currently known -- to have a null value (meaning that a dereference will surely raise -- constraint error exception). The indication can come from an @@ -2841,7 +2845,7 @@ -- Wide_Wide_Character). -- Is_Statically_Allocated (Flag28) --- Defined in all entities. This can only be set True for exception, +-- Defined in all entities. This can only be set for exception, -- variable, constant, and type/subtype entities. If the flag is set, -- then the variable or constant must be allocated statically rather -- than on the local stack frame. For exceptions, the meaning is that @@ -2951,7 +2955,7 @@ -- or Export_Valued_Procedure pragma applies to the procedure entity. -- Is_Visible_Formal (Flag206) --- Defined in all entities. Set True for instances of the formals of a +-- Defined in all entities. Set for instances of the formals of a -- formal package. Indicates that the entity must be made visible in the -- body of the instance, to reproduce the visibility of the generic. -- This simplifies visibility settings in instance bodies. @@ -3058,10 +3062,10 @@ -- Value attributes for the enumeration type in question. -- Low_Bound_Tested (Flag205) --- Defined in all entities. Currently this can only be set True for --- formal parameter entries of a standard unconstrained one-dimensional --- array or string type. Indicates that an explicit test of the low bound --- of the formal appeared in the code, e.g. in a pragma Assert. If this +-- Defined in all entities. Currently this can only be set for formal +-- parameter entries of a standard unconstrained one-dimensional array +-- or string type. Indicates that an explicit test of the low bound of +-- the formal appeared in the code, e.g. in a pragma Assert. If this -- flag is set, warnings about assuming the index low bound to be one -- are suppressed. @@ -3252,8 +3256,8 @@ -- the defining entity in the original declaration. -- Nonzero_Is_True (Flag162) [base type only] --- Defined in enumeration types. True if any non-zero value is to be --- interpreted as true. Currently this is set true for derived Boolean +-- Defined in enumeration types. Set if any non-zero value is to be +-- interpreted as true. Currently this is set for derived Boolean -- types which have a convention of C, C++ or Fortran. -- No_Pool_Assigned (Flag131) [root type only] @@ -3796,8 +3800,8 @@ -- Static_Predicate (List25) -- Defined in discrete types/subtypes with predicates (Has_Predicates --- set True). Set if the type/subtype has a static predicate. Points to --- a list of expression and N_Range nodes that represent the predicate +-- set). Set if the type/subtype has a static predicate. Points to a +-- list of expression and N_Range nodes that represent the predicate -- in canonical form. The canonical form has entries sorted in ascending -- order, with duplicates eliminated, and adjacent ranges coalesced, so -- that there is always a gap in the values between successive entries. @@ -5104,6 +5108,7 @@ -- E_Abstract_State -- Refinement_Constituents (Elist8) -- Refined_State (Node10) + -- Has_Null_Refinement (Flag263) -- Is_External_State (synth) -- Is_Input_Only_State (synth) -- Is_Null_State (synth) @@ -6344,6 +6349,7 @@ function Has_Missing_Return (Id : E) return B; function Has_Nested_Block_With_Handler (Id : E) return B; function Has_Non_Standard_Rep (Id : E) return B; + function Has_Null_Refinement (Id : E) return B; function Has_Object_Size_Clause (Id : E) return B; function Has_Per_Object_Constraint (Id : E) return B; function Has_Postconditions (Id : E) return B; @@ -6957,6 +6963,7 @@ procedure Set_Has_Missing_Return (Id : E; V : B := True); procedure Set_Has_Nested_Block_With_Handler (Id : E; V : B := True); procedure Set_Has_Non_Standard_Rep (Id : E; V : B := True); + procedure Set_Has_Null_Refinement (Id : E; V : B := True); procedure Set_Has_Object_Size_Clause (Id : E; V : B := True); procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True); procedure Set_Has_Postconditions (Id : E; V : B := True); @@ -7672,6 +7679,7 @@ pragma Inline (Has_Missing_Return); pragma Inline (Has_Nested_Block_With_Handler); pragma Inline (Has_Non_Standard_Rep); + pragma Inline (Has_Null_Refinement); pragma Inline (Has_Object_Size_Clause); pragma Inline (Has_Per_Object_Constraint); pragma Inline (Has_Postconditions); @@ -8132,6 +8140,7 @@ pragma Inline (Set_Has_Missing_Return); pragma Inline (Set_Has_Nested_Block_With_Handler); pragma Inline (Set_Has_Non_Standard_Rep); + pragma Inline (Set_Has_Null_Refinement); pragma Inline (Set_Has_Object_Size_Clause); pragma Inline (Set_Has_Per_Object_Constraint); pragma Inline (Set_Has_Postconditions); Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 203525) +++ sem_prag.adb (working copy) @@ -1600,11 +1600,14 @@ -- Start of processing for Analyze_Global_List begin + if Nkind (List) = N_Null then + null; + -- Single global item declaration - if Nkind_In (List, N_Expanded_Name, - N_Identifier, - N_Selected_Component) + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) then Analyze_Global_Item (List, Global_Mode); @@ -1691,7 +1694,7 @@ -- Local variables - List : Node_Id; + Items : Node_Id; Subp_Decl : Node_Id; Restore_Scope : Boolean := False; @@ -1704,11 +1707,11 @@ Subp_Decl := Find_Related_Subprogram (N); Subp_Id := Defining_Unit_Name (Specification (Subp_Decl)); - List := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Items := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); -- There is nothing to be done for a null global list - if Nkind (List) = N_Null then + if Nkind (Items) = N_Null then null; -- Analyze the various forms of global lists and items. Note that some @@ -1726,7 +1729,7 @@ Install_Formals (Subp_Id); end if; - Analyze_Global_List (List); + Analyze_Global_List (Items); if Restore_Scope then End_Scope; @@ -19358,6 +19361,10 @@ -- a state of mode Input, In_Out and Output respectively with a visible -- refinement. + Has_Null_State : Boolean := False; + -- This flag is set when the corresponding Global aspect/pragma has at + -- least one state with a null refinement. + In_Constits : Elist_Id := No_Elist; In_Out_Constits : Elist_Id := No_Elist; Out_Constits : Elist_Id := No_Elist; @@ -19512,7 +19519,7 @@ -- Ensure that one of the three coverage variants is satisfied if Ekind (Item_Id) = E_Abstract_State - and then Present (Refinement_Constituents (Item_Id)) + and then not Has_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -19595,7 +19602,7 @@ -- is of mode Input. if Ekind (Item_Id) = E_Abstract_State - and then Present (Refinement_Constituents (Item_Id)) + and then not Has_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -19665,7 +19672,7 @@ -- have mode Output. if Ekind (Item_Id) = E_Abstract_State - and then Present (Refinement_Constituents (Item_Id)) + and then not Has_Null_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -19881,11 +19888,14 @@ -- Start of processing for Check_Refined_Global_List begin + if Nkind (List) = N_Null then + null; + -- Single global item declaration - if Nkind_In (List, N_Expanded_Name, - N_Identifier, - N_Selected_Component) + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) then Check_Refined_Global_Item (List, Global_Mode); @@ -19963,17 +19973,20 @@ begin -- Signal that the global list contains at least one abstract - -- state with a visible refinement. + -- state with a visible refinement. Note that the refinement + -- may be null in which case there are no constituents. - if Ekind (Item_Id) = E_Abstract_State - and then Present (Refinement_Constituents (Item_Id)) - then - if Mode = Name_Input then - Has_In_State := True; - elsif Mode = Name_In_Out then - Has_In_Out_State := True; - elsif Mode = Name_Output then - Has_Out_State := True; + if Ekind (Item_Id) = E_Abstract_State then + if Has_Null_Refinement (Item_Id) then + Has_Null_State := True; + else + if Mode = Name_Input then + Has_In_State := True; + elsif Mode = Name_In_Out then + Has_In_Out_State := True; + elsif Mode = Name_Output then + Has_Out_State := True; + end if; end if; end if; @@ -19995,11 +20008,14 @@ -- Start of processing for Process_Global_List begin + if Nkind (List) = N_Null then + null; + -- Single global item declaration - if Nkind_In (List, N_Expanded_Name, - N_Identifier, - N_Selected_Component) + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) then Process_Global_Item (List, Mode); @@ -20148,11 +20164,13 @@ -- The corresponding Global aspect/pragma must mention at least one -- state with a visible refinement at the point Refined_Global is - -- processed. + -- processed. States with null refinements warrant a Refined_Global + -- aspect/pragma. if not Has_In_State and then not Has_In_Out_State and then not Has_Out_State + and then not Has_Null_State then Error_Msg_NE ("useless refinement, subprogram & does not mention abstract state " @@ -20161,13 +20179,15 @@ end if; -- The global refinement of inputs and outputs cannot be null when the - -- corresponding Global aspect/pragma contains at least one item. + -- corresponding Global aspect/pragma contains at least one item except + -- in the case where we have states with null refinements. if Nkind (List) = N_Null and then (Present (In_Items) or else Present (In_Out_Items) or else Present (Out_Items)) + and then not Has_Null_State then Error_Msg_NE ("refinement cannot be null, subprogram & has global items", @@ -20370,8 +20390,11 @@ Error_Msg_N ("cannot mix null and non-null constituents", Constit); + -- Mark the related state as having a null refinement + else Null_Seen := True; + Set_Has_Null_Refinement (State_Id); end if; -- Non-null constituents