sem_ch10.adb, atree.adb: Minor reformatting.

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.

From-SVN: r230237

gcc/ada/ChangeLog

 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):
 	Remove the guard concerning entry bodies as it is spurious.
 	(Analyze_Entry_Or_Subprogram_Contract): Skip the analysis of

gcc/ada/atree.adb

@@ -794,7 +794,7 @@ package body Atree is
    ------------------------
 
    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
@@ -803,8 +803,8 @@ package body Atree is
       --  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 --
@@ -871,8 +871,7 @@ package body Atree is
 
       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);

gcc/ada/sem_ch10.adb

@@ -1877,9 +1877,8 @@ package body Sem_Ch10 is
                   --  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;

gcc/ada/sem_elab.adb

@@ -597,6 +597,11 @@ package body Sem_Elab is
       --  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,7 +971,16 @@ package body Sem_Elab is
          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
 
@@ -1016,7 +1030,20 @@ package body Sem_Elab is
                   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

gcc/ada/sem_util.adb

@@ -12362,12 +12362,50 @@ package body Sem_Util is
       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
 

gcc/ada/sem_util.ads

@@ -1433,6 +1433,12 @@ package Sem_Util is
    --  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).