===================================================================
@@ -2710,7 +2710,7 @@
Legal : out Boolean);
-- Subsidiary to the analysis of pragmas Abstract_State and Part_Of.
-- Perform full analysis of indicator Part_Of. Item_Id is the entity of
- -- an abstract state, variable or package instantiation. State is the
+ -- an abstract state, object or package instantiation. State is the
-- encapsulating state. Indic is the Part_Of indicator. Flag Legal is
-- set when the indicator is legal.
@@ -17557,6 +17557,20 @@
Legal => Legal);
if Legal then
+
+ -- Constants without "variable input" are not considered part
+ -- of the hidden state of a package (SPARK RM 7.1.1(2)). As a
+ -- result such constants do not require a Part_Of indicator.
+
+ if Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ SPARK_Msg_NE
+ ("useless Part_Of indicator, constant & does not have "
+ & "variable input", N, Item_Id);
+ return;
+ end if;
+
State_Id := Entity (State);
-- The Part_Of indicator turns an object into a constituent of
@@ -24448,7 +24462,18 @@
-- formals to their actuals as the formals cannot be named
-- from the outside and participate in refinement.
- if No (Corresponding_Generic_Association (Decl)) then
+ if Present (Corresponding_Generic_Association (Decl)) then
+ null;
+
+ -- Constants without "variable input" are not considered a
+ -- hidden state of a package (SPARK RM 7.1.1(2)).
+
+ elsif Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ null;
+
+ else
Add_Item (Item_Id, Result);
end if;
@@ -24993,6 +25018,14 @@
elsif SPARK_Mode /= On then
return;
+
+ -- Do not consider constants without variable input because those are
+ -- not part of the hidden state of a package (SPARK RM 7.1.1(2)).
+
+ elsif Ekind (Item_Id) = E_Constant
+ and then not Has_Variable_Input (Item_Id)
+ then
+ return;
end if;
-- Find where the abstract state, variable or package instantiation
===================================================================
@@ -9317,6 +9317,18 @@
end if;
end Has_Tagged_Component;
+ ------------------------
+ -- Has_Variable_Input --
+ ------------------------
+
+ function Has_Variable_Input (Const_Id : Entity_Id) return Boolean is
+ Expr : constant Node_Id := Expression (Declaration_Node (Const_Id));
+
+ begin
+ return
+ Present (Expr) and then not Compile_Time_Known_Value_Or_Aggr (Expr);
+ end Has_Variable_Input;
+
----------------------------
-- Has_Volatile_Component --
----------------------------
===================================================================
@@ -1046,6 +1046,11 @@
-- component is present. This function is used to check if "=" has to be
-- expanded into a bunch component comparisons.
+ function Has_Variable_Input (Const_Id : Entity_Id) return Boolean;
+ -- Determine whether the initialization expression of constant Const_Id has
+ -- "variable input" (SPARK RM 7.1.1(2)). This roughly maps to the semantic
+ -- concept of a compile-time known value.
+
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
-- Given an arbitrary type, determine whether it contains at least one
-- volatile component.
This patch implements the following rule with respect to constants: SPARK RM 7.1.1(2) - The hidden state of a package P consists of: * any variables, or constants with variable inputs, declared immediately in the private part or body of P. Constants without variable input are not considered part of the hidden state of a package. These constants do not require indicator Part_Of when declared in the private part of a package. ------------ -- Source -- ------------ -- types.ads ackage Types is type CA is array (1 .. 3) of Integer; type UA is array (Integer range <>) of Integer; type VR (Discr : Boolean) is record Comp_1 : Integer; case Discr is when True => Comp_2 : Integer; when others => null; end case; end record; subtype CR is VR (True); function Get_CA return CA; function Get_CR return CR; function Get_In return Integer; function Get_UA return UA; function Get_VR return VR; end Types; -- types.adb package body Types is function Get_CA return CA is Result : constant CA := (others => 0); begin return Result; end Get_CA; function Get_CR return CR is Result : constant CR := (Discr => True, Comp_1 => 0, Comp_2 => 0); begin return Result; end Get_CR; function Get_In return Integer is begin return 0; end Get_In; function Get_UA return UA is begin return (0, 0, 0); end Get_UA; function Get_VR return VR is begin return (Discr => False, Comp_1 => 0); end Get_VR; end Types; -- legal_hidden_state.ads with Types; use Types; pragma Elaborate_All (Types); package Legal_Hidden_State with SPARK_Mode, Abstract_State => State is procedure Force_Body; private -- Constrained array C1 : constant CA := Get_CA with Part_Of => State; C2 : constant CA := (others => Get_In) with Part_Of => State; C3 : constant CA := (1, 2, Get_In) with Part_Of => State; -- Constrained record C4 : constant CR := Get_CR with Part_Of => State; C5 : constant CR := (Discr => True, Comp_1 => 1, Comp_2 => Get_In) with Part_Of => State; -- Scalar C6 : constant Integer := Get_In with Part_Of => State; -- Unconstrained array C7 : constant UA := Get_UA with Part_Of => State; C8 : constant UA (1 .. 3) := (others => Get_In) with Part_Of => State; C9 : constant UA := (1, 2, Get_In) with Part_Of => State; -- Variant record C10 : constant VR := Get_VR with Part_Of => State; C11 : constant VR := (Discr => False, Comp_1 => Get_In) with Part_Of => State; C12 : constant VR (False) := (Discr => False, Comp_1 => Get_In) with Part_Of => State; end Legal_Hidden_State; -- legal_hidden_state.adb package body Legal_Hidden_State with SPARK_Mode, Refined_State => (State => (C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, C21, C22, C23, C24)) is -- Constrained array C13 : constant CA := Get_CA; C14 : constant CA := (others => Get_In); C15 : constant CA := (1, 2, Get_In); -- Constrained record C16 : constant CR := Get_CR; C17 : constant CR := (Discr => True, Comp_1 => 17, Comp_2 => Get_In); -- Scalar C18 : constant Integer := Get_In; -- Unconstrained array C19 : constant UA := Get_UA; C20 : constant UA (1 .. 3) := (others => Get_In); C21 : constant UA := (1, 2, Get_In); -- Variant record C22 : constant VR := Get_VR; C23 : constant VR := (Discr => False, Comp_1 => Get_In); C24 : constant VR (False) := (Discr => False, Comp_1 => Get_In); procedure Force_Body is begin null; end Force_Body; end Legal_Hidden_State; ----------------- -- Compilation -- ----------------- $ gcc -c legal_hidden_state.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-05-22 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Pragma): Constants without variable input do not require indicator Part_Of. (Check_Missing_Part_Of): Constants without variable input do not requrie indicator Part_Of. (Collect_Visible_States): Constants without variable input are not part of the hidden state of a package. * sem_util.ads, sem_util.adb (Has_Variable_Input): New routine.