diff options
author | Robert Dewar <dewar@adacore.com> | 2013-04-24 13:18:21 +0000 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-04-24 15:18:21 +0200 |
commit | 7fab69059ec2423d61dfd7b5b30b0d5fc2173f9a (patch) | |
tree | bd8fedb5ef8a844095d0deffb14e0c2bb235b71d | |
parent | 1f50597830e668d54c3c08c26027e64ad92db85f (diff) | |
download | gcc-7fab69059ec2423d61dfd7b5b30b0d5fc2173f9a.zip gcc-7fab69059ec2423d61dfd7b5b30b0d5fc2173f9a.tar.gz gcc-7fab69059ec2423d61dfd7b5b30b0d5fc2173f9a.tar.bz2 |
gnat_rm.texi: Document pragma Assert_And_Cut.
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.
From-SVN: r198230
-rw-r--r-- | gcc/ada/ChangeLog | 6 | ||||
-rw-r--r-- | gcc/ada/gnat_rm.texi | 39 | ||||
-rw-r--r-- | gcc/ada/sem_prag.adb | 1 |
3 files changed, 42 insertions, 4 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f33d03b..b0eff53 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +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. + 2013-04-24 Ed Schonberg <schonberg@adacore.com> * sem_aux.adb: Add guard in Available_View. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index ae0e865..254dfdb 100644 --- a/gcc/ada/gnat_rm.texi +++ b/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 Attribute_Definition:: @@ -860,6 +861,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 Attribute_Definition:: @@ -1202,13 +1204,18 @@ Note that, as with the @code{if} statement to which it is equivalent, the type of the expression is either @code{Standard.Boolean}, or any type derived from this standard type. -If assertions are disabled (switch @option{-gnata} not used), then there +Assert checks can be either checked or ignored. By default they are ignored. +They will be checked if either the command line switch @option{-gnata} is +used, or if an @code{Assertion_Policy} or @code{Check_Policy} pragma is used +to enable @code{Assert_Checks}. + +If assertions are ignored, then there is no run-time effect (and in particular, any side effects from the expression will not occur at run time). (The expression is still analyzed at compile time, and may cause types to be frozen if they are mentioned here for the first time). -If assertions are enabled, then the given expression is tested, and if +If assertions are checked, then the given expression is tested, and if it is @code{False} then @code{System.Assertions.Raise_Assert_Failure} is called which results in the raising of @code{Assert_Failure} with the given message. @@ -1220,13 +1227,39 @@ semantic correctness whether or not assertions are enabled, so turning assertions on and off cannot affect the legality of a program. Note that the implementation defined policy @code{DISABLE}, given in a -pragma Assertion_Policy, can be used to suppress this semantic analysis. +pragma @code{Assertion_Policy}, can be used to suppress this semantic analysis. Note: this is a standard language-defined pragma in versions 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 is identical to that of pragma @code{Assert}, +except that in an @code{Assertion_Policy} pragma, the identifier +@code{Assert_And_Cut} is used to control whether it is ignored or checked +(or disabled). + +The intention is that this be used within a subprogram when the +given test expresion sums up all the work done so far in the +subprogram, so that the rest of the subprogram can be verified +(informally or formally) using only the entry preconditions, +and the expression in this pragma. This allows dividing up +a subprogram into sections for the purposes of testing or +formal verification. The pragma also serves as useful +documentation. + @node Pragma Assertion_Policy @unnumberedsec Pragma Assertion_Policy @findex Assertion_Policy diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 089c115..0b3b72c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -8849,7 +8849,6 @@ package body Sem_Prag is Ada_2005_Pragma; else -- Pragma_Assert_And_Cut GNAT_Pragma; - S14_Pragma; end if; Check_At_Least_N_Arguments (1); |