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.
* Pragma Assert::
* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
+* Pragma Assume::
* Pragma Assume_No_Invalid_Values::
* Pragma Attribute_Definition::
* Pragma Ast_Entry::
* Pragma Assert::
* Pragma Assert_And_Cut::
* Pragma Assertion_Policy::
+* Pragma Assume::
* Pragma Assume_No_Invalid_Values::
* Pragma Attribute_Definition::
* Pragma Ast_Entry::
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
end if;
end Annotate;
- ---------------------------
- -- Assert/Assert_And_Cut --
- ---------------------------
+ ----------------------------------
+ -- Assert/Assert_And_Cut/Assume --
+ ----------------------------------
-- pragma Assert
-- ( [Check => ] Boolean_EXPRESSION
-- ( [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;
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 --
------------------------------