gnat_rm.texi: Document pragma Assume.

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

	* gnat_rm.texi: Document pragma Assume.
	* sem_prag.adb (Analyze_Pragma, case Assume): Now processed as
	part of Assert, and no longer requires -gnatd.F

From-SVN: r198231

3 files changed, 53 insertions, 33 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b0eff53..5859010 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,11 @@
 2013-04-24  Robert Dewar  <dewar@adacore.com>
 
+	* gnat_rm.texi: Document pragma Assume.
+	* sem_prag.adb (Analyze_Pragma, case Assume): Now processed as
+	part of Assert, and no longer requires -gnatd.F
+
+2013-04-24  Robert Dewar  <dewar@adacore.com>
+
 	* gnat_rm.texi: Document pragma Assert_And_Cut.
 	* sem_prag.adb (Analyze_Pragma, case Assert_And_Cut): Remove
 	S14_Pragma call.
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 254dfdb..7a8b855 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -107,6 +107,7 @@ Implementation Defined Pragmas
 * Pragma Assert::
 * Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
+* Pragma Assume::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Attribute_Definition::
 * Pragma Ast_Entry::
@@ -863,6 +864,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Assert::
 * Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
+* Pragma Assume::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Attribute_Definition::
 * Pragma Ast_Entry::
@@ -1336,6 +1338,40 @@ The implementation defined policy @code{Statement_Assertions}
 applies to @code{Assert}, @code{Assert_And_Cut},
 @code{Assume}, and @code{Loop_Invariant}.
 
+@node Pragma Assume
+@unnumberedsec Pragma Assume
+@findex Assume
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Assume (
+  boolean_EXPRESSION
+  [, string_EXPRESSION]);
+@end smallexample
+
+@noindent
+The effect of this pragma is identical to that of pragma @code{Assert},
+except that in an @code{Assertion_Policy} pragma, the identifier
+@code{Assume} is used to control whether it is ignored or checked
+(or disabled).
+
+The intention is that this be used for assumptions about the
+external environment. So you cannot expect to verify formally
+or informally that the condition is met, this must be
+established by examining things outside the program itself.
+For example, we may have code that depends on the size of
+@code{Long_Long_Integer} being at least 64. So we could write:
+
+@smallexample @c ada
+pragma Assume (Long_Long_Integer'Size >= 64);
+@end smallexample
+
+@noindent
+This assumption cannot be proved from the program itself,
+but it acts as a useful run-time check that the assumption
+is met, and documents the need to ensure that it is met by
+reference to information outside the program.
+
 @node Pragma Assume_No_Invalid_Values
 @unnumberedsec Pragma Assume_No_Invalid_Values
 @findex Assume_No_Invalid_Values
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0b3b72c..c89ca84 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -8828,9 +8828,9 @@ package body Sem_Prag is
             end if;
          end Annotate;
 
-         ---------------------------
-         -- Assert/Assert_And_Cut --
-         ---------------------------
+         ----------------------------------
+         -- Assert/Assert_And_Cut/Assume --
+         ----------------------------------
 
          --  pragma Assert
          --    (   [Check => ]  Boolean_EXPRESSION
@@ -8840,7 +8840,14 @@ package body Sem_Prag is
          --    (   [Check => ]  Boolean_EXPRESSION
          --     [, [Message =>] Static_String_EXPRESSION]);
 
-         when Pragma_Assert | Pragma_Assert_And_Cut => Assert : declare
+         --  pragma Assume
+         --    (   [Check => ]  Boolean_EXPRESSION
+         --     [, [Message =>] Static_String_EXPRESSION]);
+
+         when Pragma_Assert         |
+              Pragma_Assert_And_Cut |
+              Pragma_Assume         =>
+         Assert : declare
             Expr : Node_Id;
             Newa : List_Id;
 
@@ -9056,35 +9063,6 @@ package body Sem_Prag is
             end if;
          end Assertion_Policy;
 
-         ------------
-         -- Assume --
-         ------------
-
-         --  pragma Assume (boolean_EXPRESSION);
-
-         when Pragma_Assume => Assume : declare
-         begin
-            GNAT_Pragma;
-            S14_Pragma;
-            Check_Arg_Count (1);
-
-            --  Pragma Assume is transformed into pragma Check in the following
-            --  manner:
-
-            --    pragma Check (Assume, Expr);
-
-            Rewrite (N,
-              Make_Pragma (Loc,
-                Chars                        => Name_Check,
-                Pragma_Argument_Associations => New_List (
-                  Make_Pragma_Argument_Association (Loc,
-                    Expression => Make_Identifier (Loc, Name_Assume)),
-
-                  Make_Pragma_Argument_Association (Loc,
-                    Expression => Relocate_Node (Expression (Arg1))))));
-            Analyze (N);
-         end Assume;
-
          ------------------------------
          -- Assume_No_Invalid_Values --
          ------------------------------