[multiple changes]

2011-08-03  Emmanuel Briot  <briot@adacore.com>

	* prj-pp.adb (Pretty_Print): remove trailing blank line in the file

2011-08-03  Javier Miranda  <miranda@adacore.com>

	* sem_aux.adb (Is_VM_By_Copy_Actual): Fix wrong use of
	Tagged_Type_Expansion.

2011-08-03  Yannick Moy  <moy@adacore.com>

	* sem_res.adb
	(Resolve_Op_Concat_Arg): do not issue a SPARK violation when argument of
	concatenation is the name of a constant

From-SVN: r177258

gcc/ada/ChangeLog

 2011-08-03  Emmanuel Briot  <briot@adacore.com>
 
+	* prj-pp.adb (Pretty_Print): remove trailing blank line in the file
+
+2011-08-03  Javier Miranda  <miranda@adacore.com>
+
+	* sem_aux.adb (Is_VM_By_Copy_Actual): Fix wrong use of
+	Tagged_Type_Expansion.
+
+2011-08-03  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb
+	(Resolve_Op_Concat_Arg): do not issue a SPARK violation when argument of
+	concatenation is the name of a constant
+
+2011-08-03  Emmanuel Briot  <briot@adacore.com>
+
 	* prj-proc.adb, prj-ext.adb, prj-ext.ads, prj-env.adb, prj-env.ads,
 	prj-tree.adb, prj-tree.ads (Initialize_And_Copy, Copy): new subprograms
 	(Process_Declarative_Items): new parameter Child_Env.

gcc/ada/prj-pp.adb

@@ -948,10 +948,6 @@ package body Prj.PP is
       end if;
 
       Print (Project, 0);
-
-      if W_Char = null or else W_Str = null then
-         Output.Write_Eol;
-      end if;
    end Pretty_Print;
 
    -----------------------

gcc/ada/sem_aux.adb

@@ -33,10 +33,10 @@
 with Atree;  use Atree;
 with Einfo;  use Einfo;
 with Namet;  use Namet;
-with Opt;    use Opt;
 with Sinfo;  use Sinfo;
 with Snames; use Snames;
 with Stand;  use Stand;
+with Targparm; use Targparm;
 
 package body Sem_Aux is
 
@@ -791,7 +791,7 @@ package body Sem_Aux is
 
    function Is_VM_By_Copy_Actual (N : Node_Id) return Boolean is
    begin
-      return not Tagged_Type_Expansion
+      return VM_Target /= No_VM
         and then Nkind (N) = N_Identifier
         and then Present (Renamed_Object (Entity (N)))
         and then Nkind (Renamed_Object (Entity (N))) = N_Slice;

gcc/ada/sem_res.adb

@@ -7774,10 +7774,10 @@ package body Sem_Res is
       end if;
 
       --  Concatenation is restricted in SPARK: each operand must be either a
-      --  string literal, a static character expression, or another
-      --  concatenation. Arg cannot be a concatenation here as callers of
-      --  Resolve_Op_Concat_Arg call it separately on each final operand, past
-      --  concatenation operations.
+      --  string literal, the name of a string constant, a static character or
+      --  string expression, or another concatenation. Arg cannot be a
+      --  concatenation here as callers of Resolve_Op_Concat_Arg call it
+      --  separately on each final operand, past concatenation operations.
 
       if Is_Character_Type (Etype (Arg)) then
          if not Is_Static_Expression (Arg) then
@@ -7786,7 +7786,10 @@ package body Sem_Res is
          end if;
 
       elsif Is_String_Type (Etype (Arg)) then
-         if not Is_Static_Expression (Arg) then
+         if not (Nkind_In (Arg, N_Identifier, N_Expanded_Name)
+                  and then Is_Constant_Object (Entity (Arg)))
+           and then not Is_Static_Expression (Arg)
+         then
             Check_SPARK_Restriction
               ("string operand for concatenation should be static", N);
          end if;