exp_prag.adb (Expand_Pragma_Check): Check for Assert rather than Assertion.

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

	* exp_prag.adb (Expand_Pragma_Check): Check for Assert rather
	than Assertion.
	* sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec
	(Effective_Name): New function (Analyze_Pragma, case Check):
	Disallow [Statement_]Assertions (Check_Kind): Implement
	Statement_Assertions (Check_Applicable_Policy): Use Effective_Name
	(Is_Valid_Assertion_Kind): Allow Statement_Assertions.
	* sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body
	(Effective_Name): New function.
	* sem_res.adb: Minor reformatting.
	* snames.ads-tmpl (Name_Statement_Assertions): New entry.
	* gnat_rm.texi: Add documentation of new assertion kind
	Statement_Assertions.

From-SVN: r198187

7 files changed, 205 insertions, 100 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 216d437..4bdf9e6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,21 @@
 2013-04-23  Robert Dewar  <dewar@adacore.com>
 
+	* exp_prag.adb (Expand_Pragma_Check): Check for Assert rather
+	than Assertion.
+	* sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec
+	(Effective_Name): New function (Analyze_Pragma, case Check):
+	Disallow [Statement_]Assertions (Check_Kind): Implement
+	Statement_Assertions (Check_Applicable_Policy): Use Effective_Name
+	(Is_Valid_Assertion_Kind): Allow Statement_Assertions.
+	* sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body
+	(Effective_Name): New function.
+	* sem_res.adb: Minor reformatting.
+	* snames.ads-tmpl (Name_Statement_Assertions): New entry.
+	* gnat_rm.texi: Add documentation of new assertion kind
+	Statement_Assertions.
+
+2013-04-23  Robert Dewar  <dewar@adacore.com>
+
 	* sinfo.ads, einfo.adb, sem_res.adb, exp_ch6.adb, aspects.adb: Minor
 	reformatting and code clean up.
 
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 38efb86..36191fb 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -377,7 +377,7 @@ package body Exp_Prag is
 
                --  For Assert, we just use the location
 
-               if Nam = Name_Assertion then
+               if Nam = Name_Assert then
                   null;
 
                --  For predicate, we generate the string "predicate failed
@@ -446,7 +446,7 @@ package body Exp_Prag is
          then
             return;
 
-         elsif Nam = Name_Assertion then
+         elsif Nam = Name_Assert then
             Error_Msg_N ("?A?assertion will fail at run time", N);
          else
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index a70a78d..a7c1514 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -1251,7 +1251,8 @@ RM_ASSERTION_KIND ::= Assert               |
                       Type_Invariant       |
                       Type_Invariant'Class
 
-ID_ASSERTION_KIND ::= Assert_And_Cut       |
+ID_ASSERTION_KIND ::= Assertions           |
+                      Assert_And_Cut       |
                       Assume               |
                       Contract_Cases       |
                       Debug                |
@@ -1262,6 +1263,7 @@ ID_ASSERTION_KIND ::= Assert_And_Cut       |
                       Postcondition        |
                       Precondition         |
                       Predicate
+                      Statement_Assertions
 
 POLICY_IDENTIFIER ::= Check | Disable | Ignore
 @end smallexample
@@ -1292,6 +1294,15 @@ useful when the pragma or aspect argument references subprograms
 in a with'ed package which is replaced by a dummy package
 for the final build.
 
+The implementation defined policy @code{Assertions} applies to all
+assertion kinds. The form with no assertion kind given implies this
+choice, so it applies to all assertion kinds (RM defined, and
+implementation defined).
+
+The implementation defined policy @code{Statement_Assertions}
+applies to @code{Assert}, @code{Assert_And_Cut},
+@code{Assume}, and @code{Loop_Invariant}.
+
 @node Pragma Assume_No_Invalid_Values
 @unnumberedsec Pragma Assume_No_Invalid_Values
 @findex Assume_No_Invalid_Values
