2014-01-21 Thomas Quinot <quinot@adacore.com>

	* exp_ch5.adb: Fix comment.
	* switch-c.adb: Minor comment update.
	* exp_ch3.adb: Minor reformatting.

2014-01-21  Arnaud Charlet  <charlet@adacore.com>

	* back_end.adb (Scan_Compiler_Arguments): Do not store object
	filename in gnatprove mode.

2014-01-21  Thomas Quinot  <quinot@adacore.com>

	* sinfo.ads (No_Ctrl_Actions): Clarify documentation (flag also
	suppresses usage of primitive _assign for tagged types).
	* exp_aggr.adb (Build_Array_Aggr_Code.Gen_Assign): Set
	No_Ctrl_Actions for a tagged type that does not require
	finalization, as we want to disable usage of _assign (which
	may cause undesirable discriminant checks on an uninitialized,
	invalid target).

2014-01-21  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb: Reject invariant'class on completion.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206878 138bc75d-0d04-0410-961f-82ee72b054a4

8 files changed, 81 insertions, 40 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 48891bfc4a4..859e5e04fd6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,28 @@
+2014-01-21  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_ch5.adb: Fix comment.
+	* switch-c.adb: Minor comment update.
+	* exp_ch3.adb: Minor reformatting.
+
+2014-01-21  Arnaud Charlet  <charlet@adacore.com>
+
+	* back_end.adb (Scan_Compiler_Arguments): Do not store object
+	filename in gnatprove mode.
+
+2014-01-21  Thomas Quinot  <quinot@adacore.com>
+
+	* sinfo.ads (No_Ctrl_Actions): Clarify documentation (flag also
+	suppresses usage of primitive _assign for tagged types).
+	* exp_aggr.adb (Build_Array_Aggr_Code.Gen_Assign): Set
+	No_Ctrl_Actions for a tagged type that does not require
+	finalization, as we want to disable usage of _assign (which
+	may cause undesirable discriminant checks on an uninitialized,
+	invalid target).
+
+2014-01-21  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb: Reject invariant'class on completion.
+
 2014-01-21  Javier Miranda  <miranda@adacore.com>
 
 	* exp_ch3.adb (Build_Init_Procedure): For
diff --git a/gcc/ada/back_end.adb b/gcc/ada/back_end.adb
index 6488da1e468..89cf3031338 100644
--- a/gcc/ada/back_end.adb
+++ b/gcc/ada/back_end.adb
@@ -295,6 +295,14 @@ package body Back_End is
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
 
+               --  In GNATprove_Mode, such an object file is never written, and
+               --  the call to Set_Output_Object_File_Name may fail (e.g. when
+               --  the object file name does not have the expected suffix). So
+               --  we skip that call when GNATprove_Mode is set.
+
+               elsif GNATprove_Mode then
+                  Output_File_Name_Seen := True;
+
                else
                   Set_Output_Object_File_Name (Argv);
                   Output_File_Name_Seen := True;
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 0fcebd60c7f..14926508368 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -1176,47 +1176,50 @@ package body Exp_Aggr is
             end if;
 
          else
-            --  Now generate the assignment with no associated controlled
-            --  actions since the target of the assignment may not have been
-            --  initialized, it is not possible to Finalize it as expected by
-            --  normal controlled assignment. The rest of the controlled
-            --  actions are done manually with the proper finalization list
-            --  coming from the context.
-
             A :=
               Make_OK_Assignment_Statement (Loc,
                 Name       => Indexed_Comp,
                 Expression => New_Copy_Tree (Expr));
 
-            if Present (Comp_Type) and then Needs_Finalization (Comp_Type) then
-               Set_No_Ctrl_Actions (A);
+            --  The target of the assignment may not have been initialized,
+            --  so it is not possible to call Finalize as expected in normal
+            --  controlled assignments. We must also avoid using the primitive
+            --  _assign (which depends on a valid target, and may for example
+            --  perform discriminant checks on it).
 
-               --  If this is an aggregate for an array of arrays, each
-               --  sub-aggregate will be expanded as well, and even with
-               --  No_Ctrl_Actions the assignments of inner components will
-               --  require attachment in their assignments to temporaries.
-               --  These temporaries must be finalized for each subaggregate,
-               --  to prevent multiple attachments of the same temporary
-               --  location to same finalization chain (and consequently
-               --  circular lists). To ensure that finalization takes place
-               --  for each subaggregate we wrap the assignment in a block.
+            --  Both Finalize and usage of _assign are disabled by setting
+            --  No_Ctrl_Actions on the assignment. The rest of the controlled
+            --  actions are done manually with the proper finalization list
+            --  coming from the context.
 
