1 /* Test the "verify" module.
2
3 Copyright (C) 2005, 2009-2021 Free Software Foundation, Inc.
4
5 This program is free software: you can redistribute it and/or modify
6 it under the terms of the GNU General Public License as published by
7 the Free Software Foundation; either version 3 of the License, or
8 (at your option) any later version.
9
10 This program is distributed in the hope that it will be useful,
11 but WITHOUT ANY WARRANTY; without even the implied warranty of
12 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 GNU General Public License for more details.
14
15 You should have received a copy of the GNU General Public License
16 along with this program. If not, see <https://www.gnu.org/licenses/>. */
17
18 /* Written by Bruno Haible. */
19
20 #include <config.h>
21
22 #include "verify.h"
23
24 #ifndef EXP_FAIL
25 # define EXP_FAIL 0
26 #endif
27
28 /* ======================= Test verify, verify_expr ======================= */
29
30 int gx;
31 enum { A, B, C };
32
33 #if EXP_FAIL == 1
34 verify (gx >= 0); /* should give ERROR: non-constant expression */
35 #endif
36 verify (C == 2); /* should be ok */
37 #if EXP_FAIL == 2
38 verify (1 + 1 == 3); /* should give ERROR */
39 #endif
40 verify (1 == 1); verify (1 == 1); /* should be ok */
41
42 enum
43 {
44 item = verify_expr (1 == 1, 10 * 0 + 17) /* should be ok */
45 };
46
47 static int
48 function (int n)
/* ![[previous]](../icons/n_left.png)
![[next]](../icons/right.png)
![[first]](../icons/n_first.png)
![[last]](../icons/last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
49 {
50 #if EXP_FAIL == 3
51 verify (n >= 0); /* should give ERROR: non-constant expression */
52 #endif
53 verify (C == 2); /* should be ok */
54 #if EXP_FAIL == 4
55 verify (1 + 1 == 3); /* should give ERROR */
56 #endif
57 verify (1 == 1); verify (1 == 1); /* should be ok */
58
59 if (n)
60 return ((void) verify_expr (1 == 1, 1), verify_expr (1 == 1, 8)); /* should be ok */
61 #if EXP_FAIL == 5
62 return verify_expr (1 == 2, 5); /* should give ERROR */
63 #endif
64 return 0;
65 }
66
67 /* ============================== Test assume ============================== */
68
69 static int
70 f (int a)
/* ![[previous]](../icons/left.png)
![[next]](../icons/right.png)
![[first]](../icons/first.png)
![[last]](../icons/last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
71 {
72 return a;
73 }
74
75 typedef struct { unsigned int context : 4; unsigned int halt : 1; } state;
76
77 void test_assume_expressions (state *s);
78 int test_assume_optimization (int x);
79 _Noreturn void test_assume_noreturn (void);
80
81 void
82 test_assume_expressions (state *s)
/* ![[previous]](../icons/left.png)
![[next]](../icons/right.png)
![[first]](../icons/first.png)
![[last]](../icons/last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
83 {
84 /* Check that 'assume' accepts a function call, even of a non-const
85 function. */
86 assume (f (1));
87 /* Check that 'assume' accepts a bit-field expression. */
88 assume (s->halt);
89 }
90
91 int
92 test_assume_optimization (int x)
/* ![[previous]](../icons/left.png)
![[next]](../icons/right.png)
![[first]](../icons/first.png)
![[last]](../icons/last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
93 {
94 /* Check that the compiler uses 'assume' for optimization.
95 This function, when compiled with optimization, should have code
96 equivalent to
97 return x + 3;
98 Use 'objdump --disassemble test-verify.o' to verify this. */
99 assume (x >= 4);
100 return (x > 1 ? x + 3 : 2 * x + 10);
101 }
102
103 _Noreturn void
104 test_assume_noreturn (void)
/* ![[previous]](../icons/left.png)
![[next]](../icons/right.png)
![[first]](../icons/first.png)
![[last]](../icons/last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
105 {
106 /* Check that the compiler's data-flow analysis recognizes 'assume (0)'.
107 This function should not elicit a warning. */
108 assume (0);
109 }
110
111 /* ============================== Main ===================================== */
112 int
113 main (void)
/* ![[previous]](../icons/left.png)
![[next]](../icons/n_right.png)
![[first]](../icons/first.png)
![[last]](../icons/n_last.png)
![[top]](../icons/top.png)
![[bottom]](../icons/bottom.png)
![[index]](../icons/index.png)
*/
114 {
115 state s = { 0, 1 };
116 test_assume_expressions (&s);
117 test_assume_optimization (5);
118 return !(function (0) == 0 && function (1) == 8);
119 }