This patch modifies the categorization of aspects Async_Readers, Async_Writers, Effective_Reads and Effective_Writes to no longer require delayed actions. This in turn ensures that the analysis of their aspect form correctly creates their pragma counterparts.
------------ -- Source -- ------------ -- illegal_externals.ads package Illegal_Externals with SPARK_Mode => On is type I is range 1 .. 10 with Async_Readers; type I2 is range 1 .. 10 with Async_Readers => True; type I3 is range 1 .. 10 with Async_Readers => False; type T1 is array (I) of Integer with Volatile; type T2 is array (I) of Integer with Volatile, Async_Readers => True, Async_Writers => False, Effective_Writes => False, Effective_Reads => False; subtype S1 is Integer range 1 .. 10 with Async_Readers; subtype S2 is Integer range 1 .. 10 with Async_Readers => True; subtype S3 is Integer range 1 .. 10 with Async_Readers => False; procedure P1 with Import, Convention => C; procedure P2 with Import, Async_Readers, Convention => C; end Illegal_Externals; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c illegal_externals.ads illegal_externals.ads:2:34: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:3:34: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:4:34: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:8:11: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:9:11: aspect "Async_Writers" must apply to a volatile object illegal_externals.ads:10:11: aspect "Effective_Writes" must apply to a volatile object illegal_externals.ads:11:11: aspect "Effective_Reads" must apply to a volatile object illegal_externals.ads:12:45: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:13:45: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:14:45: aspect "Async_Readers" must apply to a volatile object illegal_externals.ads:20:11: aspect "Async_Readers" must apply to a volatile object Tested on x86_64-pc-linux-gnu, committed on trunk 2014-07-30 Hristian Kirtchev <kirtc...@adacore.com> * aspects.ads Aspects Async_Readers, Async_Writers, Effective_Reads and Effective_Writes do not need to be delayed. * sem_ch13.adb (Analyze_Aspect_Specifications): Propagate the optional Boolean expression when generating the corresponding pragma for an external property aspect. * sem_prag.adb (Analyze_External_Property_In_Decl_Part): Remove local constant Obj. Add local constant Obj_Id. Reimplement the check which ensures that the related variable is in fact volatile. (Analyze_Pragma): Reimplement the analysis of external property pragmas. * sem_util.adb (Is_Enabled): New routine. (Variable_Has_Enabled_Property): Reimplement the detection of an enabled external property.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 213211) +++ sem_prag.adb (working copy) @@ -1834,29 +1834,28 @@ (N : Node_Id; Expr_Val : out Boolean) is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - Obj : constant Node_Id := Get_Pragma_Arg (Arg1); - Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1)); + Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); + Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1)); + Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1)); begin Error_Msg_Name_1 := Pragma_Name (N); - -- The Async / Effective pragmas must apply to a volatile object other - -- than a formal subprogram parameter (SPARK RM 7.1.3(2)). + -- An external property pragma must apply to a volatile object other + -- than a formal subprogram parameter (SPARK RM 7.1.3(2)). The check + -- is performed at the end of the declarative region due to a possible + -- out-of-order arrangement of pragmas: + -- + -- Obj : ...; + -- pragma Async_Readers (Obj); + -- pragma Volatile (Obj); - if Is_SPARK_Volatile_Object (Obj) then - if Is_Entity_Name (Obj) - and then Present (Entity (Obj)) - and then Is_Formal (Entity (Obj)) - then - SPARK_Msg_N ("external property % cannot apply to parameter", N); - end if; - else + if not Is_SPARK_Volatile (Obj_Id) then SPARK_Msg_N ("external property % must apply to a volatile object", N); end if; - -- Ensure that the expression (if present) is static Boolean. A missing + -- Ensure that the Boolean expression (if present) is static. A missing -- argument defaults the value to True (SPARK RM 7.1.2(5)). Expr_Val := True; @@ -1867,7 +1866,6 @@ if Is_OK_Static_Expression (Expr) then Expr_Val := Is_True (Expr_Value (Expr)); else - Error_Msg_Name_1 := Pragma_Name (N); SPARK_Msg_N ("expression of % must be static", Expr); end if; end if; @@ -11581,6 +11579,8 @@ Pragma_Effective_Writes => Async_Effective : declare Duplic : Node_Id; + Expr : Node_Id; + Obj : Node_Id; Obj_Id : Entity_Id; begin @@ -11589,48 +11589,47 @@ Check_At_Least_N_Arguments (1); Check_At_Most_N_Arguments (2); Check_Arg_Is_Local_Name (Arg1); + Error_Msg_Name_1 := Pname; - Arg1 := Get_Pragma_Arg (Arg1); + Obj := Get_Pragma_Arg (Arg1); + Expr := Get_Pragma_Arg (Arg2); -- Perform minimal verification to ensure that the argument is at -- least a variable. Subsequent finer grained checks will be done -- at the end of the declarative region the contains the pragma. - if Is_Entity_Name (Arg1) and then Present (Entity (Arg1)) then - Obj_Id := Entity (Get_Pragma_Arg (Arg1)); + if Is_Entity_Name (Obj) + and then Present (Entity (Obj)) + and then Ekind (Entity (Obj)) = E_Variable + then + Obj_Id := Entity (Obj); - -- It is not efficient to examine preceding statements in order - -- to detect duplicate pragmas as Boolean aspects may appear + -- Detect a duplicate pragma. Note that it is not efficient to + -- examine preceding statements as Boolean aspects may appear -- anywhere between the related object declaration and its -- freeze point. As an alternative, inspect the contents of the -- variable contract. - if Ekind (Obj_Id) = E_Variable then - Duplic := Get_Pragma (Obj_Id, Prag_Id); + Duplic := Get_Pragma (Obj_Id, Prag_Id); - if Present (Duplic) then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Duplic); - Error_Msg_N ("pragma % duplicates pragma declared #", N); + if Present (Duplic) then + Error_Msg_Sloc := Sloc (Duplic); + Error_Msg_N ("pragma % duplicates pragma declared #", N); - -- Chain the pragma on the contract for further processing. - -- This also aids in detecting duplicates. + -- No duplicate detected - else - Add_Contract_Item (N, Obj_Id); + else + if Present (Expr) then + Preanalyze_And_Resolve (Expr, Standard_Boolean); end if; - -- The minimum legality requirements have been met, do not - -- fall through to the error message. + -- Chain the pragma on the contract for further processing - return; + Add_Contract_Item (N, Obj_Id); end if; + else + Error_Pragma ("pragma % must apply to a volatile object"); end if; - - -- If we get here, then the pragma applies to a non-object - -- construct, issue a generic error (SPARK RM 7.1.3(2)). - - Error_Pragma ("pragma % must apply to a volatile object"); end Async_Effective; ------------------ Index: sem_util.adb =================================================================== --- sem_util.adb (revision 213236) +++ sem_util.adb (working copy) @@ -7423,10 +7423,11 @@ Property : Name_Id) return Boolean is function State_Has_Enabled_Property return Boolean; - -- Determine whether a state denoted by Item_Id has the property + -- Determine whether a state denoted by Item_Id has the property enabled function Variable_Has_Enabled_Property return Boolean; -- Determine whether a variable denoted by Item_Id has the property + -- enabled. -------------------------------- -- State_Has_Enabled_Property -- @@ -7528,6 +7529,44 @@ ----------------------------------- function Variable_Has_Enabled_Property return Boolean is + function Is_Enabled (Prag : Node_Id) return Boolean; + -- Determine whether property pragma Prag (if present) denotes an + -- enabled property. + + ---------------- + -- Is_Enabled -- + ---------------- + + function Is_Enabled (Prag : Node_Id) return Boolean is + Arg2 : Node_Id; + + begin + if Present (Prag) then + Arg2 := Next (First (Pragma_Argument_Associations (Prag))); + + -- The pragma has an optional Boolean expression, the related + -- property is enabled only when the expression evaluates to + -- True. + + if Present (Arg2) then + return Is_True (Expr_Value (Get_Pragma_Arg (Arg2))); + + -- Otherwise the lack of expression enables the property by + -- default. + + else + return True; + end if; + + -- The property was never set in the first place + + else + return False; + end if; + end Is_Enabled; + + -- Local variables + AR : constant Node_Id := Get_Pragma (Item_Id, Pragma_Async_Readers); AW : constant Node_Id := @@ -7536,6 +7575,9 @@ Get_Pragma (Item_Id, Pragma_Effective_Reads); EW : constant Node_Id := Get_Pragma (Item_Id, Pragma_Effective_Writes); + + -- Start of processing for Variable_Has_Enabled_Property + begin -- A non-volatile object can never possess external properties @@ -7544,35 +7586,27 @@ -- 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. + -- presence of a property pragma with an optional Boolean flag. The + -- property is enabled when the flag evaluates to True or the flag is + -- missing altogether. - elsif Property = Name_Async_Readers - and then - (Present (AR) - or else - (No (AW) and then No (ER) and then No (EW))) - then + elsif Property = Name_Async_Readers and then Is_Enabled (AR) 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 + elsif Property = Name_Async_Writers and then Is_Enabled (AW) 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 + elsif Property = Name_Effective_Reads and then Is_Enabled (ER) 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 + elsif Property = Name_Effective_Writes and then Is_Enabled (EW) then return True; + -- The implicit case lacks all property pragmas + + elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then + return True; + else return False; end if; Index: aspects.ads =================================================================== --- aspects.ads (revision 213201) +++ aspects.ads (working copy) @@ -590,8 +590,6 @@ (No_Aspect => Always_Delay, Aspect_Address => Always_Delay, Aspect_All_Calls_Remote => Always_Delay, - Aspect_Async_Readers => Always_Delay, - Aspect_Async_Writers => Always_Delay, Aspect_Asynchronous => Always_Delay, Aspect_Attach_Handler => Always_Delay, Aspect_Constant_Indexing => Always_Delay, @@ -604,8 +602,6 @@ Aspect_Discard_Names => Always_Delay, Aspect_Dispatching_Domain => Always_Delay, Aspect_Dynamic_Predicate => Always_Delay, - Aspect_Effective_Reads => Always_Delay, - Aspect_Effective_Writes => Always_Delay, Aspect_Elaborate_Body => Always_Delay, Aspect_External_Name => Always_Delay, Aspect_External_Tag => Always_Delay, @@ -673,9 +669,13 @@ Aspect_Abstract_State => Never_Delay, Aspect_Annotate => Never_Delay, + Aspect_Async_Readers => Never_Delay, + Aspect_Async_Writers => Never_Delay, Aspect_Convention => Never_Delay, Aspect_Dimension => Never_Delay, Aspect_Dimension_System => Never_Delay, + Aspect_Effective_Reads => Never_Delay, + Aspect_Effective_Writes => Never_Delay, Aspect_Part_Of => Never_Delay, Aspect_Refined_Post => Never_Delay, Aspect_SPARK_Mode => Never_Delay, Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 213201) +++ sem_ch13.adb (working copy) @@ -2905,10 +2905,46 @@ goto Continue; end if; + -- External property aspects are Boolean by nature, but + -- their pragmas must contain two arguments, the second + -- being the optional Boolean expression. + + if A_Id = Aspect_Async_Readers + or else A_Id = Aspect_Async_Writers + or else A_Id = Aspect_Effective_Reads + or else A_Id = Aspect_Effective_Writes + then + declare + Args : List_Id; + + begin + -- The first argument of the external property pragma + -- is the related object. + + Args := New_List ( + Make_Pragma_Argument_Association (Sloc (Ent), + Expression => Ent)); + + -- The second argument is the optional Boolean + -- expression which must be propagated even if it + -- evaluates to False as this has special semantic + -- meaning. + + if Present (Expr) then + Append_To (Args, + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))); + end if; + + Make_Aitem_Pragma + (Pragma_Argument_Associations => Args, + Pragma_Name => Nam); + end; + -- Cases where we do not delay, includes all cases where -- the expression is missing other than the above cases. - if not Delay_Required or else No (Expr) then + elsif not Delay_Required or else No (Expr) then Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Sloc (Ent), @@ -2918,7 +2954,7 @@ -- In general cases, the corresponding pragma/attribute -- definition clause will be inserted later at the freezing - -- point, and we do not need to build it now + -- point, and we do not need to build it now. else Aitem := Empty;