-               if Is_Array_Type (Comp_Type)
-                 and then Nkind (Expr) = N_Aggregate
-               then
-                  A :=
-                    Make_Block_Statement (Loc,
+            Set_No_Ctrl_Actions (A);
+
+            --  If this is an aggregate for an array of arrays, each
+            --  sub-aggregate will be expanded as well, and even with
+            --  No_Ctrl_Actions the assignments of inner components will
+            --  require attachment in their assignments to temporaries. These
+            --  temporaries must be finalized for each subaggregate, to prevent
+            --  multiple attachments of the same temporary location to same
+            --  finalization chain (and consequently circular lists). To ensure
+            --  that finalization takes place for each subaggregate we wrap the
+            --  assignment in a block.
+
+            if Present (Comp_Type)
+                 and then Needs_Finalization (Comp_Type)
+                 and then Is_Array_Type (Comp_Type)
+                 and then Present (Expr)
+            then
+               A := Make_Block_Statement (Loc,
                       Handled_Statement_Sequence =>
                         Make_Handled_Sequence_Of_Statements (Loc,
                            Statements => New_List (A)));
-               end if;
             end if;
 
             Append_To (L, A);
 
             --  Adjust the tag if tagged (because of possible view
-            --  conversions), unless compiling for a VM where
-            --  tags are implicit.
+            --  conversions), unless compiling for a VM where tags
+            --  are implicit.
 
             if Present (Comp_Type)
               and then Is_Tagged_Type (Comp_Type)
@@ -2465,9 +2468,9 @@ package body Exp_Aggr is
                Ref := Convert_To (Init_Typ, New_Copy_Tree (Target));
                Set_Assignment_OK (Ref);
 
-               --  Make the assignment without usual controlled actions since
-               --  we only want the post adjust but not the pre finalize here
-               --  Add manual adjust when necessary.
+               --  Make the assignment without usual controlled actions, since
+               --  we only want to Adjust afterwards, but not to Finalize
+               --  beforehand. Add manual Adjust when necessary.
 
                Assign := New_List (
                  Make_OK_Assignment_Statement (Loc,
@@ -2530,10 +2533,10 @@ package body Exp_Aggr is
             end if;
          end;
 
-         --  Generate assignments of hidden assignments. If the base type is an
-         --  unchecked union, the discriminants are unknown to the back-end and
-         --  absent from a value of the type, so assignments for them are not
-         --  emitted.
+         --  Generate assignments of hidden discriminants. If the base type is
+         --  an unchecked union, the discriminants are unknown to the back-end
+         --  and absent from a value of the type, so assignments for them are
+         --  not emitted.
 
          if Has_Discriminants (Typ)
            and then not Is_Unchecked_Union (Base_Type (Typ))
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index da0ac4c01bb..4a0fdf67d73 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -1863,9 +1863,7 @@ package body Exp_Ch3 is
          --  Suppress the tag adjustment when VM_Target because VM tags are
          --  represented implicitly in objects.
 
-         if Is_Tagged_Type (Typ)
-           and then Tagged_Type_Expansion
-         then
+         if Is_Tagged_Type (Typ) and then Tagged_Type_Expansion then
             Append_To (Res,
               Make_Assignment_Statement (N_Loc,
                 Name       =>
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index b71117bd252..32108620519 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -2082,7 +2082,7 @@ package body Exp_Ch5 is
                --  by a dispatching call to _assign. It is suppressed in the
                --  case of assignments created by the expander that correspond
                --  to initializations, where we do want to copy the tag
-               --  (Expand_Ctrl_Actions flag is set True in this case). It is
+               --  (Expand_Ctrl_Actions flag is set False in this case). It is
                --  also suppressed if restriction No_Dispatching_Calls is in
                --  force because in that case predefined primitives are not
                --  generated.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b98206f9a62..399753a365e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -14497,6 +14497,8 @@ package body Sem_Prag is
 
             --  An invariant must apply to a private type, or appear in the
             --  private part of a package spec and apply to a completion.
+            --  a class-wide invariant can only appear on a private declaration
+            --  or private extension, not a completion.
 
             elsif Ekind_In (Typ, E_Private_Type,
                                  E_Record_Type_With_Private,
@@ -14506,6 +14508,7 @@ package body Sem_Prag is
 
             elsif In_Private_Part (Current_Scope)
               and then Has_Private_Declaration (Typ)
+              and then not Class_Present (N)
             then
                null;
 
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index f0af4a2cbea..e036c5fd1c8 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1684,8 +1684,10 @@ package Sinfo is
    --  No_Ctrl_Actions (Flag7-Sem)
    --    Present in N_Assignment_Statement to indicate that no Finalize nor
    --    Adjust should take place on this assignment even though the RHS is
-   --    controlled. This is used in init procs and aggregate expansions where
-   --    the generated assignments are initializations, not real assignments.
+   --    controlled. Also indicates that the primitive _assign should not be
+   --    used for a tagged assignment. This is used in init procs and aggregate
+   --    expansions where the generated assignments are initializations, not
+   --    real assignments.
 
    --  No_Elaboration_Check (Flag14-Sem)
    --    Present in N_Function_Call and N_Procedure_Call_Statement. Indicates
diff --git a/gcc/ada/switch-c.adb b/gcc/ada/switch-c.adb
index 3043dde4429..201a99d1619 100644
--- a/gcc/ada/switch-c.adb
+++ b/gcc/ada/switch-c.adb
@@ -686,7 +686,9 @@ package body Switch.C is
                   --  -gnateS (generate SCO information)
 
                   --  Include Source Coverage Obligation information in ALI
-                  --  files for use by source coverage analysis tools (xcov).
+                  --  files for use by source coverage analysis tools
+                  --  (gnatcov) (equivalent to -fdump-scos, provided for
+                  --  backwards compatibility).
 
                   when 'S' =>
                      Generate_SCO := True;