This patch corrects the trigger which determines the proper context of a volatile object with enabled property Async_Writers or Effective_Reads.
------------ -- Source -- ------------ -- assert_exprs.ads package Assert_Exprs with SPARK_Mode is type T is new Integer with Volatile; procedure Error (Input : T; Output : out T) with Pre => Input > 1, Post => Output = Input * 2; end Assert_Exprs; -- assert_exprs.adb package body Assert_Exprs with SPARK_Mode is procedure Error (Input : T; Output : out T) is begin Output := Input * 2; end Error; end Assert_Exprs; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnata assert_exprs.adb assert_exprs.adb:4:17: volatile object cannot appear in this context (SPARK RM 7.1.3(13)) assert_exprs.ads:5:19: volatile object cannot appear in this context (SPARK RM 7.1.3(13)) assert_exprs.ads:6:19: volatile object cannot appear in this context (SPARK RM 7.1.3(13)) assert_exprs.ads:6:28: volatile object cannot appear in this context (SPARK RM 7.1.3(13)) Tested on x86_64-pc-linux-gnu, committed on trunk 2014-05-21 Hristian Kirtchev <kirtc...@adacore.com> * 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.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 210705) +++ sem_ch3.adb (working copy) @@ -2988,7 +2988,7 @@ -- 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 @@ -- 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 @@ -- 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 @@ -- (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; Index: sem_ch5.adb =================================================================== --- sem_ch5.adb (revision 210707) +++ sem_ch5.adb (working copy) @@ -1986,7 +1986,7 @@ 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 @@ -- 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; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 210702) +++ sem_prag.adb (working copy) @@ -2038,9 +2038,8 @@ -- 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)). Index: freeze.adb =================================================================== --- freeze.adb (revision 210697) +++ freeze.adb (working copy) @@ -3318,7 +3318,7 @@ -- 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 @@ 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 Index: sem_util.adb =================================================================== --- sem_util.adb (revision 210701) +++ sem_util.adb (working copy) @@ -7466,7 +7466,7 @@ 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 @@ -- 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 @@ 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)); + if Is_Entity_Name (N) then + return Is_SPARK_Volatile (Entity (N)); - elsif Is_Entity_Name (N) then - return - Is_SPARK_Volatile_Object (Entity (N)) - or else Is_Volatile (Etype (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)); Index: sem_util.ads =================================================================== --- sem_util.ads (revision 210697) +++ sem_util.ads (working copy) @@ -1302,10 +1302,15 @@ 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. Index: sem_res.adb =================================================================== --- sem_res.adb (revision 210697) +++ sem_res.adb (working copy) @@ -6579,8 +6579,9 @@ -- 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)) Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 210705) +++ sem_ch6.adb (working copy) @@ -11511,23 +11511,35 @@ -- 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 - Error_Msg_N - ("function cannot have parameter of mode `OUT` or `IN OUT`", - Formal); + -- A function cannot have a parameter of mode IN OUT or OUT + -- (SPARK RM 6.1). - -- A function cannot have a volatile formal parameter - -- (SPARK RM 7.1.3(10)). + 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); - elsif Is_SPARK_Volatile_Object (Formal) then + -- 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 a volatile formal parameter", Formal); + ("formal parameter of mode `IN` cannot be volatile", Formal); end if; end if;