@@ -1460,6 +1471,11 @@ Checks introduced by this pragma are normally deactivated by default. They can
 be activated either by the command line option @option{-gnata}, which turns on
 all checks, or individually controlled using pragma @code{Check_Policy}.
 
+The identifiers @code{Assertions} and @code{Statement_Assertions} are not
+permitted as check kinds, since this would cause confusion with the use
+of these identifiers in @code{Assertion_Policy} and @code{Check_Policy}
+pragmas, where they are used to refer to sets of assertions.
+
 @node Pragma Check_Float_Overflow
 @unnumberedsec Pragma Check_Float_Overflow
 @cindex Floating-point overflow
@@ -2860,7 +2876,18 @@ the standard runtime libraries be recompiled.
 The two argument form specifies the representation to be used for
 the specified floating-point type. On all systems other than OpenVMS,
 the argument must
-be @code{IEEE_Float} and the pragma has no effect. On OpenVMS, the
+be @code{IEEE_Float} to specify the use of IEEE format, as follows:
+
+@itemize @bullet
+@item
+For a digits value of 6, 32-bit IEEE short format will be used.
+@item
+For a digits value of 15, 64-bit IEEE long format will be used.
+@item
+No other value of digits is permitted.
+@end itemize
+
+On OpenVMS, the
 argument may be @code{VAX_Float} to specify the use of the VAX float
 format, as follows:
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index bacb340..f0045a3 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -181,13 +181,6 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
-   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
-   --  Returns True if Nam is one of the names recognized as a valid assertion
-   --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
-   --  represented by the corresponding special names Name_uPre, Name_uPost,
-   --  Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-   --  and _Type_Invariant).
-
    procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
    --  Preanalyze the boolean expressions in the Requires and Ensures arguments
    --  of a Test_Case pragma if present (possibly Empty). We treat these as
@@ -352,9 +345,7 @@ package body Sem_Prag is
       --  In ASIS mode, for a pragma generated from a source aspect, also
       --  analyze the original aspect expression.
 
-      if ASIS_Mode
-        and then Present (Corresponding_Aspect (N))
-      then
+      if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
          Preanalyze_Assert_Expression
            (Expression (Corresponding_Aspect (N)), Standard_Boolean);
       end if;
@@ -2222,9 +2213,7 @@ package body Sem_Prag is
                --  In ASIS mode, for a pragma generated from a source aspect,
                --  also analyze the original aspect expression.
 
-               if ASIS_Mode
-                 and then Present (Corresponding_Aspect (N))
-               then
+               if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
                   Preanalyze_Assert_Expression
                     (Expression (Corresponding_Aspect (N)), Standard_Boolean);
                end if;
@@ -2411,9 +2400,7 @@ package body Sem_Prag is
          --  In ASIS mode, for a pragma generated from a source aspect, also
          --  analyze the original aspect expression.
 
-         if ASIS_Mode
-           and then Present (Corresponding_Aspect (N))
-         then
+         if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
             Check_Expr_Is_Static_Expression
               (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String);
          end if;
@@ -2882,10 +2869,7 @@ package body Sem_Prag is
 
             --  Get name from corresponding aspect
 
-            if Present (Corresponding_Aspect (N)) then
-               Error_Msg_Name_1 :=
-                 Chars (Identifier (Corresponding_Aspect (N)));
-            end if;
+            Error_Msg_Name_1 := Effective_Name (N);
          end if;
       end Fix_Error;
 
@@ -6765,10 +6749,7 @@ package body Sem_Prag is
       --  Here to start processing for recognized pragma
 
       Prag_Id := Get_Pragma_Id (Pname);
-
-      if Present (Corresponding_Aspect (N)) then
-         Pname := Chars (Identifier (Corresponding_Aspect (N)));
-      end if;
+      Pname := Effective_Name (N);
 
       --  Check applicable policy. We skip this for a pragma that came from
       --  an aspect, since we already dealt with the Disable case, and we set
@@ -7426,9 +7407,9 @@ package body Sem_Prag is
             Check_Arg_Order ((Name_Check, Name_Message));
             Check_Optional_Identifier (Arg1, Name_Check);
 
