[multiple changes]

2014-02-25  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Analyze_Pragma/Pragma_Validity_Checks): Ignore pragma
	Validity_Checks in GNATprove and CodePeer modes.

2014-02-25  Pascal Obry  <obry@adacore.com>

	* prj-attr.adb, projects.texi, snames.ads-tmpl: Add package Install's
	Artifacts attribute.

From-SVN: r208130

gcc/ada/ChangeLog

 2014-02-25  Yannick Moy  <moy@adacore.com>
 
+	* sem_prag.adb (Analyze_Pragma/Pragma_Validity_Checks): Ignore pragma
+	Validity_Checks in GNATprove and CodePeer modes.
+
+2014-02-25  Pascal Obry  <obry@adacore.com>
+
+	* prj-attr.adb, projects.texi, snames.ads-tmpl: Add package Install's
+	Artifacts attribute.
+
+2014-02-25  Yannick Moy  <moy@adacore.com>
+
 	* sem_prag.adb: Minor reformatting to get consistent messages.
 
 2014-02-25  Robert Dewar  <dewar@adacore.com>

gcc/ada/prj-attr.adb

@@ -364,6 +364,7 @@ package body Prj.Attr is
    "SVlib_subdir#" &
    "SVproject_subdir#" &
    "SVactive#" &
+   "LAartifacts#" &
 
    --  package Remote
 

gcc/ada/projects.texi

@@ -1085,6 +1085,14 @@ The following attributes can be defined in package @code{Install}:
 Whether the project is to be installed, values are @code{true}
 (default) or @code{false}.
 
+@item @b{Artifacts}
+@cindex @code{Artifacts}
+
+An array attribute to declare a set of files not part of the sources
+to be installed. The array discriminant is the directory where the
+file is to be installed. If a relative directory then Prefix (see
+below) is prepended.
+
 @item @b{Prefix}:
 @cindex @code{Prefix}
 

gcc/ada/sem_prag.adb

@@ -5238,10 +5238,9 @@ package body Sem_Prag is
                end if;
             end if;
 
-            --  Retain a copy of the pre- or postcondition pragma for formal
-            --  verification purposes. The copy is needed because the pragma is
-            --  expanded into other constructs which are not acceptable in the
-            --  N_Contract node.
+            --  Retain copy of the pre/postcondition pragma in GNATprove mode.
+            --  The copy is needed because the pragma is expanded into other
+            --  constructs which are not acceptable in the N_Contract node.
 
             if Acts_As_Spec (PO)
               and then GNATprove_Mode
@@ -5279,10 +5278,9 @@ package body Sem_Prag is
 
          elsif Nkind (PO) = N_Compilation_Unit_Aux then
 
-            --  In formal verification mode, analyze pragma expression for
-            --  correctness, as it is not expanded later. Ditto in ASIS_Mode
-            --  where there is no later point at which the aspect will be
-            --  analyzed.
+            --  In GNATprove mode, analyze pragma expression for correctness,
+            --  as it is not expanded later. Ditto in ASIS_Mode where there is
+            --  no later point at which the aspect will be analyzed.
 
             if GNATprove_Mode or ASIS_Mode then
                Analyze_Pre_Post_Condition_In_Decl_Part
@@ -9121,8 +9119,8 @@ package body Sem_Prag is
       --  Start of processing for Process_Suppress_Unsuppress
 
       begin
-         --  Ignore pragma Suppress/Unsuppress in CodePeer and SPARK modes on
-         --  user code: we want to generate checks for analysis purposes, as
+         --  Ignore pragma Suppress/Unsuppress in CodePeer and GNATprove modes
+         --  on user code: we want to generate checks for analysis purposes, as
          --  set respectively by -gnatC and -gnatd.F
 
          if (CodePeer_Mode or GNATprove_Mode)
@@ -15026,8 +15024,8 @@ package body Sem_Prag is
             Check_Restriction (No_Initialize_Scalars, N);
 
             --  Initialize_Scalars creates false positives in CodePeer, and
-            --  incorrect negative results in SPARK mode, so ignore this pragma
-            --  in these modes.
+            --  incorrect negative results in GNATprove mode, so ignore this
+            --  pragma in these modes.
 
             if not Restriction_Active (No_Initialize_Scalars)
               and then not (CodePeer_Mode or GNATprove_Mode)
@@ -15148,8 +15146,8 @@ package body Sem_Prag is
          when Pragma_Inline_Always =>
             GNAT_Pragma;
 
