This patch corrects the predicate which determines whether an object has an enabled external property to account for implicitly enabled properties.
Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-24 Hristian Kirtchev <kirtc...@adacore.com> * sem_prag.adb (Analyze_Global_Item): Move the check concerning the use of volatile objects as global items in a function to the variable related checks section. * sem_util.adb (Async_Readers_Enabled): Directly call Has_Enabled_Property. (Async_Writers_Enabled): Directly call Has_Enabled_Property. (Effective_Reads_Enabled): Directly call Has_Enabled_Property. (Effective_Writes_Enabled): Directly call Has_Enabled_Property. (Has_Enabled_Property): Rename formal parameter State_Id to Item_Id. Update the comment on usage. State_Has_Enabled_Property how handles the original logic of the routine. Add processing for variables. (State_Has_Enabled_Property): New routine. (Variable_Has_Enabled_Property): New routine.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 208076) +++ sem_prag.adb (working copy) @@ -2060,16 +2060,28 @@ -- Variable related checks - else + elsif Is_SPARK_Volatile_Object (Item_Id) then + + -- A volatile object cannot appear as a global item of a + -- function. This check is only relevant when SPARK_Mode is + -- on as it is not a standard Ada legality rule. + + if SPARK_Mode = On + and then Ekind_In (Spec_Id, E_Function, E_Generic_Function) + then + Error_Msg_NE + ("volatile object & cannot act as global item of a " + & "function (SPARK RM 7.1.3(9))", Item, Item_Id); + return; + -- A volatile object with property Effective_Reads set to -- True must have mode Output or In_Out. - if Is_SPARK_Volatile_Object (Item_Id) - and then Effective_Reads_Enabled (Item_Id) + elsif Effective_Reads_Enabled (Item_Id) and then Global_Mode = Name_Input then Error_Msg_NE - ("volatile item & with property Effective_Reads must " + ("volatile object & with property Effective_Reads must " & "have mode In_Out or Output (SPARK RM 7.1.3(11))", Item, Item_Id); return; @@ -2100,19 +2112,6 @@ Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id); end if; - -- A volatile object cannot appear as a global item of a function. - -- This check is only relevant when SPARK_Mode is on as it is not - -- a standard Ada legality rule. - - if SPARK_Mode = On - and then Is_SPARK_Volatile_Object (Item) - and then Ekind_In (Spec_Id, E_Function, E_Generic_Function) - then - Error_Msg_NE - ("volatile object & cannot act as global item of a function " - & "(SPARK RM 7.1.3(9))", Item, Item_Id); - end if; - -- The same entity might be referenced through various way. Check -- the entity of the item rather than the item itself. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 208067) +++ sem_util.adb (working copy) @@ -116,11 +116,11 @@ -- have a default. function Has_Enabled_Property - (State_Id : Node_Id; + (Item_Id : Entity_Id; Property : Name_Id) return Boolean; -- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled. - -- Determine whether an abstract state denoted by its entity State_Id has - -- enabled property Property. + -- Determine whether an abstract state or a variable denoted by entity + -- Item_Id has enabled property Property. function Has_Null_Extension (T : Entity_Id) return Boolean; -- T is a derived tagged type. Check whether the type extension is null. @@ -575,12 +575,7 @@ function Async_Readers_Enabled (Id : Entity_Id) return Boolean is begin - if Ekind (Id) = E_Abstract_State then - return Has_Enabled_Property (Id, Name_Async_Readers); - - else pragma Assert (Ekind (Id) = E_Variable); - return Present (Get_Pragma (Id, Pragma_Async_Readers)); - end if; + return Has_Enabled_Property (Id, Name_Async_Readers); end Async_Readers_Enabled; --------------------------- @@ -589,12 +584,7 @@ function Async_Writers_Enabled (Id : Entity_Id) return Boolean is begin - if Ekind (Id) = E_Abstract_State then - return Has_Enabled_Property (Id, Name_Async_Writers); - - else pragma Assert (Ekind (Id) = E_Variable); - return Present (Get_Pragma (Id, Pragma_Async_Writers)); - end if; + return Has_Enabled_Property (Id, Name_Async_Writers); end Async_Writers_Enabled; -------------------------------------- @@ -4737,12 +4727,7 @@ function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is begin - if Ekind (Id) = E_Abstract_State then - return Has_Enabled_Property (Id, Name_Effective_Reads); - - else pragma Assert (Ekind (Id) = E_Variable); - return Present (Get_Pragma (Id, Pragma_Effective_Reads)); - end if; + return Has_Enabled_Property (Id, Name_Effective_Reads); end Effective_Reads_Enabled; ------------------------------ @@ -4751,12 +4736,7 @@ function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is begin - if Ekind (Id) = E_Abstract_State then - return Has_Enabled_Property (Id, Name_Effective_Writes); - - else pragma Assert (Ekind (Id) = E_Variable); - return Present (Get_Pragma (Id, Pragma_Effective_Writes)); - end if; + return Has_Enabled_Property (Id, Name_Effective_Writes); end Effective_Writes_Enabled; ------------------------------ @@ -7292,89 +7272,173 @@ -------------------------- function Has_Enabled_Property - (State_Id : Node_Id; + (Item_Id : Entity_Id; Property : Name_Id) return Boolean is - Decl : constant Node_Id := Parent (State_Id); - Opt : Node_Id; - Opt_Nam : Node_Id; - Prop : Node_Id; - Prop_Nam : Node_Id; - Props : Node_Id; + function State_Has_Enabled_Property return Boolean; + -- Determine whether a state denoted by Item_Id has the property - begin - -- The declaration of an external abstract state appears as an extension - -- aggregate. If this is not the case, properties can never be set. + function Variable_Has_Enabled_Property return Boolean; + -- Determine whether a variable denoted by Item_Id has the property - if Nkind (Decl) /= N_Extension_Aggregate then - return False; - end if; + -------------------------------- + -- State_Has_Enabled_Property -- + -------------------------------- - -- When External appears as a simple option, it automatically enables - -- all properties. + function State_Has_Enabled_Property return Boolean is + Decl : constant Node_Id := Parent (Item_Id); + Opt : Node_Id; + Opt_Nam : Node_Id; + Prop : Node_Id; + Prop_Nam : Node_Id; + Props : Node_Id; - Opt := First (Expressions (Decl)); - while Present (Opt) loop - if Nkind (Opt) = N_Identifier - and then Chars (Opt) = Name_External - then - return True; + begin + -- The declaration of an external abstract state appears as an + -- extension aggregate. If this is not the case, properties can never + -- be set. + + if Nkind (Decl) /= N_Extension_Aggregate then + return False; end if; - Next (Opt); - end loop; + -- When External appears as a simple option, it automatically enables + -- all properties. - -- When External specifies particular properties, inspect those and - -- find the desired one (if any). + Opt := First (Expressions (Decl)); + while Present (Opt) loop + if Nkind (Opt) = N_Identifier + and then Chars (Opt) = Name_External + then + return True; + end if; - Opt := First (Component_Associations (Decl)); - while Present (Opt) loop - Opt_Nam := First (Choices (Opt)); + Next (Opt); + end loop; - if Nkind (Opt_Nam) = N_Identifier - and then Chars (Opt_Nam) = Name_External - then - Props := Expression (Opt); + -- When External specifies particular properties, inspect those and + -- find the desired one (if any). - -- Multiple properties appear as an aggregate + Opt := First (Component_Associations (Decl)); + while Present (Opt) loop + Opt_Nam := First (Choices (Opt)); - if Nkind (Props) = N_Aggregate then + if Nkind (Opt_Nam) = N_Identifier + and then Chars (Opt_Nam) = Name_External + then + Props := Expression (Opt); - -- Simple property form + -- Multiple properties appear as an aggregate - Prop := First (Expressions (Props)); - while Present (Prop) loop - if Chars (Prop) = Property then - return True; - end if; + if Nkind (Props) = N_Aggregate then - Next (Prop); - end loop; + -- Simple property form - -- Property with expression form + Prop := First (Expressions (Props)); + while Present (Prop) loop + if Chars (Prop) = Property then + return True; + end if; - Prop := First (Component_Associations (Props)); - while Present (Prop) loop - Prop_Nam := First (Choices (Prop)); + Next (Prop); + end loop; - if Chars (Prop_Nam) = Property then - return Is_True (Expr_Value (Expression (Prop))); - end if; + -- Property with expression form - Next (Prop); - end loop; + Prop := First (Component_Associations (Props)); + while Present (Prop) loop + Prop_Nam := First (Choices (Prop)); - -- Single property + if Chars (Prop_Nam) = Property then + return Is_True (Expr_Value (Expression (Prop))); + end if; - else - return Chars (Props) = Property; + Next (Prop); + end loop; + + -- Single property + + else + return Chars (Props) = Property; + end if; end if; + + Next (Opt); + end loop; + + return False; + end State_Has_Enabled_Property; + + ----------------------------------- + -- Variable_Has_Enabled_Property -- + ----------------------------------- + + function Variable_Has_Enabled_Property return Boolean is + AR : constant Node_Id := + Get_Pragma (Item_Id, Pragma_Async_Readers); + AW : constant Node_Id := + Get_Pragma (Item_Id, Pragma_Async_Writers); + ER : constant Node_Id := + Get_Pragma (Item_Id, Pragma_Effective_Reads); + EW : constant Node_Id := + Get_Pragma (Item_Id, Pragma_Effective_Writes); + begin + -- A non-volatile object can never possess external properties + + if not Is_SPARK_Volatile_Object (Item_Id) then + return False; + + -- External properties related to variables come in two flavors - + -- explicit and implicit. The explicit case is characterized by the + -- presence of a property pragma while the implicit case lacks all + -- such pragmas. + + elsif Property = Name_Async_Readers + and then + (Present (AR) + or else + (No (AW) and then No (ER) and then No (EW))) + then + return True; + + elsif Property = Name_Async_Writers + and then + (Present (AW) + or else + (No (AR) and then No (ER) and then No (EW))) + then + return True; + + elsif Property = Name_Effective_Reads + and then + (Present (ER) + or else + (No (AR) and then No (AW) and then No (EW))) + then + return True; + + elsif Property = Name_Effective_Writes + and then + (Present (EW) + or else + (No (AR) and then No (AW) and then No (ER))) + then + return True; + + else + return False; end if; + end Variable_Has_Enabled_Property; - Next (Opt); - end loop; + -- Start of processing for Has_Enabled_Property - return False; + begin + if Ekind (Item_Id) = E_Abstract_State then + return State_Has_Enabled_Property; + + else pragma Assert (Ekind (Item_Id) = E_Variable); + return Variable_Has_Enabled_Property; + end if; end Has_Enabled_Property; --------------------