-            --  We treat pragma Assert as equivalent to:
+            --  We treat pragma Assert[_And_Cut] as equivalent to:
 
-            --    pragma Check (Assertion, condition [, msg]);
+            --    pragma Check (Assert[_And_Cut], condition [, msg]);
 
             --  So rewrite pragma in this manner, transfer the message
             --  argument if present, and analyze the result
@@ -7443,8 +7424,7 @@ package body Sem_Prag is
             Expr := Get_Pragma_Arg (Arg1);
             Newa := New_List (
               Make_Pragma_Argument_Association (Loc,
-                Expression => Make_Identifier (Loc, Name_Assertion)),
-
+                Expression => Make_Identifier (Loc, Pname)),
               Make_Pragma_Argument_Association (Sloc (Expr),
                 Expression => Expr));
 
@@ -8083,6 +8063,9 @@ package body Sem_Prag is
          --                 Invariant'Class      |
          --                 Type_Invariant'Class
 
+         --  The identifiers Assertions and Statement_Assertions are not
+         --  allowed, since they have special meaning for Check_Policy.
+
          when Pragma_Check => Check : declare
             Expr  : Node_Id;
             Eloc  : Source_Ptr;
@@ -8108,6 +8091,23 @@ package body Sem_Prag is
             Check_Arg_Is_Identifier (Arg1);
             Cname := Chars (Get_Pragma_Arg (Arg1));
 
+            --  Check forbidden name Assertions or Statement_Assertions
+
+            case Cname is
+               when Name_Assertions =>
+                  Error_Pragma_Arg
+                    ("""Assertions"" is not allowed as a check kind "
+                     & "for pragma%", Arg1);
+
+               when Name_Statement_Assertions =>
+                  Error_Pragma_Arg
+                    ("""Statement_Assertions"" is not allowed as a check kind "
+                     & "for pragma%", Arg1);
+
+               when others =>
+                  null;
+            end case;
+
             --  Set Check_On to indicate check status
 
             --  If this comes from an aspect, we have already taken care of
@@ -17945,8 +17945,13 @@ package body Sem_Prag is
 
          begin
             if Nam = Pnm
-              or else (Is_Valid_Assertion_Kind (Nam)
-                        and then Pnm = Name_Assertion)
+              or else (Pnm = Name_Assertion
+                        and then Is_Valid_Assertion_Kind (Nam))
+              or else (Pnm = Name_Statement_Assertions
+                        and then Nam_In (Nam, Name_Assert,
+                                              Name_Assert_And_Cut,
+                                              Name_Assume,
+                                              Name_Loop_Invariant))
             then
                case (Chars (Get_Pragma_Arg (Last (PPA)))) is
                   when Name_On | Name_Check =>
@@ -17985,36 +17990,9 @@ package body Sem_Prag is
       PP     : Node_Id;
       Policy : Name_Id;
 
-      Ename : Name_Id;
-      --  Effective name of aspect or pragma, this is simply the name of
-      --  the aspect or pragma, except in the case of a pragma derived from
-      --  an aspect, in which case it is the name of the aspect (which may be
-      --  different, e.g. Pre aspect generating Precondition pragma). It also
-      --  deals with the 'Class cases for an aspect.
+      Ename : constant Name_Id := Effective_Name (N);
 
    begin
-      if Nkind (N) = N_Pragma then
-         if Present (Corresponding_Aspect (N)) then
-            Ename := Chars (Identifier (Corresponding_Aspect (N)));
-         else
-            Ename := Chars (Pragma_Identifier (N));
-         end if;
-
-      else
-         pragma Assert (Nkind (N) = N_Aspect_Specification);
-         Ename := Chars (Identifier (N));
-
-         if Class_Present (N) then
-            case Ename is
-               when Name_Invariant      => Ename := Name_uInvariant;
-               when Name_Pre            => Ename := Name_uPre;
-               when Name_Post           => Ename := Name_uPost;
-               when Name_Type_Invariant => Ename := Name_uType_Invariant;
-               when others              => raise Program_Error;
-            end case;
-         end if;
-      end if;
-
       --  No effect if not valid assertion kind name
 
       if not Is_Valid_Assertion_Kind (Ename) then
