Go to the documentation of this file.
53 long_long_int_width=8*8;
57 long_double_width=16*8;
58 char_is_unsigned=
false;
59 wchar_t_is_unsigned=
false;
62 memory_operand_size=int_width/8;
77 long_long_int_width=8*8;
81 long_double_width=8*8;
82 char_is_unsigned=
false;
83 wchar_t_is_unsigned=
false;
86 memory_operand_size=int_width/8;
97 long_long_int_width=8*8;
101 long_double_width=8*8;
102 char_is_unsigned=
false;
103 wchar_t_is_unsigned=
false;
106 memory_operand_size=int_width/8;
117 long_long_int_width=8*8;
121 long_double_width=12*8;
122 char_is_unsigned=
false;
123 wchar_t_is_unsigned=
false;
126 memory_operand_size=int_width/8;
137 long_long_int_width=8*8;
141 long_double_width=8*8;
142 char_is_unsigned=
false;
143 wchar_t_is_unsigned=
false;
146 memory_operand_size=int_width/8;
152 endianness=endiannesst::IS_LITTLE_ENDIAN;
153 char_is_unsigned=
false;
159 case flavourt::CLANG:
160 defines.push_back(
"i386");
161 defines.push_back(
"__i386");
162 defines.push_back(
"__i386__");
163 if(mode == flavourt::CLANG)
164 defines.push_back(
"__LITTLE_ENDIAN__");
167 case flavourt::VISUAL_STUDIO:
168 defines.push_back(
"_M_IX86");
171 case flavourt::CODEWARRIOR:
184 endianness=endiannesst::IS_LITTLE_ENDIAN;
185 long_double_width=16*8;
186 char_is_unsigned=
false;
192 case flavourt::CLANG:
193 defines.push_back(
"__LP64__");
194 defines.push_back(
"__x86_64");
195 defines.push_back(
"__x86_64__");
196 defines.push_back(
"_LP64");
197 defines.push_back(
"__amd64__");
198 defines.push_back(
"__amd64");
200 if(os == ost::OS_MACOS)
201 defines.push_back(
"__LITTLE_ENDIAN__");
204 case flavourt::VISUAL_STUDIO:
205 defines.push_back(
"_M_X64");
206 defines.push_back(
"_M_AMD64");
209 case flavourt::CODEWARRIOR:
221 if(subarch==
"powerpc")
226 if(subarch==
"ppc64le")
227 endianness=endiannesst::IS_LITTLE_ENDIAN;
229 endianness=endiannesst::IS_BIG_ENDIAN;
231 long_double_width=16*8;
232 char_is_unsigned=
true;
238 case flavourt::CLANG:
239 defines.push_back(
"__powerpc");
240 defines.push_back(
"__powerpc__");
241 defines.push_back(
"__POWERPC__");
242 defines.push_back(
"__ppc__");
244 if(os == ost::OS_MACOS)
245 defines.push_back(
"__BIG_ENDIAN__");
247 if(subarch!=
"powerpc")
249 defines.push_back(
"__powerpc64");
250 defines.push_back(
"__powerpc64__");
251 defines.push_back(
"__PPC64__");
252 defines.push_back(
"__ppc64__");
253 if(subarch==
"ppc64le")
255 defines.push_back(
"_CALL_ELF=2");
256 defines.push_back(
"__LITTLE_ENDIAN__");
260 defines.push_back(
"_CALL_ELF=1");
261 defines.push_back(
"__BIG_ENDIAN__");
266 case flavourt::VISUAL_STUDIO:
267 defines.push_back(
"_M_PPC");
270 case flavourt::CODEWARRIOR:
285 long_double_width=16*8;
290 long_double_width=8*8;
293 endianness=endiannesst::IS_LITTLE_ENDIAN;
294 char_is_unsigned=
true;
300 case flavourt::CLANG:
302 defines.push_back(
"__aarch64__");
304 defines.push_back(
"__arm__");
306 defines.push_back(
"__ARM_PCS_VFP");
309 case flavourt::VISUAL_STUDIO:
310 defines.push_back(
"_M_ARM");
313 case flavourt::CODEWARRIOR:
326 endianness=endiannesst::IS_LITTLE_ENDIAN;
327 long_double_width=16*8;
328 char_is_unsigned=
false;
334 defines.push_back(
"__alpha__");
337 case flavourt::VISUAL_STUDIO:
338 defines.push_back(
"_M_ALPHA");
341 case flavourt::CLANG:
342 case flavourt::CODEWARRIOR:
354 if(subarch==
"mipsel" ||
356 subarch==
"mipsn32el" ||
360 long_double_width=8*8;
365 long_double_width=16*8;
368 if(subarch==
"mipsel" ||
369 subarch==
"mipsn32el" ||
371 endianness=endiannesst::IS_LITTLE_ENDIAN;
373 endianness=endiannesst::IS_BIG_ENDIAN;
375 char_is_unsigned=
false;
381 defines.push_back(
"__mips__");
382 defines.push_back(
"mips");
387 case flavourt::VISUAL_STUDIO:
391 case flavourt::CLANG:
392 case flavourt::CODEWARRIOR:
405 endianness = endiannesst::IS_LITTLE_ENDIAN;
406 long_double_width = 16 * 8;
407 char_is_unsigned =
true;
413 defines.push_back(
"__riscv");
416 case flavourt::VISUAL_STUDIO:
417 case flavourt::CLANG:
418 case flavourt::CODEWARRIOR:
431 endianness=endiannesst::IS_BIG_ENDIAN;
432 long_double_width=16*8;
433 char_is_unsigned=
true;
439 defines.push_back(
"__s390__");
442 case flavourt::VISUAL_STUDIO:
446 case flavourt::CLANG:
447 case flavourt::CODEWARRIOR:
460 endianness=endiannesst::IS_BIG_ENDIAN;
461 char_is_unsigned=
true;
467 defines.push_back(
"__s390x__");
470 case flavourt::VISUAL_STUDIO:
474 case flavourt::CLANG:
475 case flavourt::CODEWARRIOR:
487 if(subarch==
"sparc64")
490 long_double_width=16*8;
495 long_double_width=16*8;
498 endianness=endiannesst::IS_BIG_ENDIAN;
499 char_is_unsigned=
false;
505 defines.push_back(
"__sparc__");
506 if(subarch==
"sparc64")
507 defines.push_back(
"__arch64__");
510 case flavourt::VISUAL_STUDIO:
514 case flavourt::CLANG:
515 case flavourt::CODEWARRIOR:
528 long_double_width=16*8;
529 endianness=endiannesst::IS_LITTLE_ENDIAN;
530 char_is_unsigned=
false;
536 defines.push_back(
"__ia64__");
537 defines.push_back(
"_IA64");
538 defines.push_back(
"__IA64__");
541 case flavourt::VISUAL_STUDIO:
542 defines.push_back(
"_M_IA64");
545 case flavourt::CLANG:
546 case flavourt::CODEWARRIOR:
561 long_double_width=16*8;
562 endianness=endiannesst::IS_LITTLE_ENDIAN;
563 char_is_unsigned=
false;
569 defines.push_back(
"__ILP32__");
570 defines.push_back(
"__x86_64");
571 defines.push_back(
"__x86_64__");
572 defines.push_back(
"__amd64__");
573 defines.push_back(
"__amd64");
576 case flavourt::VISUAL_STUDIO:
580 case flavourt::CLANG:
581 case flavourt::CODEWARRIOR:
605 long_double_width=8*8;
606 endianness=endiannesst::IS_LITTLE_ENDIAN;
609 char_is_unsigned=
false;
618 long_double_width=8*8;
619 endianness=endiannesst::IS_BIG_ENDIAN;
620 char_is_unsigned=
false;
626 defines.push_back(
"__hppa__");
629 case flavourt::VISUAL_STUDIO:
633 case flavourt::CLANG:
634 case flavourt::CODEWARRIOR:
647 long_double_width=8*8;
648 endianness=endiannesst::IS_LITTLE_ENDIAN;
649 char_is_unsigned=
false;
655 defines.push_back(
"__sh__");
656 defines.push_back(
"__SH4__");
659 case flavourt::VISUAL_STUDIO:
663 case flavourt::CLANG:
664 case flavourt::CODEWARRIOR:
676 #if defined(__APPLE__)
678 return c_standardt::C11;
679 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
682 return c_standardt::C99;
685 return c_standardt::C11;
695 return cpp_standardt::CPP14;
697 return cpp_standardt::CPP98;
712 if(
sizeof(
long int)==8)
717 else if(arch==
"alpha")
719 else if(arch==
"arm64" ||
724 else if(arch==
"mips64el" ||
731 else if(arch==
"powerpc" ||
735 else if(arch ==
"riscv64")
737 else if(arch==
"sparc" ||
740 else if(arch==
"ia64")
742 else if(arch==
"s390x")
744 else if(arch==
"s390")
748 else if(arch==
"v850")
750 else if(arch==
"hppa")
754 else if(arch==
"x86_64")
756 else if(arch==
"i386")
775 const std::string &argument,
776 const std::size_t pointer_width)
778 const auto throw_for_reason = [&](
const std::string &reason) {
780 "Value of \"" + argument +
"\" given for object-bits is " + reason +
781 ". object-bits must be positive and less than the pointer width (" +
785 const auto object_bits = string2optional<unsigned int>(argument);
787 throw_for_reason(
"not a valid unsigned integer");
788 if(*object_bits == 0 || *object_bits >= pointer_width)
789 throw_for_reason(
"out of range");
821 if(cmdline.
isset(
"function"))
824 if(cmdline.
isset(
'D'))
827 if(cmdline.
isset(
'I'))
830 if(cmdline.
isset(
"classpath"))
836 else if(cmdline.
isset(
"cp"))
845 const char *CLASSPATH=getenv(
"CLASSPATH");
846 if(CLASSPATH!=
nullptr)
852 if(cmdline.
isset(
"main-class"))
855 if(cmdline.
isset(
"include"))
867 if(cmdline.
isset(
"i386-linux"))
872 else if(cmdline.
isset(
"i386-win32") ||
873 cmdline.
isset(
"win32"))
878 else if(cmdline.
isset(
"winx64"))
883 else if(cmdline.
isset(
"i386-macos"))
888 else if(cmdline.
isset(
"ppc-macos"))
894 if(cmdline.
isset(
"arch"))
899 if(cmdline.
isset(
"os"))
911 if(cmdline.
isset(
"gcc"))
954 else if(os==
"linux" || os==
"solaris")
961 else if(os==
"freebsd")
995 if(arch==
"x64_64" && cmdline.
isset(
"gcc"))
1000 else if(os ==
"macos" && arch ==
"arm64")
1010 if(arch==this_arch && os==this_os)
1014 "int width shall be equal to the system int width");
1017 "long int width shall be equal to the system long int width");
1020 "bool width shall be equal to the system bool width");
1023 "char width shall be equal to the system char width");
1026 "short int width shall be equal to the system short int width");
1029 "long long int width shall be equal to the system long long int width");
1032 "pointer width shall be equal to the system pointer width");
1035 "float width shall be equal to the system float width");
1038 "double width shall be equal to the system double width");
1041 "char_is_unsigned flag shall indicate system char unsignedness");
1047 "long double width shall be equal to the system long double width");
1053 if(cmdline.
isset(
"16"))
1056 if(cmdline.
isset(
"32"))
1059 if(cmdline.
isset(
"64"))
1062 if(cmdline.
isset(
"LP64"))
1065 if(cmdline.
isset(
"ILP64"))
1068 if(cmdline.
isset(
"LLP64"))
1071 if(cmdline.
isset(
"ILP32"))
1074 if(cmdline.
isset(
"LP32"))
1077 if(cmdline.
isset(
"string-abstraction"))
1082 if(cmdline.
isset(
"no-library"))
1085 if(cmdline.
isset(
"little-endian"))
1088 if(cmdline.
isset(
"big-endian"))
1091 if(cmdline.
isset(
"little-endian") &&
1092 cmdline.
isset(
"big-endian"))
1095 if(cmdline.
isset(
"unsigned-char"))
1098 if(cmdline.
isset(
"round-to-even") ||
1099 cmdline.
isset(
"round-to-nearest"))
1102 if(cmdline.
isset(
"round-to-plus-inf"))
1105 if(cmdline.
isset(
"round-to-minus-inf"))
1108 if(cmdline.
isset(
"round-to-zero"))
1111 if(cmdline.
isset(
"object-bits"))
1117 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1120 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1122 if(cmdline.
isset(
"malloc-fail-null"))
1124 if(cmdline.
isset(
"malloc-fail-assert"))
1129 if(cmdline.
isset(
"c89"))
1132 if(cmdline.
isset(
"c99"))
1135 if(cmdline.
isset(
"c11"))
1138 if(cmdline.
isset(
"cpp98"))
1141 if(cmdline.
isset(
"cpp03"))
1144 if(cmdline.
isset(
"cpp11"))
1155 case ost::OS_LINUX:
return "linux";
1156 case ost::OS_MACOS:
return "macos";
1157 case ost::OS_WIN:
return "win";
1158 case ost::NO_OS:
return "none";
1168 return ost::OS_LINUX;
1169 else if(os==
"macos")
1170 return ost::OS_MACOS;
1179 const std::string &what)
1184 const bool not_found = ns.
lookup(
id, symbol);
1190 tmp.
id() == ID_address_of &&
1194 "symbol table configuration entry '" +
id2string(
id) +
1195 "' must be a string constant");
1202 const std::string &what)
1207 const bool not_found = ns.
lookup(
id, symbol);
1214 tmp.
id() == ID_constant,
1215 "symbol table configuration entry '" +
id2string(
id) +
1216 "' must be a constant");
1223 "symbol table configuration entry '" +
id2string(
id) +
1224 "' must be convertible to mp_integer");
1226 return numeric_cast_v<unsigned>(int_value);
1300 const symbolt &entry_point_symbol=*maybe_symbol;
1302 if(entry_point_symbol.
mode==ID_java)
1304 else if(entry_point_symbol.
mode==ID_C)
1306 else if(entry_point_symbol.
mode==ID_cpp)
1310 "object_bits should fit into pointer width");
1332 this_arch =
"alpha";
1333 #elif defined(__armel__)
1334 this_arch =
"armel";
1335 #elif defined(__aarch64__)
1336 this_arch =
"arm64";
1337 #elif defined(__arm__)
1338 #ifdef __ARM_PCS_VFP
1339 this_arch =
"armhf";
1343 #elif defined(__mipsel__)
1344 #if _MIPS_SIM==_ABIO32
1345 this_arch =
"mipsel";
1346 #elif _MIPS_SIM==_ABIN32
1347 this_arch =
"mipsn32el";
1349 this_arch =
"mips64el";
1351 #elif defined(__mips__)
1352 #if _MIPS_SIM==_ABIO32
1354 #elif _MIPS_SIM==_ABIN32
1355 this_arch =
"mipsn32";
1357 this_arch =
"mips64";
1359 #elif defined(__powerpc__)
1360 #if defined(__ppc64__) || defined(__PPC64__) || \
1361 defined(__powerpc64__) || defined(__POWERPC64__)
1362 #ifdef __LITTLE_ENDIAN__
1363 this_arch =
"ppc64le";
1365 this_arch =
"ppc64";
1368 this_arch =
"powerpc";
1370 #elif defined(__riscv)
1371 this_arch =
"riscv64";
1372 #elif defined(__sparc__)
1374 this_arch =
"sparc64";
1376 this_arch =
"sparc";
1378 #elif defined(__ia64__)
1380 #elif defined(__s390x__)
1381 this_arch =
"s390x";
1382 #elif defined(__s390__)
1384 #elif defined(__x86_64__)
1388 this_arch =
"x86_64";
1390 #elif defined(__i386__)
1392 #elif defined(_WIN64)
1393 this_arch =
"x86_64";
1394 #elif defined(_WIN32)
1396 #elif defined(__hppa__)
1398 #elif defined(__sh__)
1402 this_arch =
"unknown";
1414 const char cp_separator =
';';
1416 const char cp_separator =
':';
1419 std::vector<std::string> class_path =
1422 java.
classpath.end(), class_path.begin(), class_path.end());
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool ts_18661_3_Floatn_types
std::list< std::string > defines
std::string object_bits_info()
static ost string_to_os(const std::string &)
struct configt::bv_encodingt bv_encoding
virtual bool isset(char option) const
void set_arch_spec_s390x()
std::size_t wchar_t_width
std::list< std::string > include_paths
@ malloc_failure_mode_assert_then_assume
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
void set_arch_spec_mips(const irep_idt &subarch)
optionalt< std::string > main
void set_arch_spec_i386()
Base class for all expressions.
ieee_floatt::rounding_modet rounding_mode
void set_LP32()
int=16, long=32, pointer=32
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void set_arch_spec_power(const irep_idt &subarch)
struct configt::ansi_ct ansi_c
void set_arch_spec_hppa()
Globally accessible architectural configuration.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_arch_spec_ia64()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
irep_idt mode
Language mode.
void set_arch_spec_arm(const irep_idt &subarch)
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
void set_arch_spec_s390()
preprocessort preprocessor
@ malloc_failure_mode_return_null
void set_arch_spec_riscv64()
static const std::size_t default_object_bits
static const std::size_t default_object_bits
void set_arch_spec_alpha()
API to expression classes for Pointers.
bool is_object_bits_default
std::size_t memory_operand_size
std::string get_value(char option) const
bool simplify(exprt &expr, const namespacet &ns)
std::size_t long_long_int_width
void set_ILP64()
int=64, long=64, pointer=64
mp_integer alignment(const typet &type, const namespacet &ns)
static irep_idt this_operating_system()
const irep_idt & id() const
void set_LLP64()
int=32, long=32, pointer=64
void set_from_symbol_table(const symbol_tablet &)
static std::string os_to_string(ost)
static const std::size_t default_object_bits
std::list< std::string > include_files
static c_standardt default_c_standard()
void set_ILP32()
int=32, long=32, pointer=32
static irep_idt this_architecture()
exprt value
Initial value of symbol.
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
const irep_idt & get(const irep_namet &name) const
bool set(const cmdlinet &cmdline)
static cpp_standardt default_cpp_standard()
enum configt::ansi_ct::c_standardt c_standard
void set_arch_spec_sparc(const irep_idt &subarch)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
void set_LP64()
int=32, long=64, pointer=64
std::size_t long_double_width
struct configt::javat java
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
std::size_t short_int_width
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void set_arch_spec_x86_64()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
malloc_failure_modet malloc_failure_mode
std::size_t pointer_width
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void set_classpath(const std::string &cp)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool single_precision_constant
const std::list< std::string > & get_values(const std::string &option) const
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
void set_arch(const irep_idt &)
std::size_t long_int_width
enum configt::cppt::cpp_standardt cpp_standard
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.