@@ -8083,8 +8083,14 @@ package body Einfo is
function Is_External_State (Id : E) return B is
begin
+ -- To qualify, the abstract state must appear with option "external" or
+ -- "synchronous" (SPARK RM 7.1.4(8) and (10)).
+
return
- Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_External);
+ Ekind (Id) = E_Abstract_State
+ and then (Has_Option (Id, Name_External)
+ or else
+ Has_Option (Id, Name_Synchronous));
end Is_External_State;
------------------
@@ -8255,6 +8261,9 @@ package body Einfo is
function Is_Synchronized_State (Id : E) return B is
begin
+ -- To qualify, the abstract state must appear with simple option
+ -- "synchronous" (SPARK RM 7.1.4(10)).
+
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Synchronous);
@@ -2553,7 +2553,7 @@ package Einfo is
-- Is_External_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
+-- option External or Synchronous.
-- Is_Finalized_Transient (Flag252)
-- Defined in constants, loop parameters of generalized iterators, and
@@ -10261,92 +10261,157 @@ package body Sem_Util is
--------------------------------
function State_Has_Enabled_Property return Boolean is
- Decl : constant Node_Id := Parent (Item_Id);
- Opt : Node_Id;
- Opt_Nam : Node_Id;
- Prop : Node_Id;
- Prop_Nam : Node_Id;
- Props : Node_Id;
+ Decl : constant Node_Id := Parent (Item_Id);
- begin
- -- The declaration of an external abstract state appears as an
- -- extension aggregate. If this is not the case, properties can never
- -- be set.
+ procedure Find_Simple_Properties
+ (Has_External : out Boolean;
+ Has_Synchronous : out Boolean);
+ -- Extract the simple properties associated with declaration Decl
- if Nkind (Decl) /= N_Extension_Aggregate then
- return False;
- end if;
+ function Is_Enabled_External_Property return Boolean;
+ -- Determine whether property Property appears within the external
+ -- property list of declaration Decl, and return its status.
- -- When External appears as a simple option, it automatically enables
- -- all properties.
+ ----------------------------
+ -- Find_Simple_Properties --
+ ----------------------------
- Opt := First (Expressions (Decl));
- while Present (Opt) loop
- if Nkind (Opt) = N_Identifier
- and then Chars (Opt) = Name_External
- then
- return True;
- end if;
+ procedure Find_Simple_Properties
+ (Has_External : out Boolean;
+ Has_Synchronous : out Boolean)
+ is
+ Opt : Node_Id;
- Next (Opt);
- end loop;
+ begin
+ -- Assume that none of the properties are available
- -- When External specifies particular properties, inspect those and
- -- find the desired one (if any).
+ Has_External := False;
+ Has_Synchronous := False;
- Opt := First (Component_Associations (Decl));
- while Present (Opt) loop
- Opt_Nam := First (Choices (Opt));
+ Opt := First (Expressions (Decl));
+ while Present (Opt) loop
+ if Nkind (Opt) = N_Identifier then
+ if Chars (Opt) = Name_External then
+ Has_External := True;
- if Nkind (Opt_Nam) = N_Identifier
- and then Chars (Opt_Nam) = Name_External
- then
- Props := Expression (Opt);
+ elsif Chars (Opt) = Name_Synchronous then
+ Has_Synchronous := True;
+ end if;
+ end if;
- -- Multiple properties appear as an aggregate
+ Next (Opt);
+ end loop;
+ end Find_Simple_Properties;
- if Nkind (Props) = N_Aggregate then
+ ----------------------------------
+ -- Is_Enabled_External_Property --
+ ----------------------------------
- -- Simple property form
+ function Is_Enabled_External_Property return Boolean is
+ Opt : Node_Id;
+ Opt_Nam : Node_Id;
+ Prop : Node_Id;
+ Prop_Nam : Node_Id;
+ Props : Node_Id;
- Prop := First (Expressions (Props));
- while Present (Prop) loop
- if Chars (Prop) = Property then
- return True;
- end if;
+ begin
+ Opt := First (Component_Associations (Decl));
+ while Present (Opt) loop
+ Opt_Nam := First (Choices (Opt));
- Next (Prop);
- end loop;
+ if Nkind (Opt_Nam) = N_Identifier
+ and then Chars (Opt_Nam) = Name_External
+ then
+ Props := Expression (Opt);
- -- Property with expression form
+ -- Multiple properties appear as an aggregate
- Prop := First (Component_Associations (Props));
- while Present (Prop) loop
- Prop_Nam := First (Choices (Prop));
+ if Nkind (Props) = N_Aggregate then
- -- The property can be represented in two ways:
- -- others => <value>
- -- <property> => <value>
+ -- Simple property form
- if Nkind (Prop_Nam) = N_Others_Choice
- or else (Nkind (Prop_Nam) = N_Identifier
- and then Chars (Prop_Nam) = Property)
- then
- return Is_True (Expr_Value (Expression (Prop)));
- end if;
+ Prop := First (Expressions (Props));
+ while Present (Prop) loop
+ if Chars (Prop) = Property then
+ return True;
+ end if;
- Next (Prop);
- end loop;
+ Next (Prop);
+ end loop;
- -- Single property
+ -- Property with expression form
- else
- return Chars (Props) = Property;
+ Prop := First (Component_Associations (Props));
+ while Present (Prop) loop
+ Prop_Nam := First (Choices (Prop));
+
+ -- The property can be represented in two ways:
+ -- others => <value>
+ -- <property> => <value>
+
+ if Nkind (Prop_Nam) = N_Others_Choice
+ or else (Nkind (Prop_Nam) = N_Identifier
+ and then Chars (Prop_Nam) = Property)
+ then
+ return Is_True (Expr_Value (Expression (Prop)));
+ end if;
+
+ Next (Prop);
+ end loop;
+
+ -- Single property
+
+ else
+ return Chars (Props) = Property;
+ end if;
end if;
- end if;
- Next (Opt);
- end loop;
+ Next (Opt);
+ end loop;
+
+ return False;
+ end Is_Enabled_External_Property;
+
+ -- Local variables
+
+ Has_External : Boolean;
+ Has_Synchronous : Boolean;
+
+ -- Start of processing for State_Has_Enabled_Property
+
+ begin
+ -- The declaration of an external abstract state appears as an
+ -- extension aggregate. If this is not the case, properties can
+ -- never be set.
+
+ if Nkind (Decl) /= N_Extension_Aggregate then
+ return False;
+ end if;
+
+ Find_Simple_Properties (Has_External, Has_Synchronous);
+
+ -- Simple option External enables all properties (SPARK RM 7.1.2(2))
+
+ if Has_External then
+ return True;
+
+ -- Option External may enable or disable specific properties
+
+ elsif Is_Enabled_External_Property then
+ return True;
+
+ -- Simple option Synchronous
+ --
+ -- enables disables
+ -- Asynch_Readers Effective_Reads
+ -- Asynch_Writers Effective_Writes
+ --
+ -- Note that both forms of External have higher precedence than
+ -- Synchronous (SPARK RM 7.1.4(10)).
+
+ elsif Has_Synchronous then
+ return Nam_In (Property, Name_Async_Readers, Name_Async_Writers);
+ end if;
return False;
end State_Has_Enabled_Property;
new file mode 100644
@@ -0,0 +1,27 @@
+-- { dg-do compile }
+
+package body Sync2 with
+ SPARK_Mode,
+ Refined_State => (State => (A, P, T))
+is
+ A : Integer := 0 with Atomic, Async_Readers, Async_Writers;
+
+ protected type Prot_Typ is
+ private
+ Comp : Natural := 0;
+ end Prot_Typ;
+
+ P : Prot_Typ;
+
+ task type Task_Typ;
+
+ T : Task_Typ;
+
+ protected body Prot_Typ is
+ end Prot_Typ;
+
+ task body Task_Typ is
+ begin
+ null;
+ end Task_Typ;
+end Sync2;
new file mode 100644
@@ -0,0 +1,6 @@
+package Sync2 with
+ SPARK_Mode,
+ Abstract_State => (State with Synchronous)
+is
+ pragma Elaborate_Body;
+end Sync2;