===================================================================
@@ -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
===================================================================
@@ -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).
===================================================================
@@ -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?",
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 <kirtchev@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.