===================================================================
@@ -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;
------------------
===================================================================
@@ -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;
===================================================================
@@ -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,
===================================================================
@@ -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;
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 <kirtchev@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.