Mercurial > gnulib
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 |
rev | line source |
---|---|
26457 | 1 @c GNU verify module documentation |
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 | 4 |
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 | 7 @c or any later version published by the Free Software Foundation; |
8 @c with no Invariant Sections, no Front-Cover Texts, and no Back-Cover | |
9 @c Texts. A copy of the license is included in the ``GNU Free | |
10 @c Documentation License'' file as part of this distribution. | |
11 | |
12 @node Compile-time Assertions | |
13 @section Compile-time Assertions | |
14 | |
15 @cindex assertion | |
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 | 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 | 29 Since the tests occur at compile-time, they are more reliable, and |
30 they require no runtime overhead. | |
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 | 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 | 44 of the C standard. Its leaf operands should be integer, enumeration, |
45 or character constants; or @code{sizeof} expressions that return | |
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 | 48 not contain any assignments, function calls, comma operators, casts to |
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 | 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 | 53 nonzero. |
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 | 79 |
80 @example | |
81 #include <verify.h> | |
82 | |
83 #include <limits.h> | |
84 #include <time.h> | |
85 | |
86 /* Verify that time_t is an integer type. */ | |
87 verify ((time_t) 1.5 == 1); | |
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 | 91 |
92 /* Verify that time_t is signed. */ | |
93 verify ((time_t) -1 < 0); | |
94 | |
95 /* Verify that time_t uses two's complement representation. */ | |
96 verify (~ (time_t) -1 == 0); | |
97 | |
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 | 101 so that the result is of type T |
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 | 119 @end example |