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