diff options
Diffstat (limited to 'gcc/ada/gnat_rm.texi')
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 7a8b85505b4..edad79318e2 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -180,6 +180,7 @@ Implementation Defined Pragmas * Pragma Linker_Section:: * Pragma Long_Float:: * Pragma Loop_Optimize:: +* Pragma Loop_Variant:: * Pragma Machine_Attribute:: * Pragma Main:: * Pragma Main_Storage:: @@ -937,6 +938,7 @@ consideration, the use of these pragmas should be minimized. * Pragma Linker_Section:: * Pragma Long_Float:: * Pragma Loop_Optimize:: +* Pragma Loop_Variant:: * Pragma Machine_Attribute:: * Pragma Main:: * Pragma Main_Storage:: @@ -4040,6 +4042,45 @@ compiler in order to enable the relevant optimizations, that is to say @option{-funroll-loops} for unrolling and @option{-ftree-vectorize} for vectorization. +@node Pragma Loop_Variant +@unnumberedsec Pragma Loop_Variant +@findex Loop_Variant +@noindent +Syntax: + +@smallexample @c ada +pragma Loop_Variant ( LOOP_VARIANT_ITEM @{, LOOP_VARIANT_ITEM @} ); +LOOP_VARIANT_ITEM ::= CHANGE_DIRECTION => discrete_EXPRESSION +CHANGE_DIRECTION ::= Increases | Decreases +@end smallexample + +@noindent +This pragma must appear immediately within the sequence of statements of a +loop statement. It allows the specification of quantities which must always +decrease or increase in successive iterations of the loop. In its simplest +form, just one expression is specified, whose value must increase or decrease +on each iteration of the loop. + +In a more complex form, multiple arguments can be given which are intepreted +in a nesting lexicographic manner. For example: + +@smallexample @c ada +pragma Loop_Variant (Increases => X, Decreases => Y); +@end smallexample + +@noindent +specifies that each time through the loop either X increases, or X stays +the same and Y decreases. A @code{Loop_Variant} pragma ensures that the +loop is making progress. It can be useful in helping to show informally +or prove formally that the loop always terminates. + +@code{Loop_Variant} is an assertion whose effect can be controlled using +an @code{Assertion_Policy} with a check name of @code{Loop_Variant}. The +policy can be @code{Check} to enable the loop variant check, @code{Ignore} +to ignore the check (in which case the pragma has no effect on the program), +or @code{Disable} in which case the pragma is not even checked for correct +syntax. + @node Pragma Machine_Attribute @unnumberedsec Pragma Machine_Attribute @findex Machine_Attribute |