+2015-11-12 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch10.adb, atree.adb: Minor reformatting.
+
+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.
+
2015-11-12 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
------------------------
function Copy_Separate_Tree (Source : Node_Id) return Node_Id is
- New_Id : Node_Id;
+ New_Id : Node_Id;
function Copy_Entity (E : Entity_Id) return Entity_Id;
-- Copy Entity, copying only the Ekind and Chars fields
-- Copy list
function Possible_Copy (Field : Union_Id) return Union_Id;
- -- Given a field, returns a copy of the node or list if its parent
- -- is the current source node, and otherwise returns the input
+ -- Given a field, returns a copy of the node or list if its parent is
+ -- the current source node, and otherwise returns the input.
-----------------
-- Copy_Entity --
begin
if Field in Node_Range then
- New_N :=
- Union_Id (Copy_Separate_Tree (Node_Id (Field)));
+ New_N := Union_Id (Copy_Separate_Tree (Node_Id (Field)));
if Parent (Node_Id (Field)) = Source then
Set_Parent (Node_Id (New_N), New_Id);
-- the extended main unit.
if Generate_SCO
- and then
- In_Extended_Main_Source_Unit
- (Cunit_Entity (Current_Sem_Unit))
+ and then In_Extended_Main_Source_Unit
+ (Cunit_Entity (Current_Sem_Unit))
then
SCO_Record_Raw (Unum);
end if;
-- 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
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
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
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
-- 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).
git://gcc.gnu.org / gcc.git / commitdiff