diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 33 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 232 |
3 files changed, 180 insertions, 101 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f4208df878e..97636e9a7f5 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,19 @@ +2014-02-24 Hristian Kirtchev <kirtchev@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. + 2014-02-24 Robert Dewar <dewar@adacore.com> * sinfo.ads, sem_ch12.adb, sem_res.adb, sem_ch4.adb, par-ch12.adb: diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 2b24d507f81..ba462275685 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2060,16 +2060,28 @@ package body Sem_Prag is -- 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 @@ package body Sem_Prag is 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. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 6b94f5a514e..3f872161fdf 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -116,11 +116,11 @@ package body Sem_Util is -- 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 @@ package body Sem_Util is 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 @@ package body Sem_Util is 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 @@ package body Sem_Util is 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 @@ package body Sem_Util is 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 @@ package body Sem_Util is -------------------------- 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. + + Opt := First (Expressions (Decl)); + while Present (Opt) loop + if Nkind (Opt) = N_Identifier + and then Chars (Opt) = Name_External + then + return True; + end if; - -- When External specifies particular properties, inspect those and - -- find the desired one (if any). + Next (Opt); + end loop; - Opt := First (Component_Associations (Decl)); - while Present (Opt) loop - Opt_Nam := First (Choices (Opt)); + -- When External specifies particular properties, inspect those and + -- find the desired one (if any). - if Nkind (Opt_Nam) = N_Identifier - and then Chars (Opt_Nam) = Name_External - then - Props := Expression (Opt); + Opt := First (Component_Associations (Decl)); + while Present (Opt) loop + Opt_Nam := First (Choices (Opt)); - -- Multiple properties appear as an aggregate + if Nkind (Opt_Nam) = N_Identifier + and then Chars (Opt_Nam) = Name_External + then + Props := Expression (Opt); - if Nkind (Props) = N_Aggregate then + -- Multiple properties appear as an aggregate - -- Simple property form + if Nkind (Props) = N_Aggregate then - Prop := First (Expressions (Props)); - while Present (Prop) loop - if Chars (Prop) = Property then - return True; - end if; + -- Simple property form - Next (Prop); - end loop; + Prop := First (Expressions (Props)); + while Present (Prop) loop + if Chars (Prop) = Property then + return True; + end if; - -- Property with expression form + Next (Prop); + end loop; - Prop := First (Component_Associations (Props)); - while Present (Prop) loop - Prop_Nam := First (Choices (Prop)); + -- Property with expression form - if Chars (Prop_Nam) = Property then - return Is_True (Expr_Value (Expression (Prop))); - 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; - -- Single property + Next (Prop); + end loop; - else - return Chars (Props) = Property; + -- 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; -------------------- |