@@ -18072,6 +18050,66 @@ package body Sem_Prag is
                                       Name_Priority_Specific_Dispatching);
    end Delay_Config_Pragma_Analyze;
 
+   --------------------
+   -- Effective_Name --
+   --------------------
+
+   function Effective_Name (N : Node_Id) return Name_Id is
+      Pras : Node_Id;
+      Name : Name_Id;
+
+   begin
+      pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
+      Pras := N;
+
+      if Is_Rewrite_Substitution (Pras)
+        and then Nkind (Original_Node (Pras)) = N_Pragma
+      then
+         Pras := Original_Node (Pras);
+      end if;
+
+      --  Case where we came from aspect specication
+
+      if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
+         Pras := Corresponding_Aspect (Pras);
+      end if;
+
+      --  Get name from aspect or pragma
+
+      if Nkind (Pras) = N_Pragma then
+         Name := Pragma_Name (Pras);
+      else
+         Name := Chars (Identifier (Pras));
+      end if;
+
+      --  Deal with 'Class
+
+      if Class_Present (Pras) then
+         case Name is
+
+         --  Names that need converting to special _xxx form
+
+            when Name_Pre             => Name := Name_uPre;
+            when Name_Post            => Name := Name_uPost;
+            when Name_Invariant       => Name := Name_uInvariant;
+            when Name_Type_Invariant  => Name := Name_uType_Invariant;
+
+               --  Names already in special _xxx form (leave them alone)
+
+            when Name_uPre            => null;
+            when Name_uPost           => null;
+            when Name_uInvariant      => null;
+            when Name_uType_Invariant => null;
+
+               --  Anything else is impossible with Class_Present set True
+
+            when others               => raise Program_Error;
+         end case;
+      end if;
+
+      return Name;
+   end Effective_Name;
+
    -------------------------
    -- Get_Base_Subprogram --
    -------------------------
@@ -18521,31 +18559,32 @@ package body Sem_Prag is
          when
             --  RM defined
 
-            Name_Assert            |
-            Name_Static_Predicate  |
-            Name_Dynamic_Predicate |
-            Name_Pre               |
-            Name_uPre              |
-            Name_Post              |
-            Name_uPost             |
-            Name_Type_Invariant    |
-            Name_uType_Invariant   |
+            Name_Assert               |
+            Name_Static_Predicate     |
+            Name_Dynamic_Predicate    |
+            Name_Pre                  |
+            Name_uPre                 |
+            Name_Post                 |
+            Name_uPost                |
+            Name_Type_Invariant       |
+            Name_uType_Invariant      |
 
             --  Impl defined
 
-            Name_Assert_And_Cut    |
-            Name_Assume            |
-            Name_Contract_Cases    |
-            Name_Debug             |
-            Name_Invariant         |
-            Name_uInvariant        |
-            Name_Loop_Invariant    |
-            Name_Loop_Variant      |
-            Name_Postcondition     |
-            Name_Precondition      |
-            Name_Predicate         => return True;
-
-         when others               => return False;
+            Name_Assert_And_Cut       |
+            Name_Assume               |
+            Name_Contract_Cases       |
+            Name_Debug                |
+            Name_Invariant            |
+            Name_uInvariant           |
+            Name_Loop_Invariant       |
+            Name_Loop_Variant         |
+            Name_Postcondition        |
+            Name_Precondition         |
+            Name_Predicate            |
+            Name_Statement_Assertions => return True;
+
+         when others                  => return False;
       end case;
    end Is_Valid_Assertion_Kind;
 
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 860005e..54ddc43 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -104,10 +104,30 @@ package Sem_Prag is
    --  True have their analysis delayed until after the main program is parsed
    --  and analyzed.
 
