2013-04-12 Robert Dewar <dewar@adacore.com>

	* makeutl.adb, prj-nmsc.adb: Minor reformatting.

2013-04-12  Robert Dewar  <dewar@adacore.com>

	* exp_util.adb (Make_Invariant_Call): Use Check_Kind instead
	of Check_Enabled.
	* gnat_rm.texi (Check_Policy): Update documentation for new
	Check_Policy syntax.
	* sem_prag.adb (Check_Kind): Replaces Check_Enabled
	(Analyze_Pragma, case Check_Policy): Rework to accomodate new
	syntax (like Assertion_Policy).
	* sem_prag.ads (Check_Kind): Replaces Check_Enabled.



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

7 files changed, 217 insertions, 67 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c6e9cdd0270..e3661882299 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2013-04-12  Robert Dewar  <dewar@adacore.com>
+
+	* makeutl.adb, prj-nmsc.adb: Minor reformatting.
+
+2013-04-12  Robert Dewar  <dewar@adacore.com>
+
+	* exp_util.adb (Make_Invariant_Call): Use Check_Kind instead
+	of Check_Enabled.
+	* gnat_rm.texi (Check_Policy): Update documentation for new
+	Check_Policy syntax.
+	* sem_prag.adb (Check_Kind): Replaces Check_Enabled
+	(Analyze_Pragma, case Check_Policy): Rework to accomodate new
+	syntax (like Assertion_Policy).
+	* sem_prag.ads (Check_Kind): Replaces Check_Enabled.
+
 2013-04-12  Doug Rupp  <rupp@adacore.com>
 
 	* init.c (SS$_CONTROLC, SS$_CONTINUE) [VMS]: New macros.
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 38114c1f408..79b9d372afa 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -5456,7 +5456,7 @@ package body Exp_Util is
       pragma Assert
         (Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
 
-      if Check_Enabled (Name_Invariant) then
+      if Check_Kind (Name_Invariant) = Name_Check then
          return
            Make_Procedure_Call_Statement (Loc,
              Name                   =>
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index ce5a35d1b63..130ee3c0f72 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -1557,15 +1557,27 @@ pragma Check_Policy
  ([Name   =>] CHECK_KIND,
   [Policy =>] POLICY_IDENTIFIER);
 
-CHECK_KIND ::= IDENTIFIER |
-                   Pre'Class | Post'Class | Type_Invariant'Class
+Pragma Check_Policy (
+    CHECK_KIND => POLICY_IDENTIFIER
+ @{, CHECK_KIND => POLICY_IDENTIFIER@});
+
+ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
+
+CHECK_KIND ::= IDENTIFIER           |
+               Pre'Class            |
+               Post'Class           |
+               Type_Invariant'Class |
+               Invariant'Class
+
+The identifiers Name and Policy are not allowed as CHECK_KIND values. This
+avoids confusion between the two possible syntax forms for this pragma.
 
 POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE
 @end smallexample
 
 @noindent
 This pragma is used to set the checking policy for assertions (specified
-by aspects of pragmas), the @code{Debug} pragma, or additional checks
+by aspects or pragmas), the @code{Debug} pragma, or additional checks
 to be checked using the @code{Check} pragma. It may appear either as
 a configuration pragma, or within a declarative part of package. In the
 latter case, it applies from the point where it appears to the end of
@@ -1573,10 +1585,8 @@ the declarative region (like pragma @code{Suppress}).
 
 The @code{Check_Policy} pragma is similar to the
 predefined @code{Assertion_Policy} pragma,
-and if the first argument corresponds to one of the assertion kinds that
+and if the check kind corresponds to one of the assertion kinds that
 are allowed by @code{Assertion_Policy}, then the effect is identical.
-The identifiers @code{Precondition} and @code{Postcondition} are allowed
-synonyms for @code{Pre} and @code{Post}.
 
 If the first argument is Debug, then the policy applies to Debug pragmas,
 disabling their effect if the policy is @code{Off}, @code{Disable}, or
@@ -1605,9 +1615,8 @@ to turn on corresponding checks. The default for a set of checks for which no
 The check policy settings @code{CHECK} and @code{IGNORE} are recognized
 as synonyms for @code{ON} and @code{OFF}. These synonyms are provided for
 compatibility with the standard @code{Assertion_Policy} pragma. The check
-policy setting @code{DISABLE} is also synonymous with @code{OFF} in this
-context, but does not have any other significance for check
-names other than assertion kinds.
+policy setting @code{DISABLE} causes the second argument of a corresponding
+@code{Check} pragma to be completely ignored and not analyzed.
 
 @node Pragma Comment
 @unnumberedsec Pragma Comment
diff --git a/gcc/ada/makeutl.adb b/gcc/ada/makeutl.adb
index d81aa0a44f5..aef82cba856 100644
--- a/gcc/ada/makeutl.adb
+++ b/gcc/ada/makeutl.adb
@@ -1258,20 +1258,19 @@ package body Makeutl is
          while Obj_Proj /= No_Project loop
             if Obj_Proj.Object_Directory /= No_Path_Information then
                declare
-                  Dir  : constant String :=
-                    Get_Name_String
-                      (Obj_Proj.Object_Directory.Display_Name);
+                  Dir : constant String :=
+                    Get_Name_String (Obj_Proj.Object_Directory.Display_Name);
 
                   Object_Path : constant String :=
                     Normalize_Pathname
-                      (Name          =>
-                           Get_Name_String (Source.Object),
+                      (Name          => Get_Name_String (Source.Object),
                        Resolve_Links => Opt.Follow_Links_For_Files,
                        Directory     => Dir);
 
                   Obj_Path : constant Path_Name_Type :=
                     Create_Name (Object_Path);
-                  Stamp    : Time_Stamp_Type := Empty_Time_Stamp;
+
+                  Stamp : Time_Stamp_Type := Empty_Time_Stamp;
 
                begin
                   --  For specs, we do not check object files if there is a
@@ -1301,14 +1300,12 @@ package body Makeutl is
       elsif Source.Language.Config.Dependency_Kind = Makefile then
          declare
             Object_Dir : constant String :=
-                           Get_Name_String
-                             (Source.Project.Object_Directory.Display_Name);
+              Get_Name_String (Source.Project.Object_Directory.Display_Name);
             Dep_Path   : constant String :=
-                           Normalize_Pathname
-                             (Name        => Get_Name_String (Source.Dep_Name),
-                              Resolve_Links =>
-                                Opt.Follow_Links_For_Files,
-                              Directory     => Object_Dir);
+              Normalize_Pathname
+                (Name          => Get_Name_String (Source.Dep_Name),
+                 Resolve_Links => Opt.Follow_Links_For_Files,
+                 Directory     => Object_Dir);
          begin
             Source.Dep_Path := Create_Name (Dep_Path);
             Source.Dep_TS   := Osint.Unknown_Attributes;
@@ -1326,8 +1323,8 @@ package body Makeutl is
      (Env  : Prj.Tree.Environment;
       Argv : String) return Boolean
    is
-      Start     : Positive := 3;
-      Finish    : Natural := Argv'Last;
+      Start  : Positive := 3;
+      Finish : Natural := Argv'Last;
 
       pragma Assert (Argv'First = 1);
       pragma Assert (Argv (1 .. 2) = "-X");
diff --git a/gcc/ada/prj-nmsc.adb b/gcc/ada/prj-nmsc.adb
index c3b6ed5a8b3..751dab8dd08 100644
--- a/gcc/ada/prj-nmsc.adb
+++ b/gcc/ada/prj-nmsc.adb
@@ -3156,6 +3156,7 @@ package body Prj.Nmsc is
 
             if not Dir_Exists then
                if Directories_Must_Exist_In_Projects then
+
                   --  Get the absolute name of the library directory that does
                   --  not exist, to report an error.
 
@@ -3211,8 +3212,8 @@ package body Prj.Nmsc is
                              File_Name_Type (Dir_Elem.Value);
                            Error_Msg
                              (Data.Flags,
-                              "library directory cannot be the same " &
-                              "as source directory {",
+                              "library directory cannot be the same "
+                              & "as source directory {",
                               Lib_Dir.Location, Project);
                            OK := False;
                            exit;
@@ -3246,8 +3247,8 @@ package body Prj.Nmsc is
 
                                     Error_Msg
                                       (Data.Flags,
-                                       "library directory cannot be the same" &
-                                       " as source directory { of project %%",
+                                       "library directory cannot be the same "
+                                       & "as source directory { of project %%",
                                        Lib_Dir.Location, Project);
                                     OK := False;
                                     exit Project_Loop;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 8cd435b065b..0636b8e272b 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2320,12 +2320,12 @@ package body Sem_Prag is
          --  For a pragma PPC in the extended main source unit, record enabled
          --  status in SCO.
 
-         --  This may seem redundant with the call to Check_Enabled occurring
-         --  later on when the pragma is rewritten into a pragma Check but
-         --  is actually required in the case of a postcondition within a
+         --  This may seem redundant with the call to Check_Kind test that
+         --  occurs later on when the pragma is rewritten into a pragma Check
+         --  but is actually required in the case of a postcondition within a
          --  generic.
 
-         if Check_Enabled (Pname) and then not Split_PPC (N) then
+         if Check_Kind (Pname) = Name_Check and then not Split_PPC (N) then
             Set_SCO_Pragma_Enabled (Loc);
          end if;
 
@@ -6763,7 +6763,11 @@ package body Sem_Prag is
 
       Check_Applicable_Policy (N);
 
+      --  If pragma is disable, rewrite as Null statement and skip analysis
+
       if Is_Disabled (N) then
+         Rewrite (N, Make_Null_Statement (Loc));
+         Analyze (N);
          raise Pragma_Exit;
       end if;
 
@@ -7612,6 +7616,7 @@ package body Sem_Prag is
                --  now inserted all the equivalent Check pragmas.
 
                Rewrite (N, Make_Null_Statement (Loc));
+               Analyze (N);
             end if;
          end Assertion_Policy;
 
@@ -8096,7 +8101,32 @@ package body Sem_Prag is
             Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
             Check_Arg_Is_Identifier (Arg1);
             Cname := Chars (Get_Pragma_Arg (Arg1));
-            Check_On := Check_Enabled (Cname);
+
+            --  Set Check_On to indicate check status
+
+            case Check_Kind (Cname) is
+               when Name_Ignore =>
+                  Check_On := False;
+
+               when Name_Check =>
+                  Check_On := True;
+
+               --  For disable, rewrite pragma as null statement and skip
+               --  rest of the analysis of the pragma.
+
+               when Name_Disable =>
+                  Rewrite (N, Make_Null_Statement (Loc));
+                  Analyze (N);
+                  raise Pragma_Exit;
+
+               --  No other possibilities
+
+               when others =>
+                  raise Program_Error;
+            end case;
+
+            --  If check kind was not Disable, then continue pragma analysis
+
             Expr := Get_Pragma_Arg (Arg2);
 
             --  Deal with SCO generation
@@ -8233,24 +8263,36 @@ package body Sem_Prag is
          -- Check_Policy --
          ------------------
 
+         --  This is the old style syntax, which is still allowed in all modes:
+
          --  pragma Check_Policy ([Name   =>] CHECK_KIND
          --                       [Policy =>] POLICY_IDENTIFIER);
 
          --  POLICY_IDENTIFIER ::= On | Off | Check | Disable | Ignore
 
-         --  CHECK_KIND ::= IDENTIFIER |
-         --                 Pre'Class | Post'Class | Identifier'Class
+         --  CHECK_KIND ::= IDENTIFIER           |
+         --                 Pre'Class            |
+         --                 Post'Class           |
+         --                 Type_Invariant'Class |
+         --                 Invariant'Class
+
+         --  This is the new style syntax, compatible with Assertion_Policy
+         --  and also allowed in all modes.
+
+         --  Pragma Check_Policy (
+         --      CHECK_KIND => POLICY_IDENTIFIER
+         --   {, CHECK_KIND => POLICY_IDENTIFIER});
+
+         --  Note: the identifiers Name and Policy are not allowed as
+         --  Check_Kind values. This avoids ambiguities between the old and
+         --  new form syntax.
+
+         when Pragma_Check_Policy => Check_Policy : declare
+            Kind : Node_Id;
 
-         when Pragma_Check_Policy => Check_Policy :
          begin
             GNAT_Pragma;
-            Check_Arg_Count (2);
-            Check_Optional_Identifier (Arg1, Name_Name);
-            Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
-            Check_Arg_Is_Identifier (Arg1);
-            Check_Optional_Identifier (Arg2, Name_Policy);
-            Check_Arg_Is_One_Of
-              (Arg2, Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+            Check_At_Least_N_Arguments (1);
 
             --  A Check_Policy pragma can appear either as a configuration
             --  pragma, or in a declarative part or a package spec (see RM
@@ -8261,8 +8303,90 @@ package body Sem_Prag is
                Check_Is_In_Decl_Part_Or_Package_Spec;
             end if;
 
-            Set_Next_Pragma (N, Opt.Check_Policy_List);
-            Opt.Check_Policy_List := N;
+            --  Figure out if we have the old or new syntax. We have the
+            --  old syntax if the first argument has no identifier, or the
+            --  identifier is Name.
+
+            if Nkind (Arg1) /= N_Pragma_Argument_Association
+               or else Nam_In (Chars (Arg1), No_Name, Name_Name)
+            then
+               --  Old syntax
+
+               Check_Arg_Count (2);
+               Check_Optional_Identifier (Arg1, Name_Name);
+               Kind := Get_Pragma_Arg (Arg1);
+               Rewrite_Assertion_Kind (Kind);
+               Check_Arg_Is_Identifier (Arg1);
+
+               --  Check forbidden check kind
+
+               if Nam_In (Chars (Kind), Name_Name, Name_Policy) then
+                  Error_Msg_Name_2 := Chars (Kind);
+                     Error_Pragma_Arg
+                       ("pragma% does not allow% as check name", Arg1);
+               end if;
+
+               --  Check policy
+
+               Check_Optional_Identifier (Arg2, Name_Policy);
+               Check_Arg_Is_One_Of
+                 (Arg2,
+                  Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+
+               --  And chain pragma on the Check_Policy_List for search
+
+               Set_Next_Pragma (N, Opt.Check_Policy_List);
+               Opt.Check_Policy_List := N;
+
+            --  For the new syntax, what we do is to convert each argument to
+            --  an old syntax equivalent. We do that because we want to chain
+            --  old style Check_Pragmas for the search (we don't wnat to have
+            --  to deal with multiple arguments in the search)
+
+            else
+               declare
+                  Arg  : Node_Id;
+                  Argx : Node_Id;
+                  LocP : Source_Ptr;
+
+               begin
+                  Arg := Arg1;
+                  while Present (Arg) loop
+                     LocP := Sloc (Arg);
+                     Argx := Get_Pragma_Arg (Arg);
+
+                     --  Kind must be specified
+
+                     if Nkind (Arg) /= N_Pragma_Argument_Association
+                       or else Chars (Arg) = No_Name
+                     then
+                        Error_Pragma_Arg
+                          ("missing assertion kind for pragma%", Arg);
+                     end if;
+
+                     --  Construct equivalent old form syntax Check_Policy
+                     --  pragma and insert it to get remaining checks.
+
+                     Insert_Action (N,
+                       Make_Pragma (LocP,
+                         Chars                        => Name_Check_Policy,
+                         Pragma_Argument_Associations => New_List (
+                           Make_Pragma_Argument_Association (LocP,
+                             Expression =>
+                               Make_Identifier (LocP, Chars (Arg))),
+                           Make_Pragma_Argument_Association (Sloc (Argx),
+                             Expression => Argx))));
+
+                     Arg := Next (Arg);
+                  end loop;
+
+                  --  Rewrite original Check_Policy pragma to null, since we
+                  --  have converted it into a series of old syntax pragmas.
+
+                  Rewrite (N, Make_Null_Statement (Loc));
+                  Analyze (N);
+               end;
+            end if;
          end Check_Policy;
 
          ---------------------
@@ -17734,11 +17858,11 @@ package body Sem_Prag is
       when Pragma_Exit => null;
    end Analyze_Pragma;
 
-   -------------------
-   -- Check_Enabled --
-   -------------------
+   ----------------
+   -- Check_Kind --
+   ----------------
 
-   function Check_Enabled (Nam : Name_Id) return Boolean is
+   function Check_Kind (Nam : Name_Id) return Name_Id is
       PP : Node_Id;
 
    begin
@@ -17757,9 +17881,11 @@ package body Sem_Prag is
             then
                case (Chars (Get_Pragma_Arg (Last (PPA)))) is
                   when Name_On | Name_Check =>
-                     return True;
-                  when Name_Off | Name_Disable | Name_Ignore =>
-                     return False;
+                     return Name_Check;
+                  when Name_Off | Name_Ignore =>
+                     return Name_Ignore;
+                  when Name_Disable =>
+                     return Name_Disable;
                   when others =>
                      raise Program_Error;
                end case;
@@ -17775,8 +17901,12 @@ package body Sem_Prag is
       --  compatibility with the RM for the cases of assertion, invariant,
       --  precondition, predicate, and postcondition.
 
-      return Assertions_Enabled;
-   end Check_Enabled;
+      if Assertions_Enabled then
+         return Name_Check;
+      else
+         return Name_Ignore;
+      end if;
+   end Check_Kind;
 
    -----------------------------
    -- Check_Applicable_Policy --
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index f1e06b3fecf..38e39ed2f8a 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -54,7 +54,7 @@ package Sem_Prag is
    --  of the expressions in the pragma as "spec expressions" (see section
    --  in Sem "Handling of Default and Per-Object Expressions...").
 
-   function Check_Enabled (Nam : Name_Id) return Boolean;
+   function Check_Kind (Nam : Name_Id) return Name_Id;
    --  This function is used in connection with pragmas Assertion, Check,
    --  and assertion aspects and pragmas, to determine if Check pragmas
    --  (or corresponding assertion aspects or pragmas) are currently active
@@ -63,17 +63,15 @@ package Sem_Prag is
    --  Assertion_Policy as configuration pragmas either in a configuration
    --  pragma file, or at the start of the current unit, or locally given
    --  Check_Policy and Assertion_Policy pragmas that are currently active.
-   --  True is returned if the specified check is enabled.
    --
-   --  This function knows about all relevant synonyms (e.g. Precondition or
-   --  Pre can be used to refer to the Pre aspect or Precondition pragma, and
-   --  Predicate refers to both static and dynamic predicates, and Assertion
-   --  applies to all assertion aspects and pragmas).
+   --  The value returned is one of the names Check, Ignore, Disable (On
+   --  returns Check, and Off returns Ignore).
    --
-   --  Note: for assertion kinds Pre'Class, Post'Class, Type_Invariant'Class,
-   --  the name passed is Name_uPre, Name_uPost, Name_uType_Invariant, which
-   --  corresponds to _Pre, _Post, _Type_Invariant, which are special names
-   --  used in identifiers to represent these attribute references.
+   --  Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
+   --  and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
+   --  Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
+   --  _Post, _Invariant, or _Type_Invariant, which are special names used
+   --  in identifiers to represent these attribute references.
 
    procedure Check_Applicable_Policy (N : Node_Id);
    --  N is either an N_Aspect or an N_Pragma node. There are two cases. If
@@ -83,9 +81,9 @@ package Sem_Prag is
    --  we use for the purpose of this procedure is the aspect name, which may
    --  be different from the pragma name (e.g. Precondition for Pre aspect).
    --  In addition, 'Class aspects are recognized (and the corresponding
-   --  special names used in the processing.
+   --  special names used in the processing).
    --
-   --  If the name is valid assertion_Kind name, then the Check_Policy pragma
+   --  If the name is valid ASSERTION_KIND name, then the Check_Policy pragma
    --  chain is checked for a matching entry (or for an Assertion entry which
    --  matches all possibilities). If a matching entry is found then the policy
    --  is checked. If it is Off, Ignore, or Disable, then the Is_Ignored flag