annotate doc/verify.texi @ 37203:2f0a7cf7ea66

verify: document some 'assume' pitfalls * doc/verify.texi (Compile-time Assertions): Mention that 'assume (E)' can sometimes slow things down. Use CHAR_MAX + 1, not UCHAR_MAX + 1.
author Paul Eggert <eggert@cs.ucla.edu>
date Thu, 10 Oct 2013 21:30:16 -0700
parents 2f1343191e67
children 344018b6e5d7
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
1 @c GNU verify module documentation
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
2
36940
c741bc27922a maint: update all copyright year number ranges
Eric Blake <eblake@redhat.com>
parents: 35930
diff changeset
3 @c Copyright (C) 2006, 2009-2013 Free Software Foundation, Inc.
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
4
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
5 @c Permission is granted to copy, distribute and/or modify this document
30453
655d9a8243af Change license to GFDLv1.3+.
Simon Josefsson <simon@josefsson.org>
parents: 26457
diff changeset
6 @c under the terms of the GNU Free Documentation License, Version 1.3
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
7 @c or any later version published by the Free Software Foundation;
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
8 @c with no Invariant Sections, no Front-Cover Texts, and no Back-Cover
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
9 @c Texts. A copy of the license is included in the ``GNU Free
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
10 @c Documentation License'' file as part of this distribution.
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
11
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
12 @node Compile-time Assertions
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
13 @section Compile-time Assertions
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
14
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
15 @cindex assertion
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
16 @findex verify
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
17 @findex verify_expr
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
18
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
19 This module provides a header file @file{verify.h} that defines
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
20 macros related to compile-time verification.
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
21
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
22 Two of these macros are @code{verify (@var{V})} and @code{verify_expr
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
23 (@var{V}, @var{EXPR})}. Both accept an integer constant expression
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
24 argument @var{V} and verify that it is nonzero. If not, a compile-time error
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
25 results.
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
26
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
27 These two macros implement compile-time tests, as opposed to
34443
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
28 the standard @code{assert} macro which supports only runtime tests.
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
29 Since the tests occur at compile-time, they are more reliable, and
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
30 they require no runtime overhead.
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
31
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
32 @code{verify (@var{V});} is a declaration; it can occur outside of
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
33 functions. In contrast, @code{verify_expr (@var{V}, @var{EXPR})} is
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
34 an expression that returns the value of @var{EXPR}; it can be used in
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
35 macros that expand to expressions. If @var{EXPR} is an integer
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
36 constant expression, then @code{verify_expr (@var{V}, @var{EXPR})} is
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
37 also an integer constant expression. Although @var{EXPR} and
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
38 @code{verify_expr (@var{V}, @var{EXPR})}@ are guaranteed to have the
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
39 same side effects and value and type (after integer promotion), they
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
40 need not have the same type if @var{EXPR}'s type is an integer that is
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
41 narrower than @code{int} or @code{unsigned int}.
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
42
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
43 @var{V} should be an integer constant expression in the sense
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
44 of the C standard. Its leaf operands should be integer, enumeration,
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
45 or character constants; or @code{sizeof} expressions that return
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
46 constants; or floating constants that are the immediate operands of
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
47 casts. Outside a @code{sizeof} subexpression, @var{V} should
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
48 not contain any assignments, function calls, comma operators, casts to
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
49 non-integer types, or subexpressions whose values are outside the
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
50 representable ranges for their types. If @var{V} is not an
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
51 integer constant expression, then a compiler might reject a usage like
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
52 @samp{verify (@var{V});} even when @var{V} is
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
53 nonzero.
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
54
35930
3bcc1fcf6faf doc: C11 and C++11 are now official
Paul Eggert <eggert@cs.ucla.edu>
parents: 35892
diff changeset
55 Although the standard @code{assert} macro is a runtime test, C11
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
56 specifies a builtin @code{_Static_assert (@var{V},
34443
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
57 @var{STRING-LITERAL})}, its @file{assert.h} header has a similar macro
35930
3bcc1fcf6faf doc: C11 and C++11 are now official
Paul Eggert <eggert@cs.ucla.edu>
parents: 35892
diff changeset
58 named @code{static_assert}, and C++11 has a similar
3bcc1fcf6faf doc: C11 and C++11 are now official
Paul Eggert <eggert@cs.ucla.edu>
parents: 35892
diff changeset
59 @code{static_assert} builtin. These builtins and macros differ
34443
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
60 from @code{verify} in two major ways. First, they can also be used
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
61 within a @code{struct} or @code{union} specifier, in place of an
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
62 ordinary member declaration. Second, they require the programmer to
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
63 specify a compile-time diagnostic as a string literal.
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
64
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
65 The @file{verify.h} header defines one more macro, @code{assume
37203
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
66 (@var{E})}, which expands to an expression of type @code{void}
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
67 that causes the compiler to assume that @var{E} yields a nonzero
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
68 value. @var{E} should be a scalar expression, and should not
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
69 have side effects; it may or may not be evaluated. The behavior is
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
70 undefined if @var{E} would yield zero. The main use of @code{assume}
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
71 is optimization, as the compiler may be able to generate better code
37203
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
72 if it assumes @var{E}. For best results, @var{E} should be simple
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
73 enough that a compiler can determine that it has no side effects: if
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
74 @var{E} calls an external function or accesses volatile storage the
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
75 compiler may not be able to optimize @var{E} away and @code{assume
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
76 (@var{E})} may therefore slow down the program.
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
77
37203
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
78 Here are some example uses of these macros.
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
79
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
80 @example
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
81 #include <verify.h>
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
82
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
83 #include <limits.h>
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
84 #include <time.h>
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
85
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
86 /* Verify that time_t is an integer type. */
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
87 verify ((time_t) 1.5 == 1);
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
88
34443
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
89 /* Verify that time_t is no smaller than int. */
93f57bb933fc verify: add doc to gnulib manual and fix example
Paul Eggert <eggert@cs.ucla.edu>
parents: 33770
diff changeset
90 verify (sizeof (int) <= sizeof (time_t));
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
91
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
92 /* Verify that time_t is signed. */
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
93 verify ((time_t) -1 < 0);
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
94
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
95 /* Verify that time_t uses two's complement representation. */
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
96 verify (~ (time_t) -1 == 0);
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
97
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
98 /* Return the maximum value of the integer type T,
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
99 verifying that T is an unsigned integer type.
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
100 The cast to (T) is outside the call to verify_expr
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
101 so that the result is of type T
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
102 even when T is narrower than unsigned int. */
34613
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
103 #define MAX_UNSIGNED_VAL(t) \
79a7919f1aa2 verify: new macro verify_expr; verify_true deprecated
Paul Eggert <eggert@cs.ucla.edu>
parents: 34443
diff changeset
104 ((T) verify_expr (0 < (T) -1, -1))
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
105
37203
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
106 /* Return T divided by CHAR_MAX + 1, where behavior is
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
107 undefined if T < 0. In the common case where CHAR_MAX
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
108 is 127 the compiler can therefore implement the division
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
109 by shifting T right 7 bits, an optimization that would
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
110 not be valid if T were negative. */
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
111 time_t
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
112 time_index (time_t t)
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
113 @{
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
114 assume (0 <= t);
37203
2f0a7cf7ea66 verify: document some 'assume' pitfalls
Paul Eggert <eggert@cs.ucla.edu>
parents: 37191
diff changeset
115 return t / (CHAR_MAX + 1);
37191
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
116 @}
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
117
2f1343191e67 verify: new macro 'assume'
Paul Eggert <eggert@cs.ucla.edu>
parents: 36940
diff changeset
118
26457
a18f48244638 * doc/verify.texi: New file.
Paul Eggert <eggert@cs.ucla.edu>
parents:
diff changeset
119 @end example