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__)
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")
795 if(cmdline.
isset(
"function"))
798 if(cmdline.
isset(
'D'))
801 if(cmdline.
isset(
'I'))
804 if(cmdline.
isset(
"classpath"))
810 else if(cmdline.
isset(
"cp"))
819 const char *CLASSPATH=getenv(
"CLASSPATH");
820 if(CLASSPATH!=
nullptr)
826 if(cmdline.
isset(
"main-class"))
829 if(cmdline.
isset(
"include"))
841 if(cmdline.
isset(
"i386-linux"))
846 else if(cmdline.
isset(
"i386-win32") ||
847 cmdline.
isset(
"win32"))
852 else if(cmdline.
isset(
"winx64"))
857 else if(cmdline.
isset(
"i386-macos"))
862 else if(cmdline.
isset(
"ppc-macos"))
868 if(cmdline.
isset(
"arch"))
873 if(cmdline.
isset(
"os"))
885 if(cmdline.
isset(
"gcc"))
926 else if(os==
"linux" || os==
"solaris")
933 else if(os==
"freebsd")
967 if(arch==
"x64_64" && cmdline.
isset(
"gcc"))
975 if(arch==this_arch && os==this_os)
979 "int width shall be equal to the system int width");
982 "long int width shall be equal to the system long int width");
985 "bool width shall be equal to the system bool width");
988 "char width shall be equal to the system char width");
991 "short int width shall be equal to the system short int width");
994 "long long int width shall be equal to the system long long int width");
997 "pointer width shall be equal to the system pointer width");
1000 "float width shall be equal to the system float width");
1003 "double width shall be equal to the system double width");
1006 "char_is_unsigned flag shall indicate system char unsignedness");
1012 "long double width shall be equal to the system long double width");
1018 if(cmdline.
isset(
"16"))
1021 if(cmdline.
isset(
"32"))
1024 if(cmdline.
isset(
"64"))
1027 if(cmdline.
isset(
"LP64"))
1030 if(cmdline.
isset(
"ILP64"))
1033 if(cmdline.
isset(
"LLP64"))
1036 if(cmdline.
isset(
"ILP32"))
1039 if(cmdline.
isset(
"LP32"))
1042 if(cmdline.
isset(
"string-abstraction"))
1047 if(cmdline.
isset(
"no-library"))
1050 if(cmdline.
isset(
"little-endian"))
1053 if(cmdline.
isset(
"big-endian"))
1056 if(cmdline.
isset(
"little-endian") &&
1057 cmdline.
isset(
"big-endian"))
1060 if(cmdline.
isset(
"unsigned-char"))
1063 if(cmdline.
isset(
"round-to-even") ||
1064 cmdline.
isset(
"round-to-nearest"))
1067 if(cmdline.
isset(
"round-to-plus-inf"))
1070 if(cmdline.
isset(
"round-to-minus-inf"))
1073 if(cmdline.
isset(
"round-to-zero"))
1076 if(cmdline.
isset(
"object-bits"))
1085 "object-bits must be positive and less than the pointer width (" +
1100 case ost::OS_LINUX:
return "linux";
1101 case ost::OS_MACOS:
return "macos";
1102 case ost::OS_WIN:
return "win";
1103 default:
return "none";
1110 return ost::OS_LINUX;
1111 else if(os==
"macos")
1112 return ost::OS_MACOS;
1121 const std::string &what)
1126 const bool not_found = ns.
lookup(
id, symbol);
1132 tmp.
id() == ID_address_of &&
1136 "symbol table configuration entry `" +
id2string(
id) +
1137 "' must be a string constant");
1144 const std::string &what)
1149 const bool not_found = ns.
lookup(
id, symbol);
1156 tmp.
id() == ID_constant,
1157 "symbol table configuration entry `" +
id2string(
id) +
1158 "' must be a constant");
1165 "symbol table configuration entry `" +
id2string(
id) +
1166 "' must be convertible to mp_integer");
1168 return numeric_cast_v<unsigned>(int_value);
1243 const symbolt &entry_point_symbol=*maybe_symbol;
1245 if(entry_point_symbol.
mode==ID_java)
1247 else if(entry_point_symbol.
mode==ID_C)
1249 else if(entry_point_symbol.
mode==ID_cpp)
1253 "object_bits should fit into pointer width");
1275 this_arch =
"alpha";
1276 #elif defined(__armel__)
1277 this_arch =
"armel";
1278 #elif defined(__aarch64__)
1279 this_arch =
"arm64";
1280 #elif defined(__arm__)
1281 #ifdef __ARM_PCS_VFP
1282 this_arch =
"armhf";
1286 #elif defined(__mipsel__)
1287 #if _MIPS_SIM==_ABIO32
1288 this_arch =
"mipsel";
1289 #elif _MIPS_SIM==_ABIN32
1290 this_arch =
"mipsn32el";
1292 this_arch =
"mips64el";
1294 #elif defined(__mips__)
1295 #if _MIPS_SIM==_ABIO32
1297 #elif _MIPS_SIM==_ABIN32
1298 this_arch =
"mipsn32";
1300 this_arch =
"mips64";
1302 #elif defined(__powerpc__)
1303 #if defined(__ppc64__) || defined(__PPC64__) || \
1304 defined(__powerpc64__) || defined(__POWERPC64__)
1305 #ifdef __LITTLE_ENDIAN__
1306 this_arch =
"ppc64le";
1308 this_arch =
"ppc64";
1311 this_arch =
"powerpc";
1313 #elif defined(__riscv)
1314 this_arch =
"riscv64";
1315 #elif defined(__sparc__)
1317 this_arch =
"sparc64";
1319 this_arch =
"sparc";
1321 #elif defined(__ia64__)
1323 #elif defined(__s390x__)
1324 this_arch =
"s390x";
1325 #elif defined(__s390__)
1327 #elif defined(__x86_64__)
1331 this_arch =
"x86_64";
1333 #elif defined(__i386__)
1335 #elif defined(_WIN64)
1336 this_arch =
"x86_64";
1337 #elif defined(_WIN32)
1339 #elif defined(__hppa__)
1341 #elif defined(__sh__)
1345 this_arch =
"unknown";
1357 const char cp_separator =
';';
1359 const char cp_separator =
':';
1362 std::vector<std::string> class_path =
1365 java.
classpath.end(), class_path.begin(), class_path.end());
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()
struct configt::javat java
static ost string_to_os(const std::string &)
virtual bool isset(char option) const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void set_arch_spec_s390x()
std::size_t wchar_t_width
std::list< std::string > include_paths
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)
void set_arch_spec_i386()
Base class for all expressions.
ieee_floatt::rounding_modet rounding_mode
struct configt::ansi_ct ansi_c
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)
void set_arch_spec_hppa()
#define UNREACHABLE
This should be used to mark dead code.
Globally accessible architectural configuration.
enum configt::cppt::cpp_standardt cpp_standard
struct configt::bv_encodingt bv_encoding
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)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
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)
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
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
enum configt::ansi_ct::c_standardt c_standard
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()
void set_arch_spec_sparc(const irep_idt &subarch)
void set_LP64()
int=32, long=64, pointer=64
std::size_t long_double_width
unsigned unsafe_string2unsigned(const std::string &str, int base)
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()
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
static const std::size_t default_object_bits
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
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.