===================================================================
@@ -115,10 +115,10 @@
function Has_Enabled_Property
(State_Id : Node_Id;
- Prop_Nam : Name_Id) return Boolean;
+ Property : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-- Determine whether an abstract state denoted by its entity State_Id has
- -- enabled property Prop_Name.
+ -- enabled property Property.
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
@@ -7255,13 +7255,14 @@
function Has_Enabled_Property
(State_Id : Node_Id;
- Prop_Nam : Name_Id) return Boolean
+ Property : Name_Id) return Boolean
is
- Decl : constant Node_Id := Parent (State_Id);
- Opt : Node_Id;
- Opt_Nam : Node_Id;
- Prop : Node_Id;
- Props : Node_Id;
+ Decl : constant Node_Id := Parent (State_Id);
+ Opt : Node_Id;
+ Opt_Nam : Node_Id;
+ Prop : Node_Id;
+ Prop_Nam : Node_Id;
+ Props : Node_Id;
begin
-- The declaration of an external abstract state appears as an extension
@@ -7305,7 +7306,7 @@
Prop := First (Expressions (Props));
while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
+ if Chars (Prop) = Property then
return True;
end if;
@@ -7316,7 +7317,9 @@
Prop := First (Component_Associations (Props));
while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
+ Prop_Nam := First (Choices (Prop));
+
+ if Chars (Prop_Nam) = Property then
return Is_True (Expr_Value (Expression (Prop)));
end if;
@@ -7326,7 +7329,7 @@
-- Single property
else
- return Chars (Props) = Prop_Nam;
+ return Chars (Props) = Property;
end if;
end if;
This patch modifies the mechanism that detects an enabled property to handle the case where the property appears with an expression. ------------ -- Source -- ------------ -- serial_port.ads pragma SPARK_Mode; package Serial_Port with Abstract_State => (Input_Port with External => (Async_Writers, Effective_Reads => False)) is procedure Read_Port (X1, X2 : out Integer; Y : in Boolean) with Global => (In_Out => Input_Port), Depends => (X1 => (Input_Port, Y), X2 => Input_Port, Input_Port => Input_Port); end Serial_Port; -- serial_port.adb pragma SPARK_Mode; with System.Storage_Elements; package body Serial_Port with Refined_State => (Input_Port => Port_23) is Port_23 : Integer with Volatile, Async_Writers, Effective_Reads, Address => System.Storage_Elements.To_Address (16#A11CAF0#); procedure Read_Port (X1, X2 : out Integer; Y : in Boolean) with Refined_Global => (In_Out => Port_23), Refined_Depends => (X1 => (Port_23, Y), X2 => Port_23, Port_23 => Port_23) is begin if Y then X1 := Port_23; end if; X2 := Port_23; end Read_Port; end Serial_Port; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c serial_port.adb serial_port.adb:6:09: external state "Input_Port" lacks property "Effective_Reads" set by constituent "Port_23" (SPARK RM 7.2.8(3)) Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-06 Hristian Kirtchev <kirtchev@adacore.com> * sem_util.adb (Has_Enabled_Property): Rename formal parameter Prop_Nam to Property. Update the comment on usage and all occurrences in the body. Add local variable Prop_Nam. When inspecting a property with an expression, the property name appears as the first choice of the component association.