Implement new rule SPARK RM 7.1.2(16) that only assigns the Async_Readers and
Async_Writers flavors of volatility to protected objects by default, and makes
protected objects inherit the Effective_Reads and Effective_Writes flavors of
volatility from their Part_Of components.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-01-23 Yannick Moy <m...@adacore.com>
* sem_util.adb (Has_Enabled_Property): Treat
protected objects and variables differently from other variables.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 244778)
+++ sem_util.adb (working copy)
@@ -9118,6 +9118,10 @@
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean
is
+ function Protected_Object_Has_Enabled_Property return Boolean;
+ -- Determine whether a protected object denoted by Item_Id has the
+ -- property enabled.
+
function State_Has_Enabled_Property return Boolean;
-- Determine whether a state denoted by Item_Id has the property enabled
@@ -9125,6 +9129,44 @@
-- Determine whether a variable denoted by Item_Id has the property
-- enabled.
+ -------------------------------------------
+ -- Protected_Object_Has_Enabled_Property --
+ -------------------------------------------
+
+ function Protected_Object_Has_Enabled_Property return Boolean is
+ Constits : constant Elist_Id := Part_Of_Constituents (Item_Id);
+ Constit_Elmt : Elmt_Id;
+ Constit_Id : Entity_Id;
+
+ begin
+ -- Protected objects always have the properties Async_Readers and
+ -- Async_Writers. (SPARK RM 7.1.2(16))
+
+ if Property = Name_Async_Readers
+ or else Property = Name_Async_Writers
+ then
+ return True;
+
+ -- Protected objects that have Part_Of components also inherit
+ -- their properties Effective_Reads and Effective_Writes. (SPARK
+ -- RM 7.1.2(16))
+
+ elsif Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
+
+ if Has_Enabled_Property (Constit_Id, Property) then
+ return True;
+ end if;
+
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Protected_Object_Has_Enabled_Property;
+
--------------------------------
-- State_Has_Enabled_Property --
--------------------------------
@@ -9302,8 +9344,20 @@
-- 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;
+ -- A variable of a protected type only has the properties
+ -- Async_Readers and Async_Writers. It cannot have Part_Of
+ -- components (only protected objects can), hence it cannot
+ -- inherit their properties Effective_Reads and Effective_Writes.
+ -- (SPARK RM 7.1.2(16))
+
+ if Is_Protected_Type (Etype (Item_Id)) then
+ return Property = Name_Async_Readers
+ or else Property = Name_Async_Writers;
+ else
+ return True;
+ end if;
+
else
return False;
end if;
@@ -9321,6 +9375,14 @@
elsif Ekind (Item_Id) = E_Variable then
return Variable_Has_Enabled_Property;
+ -- By default, protected objects only have the properties Async_Readers
+ -- and Async_Writers. If they have Part_Of components, they also inherit
+ -- their properties Effective_Reads and Effective_Writes. (SPARK RM
+ -- 7.1.2(16))
+
+ elsif Ekind (Item_Id) = E_Protected_Object then
+ return Protected_Object_Has_Enabled_Property;
+
-- Otherwise a property is enabled when the related item is effectively
-- volatile.
