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:
678 endianness = endiannesst::IS_LITTLE_ENDIAN;
679 long_double_width = 16 * 8;
680 char_is_unsigned =
false;
686 defines.push_back(
"__loongarch__");
689 case flavourt::VISUAL_STUDIO:
693 case flavourt::CODEWARRIOR:
694 case flavourt::CLANG:
707 endianness = endiannesst::IS_LITTLE_ENDIAN;
708 long_double_width = 16 * 8;
709 char_is_unsigned =
false;
714 case flavourt::CLANG:
715 defines.push_back(
"__EMSCRIPTEN__");
718 case flavourt::VISUAL_STUDIO:
723 case flavourt::CODEWARRIOR:
735#if defined(__APPLE__)
737 return c_standardt::C11;
738#elif defined(__FreeBSD__) || defined(__OpenBSD__)
741 return c_standardt::C99;
744 return c_standardt::C11;
754 return cpp_standardt::CPP14;
756 return cpp_standardt::CPP98;
771 if(
sizeof(
long int)==8)
776 else if(arch==
"alpha")
778 else if(arch==
"arm64" ||
783 else if(arch==
"mips64el" ||
790 else if(arch==
"powerpc" ||
794 else if(arch ==
"riscv64")
796 else if(arch==
"sparc" ||
799 else if(arch==
"ia64")
801 else if(arch==
"s390x")
803 else if(arch==
"s390")
807 else if(arch==
"v850")
809 else if(arch==
"hppa")
813 else if(arch==
"x86_64")
815 else if(arch==
"i386")
817 else if(arch ==
"loongarch64")
819 else if(arch ==
"emscripten")
838 const std::string &argument,
839 const std::size_t pointer_width)
841 const auto throw_for_reason = [&](
const std::string &reason) {
843 "Value of \"" + argument +
"\" given for object-bits is " + reason +
844 ". object-bits must be positive and less than the pointer width (" +
845 std::to_string(pointer_width) +
") ",
850 throw_for_reason(
"not a valid unsigned integer");
851 if(*object_bits == 0 || *object_bits >= pointer_width)
852 throw_for_reason(
"out of range");
888 if(cmdline.
isset(
"function"))
891 if(cmdline.
isset(
'D'))
894 if(cmdline.
isset(
'I'))
897 if(cmdline.
isset(
"classpath"))
903 else if(cmdline.
isset(
"cp"))
912 const char *CLASSPATH=getenv(
"CLASSPATH");
913 if(CLASSPATH!=
nullptr)
919 if(cmdline.
isset(
"main-class"))
922 if(cmdline.
isset(
"include"))
934 if(cmdline.
isset(
"i386-linux"))
939 else if(cmdline.
isset(
"i386-win32") ||
940 cmdline.
isset(
"win32"))
945 else if(cmdline.
isset(
"winx64"))
950 else if(cmdline.
isset(
"i386-macos"))
955 else if(cmdline.
isset(
"ppc-macos"))
961 if(cmdline.
isset(
"arch"))
966 if(cmdline.
isset(
"os"))
978 if(cmdline.
isset(
"gcc"))
1003#elif defined(__FreeBSD__) || defined(__OpenBSD__)
1014 else if(os==
"macos")
1028 else if(os ==
"linux" || os ==
"solaris" || os ==
"netbsd" || os ==
"hurd")
1035 else if(os ==
"freebsd" || os ==
"openbsd")
1076 if(arch ==
"x86_64" && cmdline.
isset(
"gcc"))
1081 else if(os ==
"macos" && arch ==
"arm64")
1091 if(arch==this_arch && os==this_os)
1095 "int width shall be equal to the system int width");
1098 "long int width shall be equal to the system long int width");
1101 "bool width shall be equal to the system bool width");
1104 "char width shall be equal to the system char width");
1107 "short int width shall be equal to the system short int width");
1110 "long long int width shall be equal to the system long long int width");
1113 "pointer width shall be equal to the system pointer width");
1116 "float width shall be equal to the system float width");
1119 "double width shall be equal to the system double width");
1122 (
static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1123 "char_is_unsigned flag shall indicate system char unsignedness");
1129 "long double width shall be equal to the system long double width");
1135 if(cmdline.
isset(
"16"))
1138 if(cmdline.
isset(
"32"))
1141 if(cmdline.
isset(
"64"))
1144 if(cmdline.
isset(
"LP64"))
1147 if(cmdline.
isset(
"ILP64"))
1150 if(cmdline.
isset(
"LLP64"))
1153 if(cmdline.
isset(
"ILP32"))
1156 if(cmdline.
isset(
"LP32"))
1159 if(cmdline.
isset(
"string-abstraction"))
1164 if(cmdline.
isset(
"no-library"))
1167 if(cmdline.
isset(
"little-endian"))
1170 if(cmdline.
isset(
"big-endian"))
1173 if(cmdline.
isset(
"little-endian") &&
1174 cmdline.
isset(
"big-endian"))
1177 if(cmdline.
isset(
"unsigned-char"))
1180 if(cmdline.
isset(
"round-to-even") ||
1181 cmdline.
isset(
"round-to-nearest"))
1184 if(cmdline.
isset(
"round-to-plus-inf"))
1187 if(cmdline.
isset(
"round-to-minus-inf"))
1190 if(cmdline.
isset(
"round-to-zero"))
1193 if(cmdline.
isset(
"object-bits"))
1199 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1202 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1204 if(cmdline.
isset(
"malloc-fail-null"))
1206 if(cmdline.
isset(
"malloc-fail-assert"))
1209 if(cmdline.
isset(
"malloc-may-fail"))
1213 if(cmdline.
isset(
"no-malloc-may-fail"))
1219 if(cmdline.
isset(
"c89"))
1222 if(cmdline.
isset(
"c99"))
1225 if(cmdline.
isset(
"c11"))
1228 if(cmdline.
isset(
"cpp98"))
1231 if(cmdline.
isset(
"cpp03"))
1234 if(cmdline.
isset(
"cpp11"))
1252 const auto pointer_bits_2log =
1270 case ost::OS_LINUX:
return "linux";
1271 case ost::OS_MACOS:
return "macos";
1272 case ost::OS_WIN:
return "win";
1273 case ost::NO_OS:
return "none";
1283 return ost::OS_LINUX;
1284 else if(os==
"macos")
1285 return ost::OS_MACOS;
1294 const std::string &what)
1299 const bool not_found = ns.
lookup(
id, symbol);
1305 tmp.
id() == ID_address_of &&
1309 "symbol table configuration entry '" +
id2string(
id) +
1310 "' must be a string constant");
1317 const std::string &what)
1322 const bool not_found = ns.
lookup(
id, symbol);
1330 "symbol table configuration entry '" +
id2string(
id) +
1331 "' must be a constant");
1338 "symbol table configuration entry '" +
id2string(
id) +
1339 "' must be convertible to mp_integer");
1414 const symbolt &entry_point_symbol=*maybe_symbol;
1416 if(entry_point_symbol.
mode==ID_java)
1418 else if(entry_point_symbol.
mode==ID_C)
1420 else if(entry_point_symbol.
mode==ID_cpp)
1424 "object_bits should fit into pointer width");
1446 this_arch =
"alpha";
1447 #elif defined(__armel__)
1448 this_arch =
"armel";
1449 #elif defined(__aarch64__)
1450 this_arch =
"arm64";
1451 #elif defined(__arm__)
1452 #ifdef __ARM_PCS_VFP
1453 this_arch =
"armhf";
1457 #elif defined(_MIPSEL)
1458 #if _MIPS_SIM==_ABIO32
1459 this_arch =
"mipsel";
1460 #elif _MIPS_SIM==_ABIN32
1461 this_arch =
"mipsn32el";
1463 this_arch =
"mips64el";
1465 #elif defined(__mips__)
1466 #if _MIPS_SIM==_ABIO32
1468 #elif _MIPS_SIM==_ABIN32
1469 this_arch =
"mipsn32";
1471 this_arch =
"mips64";
1473 #elif defined(__powerpc__)
1474 #if defined(__ppc64__) || defined(__PPC64__) || \
1475 defined(__powerpc64__) || defined(__POWERPC64__)
1476 #ifdef __LITTLE_ENDIAN__
1477 this_arch =
"ppc64le";
1479 this_arch =
"ppc64";
1482 this_arch =
"powerpc";
1484 #elif defined(__riscv)
1485 this_arch =
"riscv64";
1486 #elif defined(__sparc__)
1488 this_arch =
"sparc64";
1490 this_arch =
"sparc";
1492 #elif defined(__ia64__)
1494 #elif defined(__s390x__)
1495 this_arch =
"s390x";
1496 #elif defined(__s390__)
1498 #elif defined(__x86_64__)
1502 this_arch =
"x86_64";
1504 #elif defined(__i386__)
1506 #elif defined(_WIN64)
1507 this_arch =
"x86_64";
1508 #elif defined(_WIN32)
1510 #elif defined(__hppa__)
1512 #elif defined(__sh__)
1514 #elif defined(__loongarch__)
1515 this_arch =
"loongarch64";
1516 #elif defined(__EMSCRIPTEN__)
1517 this_arch =
"emscripten";
1520 this_arch =
"unknown";
1532 const char cp_separator =
';';
1534 const char cp_separator =
':';
1537 std::vector<std::string> class_path =
1540 java.
classpath.end(), class_path.begin(), class_path.end());
1554 this_os =
"openbsd";
1564 this_os =
"emscripten";
1593 const auto bits_for_positive_offset = offset_bits - 1;
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)
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
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,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::optional< T > string2optional(const std::string &str, int base=10)
convert a string to an integer, given the base of the representation works with signed and unsigned i...
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_arch_spec_loongarch64()
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
bool __float128_is_keyword
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()
void set_arch_spec_emscripten()
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