54 long_long_int_width=8*8;
58 long_double_width=16*8;
59 char_is_unsigned=
false;
60 wchar_t_is_unsigned=
false;
63 memory_operand_size=int_width/8;
78 long_long_int_width=8*8;
82 long_double_width=8*8;
83 char_is_unsigned=
false;
84 wchar_t_is_unsigned=
false;
87 memory_operand_size=int_width/8;
98 long_long_int_width=8*8;
102 long_double_width=8*8;
103 char_is_unsigned=
false;
104 wchar_t_is_unsigned=
false;
107 memory_operand_size=int_width/8;
118 long_long_int_width=8*8;
122 long_double_width=12*8;
123 char_is_unsigned=
false;
124 wchar_t_is_unsigned=
false;
127 memory_operand_size=int_width/8;
138 long_long_int_width=8*8;
142 long_double_width=8*8;
143 char_is_unsigned=
false;
144 wchar_t_is_unsigned=
false;
147 memory_operand_size=int_width/8;
153 endianness=endiannesst::IS_LITTLE_ENDIAN;
154 char_is_unsigned=
false;
160 case flavourt::CLANG:
161 defines.push_back(
"i386");
162 defines.push_back(
"__i386");
163 defines.push_back(
"__i386__");
164 if(mode == flavourt::CLANG)
165 defines.push_back(
"__LITTLE_ENDIAN__");
168 case flavourt::VISUAL_STUDIO:
169 defines.push_back(
"_M_IX86");
172 case flavourt::CODEWARRIOR:
185 endianness=endiannesst::IS_LITTLE_ENDIAN;
186 long_double_width=16*8;
187 char_is_unsigned=
false;
193 case flavourt::CLANG:
194 defines.push_back(
"__LP64__");
195 defines.push_back(
"__x86_64");
196 defines.push_back(
"__x86_64__");
197 defines.push_back(
"_LP64");
198 defines.push_back(
"__amd64__");
199 defines.push_back(
"__amd64");
201 if(os == ost::OS_MACOS)
202 defines.push_back(
"__LITTLE_ENDIAN__");
205 case flavourt::VISUAL_STUDIO:
206 defines.push_back(
"_M_X64");
207 defines.push_back(
"_M_AMD64");
210 case flavourt::CODEWARRIOR:
222 if(subarch==
"powerpc")
227 if(subarch==
"ppc64le")
228 endianness=endiannesst::IS_LITTLE_ENDIAN;
230 endianness=endiannesst::IS_BIG_ENDIAN;
232 long_double_width=16*8;
233 char_is_unsigned=
true;
239 case flavourt::CLANG:
240 defines.push_back(
"__powerpc");
241 defines.push_back(
"__powerpc__");
242 defines.push_back(
"__POWERPC__");
243 defines.push_back(
"__ppc__");
245 if(os == ost::OS_MACOS)
246 defines.push_back(
"__BIG_ENDIAN__");
248 if(subarch!=
"powerpc")
250 defines.push_back(
"__powerpc64");
251 defines.push_back(
"__powerpc64__");
252 defines.push_back(
"__PPC64__");
253 defines.push_back(
"__ppc64__");
254 if(subarch==
"ppc64le")
256 defines.push_back(
"_CALL_ELF=2");
257 defines.push_back(
"__LITTLE_ENDIAN__");
261 defines.push_back(
"_CALL_ELF=1");
262 defines.push_back(
"__BIG_ENDIAN__");
267 case flavourt::VISUAL_STUDIO:
268 defines.push_back(
"_M_PPC");
271 case flavourt::CODEWARRIOR:
286 long_double_width=16*8;
291 long_double_width=8*8;
294 endianness=endiannesst::IS_LITTLE_ENDIAN;
295 char_is_unsigned=
true;
301 case flavourt::CLANG:
303 defines.push_back(
"__aarch64__");
305 defines.push_back(
"__arm__");
307 defines.push_back(
"__ARM_PCS_VFP");
310 case flavourt::VISUAL_STUDIO:
311 defines.push_back(
"_M_ARM");
314 case flavourt::CODEWARRIOR:
327 endianness=endiannesst::IS_LITTLE_ENDIAN;
328 long_double_width=16*8;
329 char_is_unsigned=
false;
335 defines.push_back(
"__alpha__");
338 case flavourt::VISUAL_STUDIO:
339 defines.push_back(
"_M_ALPHA");
342 case flavourt::CLANG:
343 case flavourt::CODEWARRIOR:
355 if(subarch==
"mipsel" ||
357 subarch==
"mipsn32el" ||
361 long_double_width=8*8;
366 long_double_width=16*8;
369 if(subarch==
"mipsel" ||
370 subarch==
"mipsn32el" ||
372 endianness=endiannesst::IS_LITTLE_ENDIAN;
374 endianness=endiannesst::IS_BIG_ENDIAN;
376 char_is_unsigned=
false;
382 defines.push_back(
"__mips__");
383 defines.push_back(
"mips");
388 case flavourt::VISUAL_STUDIO:
392 case flavourt::CLANG:
393 case flavourt::CODEWARRIOR:
406 endianness = endiannesst::IS_LITTLE_ENDIAN;
407 long_double_width = 16 * 8;
408 char_is_unsigned =
true;
414 defines.push_back(
"__riscv");
417 case flavourt::VISUAL_STUDIO:
418 case flavourt::CLANG:
419 case flavourt::CODEWARRIOR:
432 endianness=endiannesst::IS_BIG_ENDIAN;
433 long_double_width=16*8;
434 char_is_unsigned=
true;
440 defines.push_back(
"__s390__");
443 case flavourt::VISUAL_STUDIO:
447 case flavourt::CLANG:
448 case flavourt::CODEWARRIOR:
461 endianness=endiannesst::IS_BIG_ENDIAN;
462 char_is_unsigned=
true;
468 defines.push_back(
"__s390x__");
471 case flavourt::VISUAL_STUDIO:
475 case flavourt::CLANG:
476 case flavourt::CODEWARRIOR:
488 if(subarch==
"sparc64")
491 long_double_width=16*8;
496 long_double_width=16*8;
499 endianness=endiannesst::IS_BIG_ENDIAN;
500 char_is_unsigned=
false;
506 defines.push_back(
"__sparc__");
507 if(subarch==
"sparc64")
508 defines.push_back(
"__arch64__");
511 case flavourt::VISUAL_STUDIO:
515 case flavourt::CLANG:
516 case flavourt::CODEWARRIOR:
529 long_double_width=16*8;
530 endianness=endiannesst::IS_LITTLE_ENDIAN;
531 char_is_unsigned=
false;
537 defines.push_back(
"__ia64__");
538 defines.push_back(
"_IA64");
539 defines.push_back(
"__IA64__");
542 case flavourt::VISUAL_STUDIO:
543 defines.push_back(
"_M_IA64");
546 case flavourt::CLANG:
547 case flavourt::CODEWARRIOR:
562 long_double_width=16*8;
563 endianness=endiannesst::IS_LITTLE_ENDIAN;
564 char_is_unsigned=
false;
570 defines.push_back(
"__ILP32__");
571 defines.push_back(
"__x86_64");
572 defines.push_back(
"__x86_64__");
573 defines.push_back(
"__amd64__");
574 defines.push_back(
"__amd64");
577 case flavourt::VISUAL_STUDIO:
581 case flavourt::CLANG:
582 case flavourt::CODEWARRIOR:
606 long_double_width=8*8;
607 endianness=endiannesst::IS_LITTLE_ENDIAN;
610 char_is_unsigned=
false;
619 long_double_width=8*8;
620 endianness=endiannesst::IS_BIG_ENDIAN;
621 char_is_unsigned=
false;
627 defines.push_back(
"__hppa__");
630 case flavourt::VISUAL_STUDIO:
634 case flavourt::CLANG:
635 case flavourt::CODEWARRIOR:
648 long_double_width=8*8;
649 endianness=endiannesst::IS_LITTLE_ENDIAN;
650 char_is_unsigned=
false;
656 defines.push_back(
"__sh__");
657 defines.push_back(
"__SH4__");
660 case flavourt::VISUAL_STUDIO:
664 case flavourt::CLANG:
665 case flavourt::CODEWARRIOR:
677 #if defined(__APPLE__)
679 return c_standardt::C11;
680 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
683 return c_standardt::C99;
686 return c_standardt::C11;
696 return cpp_standardt::CPP14;
698 return cpp_standardt::CPP98;
713 if(
sizeof(
long int)==8)
718 else if(arch==
"alpha")
720 else if(arch==
"arm64" ||
725 else if(arch==
"mips64el" ||
732 else if(arch==
"powerpc" ||
736 else if(arch ==
"riscv64")
738 else if(arch==
"sparc" ||
741 else if(arch==
"ia64")
743 else if(arch==
"s390x")
745 else if(arch==
"s390")
749 else if(arch==
"v850")
751 else if(arch==
"hppa")
755 else if(arch==
"x86_64")
757 else if(arch==
"i386")
776 const std::string &argument,
777 const std::size_t pointer_width)
779 const auto throw_for_reason = [&](
const std::string &reason) {
781 "Value of \"" + argument +
"\" given for object-bits is " + reason +
782 ". object-bits must be positive and less than the pointer width (" +
786 const auto object_bits = string2optional<unsigned int>(argument);
788 throw_for_reason(
"not a valid unsigned integer");
789 if(*object_bits == 0 || *object_bits >= pointer_width)
790 throw_for_reason(
"out of range");
824 if(cmdline.
isset(
"function"))
827 if(cmdline.
isset(
'D'))
830 if(cmdline.
isset(
'I'))
833 if(cmdline.
isset(
"classpath"))
839 else if(cmdline.
isset(
"cp"))
848 const char *CLASSPATH=
getenv(
"CLASSPATH");
849 if(CLASSPATH!=
nullptr)
855 if(cmdline.
isset(
"main-class"))
858 if(cmdline.
isset(
"include"))
870 if(cmdline.
isset(
"i386-linux"))
875 else if(cmdline.
isset(
"i386-win32") ||
876 cmdline.
isset(
"win32"))
881 else if(cmdline.
isset(
"winx64"))
886 else if(cmdline.
isset(
"i386-macos"))
891 else if(cmdline.
isset(
"ppc-macos"))
897 if(cmdline.
isset(
"arch"))
902 if(cmdline.
isset(
"os"))
914 if(cmdline.
isset(
"gcc"))
939 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
957 else if(os ==
"linux" || os ==
"solaris" || os ==
"netbsd")
964 else if(os ==
"freebsd" || os ==
"openbsd")
998 if(arch ==
"x86_64" && cmdline.
isset(
"gcc"))
1003 else if(os ==
"macos" && arch ==
"arm64")
1013 if(arch==this_arch && os==this_os)
1017 "int width shall be equal to the system int width");
1020 "long int width shall be equal to the system long int width");
1023 "bool width shall be equal to the system bool width");
1026 "char width shall be equal to the system char width");
1029 "short int width shall be equal to the system short int width");
1032 "long long int width shall be equal to the system long long int width");
1035 "pointer width shall be equal to the system pointer width");
1038 "float width shall be equal to the system float width");
1041 "double width shall be equal to the system double width");
1044 (
static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1045 "char_is_unsigned flag shall indicate system char unsignedness");
1051 "long double width shall be equal to the system long double width");
1057 if(cmdline.
isset(
"16"))
1060 if(cmdline.
isset(
"32"))
1063 if(cmdline.
isset(
"64"))
1066 if(cmdline.
isset(
"LP64"))
1069 if(cmdline.
isset(
"ILP64"))
1072 if(cmdline.
isset(
"LLP64"))
1075 if(cmdline.
isset(
"ILP32"))
1078 if(cmdline.
isset(
"LP32"))
1081 if(cmdline.
isset(
"string-abstraction"))
1086 if(cmdline.
isset(
"no-library"))
1089 if(cmdline.
isset(
"little-endian"))
1092 if(cmdline.
isset(
"big-endian"))
1095 if(cmdline.
isset(
"little-endian") &&
1096 cmdline.
isset(
"big-endian"))
1099 if(cmdline.
isset(
"unsigned-char"))
1102 if(cmdline.
isset(
"round-to-even") ||
1103 cmdline.
isset(
"round-to-nearest"))
1106 if(cmdline.
isset(
"round-to-plus-inf"))
1109 if(cmdline.
isset(
"round-to-minus-inf"))
1112 if(cmdline.
isset(
"round-to-zero"))
1115 if(cmdline.
isset(
"object-bits"))
1121 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1124 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1126 if(cmdline.
isset(
"malloc-fail-null"))
1128 if(cmdline.
isset(
"malloc-fail-assert"))
1131 if(cmdline.
isset(
"malloc-may-fail"))
1135 if(cmdline.
isset(
"no-malloc-may-fail"))
1141 if(cmdline.
isset(
"c89"))
1144 if(cmdline.
isset(
"c99"))
1147 if(cmdline.
isset(
"c11"))
1150 if(cmdline.
isset(
"cpp98"))
1153 if(cmdline.
isset(
"cpp03"))
1156 if(cmdline.
isset(
"cpp11"))
1174 const auto pointer_bits_2log =
1192 case ost::OS_LINUX:
return "linux";
1193 case ost::OS_MACOS:
return "macos";
1194 case ost::OS_WIN:
return "win";
1195 case ost::NO_OS:
return "none";
1205 return ost::OS_LINUX;
1206 else if(os==
"macos")
1207 return ost::OS_MACOS;
1216 const std::string &what)
1221 const bool not_found = ns.
lookup(
id, symbol);
1227 tmp.
id() == ID_address_of &&
1231 "symbol table configuration entry '" +
id2string(
id) +
1232 "' must be a string constant");
1239 const std::string &what)
1244 const bool not_found = ns.
lookup(
id, symbol);
1252 "symbol table configuration entry '" +
id2string(
id) +
1253 "' must be a constant");
1260 "symbol table configuration entry '" +
id2string(
id) +
1261 "' must be convertible to mp_integer");
1263 return numeric_cast_v<unsigned>(int_value);
1336 const symbolt &entry_point_symbol=*maybe_symbol;
1338 if(entry_point_symbol.
mode==ID_java)
1340 else if(entry_point_symbol.
mode==ID_C)
1342 else if(entry_point_symbol.
mode==ID_cpp)
1346 "object_bits should fit into pointer width");
1368 this_arch =
"alpha";
1369 #elif defined(__armel__)
1370 this_arch =
"armel";
1371 #elif defined(__aarch64__)
1372 this_arch =
"arm64";
1373 #elif defined(__arm__)
1374 #ifdef __ARM_PCS_VFP
1375 this_arch =
"armhf";
1379 #elif defined(_MIPSEL)
1380 #if _MIPS_SIM==_ABIO32
1381 this_arch =
"mipsel";
1382 #elif _MIPS_SIM==_ABIN32
1383 this_arch =
"mipsn32el";
1385 this_arch =
"mips64el";
1387 #elif defined(__mips__)
1388 #if _MIPS_SIM==_ABIO32
1390 #elif _MIPS_SIM==_ABIN32
1391 this_arch =
"mipsn32";
1393 this_arch =
"mips64";
1395 #elif defined(__powerpc__)
1396 #if defined(__ppc64__) || defined(__PPC64__) || \
1397 defined(__powerpc64__) || defined(__POWERPC64__)
1398 #ifdef __LITTLE_ENDIAN__
1399 this_arch =
"ppc64le";
1401 this_arch =
"ppc64";
1404 this_arch =
"powerpc";
1406 #elif defined(__riscv)
1407 this_arch =
"riscv64";
1408 #elif defined(__sparc__)
1410 this_arch =
"sparc64";
1412 this_arch =
"sparc";
1414 #elif defined(__ia64__)
1416 #elif defined(__s390x__)
1417 this_arch =
"s390x";
1418 #elif defined(__s390__)
1420 #elif defined(__x86_64__)
1424 this_arch =
"x86_64";
1426 #elif defined(__i386__)
1428 #elif defined(_WIN64)
1429 this_arch =
"x86_64";
1430 #elif defined(_WIN32)
1432 #elif defined(__hppa__)
1434 #elif defined(__sh__)
1438 this_arch =
"unknown";
1450 const char cp_separator =
';';
1452 const char cp_separator =
':';
1455 std::vector<std::string> class_path =
1458 java.
classpath.end(), class_path.begin(), class_path.end());
1472 this_os =
"openbsd";
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
Globally accessible architectural configuration.
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
void set_arch(const irep_idt &)
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
std::string object_bits_info()
void set_classpath(const std::string &cp)
void set_from_symbol_table(const symbol_table_baset &)
static irep_idt this_architecture()
std::optional< std::string > main
struct configt::javat java
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_constant() const
Return whether the expression is a constant.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
configt::bv_encodingt parse_object_bits_encoding(const std::string &argument, const std::size_t pointer_width)
Parses the object_bits argument from the command line arguments.
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
const std::string & id2string(const irep_idt &d)
mp_integer alignment(const typet &type, const namespacet &ns)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool simplify(exprt &expr, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
char * getenv(const char *name)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::size_t long_double_width
std::list< std::string > include_paths
enum configt::ansi_ct::c_standardt c_standard
void set_arch_spec_riscv64()
void set_ILP32()
int=32, long=32, pointer=32
bool ts_18661_3_Floatn_types
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
void set_arch_spec_hppa()
static std::string os_to_string(ost)
std::size_t pointer_width
std::optional< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
std::list< std::string > include_files
void set_ILP64()
int=64, long=64, pointer=64
ieee_floatt::rounding_modet rounding_mode
void set_arch_spec_sparc(const irep_idt &subarch)
static ost string_to_os(const std::string &)
std::list< std::string > defines
bool single_precision_constant
void set_LLP64()
int=32, long=32, pointer=64
void set_arch_spec_arm(const irep_idt &subarch)
std::size_t wchar_t_width
preprocessort preprocessor
@ malloc_failure_mode_return_null
@ malloc_failure_mode_none
@ malloc_failure_mode_assert_then_assume
static c_standardt default_c_standard()
void set_arch_spec_alpha()
void set_arch_spec_power(const irep_idt &subarch)
void set_arch_spec_s390()
void set_LP64()
int=32, long=64, pointer=64
void set_arch_spec_x86_64()
void set_LP32()
int=16, long=32, pointer=32
std::size_t memory_operand_size
std::size_t long_long_int_width
void set_arch_spec_s390x()
std::size_t long_int_width
void set_arch_spec_mips(const irep_idt &subarch)
void set_arch_spec_i386()
std::size_t short_int_width
static const std::size_t default_object_bits
malloc_failure_modet malloc_failure_mode
void set_arch_spec_ia64()
bool is_object_bits_default
enum configt::cppt::cpp_standardt cpp_standard
static const std::size_t default_object_bits
static cpp_standardt default_cpp_standard()
static const std::size_t default_object_bits