This patch updates the analysis of pragma Refined_State to reject constants
which are used as refinement constituents and are either
* Part of the visible state of a package
* Part of the hidden state of a package, and lack indicator Part_Of.
------------
-- Source --
------------
-- var.ads
package Var
with SPARK_Mode,
Initializes => Input
is
Input : Integer := 0;
end Var;
-- pack.ads
with Var;
package Pack
with SPARK_Mode,
Abstract_State => State
is
procedure Force_Body;
private
Const_1 : constant Integer := Var.Input;
Const_2 : constant Integer := 2 with Part_Of => State;
Var_1 : Integer := 1;
Var_2 : Integer := 2 with Part_Of => State;
package Priv_Pack is
Const_3 : constant Integer := Var.Input;
Const_4 : constant Integer := 4 with Part_Of => State;
Var_3 : Integer := 3;
Var_4 : Integer := 4 with Part_Of => State;
end Priv_Pack;
end Pack;
-- pack.adb
package body Pack
with SPARK_Mode,
Refined_State =>
(State =>
(Const_1, -- Error
Const_2, -- OK
Var_1, -- Error
Var_2, -- OK
Priv_Pack.Const_3, -- Error
Priv_Pack.Const_4, -- OK
Priv_Pack.Var_3, -- Error
Priv_Pack.Var_4, -- OK
Const_5, -- OK
Const_6, -- OK
Body_Pack.Const_7, -- OK
Body_Pack.Const_8)) -- OK
is
Const_5 : constant Integer := Var.Input;
Const_6 : constant Integer := 6;
package Body_Pack is
Const_7 : constant Integer := Var.Input;
Const_8 : constant Integer := 8;
end Body_Pack;
procedure Force_Body is begin null; end Force_Body;
end Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatf pack.adb
pack.adb:5:13: cannot use "Const_1" in refinement, constituent is not a hidden
state of package "Pack"
pack.adb:7:13: cannot use "Var_1" in refinement, constituent is not a hidden
state of package "Pack"
pack.adb:9:22: cannot use "Const_3" in refinement, constituent is not a hidden
state of package "Pack"
pack.adb:11:22: cannot use "Var_3" in refinement, constituent is not a hidden
state of package "Pack"
pack.ads:13:04: indicator Part_Of is required in this context (SPARK RM
7.2.6(2))
pack.ads:13:04: "Var_1" is declared in the private part of package "Pack"
pack.ads:20:07: indicator Part_Of is required in this context (SPARK RM
7.2.6(2))
pack.ads:20:07: "Var_3" is declared in the private part of package "Pack"
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-12-15 Hristian Kirtchev <kirtc...@adacore.com>
* sem_prag.adb (Match_Constituent): Do not quietly accept constants as
suitable constituents.
* exp_util.adb: Minor reformatting.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 255683)
+++ exp_util.adb (working copy)
@@ -165,6 +165,10 @@
-- Force evaluation of bounds of a slice, which may be given by a range
-- or by a subtype indication with or without a constraint.
+ function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
+ -- Determine whether pragma Default_Initial_Condition denoted by Prag has
+ -- an assertion expression that should be verified at run time.
+
function Make_CW_Equivalent_Type
(T : Entity_Id;
E : Node_Id) return Entity_Id;
@@ -1500,6 +1504,7 @@
-- Start of processing for Add_Own_DIC
begin
+ pragma Assert (Present (DIC_Expr));
Expr := New_Copy_Tree (DIC_Expr);
-- Perform the following substitution:
@@ -1733,8 +1738,6 @@
-- Produce an empty completing body in the following cases:
-- * Assertions are disabled
-- * The DIC Assertion_Policy is Ignore
- -- * Pragma DIC appears without an argument
- -- * Pragma DIC appears with argument "null"
if No (Stmts) then
Stmts := New_List (Make_Null_Statement (Loc));
@@ -8715,6 +8718,21 @@
and then Is_Itype (Full_Typ);
end Is_Untagged_Private_Derivation;
+ ------------------------------
+ -- Is_Verifiable_DIC_Pragma --
+ ------------------------------
+
+ function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+
+ begin
+ -- To qualify as verifiable, a DIC pragma must have a non-null argument
+
+ return
+ Present (Args)
+ and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
+ end Is_Verifiable_DIC_Pragma;
+
---------------------------
-- Is_Volatile_Reference --
---------------------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 255678)
+++ sem_prag.adb (working copy)
@@ -27327,25 +27327,14 @@
end loop;
end if;
- -- Constants are part of the hidden state of a package, but
- -- the compiler cannot determine whether they have variable
- -- input (SPARK RM 7.1.1(2)) and cannot classify them as a
- -- hidden state. Accept the constant quietly even if it is
- -- a visible state or lacks a Part_Of indicator.
+ -- At this point it is known that the constituent is not
+ -- part of the package hidden state and cannot be used in
+ -- a refinement (SPARK RM 7.2.2(9)).
- if Ekind (Constit_Id) = E_Constant then
- Collect_Constituent;
-
- -- If we get here, then the constituent is not a hidden
- -- state of the related package and may not be used in a
- -- refinement (SPARK RM 7.2.2(9)).
-
- else
- Error_Msg_Name_1 := Chars (Spec_Id);
- SPARK_Msg_NE
- ("cannot use & in refinement, constituent is not a "
- & "hidden state of package %", Constit, Constit_Id);
- end if;
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ SPARK_Msg_NE
+ ("cannot use & in refinement, constituent is not a hidden "
+ & "state of package %", Constit, Constit_Id);
end if;
end Match_Constituent;
