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:
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");
822 if(cmdline.
isset(
"function"))
825 if(cmdline.
isset(
'D'))
828 if(cmdline.
isset(
'I'))
831 if(cmdline.
isset(
"classpath"))
837 else if(cmdline.
isset(
"cp"))
846 const char *CLASSPATH=getenv(
"CLASSPATH");
847 if(CLASSPATH!=
nullptr)
853 if(cmdline.
isset(
"main-class"))
856 if(cmdline.
isset(
"include"))
868 if(cmdline.
isset(
"i386-linux"))
873 else if(cmdline.
isset(
"i386-win32") ||
874 cmdline.
isset(
"win32"))
879 else if(cmdline.
isset(
"winx64"))
884 else if(cmdline.
isset(
"i386-macos"))
889 else if(cmdline.
isset(
"ppc-macos"))
895 if(cmdline.
isset(
"arch"))
900 if(cmdline.
isset(
"os"))
912 if(cmdline.
isset(
"gcc"))
955 else if(os==
"linux" || os==
"solaris")
962 else if(os==
"freebsd")
996 if(arch==
"x64_64" && cmdline.
isset(
"gcc"))
1004 if(arch==this_arch && os==this_os)
1008 "int width shall be equal to the system int width");
1011 "long int width shall be equal to the system long int width");
1014 "bool width shall be equal to the system bool width");
1017 "char width shall be equal to the system char width");
1020 "short int width shall be equal to the system short int width");
1023 "long long int width shall be equal to the system long long int width");
1026 "pointer width shall be equal to the system pointer width");
1029 "float width shall be equal to the system float width");
1032 "double width shall be equal to the system double width");
1035 "char_is_unsigned flag shall indicate system char unsignedness");
1041 "long double width shall be equal to the system long double width");
1047 if(cmdline.
isset(
"16"))
1050 if(cmdline.
isset(
"32"))
1053 if(cmdline.
isset(
"64"))
1056 if(cmdline.
isset(
"LP64"))
1059 if(cmdline.
isset(
"ILP64"))
1062 if(cmdline.
isset(
"LLP64"))
1065 if(cmdline.
isset(
"ILP32"))
1068 if(cmdline.
isset(
"LP32"))
1071 if(cmdline.
isset(
"string-abstraction"))
1076 if(cmdline.
isset(
"no-library"))
1079 if(cmdline.
isset(
"little-endian"))
1082 if(cmdline.
isset(
"big-endian"))
1085 if(cmdline.
isset(
"little-endian") &&
1086 cmdline.
isset(
"big-endian"))
1089 if(cmdline.
isset(
"unsigned-char"))
1092 if(cmdline.
isset(
"round-to-even") ||
1093 cmdline.
isset(
"round-to-nearest"))
1096 if(cmdline.
isset(
"round-to-plus-inf"))
1099 if(cmdline.
isset(
"round-to-minus-inf"))
1102 if(cmdline.
isset(
"round-to-zero"))
1105 if(cmdline.
isset(
"object-bits"))
1111 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1114 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1116 if(cmdline.
isset(
"malloc-fail-null"))
1118 if(cmdline.
isset(
"malloc-fail-assert"))
1131 case ost::OS_LINUX:
return "linux";
1132 case ost::OS_MACOS:
return "macos";
1133 case ost::OS_WIN:
return "win";
1134 case ost::NO_OS:
return "none";
1144 return ost::OS_LINUX;
1145 else if(os==
"macos")
1146 return ost::OS_MACOS;
1155 const std::string &what)
1160 const bool not_found = ns.
lookup(
id, symbol);
1166 tmp.
id() == ID_address_of &&
1170 "symbol table configuration entry '" +
id2string(
id) +
1171 "' must be a string constant");
1178 const std::string &what)
1183 const bool not_found = ns.
lookup(
id, symbol);
1190 tmp.
id() == ID_constant,
1191 "symbol table configuration entry '" +
id2string(
id) +
1192 "' must be a constant");
1199 "symbol table configuration entry '" +
id2string(
id) +
1200 "' must be convertible to mp_integer");
1202 return numeric_cast_v<unsigned>(int_value);
1277 const symbolt &entry_point_symbol=*maybe_symbol;
1279 if(entry_point_symbol.
mode==ID_java)
1281 else if(entry_point_symbol.
mode==ID_C)
1283 else if(entry_point_symbol.
mode==ID_cpp)
1287 "object_bits should fit into pointer width");
1309 this_arch =
"alpha";
1310 #elif defined(__armel__)
1311 this_arch =
"armel";
1312 #elif defined(__aarch64__)
1313 this_arch =
"arm64";
1314 #elif defined(__arm__)
1315 #ifdef __ARM_PCS_VFP
1316 this_arch =
"armhf";
1320 #elif defined(__mipsel__)
1321 #if _MIPS_SIM==_ABIO32
1322 this_arch =
"mipsel";
1323 #elif _MIPS_SIM==_ABIN32
1324 this_arch =
"mipsn32el";
1326 this_arch =
"mips64el";
1328 #elif defined(__mips__)
1329 #if _MIPS_SIM==_ABIO32
1331 #elif _MIPS_SIM==_ABIN32
1332 this_arch =
"mipsn32";
1334 this_arch =
"mips64";
1336 #elif defined(__powerpc__)
1337 #if defined(__ppc64__) || defined(__PPC64__) || \
1338 defined(__powerpc64__) || defined(__POWERPC64__)
1339 #ifdef __LITTLE_ENDIAN__
1340 this_arch =
"ppc64le";
1342 this_arch =
"ppc64";
1345 this_arch =
"powerpc";
1347 #elif defined(__riscv)
1348 this_arch =
"riscv64";
1349 #elif defined(__sparc__)
1351 this_arch =
"sparc64";
1353 this_arch =
"sparc";
1355 #elif defined(__ia64__)
1357 #elif defined(__s390x__)
1358 this_arch =
"s390x";
1359 #elif defined(__s390__)
1361 #elif defined(__x86_64__)
1365 this_arch =
"x86_64";
1367 #elif defined(__i386__)
1369 #elif defined(_WIN64)
1370 this_arch =
"x86_64";
1371 #elif defined(_WIN32)
1373 #elif defined(__hppa__)
1375 #elif defined(__sh__)
1379 this_arch =
"unknown";
1391 const char cp_separator =
';';
1393 const char cp_separator =
':';
1396 std::vector<std::string> class_path =
1399 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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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()
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()
malloc_failure_modet malloc_failure_mode
std::size_t pointer_width
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
API to expression classes.
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.