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;
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#define OPT_CONFIG_C_CPP \
25 "D:I:(include)(function)" \
26 "(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
27 "(unsigned-char)" \
28 "(round-to-even)(round-to-nearest)" \
29 "(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
30 "(no-library)"
31
32#define HELP_CONFIG_C_CPP \
33 " {y-I} {upath} \t set include path (C/C++)\n" \
34 " {y--include} {ufile} \t set include file (C/C++)\n" \
35 " {y-D} {umacro} \t define preprocessor macro (C/C++)\n" \
36 " {y--c89}, {y--c99}, {y--c11} \t " \
37 "set C language standard (default: " + \
38 std::string( \
39 configt::ansi_ct::default_c_standard() == \
40 configt::ansi_ct::c_standardt::C89 \
41 ? "c89" \
42 : configt::ansi_ct::default_c_standard() == \
43 configt::ansi_ct::c_standardt::C99 \
44 ? "c99" \
45 : configt::ansi_ct::default_c_standard() == \
46 configt::ansi_ct::c_standardt::C11 \
47 ? "c11" \
48 : "") + \
49 ")\n" \
50 " {y--cpp98}, {y--cpp03}, {y--cpp11} \t " \
51 "set C++ language standard (default: " + \
52 std::string( \
53 configt::cppt::default_cpp_standard() == \
54 configt::cppt::cpp_standardt::CPP98 \
55 ? "cpp98" \
56 : configt::cppt::default_cpp_standard() == \
57 configt::cppt::cpp_standardt::CPP03 \
58 ? "cpp03" \
59 : configt::cppt::default_cpp_standard() == \
60 configt::cppt::cpp_standardt::CPP11 \
61 ? "cpp11" \
62 : "") + \
63 ")\n" \
64 " {y--unsigned-char} \t make \"char\" unsigned by default\n" \
65 " {y--round-to-nearest}, {y--round-to-even} \t " \
66 "rounding towards nearest even (default)\n" \
67 " {y--round-to-plus-inf} \t rounding towards plus infinity\n" \
68 " {y--round-to-minus-inf} \t rounding towards minus infinity\n" \
69 " {y--round-to-zero} \t rounding towards zero\n" \
70 " {y--no-library} \t disable built-in abstract C library\n"
71
72#define OPT_CONFIG_LIBRARY \
73 "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
74 "(string-abstraction)"
75
76#define HELP_CONFIG_LIBRARY \
77 " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \
78 " {y--malloc-fail-assert} \t " \
79 "set malloc failure mode to assert-then-assume\n" \
80 " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \
81 " {y--string-abstraction} \t track C string lengths and zero-termination\n"
82
83#define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"
84
85#define OPT_CONFIG_PLATFORM \
86 "(arch):(os):" \
87 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
88 "(little-endian)(big-endian)" \
89 "(i386-linux)" \
90 "(i386-win32)(win32)(winx64)" \
91 "(i386-macos)(ppc-macos)" \
92 "(gcc)"
93
94#define HELP_CONFIG_PLATFORM \
95 " {y--arch} {uarch_name} \t " \
96 "set architecture (default: " + \
97 id2string(configt::this_architecture()) + \
98 ") to one of: {yalpha}, {yarm}, {yarm64}, {yarmel}, {yarmhf}, {yhppa}, " \
99 "{yi386}, {yia64}, {ymips}, {ymips64}, {ymips64el}, {ymipsel}, " \
100 "{ymipsn32}, " \
101 "{ymipsn32el}, {ypowerpc}, {yppc64}, {yppc64le}, {yriscv64}, {ys390}, " \
102 "{ys390x}, {ysh4}, {ysparc}, {ysparc64}, {yv850}, {yx32}, {yx86_64}, or " \
103 "{ynone}\n" \
104 " {y--os} {uos_name} \t " \
105 "set operating system (default: " + \
106 id2string(configt::this_operating_system()) + \
107 ") to one of: {yfreebsd}, {ylinux}, {ymacos}, {ysolaris}, or {ywindows}\n" \
108 " {y--i386-linux}, {y--i386-win32}, {y--i386-macos}, {y--ppc-macos}, " \
109 "{y--win32}, {y--winx64} \t " \
110 "set architecture and operating system\n" \
111 " {y--LP64}, {y--ILP64}, {y--LLP64}, {y--ILP32}, {y--LP32} \t " \
112 "set width of int, long and pointers, but don't override default " \
113 "architecture and operating system\n" \
114 " {y--16}, {y--32}, {y--64} \t " \
115 "equivalent to {y--LP32}, {y--ILP32}, {y--LP64} (on Windows: " \
116 "{y--LLP64})\n" \
117 " {y--little-endian} \t allow little-endian word-byte conversions\n" \
118 " {y--big-endian} \t allow big-endian word-byte conversions\n" \
119 " {y--gcc} \t use GCC as preprocessor\n"
120
121#define OPT_CONFIG_BACKEND "(object-bits):"
122
123#define HELP_CONFIG_BACKEND \
124 " {y--object-bits} {un} \t number of bits used for object addresses\n"
125
129{
130public:
131 struct ansi_ct
132 {
133 // for ANSI-C
134 std::size_t int_width;
135 std::size_t long_int_width;
136 std::size_t bool_width;
137 std::size_t char_width;
138 std::size_t short_int_width;
140 std::size_t pointer_width;
141 std::size_t single_width;
142 std::size_t double_width;
143 std::size_t long_double_width;
144 std::size_t wchar_t_width;
145
146 // various language options
149 bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
150 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
152 enum class c_standardt
153 {
154 C89,
155 C99,
156 C11
159
160 void set_c89()
161 {
163 for_has_scope = false;
164 }
165 void set_c99()
166 {
168 for_has_scope = true;
169 }
170 void set_c11()
171 {
173 for_has_scope = true;
174 }
175
177
178 void set_16();
179 void set_32();
180 void set_64();
181
182 // http://www.unix.org/version2/whatsnew/lp64_wp.html
183 void set_LP64(); // int=32, long=64, pointer=64
184 void set_ILP64(); // int=64, long=64, pointer=64
185 void set_LLP64(); // int=32, long=32, pointer=64
186 void set_ILP32(); // int=32, long=32, pointer=32
187 void set_LP32(); // int=16, long=32, pointer=32
188
189 // minimum alignment (in structs) measured in bytes
190 std::size_t alignment;
191
192 // maximum minimum size of the operands for a machine
193 // instruction (in bytes)
195
196 enum class endiannesst
197 {
201 };
203
204 enum class ost
205 {
206 NO_OS,
207 OS_LINUX,
208 OS_MACOS,
209 OS_WIN
210 };
212
213 static std::string os_to_string(ost);
214 static ost string_to_os(const std::string &);
215
217
218 // architecture-specific integer value of null pointer constant
220
221 void set_arch_spec_i386();
225 void set_arch_spec_alpha();
228 void set_arch_spec_s390();
229 void set_arch_spec_s390x();
231 void set_arch_spec_ia64();
232 void set_arch_spec_x32();
233 void set_arch_spec_v850();
234 void set_arch_spec_hppa();
235 void set_arch_spec_sh4();
236
237 enum class flavourt
238 {
239 NONE,
240 ANSI,
241 GCC,
242 ARM,
243 CLANG,
246 };
247 flavourt mode; // the syntax of source files
248
249 enum class preprocessort
250 {
251 NONE,
252 GCC,
253 CLANG,
256 ARM
257 };
258 preprocessort preprocessor; // the preprocessor to use
259
260 std::list<std::string> defines;
261 std::list<std::string> undefines;
262 std::list<std::string> preprocessor_options;
263 std::list<std::string> include_paths;
264 std::list<std::string> include_files;
265
266 enum class libt
267 {
268 LIB_NONE,
270 };
272
274 bool malloc_may_fail = false;
275
282
284
285 static const std::size_t default_object_bits = 8;
286
292
293 struct cppt
294 {
295 enum class cpp_standardt
296 {
297 CPP98,
298 CPP03,
299 CPP11,
300 CPP14,
301 CPP17
304
306 {
308 }
310 {
312 }
314 {
316 }
318 {
320 }
322 {
324 }
325
326 static const std::size_t default_object_bits = 8;
328
329 struct verilogt
330 {
331 std::list<std::string> include_paths;
333
334 struct javat
335 {
336 typedef std::list<std::string> classpatht;
339
340 static const std::size_t default_object_bits = 16;
342
344 {
345 // number of bits to encode heap object addresses
346 std::size_t object_bits = 8;
349
350 // this is the function to start executing
352
353 void set_arch(const irep_idt &);
354
356
357 bool set(const cmdlinet &cmdline);
358
360 std::string object_bits_info();
361
364
365private:
366 void set_classpath(const std::string &cp);
367};
368
369extern configt config;
370
371#endif // CPROVER_UTIL_CONFIG_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Globally accessible architectural configuration.
Definition config.h:129
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1315
void set_arch(const irep_idt &)
Definition config.cpp:702
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
optionalt< std::string > main
Definition config.h:351
struct configt::verilogt verilog
std::string object_bits_info()
Definition config.cpp:1340
void set_classpath(const std::string &cp)
Definition config.cpp:1435
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1256
static irep_idt this_architecture()
Definition config.cpp:1351
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition config.cpp:1451
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:39
The symbol table base class interface.
configt config
Definition config.cpp:25
std::size_t long_double_width
Definition config.h:143
std::list< std::string > include_paths
Definition config.h:263
bool for_has_scope
Definition config.h:148
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition config.h:290
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:202
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:149
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:147
void set_arch_spec_hppa()
Definition config.cpp:616
static std::string os_to_string(ost)
Definition config.cpp:1177
std::size_t pointer_width
Definition config.h:140
bool gcc__float128_type
Definition config.h:150
void set_c89()
Definition config.h:160
std::list< std::string > include_files
Definition config.h:264
void set_ILP64()
int=64, long=64, pointer=64
Definition config.cpp:71
irep_idt arch
Definition config.h:216
std::list< std::string > undefines
Definition config.h:261
ieee_floatt::rounding_modet rounding_mode
Definition config.h:176
std::list< std::string > preprocessor_options
Definition config.h:262
void set_arch_spec_sparc(const irep_idt &subarch)
Definition config.cpp:486
static ost string_to_os(const std::string &)
Definition config.cpp:1192
std::list< std::string > defines
Definition config.h:260
void set_c99()
Definition config.h:165
bool single_precision_constant
Definition config.h:151
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:144
preprocessort preprocessor
Definition config.h:258
@ malloc_failure_mode_return_null
Definition config.h:279
@ malloc_failure_mode_none
Definition config.h:278
@ malloc_failure_mode_assert_then_assume
Definition config.h:280
std::size_t double_width
Definition config.h:142
bool malloc_may_fail
Definition config.h:274
bool char_is_unsigned
Definition config.h:147
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:190
void set_arch_spec_power(const irep_idt &subarch)
Definition config.cpp:220
std::size_t bool_width
Definition config.h:136
bool string_abstraction
Definition config.h:273
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:194
std::size_t long_long_int_width
Definition config.h:139
void set_arch_spec_s390x()
Definition config.cpp:458
bool NULL_is_zero
Definition config.h:219
std::size_t long_int_width
Definition config.h:135
void set_arch_spec_mips(const irep_idt &subarch)
Definition config.cpp:353
std::size_t single_width
Definition config.h:141
void set_arch_spec_i386()
Definition config.cpp:150
std::size_t short_int_width
Definition config.h:138
std::size_t char_width
Definition config.h:137
void set_c11()
Definition config.h:170
static const std::size_t default_object_bits
Definition config.h:285
flavourt mode
Definition config.h:247
std::size_t int_width
Definition config.h:134
malloc_failure_modet malloc_failure_mode
Definition config.h:283
void set_arch_spec_ia64()
Definition config.cpp:526
bool is_object_bits_default
Definition config.h:347
std::size_t object_bits
Definition config.h:346
void set_cpp14()
Definition config.h:317
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition config.h:313
static const std::size_t default_object_bits
Definition config.h:326
void set_cpp17()
Definition config.h:321
void set_cpp03()
Definition config.h:309
static cpp_standardt default_cpp_standard()
Definition config.cpp:690
void set_cpp98()
Definition config.h:305
classpatht classpath
Definition config.h:337
std::list< std::string > classpatht
Definition config.h:336
irep_idt main_class
Definition config.h:338
static const std::size_t default_object_bits
Definition config.h:340
std::list< std::string > include_paths
Definition config.h:331