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

gcc/ada/ChangeLog

 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.
 

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
 

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:
 

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

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

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 + $;