cprover
Loading...
Searching...
No Matches
config.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_CONFIG_H
10#define CPROVER_UTIL_CONFIG_H
11
12#include <list>
13
14#include "ieee_float.h"
15#include "irep.h"
16#include "optional.h"
17
18class cmdlinet;
19class symbol_tablet;
20
21// Configt is the one place beyond *_parse_options where options are ... parsed.
22// Options that are handled by configt are documented here.
23
24// clang-format off
25#define OPT_CONFIG_C_CPP \
26 "D:I:(include)(function)" \
27 "(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
28 "(unsigned-char)" \
29 "(round-to-even)(round-to-nearest)" \
30 "(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
31 "(no-library)" \
32
33#define HELP_CONFIG_C_CPP \
34 " -I path set include path (C/C++)\n" \
35 " -D macro define preprocessor macro (C/C++)\n" \
36 " --c89/99/11 set C language standard (default: " \
37 << (configt::ansi_ct::default_c_standard()== \
38 configt::ansi_ct::c_standardt::C89?"c89": \
39 configt::ansi_ct::default_c_standard()== \
40 configt::ansi_ct::c_standardt::C99?"c99": \
41 configt::ansi_ct::default_c_standard()== \
42 configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"\
43 " --cpp98/03/11 set C++ language standard (default: " \
44 << (configt::cppt::default_cpp_standard()== \
45 configt::cppt::cpp_standardt::CPP98?"cpp98":\
46 configt::cppt::default_cpp_standard()== \
47 configt::cppt::cpp_standardt::CPP03?"cpp03":\
48 configt::cppt::default_cpp_standard()== \
49 configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"\
50 " --unsigned-char make \"char\" unsigned by default\n" \
51 " --round-to-nearest rounding towards nearest even (default)\n" \
52 " --round-to-plus-inf rounding towards plus infinity\n" \
53 " --round-to-minus-inf rounding towards minus infinity\n" \
54 " --round-to-zero rounding towards zero\n" \
55 " --no-library disable built-in abstract C library\n" \
56
57
58#define OPT_CONFIG_LIBRARY \
59 "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
60 "(string-abstraction)" \
61
62#define HELP_CONFIG_LIBRARY \
63" --malloc-may-fail allow malloc calls to return a null pointer\n" \
64" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"\
65" --malloc-fail-null set malloc failure mode to return null\n" \
66
67
68#define OPT_CONFIG_JAVA \
69 "(classpath)(cp)(main-class)" \
70
71
72#define OPT_CONFIG_PLATFORM \
73 "(arch):(os):" \
74 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
75 "(little-endian)(big-endian)" \
76 "(i386-linux)" \
77 "(i386-win32)(win32)(winx64)" \
78 "(i386-macos)(ppc-macos)" \
79 "(gcc)" \
80
81#define HELP_CONFIG_PLATFORM \
82 " --arch set architecture (default: " \
83 << configt::this_architecture() << ")\n" \
84 " --os set operating system (default: " \
85 << configt::this_operating_system() << ")\n" \
86 " --16, --32, --64 set width of int\n" \
87 " --LP64, --ILP64, --LLP64,\n" \
88 " --ILP32, --LP32 set width of int, long and pointers\n" \
89 " --little-endian allow little-endian word-byte conversions\n" \
90 " --big-endian allow big-endian word-byte conversions\n" \
91 " --gcc use GCC as preprocessor\n" \
92
93#define OPT_CONFIG_BACKEND \
94 "(object-bits):" \
95
96#define HELP_CONFIG_BACKEND \
97 " --object-bits n number of bits used for object addresses\n"
98
99// clang-format on
100
104{
105public:
106 struct ansi_ct
107 {
108 // for ANSI-C
109 std::size_t int_width;
110 std::size_t long_int_width;
111 std::size_t bool_width;
112 std::size_t char_width;
113 std::size_t short_int_width;
115 std::size_t pointer_width;
116 std::size_t single_width;
117 std::size_t double_width;
118 std::size_t long_double_width;
119 std::size_t wchar_t_width;
120
121 // various language options
124 bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
125 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
127 enum class c_standardt
128 {
129 C89,
130 C99,
131 C11
134
135 void set_c89()
136 {
138 for_has_scope = false;
139 }
140 void set_c99()
141 {
143 for_has_scope = true;
144 }
145 void set_c11()
146 {
148 for_has_scope = true;
149 }
150
152
153 void set_16();
154 void set_32();
155 void set_64();
156
157 // http://www.unix.org/version2/whatsnew/lp64_wp.html
158 void set_LP64(); // int=32, long=64, pointer=64
159 void set_ILP64(); // int=64, long=64, pointer=64
160 void set_LLP64(); // int=32, long=32, pointer=64
161 void set_ILP32(); // int=32, long=32, pointer=32
162 void set_LP32(); // int=16, long=32, pointer=32
163
164 // minimum alignment (in structs) measured in bytes
165 std::size_t alignment;
166
167 // maximum minimum size of the operands for a machine
168 // instruction (in bytes)
170
171 enum class endiannesst
172 {
176 };
178
179 enum class ost
180 {
181 NO_OS,
182 OS_LINUX,
183 OS_MACOS,
184 OS_WIN
185 };
187
188 static std::string os_to_string(ost);
189 static ost string_to_os(const std::string &);
190
192
193 // architecture-specific integer value of null pointer constant
195
196 void set_arch_spec_i386();
198 void set_arch_spec_power(const irep_idt &subarch);
199 void set_arch_spec_arm(const irep_idt &subarch);
200 void set_arch_spec_alpha();
201 void set_arch_spec_mips(const irep_idt &subarch);
203 void set_arch_spec_s390();
204 void set_arch_spec_s390x();
205 void set_arch_spec_sparc(const irep_idt &subarch);
206 void set_arch_spec_ia64();
207 void set_arch_spec_x32();
208 void set_arch_spec_v850();
209 void set_arch_spec_hppa();
210 void set_arch_spec_sh4();
211
212 enum class flavourt
213 {
214 NONE,
215 ANSI,
216 GCC,
217 ARM,
218 CLANG,
221 };
222 flavourt mode; // the syntax of source files
223
224 enum class preprocessort
225 {
226 NONE,
227 GCC,
228 CLANG,
231 ARM
232 };
233 preprocessort preprocessor; // the preprocessor to use
234
235 std::list<std::string> defines;
236 std::list<std::string> undefines;
237 std::list<std::string> preprocessor_options;
238 std::list<std::string> include_paths;
239 std::list<std::string> include_files;
240
241 enum class libt
242 {
243 LIB_NONE,
245 };
247
249 bool malloc_may_fail = false;
250
252 {
256 };
257
259
260 static const std::size_t default_object_bits = 8;
261
267
268 struct cppt
269 {
270 enum class cpp_standardt
271 {
272 CPP98,
273 CPP03,
274 CPP11,
275 CPP14,
276 CPP17
279
281 {
283 }
285 {
287 }
289 {
291 }
293 {
295 }
297 {
299 }
300
301 static const std::size_t default_object_bits = 8;
303
304 struct verilogt
305 {
306 std::list<std::string> include_paths;
308
309 struct javat
310 {
311 typedef std::list<std::string> classpatht;
314
315 static const std::size_t default_object_bits = 16;
317
319 {
320 // number of bits to encode heap object addresses
321 std::size_t object_bits = 8;
324
325 // this is the function to start executing
327
328 void set_arch(const irep_idt &);
329
331
332 bool set(const cmdlinet &cmdline);
333
335 std::string object_bits_info();
336
339
340private:
341 void set_classpath(const std::string &cp);
342};
343
344extern configt config;
345
346#endif // CPROVER_UTIL_CONFIG_H
Globally accessible architectural configuration.
Definition config.h:104
void set_from_symbol_table(const symbol_tablet &)
Definition config.cpp:1254
void set_arch(const irep_idt &)
Definition config.cpp:702
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition config.cpp:1314
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
optionalt< std::string > main
Definition config.h:326
struct configt::verilogt verilog
std::string object_bits_info()
Definition config.cpp:1339
void set_classpath(const std::string &cp)
Definition config.cpp:1434
static irep_idt this_architecture()
Definition config.cpp:1350
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition config.cpp:1450
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The symbol table.
configt config
Definition config.cpp:25
nonstd::optional< T > optionalt
Definition optional.h:35
std::size_t long_double_width
Definition config.h:118
std::list< std::string > include_paths
Definition config.h:238
bool for_has_scope
Definition config.h:123
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition config.h:265
void set_arch_spec_x32()
Definition config.cpp:557
enum configt::ansi_ct::c_standardt c_standard
void set_arch_spec_riscv64()
Definition config.cpp:403
endiannesst endianness
Definition config.h:177
void set_arch_spec_sh4()
Definition config.cpp:645
void set_ILP32()
int=32, long=32, pointer=32
Definition config.cpp:111
bool ts_18661_3_Floatn_types
Definition config.h:124
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition config.cpp:593
bool wchar_t_is_unsigned
Definition config.h:122
void set_arch_spec_hppa()
Definition config.cpp:616
static std::string os_to_string(ost)
Definition config.cpp:1175
std::size_t pointer_width
Definition config.h:115
bool gcc__float128_type
Definition config.h:125
void set_c89()
Definition config.h:135
std::list< std::string > include_files
Definition config.h:239
void set_ILP64()
int=64, long=64, pointer=64
Definition config.cpp:71
irep_idt arch
Definition config.h:191
std::list< std::string > undefines
Definition config.h:236
ieee_floatt::rounding_modet rounding_mode
Definition config.h:151
std::list< std::string > preprocessor_options
Definition config.h:237
void set_arch_spec_sparc(const irep_idt &subarch)
Definition config.cpp:486
static ost string_to_os(const std::string &)
Definition config.cpp:1190
std::list< std::string > defines
Definition config.h:235
void set_c99()
Definition config.h:140
bool single_precision_constant
Definition config.h:126
void set_LLP64()
int=32, long=32, pointer=64
Definition config.cpp:91
void set_arch_spec_arm(const irep_idt &subarch)
Definition config.cpp:281
std::size_t wchar_t_width
Definition config.h:119
preprocessort preprocessor
Definition config.h:233
@ malloc_failure_mode_return_null
Definition config.h:254
@ malloc_failure_mode_none
Definition config.h:253
@ malloc_failure_mode_assert_then_assume
Definition config.h:255
std::size_t double_width
Definition config.h:117
bool malloc_may_fail
Definition config.h:249
bool char_is_unsigned
Definition config.h:122
static c_standardt default_c_standard()
Definition config.cpp:675
void set_arch_spec_alpha()
Definition config.cpp:324
std::size_t alignment
Definition config.h:165
void set_arch_spec_power(const irep_idt &subarch)
Definition config.cpp:220
std::size_t bool_width
Definition config.h:111
bool string_abstraction
Definition config.h:248
void set_arch_spec_s390()
Definition config.cpp:429
void set_LP64()
int=32, long=64, pointer=64
Definition config.cpp:47
void set_arch_spec_x86_64()
Definition config.cpp:182
void set_LP32()
int=16, long=32, pointer=32
Definition config.cpp:131
std::size_t memory_operand_size
Definition config.h:169
std::size_t long_long_int_width
Definition config.h:114
void set_arch_spec_s390x()
Definition config.cpp:458
bool NULL_is_zero
Definition config.h:194
std::size_t long_int_width
Definition config.h:110
void set_arch_spec_mips(const irep_idt &subarch)
Definition config.cpp:353
std::size_t single_width
Definition config.h:116
void set_arch_spec_i386()
Definition config.cpp:150
std::size_t short_int_width
Definition config.h:113
std::size_t char_width
Definition config.h:112
void set_c11()
Definition config.h:145
static const std::size_t default_object_bits
Definition config.h:260
flavourt mode
Definition config.h:222
std::size_t int_width
Definition config.h:109
malloc_failure_modet malloc_failure_mode
Definition config.h:258
void set_arch_spec_ia64()
Definition config.cpp:526
bool is_object_bits_default
Definition config.h:322
std::size_t object_bits
Definition config.h:321
void set_cpp14()
Definition config.h:292
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition config.h:288
static const std::size_t default_object_bits
Definition config.h:301
void set_cpp17()
Definition config.h:296
void set_cpp03()
Definition config.h:284
static cpp_standardt default_cpp_standard()
Definition config.cpp:690
void set_cpp98()
Definition config.h:280
classpatht classpath
Definition config.h:312
std::list< std::string > classpatht
Definition config.h:311
irep_idt main_class
Definition config.h:313
static const std::size_t default_object_bits
Definition config.h:315
std::list< std::string > include_paths
Definition config.h:306