+   function Effective_Name (N : Node_Id) return Name_Id;
+   --  N is a pragma node or aspect specification node. This function returns
+   --  the name of the pragma or aspect, taking into account possible rewrites,
+   --  and also cases where a pragma comes from an attribute (in such cases,
+   --  the name can be different from the pragma name, e.g. Pre generates
+   --  a Precondition pragma. This also deals with the presence of 'Class
+   --  which results in one of the special names Name_uPre, Name_uPost,
+   --  Name_uInvariant, or Name_uType_Invariant being returned to represent
+   --  the corresponding aspects with x'Class names.
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
 
+   function Is_Config_Static_String (Arg : Node_Id) return Boolean;
+   --  This is called for a configuration pragma that requires either string
+   --  literal or a concatenation of string literals. We cannot use normal
+   --  static string processing because it is too early in the case of the
+   --  pragma appearing in a configuration pragmas file. If Arg is of an
+   --  appropriate form, then this call obtains the string (doing any necessary
+   --  concatenations) and places it in Name_Buffer, setting Name_Len to its
+   --  length, and then returns True. If it is not of the correct form, then an
+   --  appropriate error message is posted, and False is returned.
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
@@ -124,15 +144,12 @@ package Sem_Prag is
    --  False is returned, then the argument is treated as an entity reference
    --  to the operator.
 
-   function Is_Config_Static_String (Arg : Node_Id) return Boolean;
-   --  This is called for a configuration pragma that requires either string
-   --  literal or a concatenation of string literals. We cannot use normal
-   --  static string processing because it is too early in the case of the
-   --  pragma appearing in a configuration pragmas file. If Arg is of an
-   --  appropriate form, then this call obtains the string (doing any necessary
-   --  concatenations) and places it in Name_Buffer, setting Name_Len to its
-   --  length, and then returns True. If it is not of the correct form, then an
-   --  appropriate error message is posted, and False is returned.
+   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
+   --  Returns True if Nam is one of the names recognized as a valid assertion
+   --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
+   --  represented by the corresponding special names Name_uPre, Name_uPost,
+   --  Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
+   --  and _Type_Invariant).
 
    procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id);
    --  This routine makes aspects from precondition or postcondition pragmas
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 1cb465a..6a0f666 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -8908,27 +8908,32 @@ package body Sem_Res is
             Orig : constant Node_Id := Original_Node (Parent (N));
 
          begin
+            --  Special handling of Asssert pragma
+
             if Nkind (Orig) = N_Pragma
               and then Pragma_Name (Orig) = Name_Assert
             then
-               --  Don't want to warn if original condition is explicit False
-
                declare
                   Expr : constant Node_Id :=
                            Original_Node
                              (Expression
                                (First (Pragma_Argument_Associations (Orig))));
+
                begin
+                  --  Don't warn if original condition is explicit False,
+                  --  since obviously the failure is expected in this case.
+
                   if Is_Entity_Name (Expr)
                     and then Entity (Expr) = Standard_False
                   then
                      null;
-                  else
-                     --  Issue warning. We do not want the deletion of the
-                     --  IF/AND-THEN to take this message with it. We achieve
-                     --  this by making sure that the expanded code points to
-                     --  the Sloc of the expression, not the original pragma.
 
+                  --  Issue warning. We do not want the deletion of the
+                  --  IF/AND-THEN to take this message with it. We achieve this
+                  --  by making sure that the expanded code points to the Sloc
+                  --  of the expression, not the original pragma.
+
+                  else
                      --  Note: Use Error_Msg_F here rather than Error_Msg_N.
                      --  The source location of the expression is not usually
                      --  the best choice here. For example, it gets located on
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index d1854b2..ad98f55 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -761,6 +761,7 @@ package Snames is
    Name_Simple_Barriers                : constant Name_Id := N + $;
    Name_Spec_File_Name                 : constant Name_Id := N + $;
    Name_State                          : constant Name_Id := N + $;
+   Name_Statement_Assertions           : constant Name_Id := N + $;
    Name_Static                         : constant Name_Id := N + $;
    Name_Stack_Size                     : constant Name_Id := N + $;
    Name_Strict                         : constant Name_Id := N + $;