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 <kirtc...@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.
Index: sem_util.adb =================================================================== --- sem_util.adb (revision 207533) +++ sem_util.adb (working copy) @@ -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;