-            --  Pragma always active unless in CodePeer or SPARK mode, since
-            --  this causes walk order issues.
+            --  Pragma always active unless in CodePeer or GNATprove mode,
+            --  since this causes walk order issues.
 
             if not (CodePeer_Mode or GNATprove_Mode) then
                Process_Inline (Enabled);
@@ -16832,8 +16830,8 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
 
             --  Normalize_Scalars creates false positives in CodePeer, and
-            --  incorrect negative results in SPARK mode, so ignore this pragma
-            --  in these modes.
+            --  incorrect negative results in GNATprove mode, so ignore this
+            --  pragma in these modes.
 
             if not (CodePeer_Mode or GNATprove_Mode) then
                Normalize_Scalars := True;
@@ -20964,7 +20962,7 @@ package body Sem_Prag is
          --  pragma Validity_Checks (On | Off | ALL_CHECKS | STRING_LITERAL);
 
          when Pragma_Validity_Checks => Validity_Checks : declare
-            A  : constant Node_Id   := Get_Pragma_Arg (Arg1);
+            A  : constant Node_Id := Get_Pragma_Arg (Arg1);
             S  : String_Id;
             C  : Char_Code;
 
@@ -20973,37 +20971,49 @@ package body Sem_Prag is
             Check_Arg_Count (1);
             Check_No_Identifiers;
 
-            if Nkind (A) = N_String_Literal then
-               S   := Strval (A);
+            --  Pragma always active unless in CodePeer or GNATprove modes,
+            --  which use a fixed configuration of validity checks.
 
-               declare
-                  Slen    : constant Natural := Natural (String_Length (S));
-                  Options : String (1 .. Slen);
-                  J       : Natural;
+            if not (CodePeer_Mode or GNATprove_Mode) then
+               if Nkind (A) = N_String_Literal then
+                  S := Strval (A);
 
-               begin
-                  J := 1;
-                  loop
-                     C := Get_String_Char (S, Int (J));
-                     exit when not In_Character_Range (C);
-                     Options (J) := Get_Character (C);
+                  declare
+                     Slen    : constant Natural := Natural (String_Length (S));
+                     Options : String (1 .. Slen);
+                     J       : Natural;
 
-                     if J = Slen then
-                        Set_Validity_Check_Options (Options);
-                        exit;
-                     else
-                        J := J + 1;
-                     end if;
-                  end loop;
-               end;
+                  begin
+                     --  Couldn't we use a for loop here over Options'Range???
 
-            elsif Nkind (A) = N_Identifier then
-               if Chars (A) = Name_All_Checks then
-                  Set_Validity_Check_Options ("a");
-               elsif Chars (A) = Name_On then
-                  Validity_Checks_On := True;
-               elsif Chars (A) = Name_Off then
-                  Validity_Checks_On := False;
+                     J := 1;
+                     loop
+                        C := Get_String_Char (S, Int (J));
+
+                        --  This is a weird test, it skips setting validity
+                        --  checks entirely if any element of S is out of
+                        --  range of Character, what is that about ???
+
+                        exit when not In_Character_Range (C);
+                        Options (J) := Get_Character (C);
+
+                        if J = Slen then
+                           Set_Validity_Check_Options (Options);
+                           exit;
+                        else
+                           J := J + 1;
+                        end if;
+                     end loop;
+                  end;
+
+               elsif Nkind (A) = N_Identifier then
+                  if Chars (A) = Name_All_Checks then
+                     Set_Validity_Check_Options ("a");
+                  elsif Chars (A) = Name_On then
+                     Validity_Checks_On := True;
+                  elsif Chars (A) = Name_Off then
+                     Validity_Checks_On := False;
+                  end if;
                end if;
             end if;
          end Validity_Checks;
@@ -23119,7 +23129,7 @@ package body Sem_Prag is
         and then not Has_Null_State
       then
          Error_Msg_NE
-           ("useless refinement, subprogram & does not depends on abstract "
+           ("useless refinement, subprogram & does not depend on abstract "
             & "state with visible refinement", N, Spec_Id);
          return;
       end if;

gcc/ada/snames.ads-tmpl

@@ -1232,6 +1232,7 @@ package Snames is
    Name_Archive_Builder_Append_Option      : constant Name_Id := N + $;
    Name_Archive_Indexer                    : constant Name_Id := N + $;
    Name_Archive_Suffix                     : constant Name_Id := N + $;
+   Name_Artifacts                          : constant Name_Id := N + $;
    Name_Artifacts_In_Exec_Dir              : constant Name_Id := N + $; -- GB
    Name_Artifacts_In_Object_Dir            : constant Name_Id := N + $; -- GB
    Name_Binder                             : constant Name_Id := N + $;