This patch modifies the elaboration circuitry to detect an issue in SPARK
where an object in package P of a private type in package T subject to
pragma Default_Initial_Condition is default initialized and package P
lacks Elaborate_All (T).
------------
-- Source --
------------
-- pack.ads
package Pack with SPARK_Mode is
type Elab_Typ is private
with Default_Initial_Condition => Get_Val (Elab_Typ) = Expect_Val;
type False_Typ is private
with Default_Initial_Condition => False;
type True_Typ is private
with Default_Initial_Condition => True;
function Expect_Val return Integer;
function Get_Val (Obj : Elab_Typ) return Integer;
private
type Elab_Typ is record
Comp : Integer;
end record;
type False_Typ is null record;
type True_Typ is null record;
end Pack;
-- pack.adb
package body Pack with SPARK_Mode is
function Expect_Val return Integer is
begin
return 1234;
end Expect_Val;
function Get_Val (Obj : Elab_Typ) return Integer is
begin
return Obj.Comp;
end Get_Val;
end Pack;
-- main_pack.ads
with Pack; use Pack;
package Main_Pack with SPARK_Mode is
Obj_1 : Elab_Typ;
Obj_2 : False_Typ;
Obj_3 : True_Typ;
end Main_Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnata main_pack.ads
main_pack.ads:4:04: call to Default_Initial_Condition during elaboration in
SPARK
main_pack.ads:4:04: Elaborate_All pragma required for "Pack"
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-11-12 Hristian Kirtchev <kirtc...@adacore.com>
* sem_elab.adb (Check_A_Call): Add new variable
Is_DIC_Proc. Report elaboration issue in SPARK concerning calls
to source subprograms or nontrivial Default_Initial_Condition
procedures. Add specialized error message to avoid outputting
the internal name of the Default_Initial_Condition procedure.
* sem_util.ads, sem_util.adb
(Is_Non_Trivial_Default_Init_Cond_Procedure): New routine.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 230235)
+++ sem_util.adb (working copy)
@@ -12362,12 +12362,50 @@
end if;
end Is_Local_Variable_Reference;
+ ------------------------------------------------
+ -- Is_Non_Trivial_Default_Init_Cond_Procedure --
+ ------------------------------------------------
+
+ function Is_Non_Trivial_Default_Init_Cond_Procedure
+ (Id : Entity_Id) return Boolean
+ is
+ Body_Decl : Node_Id;
+ Stmt : Node_Id;
+
+ begin
+ if Ekind (Id) = E_Procedure
+ and then Is_Default_Init_Cond_Procedure (Id)
+ then
+ Body_Decl :=
+ Unit_Declaration_Node
+ (Corresponding_Body (Unit_Declaration_Node (Id)));
+
+ -- The body of the Default_Initial_Condition procedure must contain
+ -- at least one statement, otherwise the generation of the subprogram
+ -- body failed.
+
+ pragma Assert (Present (Handled_Statement_Sequence (Body_Decl)));
+
+ -- To qualify as non-trivial, the first statement of the procedure
+ -- must be a check in the form of an if statement. If the original
+ -- Default_Initial_Condition expression was folded, then the first
+ -- statement is not a check.
+
+ Stmt := First (Statements (Handled_Statement_Sequence (Body_Decl)));
+
+ return
+ Nkind (Stmt) = N_If_Statement
+ and then Nkind (Original_Node (Stmt)) = N_Pragma;
+ end if;
+
+ return False;
+ end Is_Non_Trivial_Default_Init_Cond_Procedure;
+
-------------------------
-- Is_Object_Reference --
-------------------------
function Is_Object_Reference (N : Node_Id) return Boolean is
-
function Is_Internally_Generated_Renaming (N : Node_Id) return Boolean;
-- Determine whether N is the name of an internally-generated renaming
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 230223)
+++ sem_util.ads (working copy)
@@ -1433,6 +1433,12 @@
-- parameter of the current enclosing subprogram.
-- Why are OUT parameters not considered here ???
+ function Is_Non_Trivial_Default_Init_Cond_Procedure
+ (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id denotes the procedure which verifies the
+ -- assertion expression of pragma Default_Initial_Condition and if it does,
+ -- the encapsulated expression is non-trivial.
+
function Is_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object. Both
-- variable and constant objects return True (compare Is_Variable).
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 230223)
+++ sem_elab.adb (working copy)
@@ -597,6 +597,11 @@
-- non-visible unit. This is the scope that is to be investigated to
-- see whether an elaboration check is required.
+ Is_DIC_Proc : Boolean := False;
+ -- Flag set when the call denotes the Default_Initial_Condition
+ -- procedure of a private type which wraps a non-trivila assertion
+ -- expression.
+
Issue_In_SPARK : Boolean;
-- Flag set when a source entity is called during elaboration in SPARK
@@ -966,8 +971,17 @@
return;
end if;
- Issue_In_SPARK := SPARK_Mode = On and Comes_From_Source (Ent);
+ Is_DIC_Proc := Is_Non_Trivial_Default_Init_Cond_Procedure (Ent);
+ -- Elaboration issues in SPARK are reported only for source constructs
+ -- and for non-trivial Default_Initial_Condition procedures. The latter
+ -- must be checked because the default initialization of an object of a
+ -- private type triggers the evaluation of the Default_Initial_Condition
+ -- expression which in turn may have side effects.
+
+ Issue_In_SPARK :=
+ SPARK_Mode = On and (Comes_From_Source (Ent) or Is_DIC_Proc);
+
-- Now check if an Elaborate_All (or dynamic check) is needed
if not Suppress_Elaboration_Warnings (Ent)
@@ -1016,8 +1030,21 @@
Ent);
elsif Issue_In_SPARK then
- Error_Msg_NE ("call to & during elaboration in SPARK", N, Ent);
+ -- Emit a specialized error message when the elaboration of an
+ -- object of a private type evaluates the expression of pragma
+ -- Default_Initial_Condition. This prevents the internal name
+ -- of the procedure from appearing in the error message.
+
+ if Is_DIC_Proc then
+ Error_Msg_N
+ ("call to Default_Initial_Condition during elaboration in "
+ & "SPARK", N);
+ else
+ Error_Msg_NE
+ ("call to & during elaboration in SPARK", N, Ent);
+ end if;
+
else
Elab_Warning
("call to & may raise Program_Error?l?",
