From ea26c8e414ff21cc2dccf2a65476931c636c8147 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Wed, 21 May 2014 13:21:38 +0000 Subject: [PATCH] freeze.adb (Freeze_Record_Type): Update the use of Is_SPARK_Volatile. 2014-05-21 Hristian Kirtchev * freeze.adb (Freeze_Record_Type): Update the use of Is_SPARK_Volatile. * sem_ch3.adb (Analyze_Object_Contract): Update the use of Is_SPARK_Volatile. (Process_Discriminants): Update the use of Is_SPARK_Volatile. * sem_ch5.adb (Analyze_Iterator_Specification): Update the use of Is_SPARK_Volatile. (Analyze_Loop_Parameter_Specification): Update the use of Is_SPARK_Volatile. * sem_ch6.adb (Process_Formals): Catch an illegal use of an IN formal parameter when its type is volatile. * sem_prag.adb (Analyze_Global_Item): Update the use of Is_SPARK_Volatile. * sem_res.adb (Resolve_Entity_Name): Correct the guard which determines whether an entity is a volatile source SPARK object. * sem_util.adb (Has_Enabled_Property): Accout for external properties being set on objects other than abstract states and variables. An example would be a formal parameter. (Is_SPARK_Volatile): New routine. (Is_SPARK_Volatile_Object): Remove the entity-specific tests. Call routine Is_SPARK_Volatile when checking entities and/or types. * sem_util.ads (Is_SPARK_Volatile): New routine. From-SVN: r210708 --- gcc/ada/ChangeLog | 26 ++++++++++++++++++++++++++ gcc/ada/freeze.adb | 4 ++-- gcc/ada/sem_ch3.adb | 8 ++++---- gcc/ada/sem_ch5.adb | 4 ++-- gcc/ada/sem_ch6.adb | 42 +++++++++++++++++++++++++++--------------- gcc/ada/sem_prag.adb | 5 ++--- gcc/ada/sem_res.adb | 5 +++-- gcc/ada/sem_util.adb | 32 ++++++++++++++++++++++---------- gcc/ada/sem_util.ads | 7 ++++++- 9 files changed, 94 insertions(+), 39 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 26df7be2dc12..dd5f7e1f42ca 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,29 @@ +2014-05-21 Hristian Kirtchev + + * freeze.adb (Freeze_Record_Type): Update the use of + Is_SPARK_Volatile. + * sem_ch3.adb (Analyze_Object_Contract): Update the use of + Is_SPARK_Volatile. + (Process_Discriminants): Update the use of Is_SPARK_Volatile. + * sem_ch5.adb (Analyze_Iterator_Specification): Update the use + of Is_SPARK_Volatile. + (Analyze_Loop_Parameter_Specification): + Update the use of Is_SPARK_Volatile. + * sem_ch6.adb (Process_Formals): Catch an illegal use of an IN + formal parameter when its type is volatile. + * sem_prag.adb (Analyze_Global_Item): Update the use of + Is_SPARK_Volatile. + * sem_res.adb (Resolve_Entity_Name): Correct the guard which + determines whether an entity is a volatile source SPARK object. + * sem_util.adb (Has_Enabled_Property): Accout for external + properties being set on objects other than abstract states + and variables. An example would be a formal parameter. + (Is_SPARK_Volatile): New routine. + (Is_SPARK_Volatile_Object): + Remove the entity-specific tests. Call routine Is_SPARK_Volatile + when checking entities and/or types. + * sem_util.ads (Is_SPARK_Volatile): New routine. + 2014-05-21 Robert Dewar * sem_warn.adb: Minor fix to warning messages (use ?? instead diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 6a382b9e7dcf..e48cb9fb5422 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -3318,7 +3318,7 @@ package body Freeze is -- they are not standard Ada legality rules. if SPARK_Mode = On then - if Is_SPARK_Volatile_Object (Rec) then + if Is_SPARK_Volatile (Rec) then -- A discriminated type cannot be volatile (SPARK RM C.6(4)) @@ -3340,7 +3340,7 @@ package body Freeze is Comp := First_Component (Rec); while Present (Comp) loop if Comes_From_Source (Comp) - and then Is_SPARK_Volatile_Object (Comp) + and then Is_SPARK_Volatile (Comp) then Error_Msg_Name_1 := Chars (Rec); Error_Msg_N diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 5db4bb763135..293a3f695cdb 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2988,7 +2988,7 @@ package body Sem_Ch3 is -- actuals in instantiations (SPARK RM 7.1.3(6)). if SPARK_Mode = On - and then Is_SPARK_Volatile_Object (Obj_Id) + and then Is_SPARK_Volatile (Obj_Id) and then No (Corresponding_Generic_Association (Parent (Obj_Id))) then Error_Msg_N ("constant cannot be volatile", Obj_Id); @@ -3000,7 +3000,7 @@ package body Sem_Ch3 is -- they are not standard Ada legality rules. if SPARK_Mode = On then - if Is_SPARK_Volatile_Object (Obj_Id) then + if Is_SPARK_Volatile (Obj_Id) then -- The declaration of a volatile object must appear at the -- library level (SPARK RM 7.1.3(7), C.6(6)). @@ -3030,7 +3030,7 @@ package body Sem_Ch3 is -- A non-volatile object cannot have volatile components -- (SPARK RM 7.1.3(7)). - if not Is_SPARK_Volatile_Object (Obj_Id) + if not Is_SPARK_Volatile (Obj_Id) and then Has_Volatile_Component (Obj_Typ) then Error_Msg_N @@ -18051,7 +18051,7 @@ package body Sem_Ch3 is -- (SPARK RM 7.1.3(6)). if SPARK_Mode = On - and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr)) + and then Is_SPARK_Volatile (Defining_Identifier (Discr)) then Error_Msg_N ("discriminant cannot be volatile", Discr); end if; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 5f14622a29c8..60080ed3d864 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1986,7 +1986,7 @@ package body Sem_Ch5 is if SPARK_Mode = On and then not Of_Present (N) - and then Is_SPARK_Volatile_Object (Ent) + and then Is_SPARK_Volatile (Ent) then Error_Msg_N ("loop parameter cannot be volatile", Ent); end if; @@ -2706,7 +2706,7 @@ package body Sem_Ch5 is -- when SPARK_Mode is on as it is not a standard Ada legality check -- (SPARK RM 7.1.3(6)). - if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then + if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then Error_Msg_N ("loop parameter cannot be volatile", Id); end if; end Analyze_Loop_Parameter_Specification; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 5305b31d5fee..01187831fe15 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -11511,23 +11511,35 @@ package body Sem_Ch6 is -- The following checks are relevant when SPARK_Mode is on as these -- are not standard Ada legality rules. - if SPARK_Mode = On - and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function) - then - -- A function cannot have a parameter of mode IN OUT or OUT - -- (SPARK RM 6.1). + if SPARK_Mode = On then + if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then - if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then + -- A function cannot have a parameter of mode IN OUT or OUT + -- (SPARK RM 6.1). + + if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then + Error_Msg_N + ("function cannot have parameter of mode `OUT` or " + & "`IN OUT`", Formal); + + -- A function cannot have a volatile formal parameter + -- (SPARK RM 7.1.3(10)). + + elsif Is_SPARK_Volatile (Formal) then + Error_Msg_N + ("function cannot have a volatile formal parameter", + Formal); + end if; + + -- A procedure cannot have a formal parameter of mode IN because + -- it behaves as a constant (SPARK RM 7.1.3(6)). + + elsif Ekind (Scope (Formal)) = E_Procedure + and then Ekind (Formal) = E_In_Parameter + and then Is_SPARK_Volatile (Formal) + then Error_Msg_N - ("function cannot have parameter of mode `OUT` or `IN OUT`", - Formal); - - -- A function cannot have a volatile formal parameter - -- (SPARK RM 7.1.3(10)). - - elsif Is_SPARK_Volatile_Object (Formal) then - Error_Msg_N - ("function cannot have a volatile formal parameter", Formal); + ("formal parameter of mode `IN` cannot be volatile", Formal); end if; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 416eb047f843..62caba6abc48 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2038,9 +2038,8 @@ package body Sem_Prag is -- SPARK_Mode is on as they are not standard Ada legality -- rules. - elsif SPARK_Mode = On - and then Is_SPARK_Volatile_Object (Item_Id) - then + elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then + -- A volatile object cannot appear as a global item of a -- function (SPARK RM 7.1.3(9)). diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 50b7f4843b8f..2273fe873fc4 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6579,8 +6579,9 @@ package body Sem_Res is -- standard Ada legality rules. if SPARK_Mode = On - and then Ekind_In (E, E_Abstract_State, E_Variable) - and then Is_SPARK_Volatile_Object (E) + and then Is_Object (E) + and then Is_SPARK_Volatile (E) + and then Comes_From_Source (E) and then (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E)) diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 18a2472d543d..29de16bdcd5c 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7466,7 +7466,7 @@ package body Sem_Util is begin -- A non-volatile object can never possess external properties - if not Is_SPARK_Volatile_Object (Item_Id) then + if not Is_SPARK_Volatile (Item_Id) then return False; -- External properties related to variables come in two flavors - @@ -7514,11 +7514,19 @@ package body Sem_Util is -- Start of processing for Has_Enabled_Property begin + -- Abstract states and variables have a flexible scheme of specifying + -- external properties. + if Ekind (Item_Id) = E_Abstract_State then return State_Has_Enabled_Property; - else pragma Assert (Ekind (Item_Id) = E_Variable); + elsif Ekind (Item_Id) = E_Variable then return Variable_Has_Enabled_Property; + + -- Otherwise a property is enabled when the related object is volatile + + else + return Is_SPARK_Volatile (Item_Id); end if; end Has_Enabled_Property; @@ -11413,22 +11421,26 @@ package body Sem_Util is end if; end Is_SPARK_Object_Reference; + ----------------------- + -- Is_SPARK_Volatile -- + ----------------------- + + function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is + begin + return Is_Volatile (Id) or else Is_Volatile (Etype (Id)); + end Is_SPARK_Volatile; + ------------------------------ -- Is_SPARK_Volatile_Object -- ------------------------------ function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is begin - if Nkind (N) = N_Defining_Identifier then - return Is_Volatile (N) or else Is_Volatile (Etype (N)); - - elsif Is_Entity_Name (N) then - return - Is_SPARK_Volatile_Object (Entity (N)) - or else Is_Volatile (Etype (N)); + if Is_Entity_Name (N) then + return Is_SPARK_Volatile (Entity (N)); elsif Nkind (N) = N_Expanded_Name then - return Is_SPARK_Volatile_Object (Entity (N)); + return Is_SPARK_Volatile (Entity (N)); elsif Nkind (N) = N_Indexed_Component then return Is_SPARK_Volatile_Object (Prefix (N)); diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 13fe68897f62..8629d767d2b9 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1302,10 +1302,15 @@ package Sem_Util is function Is_SPARK_Object_Reference (N : Node_Id) return Boolean; -- Determines if the tree referenced by N represents an object in SPARK + function Is_SPARK_Volatile (Id : Entity_Id) return Boolean; + -- This routine is similar to predicate Is_Volatile, but it takes SPARK + -- semantics into account. In SPARK volatile components to not render a + -- type volatile. + function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean; -- Determine whether an arbitrary node denotes a volatile object reference -- according to the semantics of SPARK. To qualify as volatile, an object - -- must be subject to aspect/pragma Volatile or Atomic or have a [sub]type + -- must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type -- subject to the same attributes. Note that volatile components do not -- render an object volatile.