[multiple changes]

2012-10-29  Arnaud Charlet  <charlet@adacore.com>

	* s-win32.ads: Kill potential warning.

2012-10-29  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Describe new pragma Assert_And_Cut.
	* par-prag.adb, sem_prag.adb, snames.ads-tmpl: Add new pragma
	and treat it like pragma Assert.

From-SVN: r192923

gcc/ada/gnat_rm.texi

@@ -105,6 +105,7 @@ Implementation Defined Pragmas
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
+* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -843,6 +844,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
+* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -1195,6 +1197,22 @@ of Ada from 2005 on. In GNAT, it is implemented in all versions
 of Ada, and the DISABLE policy is an implementation-defined
 addition.
 
+@node Pragma Assert_And_Cut
+@unnumberedsec Pragma Assert_And_Cut
+@findex Assert_And_Cut
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Assert_And_Cut (
+  boolean_EXPRESSION
+  [, string_EXPRESSION]);
+@end smallexample
+
+@noindent
+The effect of this pragma for compilation is exactly the same as the one
+of pragma @code{Assert}. This pragma is used to help formal verification
+tools by marking program points where the tool can simplify precise
+knowledge about execution based on the assertion given.
 
 @node Pragma Assertion_Policy
 @unnumberedsec Pragma Assertion_Policy

gcc/ada/par-prag.adb

@@ -1098,6 +1098,7 @@ begin
            Pragma_All_Calls_Remote               |
            Pragma_Annotate                       |
            Pragma_Assert                         |
+           Pragma_Assert_And_Cut                 |
            Pragma_Asynchronous                   |
            Pragma_Atomic                         |
            Pragma_Atomic_Components              |

gcc/ada/s-win32.ads

@@ -32,7 +32,7 @@
 --  This package plus its child provide the low level interface to the Win32
 --  API. The core part of the Win32 API (common to RTX and Win32) is in this
 --  package, and an additional part of the Win32 API which is not supported by
---  RTX is in package System.Win33.Ext.
+--  RTX is in package System.Win32.Ext.
 
 with Interfaces.C;
 
@@ -73,8 +73,13 @@ package System.Win32 is
    for Bits2'Size  use 2;
    for Bits17'Size use 17;
 
+   --  Note that the following clashes with standard names are to stay
+   --  compatible with the historical choice of following the C names.
+
+   pragma Warnings (Off);
    FALSE : constant := 0;
    TRUE  : constant := 1;
+   pragma Warnings (On);
 
    function GetLastError return DWORD;
    pragma Import (Stdcall, GetLastError, "GetLastError");

gcc/ada/sem_prag.adb

@@ -6759,14 +6759,17 @@ package body Sem_Prag is
             end if;
          end Annotate;
 
-         ------------
-         -- Assert --
-         ------------
+         -----------------------------
+         -- Assert & Assert_And_Cut --
+         -----------------------------
 
          --  pragma Assert ([Check =>] Boolean_EXPRESSION
          --                 [, [Message =>] Static_String_EXPRESSION]);
 
-         when Pragma_Assert => Assert : declare
+         --  pragma Assert_And_Cut ([Check =>] Boolean_EXPRESSION
+         --                         [, [Message =>] Static_String_EXPRESSION]);
+
+         when Pragma_Assert | Pragma_Assert_And_Cut => Assert : declare
             Expr : Node_Id;
             Newa : List_Id;
 
@@ -6784,6 +6787,13 @@ package body Sem_Prag is
             --  So rewrite pragma in this manner, transfer the message
             --  argument if present, and analyze the result
 
+            --  Pragma Assert_And_Cut is treated exactly like pragma Assert by
+            --  the frontend. Formal verification tools may use it to "cut" the
+            --  paths through the code, to make verification tractable. When
+            --  dealing with a semantically analyzed tree, the information that
+            --  a Check node N corresponds to a source Assert_And_Cut pragma
+            --  can be retrieved from the pragma kind of Original_Node(N).
+
             Expr := Get_Pragma_Arg (Arg1);
             Newa := New_List (
               Make_Pragma_Argument_Association (Loc,
@@ -15185,6 +15195,7 @@ package body Sem_Prag is
       Pragma_All_Calls_Remote               => -1,
       Pragma_Annotate                       => -1,
       Pragma_Assert                         => -1,
+      Pragma_Assert_And_Cut                 => -1,
       Pragma_Assertion_Policy               =>  0,
       Pragma_Assume_No_Invalid_Values       =>  0,
       Pragma_Asynchronous                   => -1,

gcc/ada/snames.ads-tmpl

@@ -448,6 +448,7 @@ package Snames is
    --  correctly recognize and process Name_AST_Entry.
 
    Name_Assert                         : constant Name_Id := N + $; -- Ada 05
+   Name_Assert_And_Cut                 : constant Name_Id := N + $; -- GNAT
    Name_Asynchronous                   : constant Name_Id := N + $;
    Name_Atomic                         : constant Name_Id := N + $;
    Name_Atomic_Components              : constant Name_Id := N + $;
@@ -1697,6 +1698,7 @@ package Snames is
       Pragma_Abort_Defer,
       Pragma_All_Calls_Remote,
       Pragma_Assert,
+      Pragma_Assert_And_Cut,
       Pragma_Asynchronous,
       Pragma_Atomic,
       Pragma_Atomic_Components,