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());
void set_arch_spec_arm(const irep_idt &subarch)
const std::list< std::string > & get_values(const std::string &option) const
void set_LP32()
int=16, long=32, pointer=32
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
void set_arch_spec_power(const irep_idt &subarch)
Globally accessible architectural configuration.
irep_idt mode
Language mode.
void set_classpath(const std::string &cp)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string object_bits_info()
static std::string os_to_string(ost)
unsigned unsafe_string2unsigned(const std::string &str, int base)
bool single_precision_constant
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
std::list< std::string > defines
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
exprt value
Initial value of symbol.
std::string get_value(char option) const
void set_arch_spec_riscv64()
void set_LP64()
int=32, long=64, pointer=64
void set_arch_spec_ia64()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
static const std::size_t default_object_bits
void set_arch_spec_mips(const irep_idt &subarch)
static const std::size_t default_object_bits
struct configt::bv_encodingt bv_encoding
preprocessort preprocessor
bool set(const cmdlinet &cmdline)
const irep_idt & id() const
std::list< std::string > include_files
std::size_t long_long_int_width
virtual bool isset(char option) const
void set_arch_spec_sparc(const irep_idt &subarch)
void set_arch_spec_x86_64()
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
static const std::size_t default_object_bits
void set_arch(const irep_idt &)
API to expression classes.
mp_integer alignment(const typet &type, const namespacet &ns)
const irep_idt & get(const irep_namet &name) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_arch_spec_alpha()
enum configt::cppt::cpp_standardt cpp_standard
void set_ILP32()
int=32, long=32, pointer=32
struct configt::javat java
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void set_arch_spec_s390()
std::size_t pointer_width
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void set_from_symbol_table(const symbol_tablet &)
enum configt::ansi_ct::c_standardt c_standard
static c_standardt default_c_standard()
std::size_t wchar_t_width
static irep_idt this_operating_system()
ieee_floatt::rounding_modet rounding_mode
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...
bool is_object_bits_default
Base class for all expressions.
void set_arch_spec_hppa()
void set_arch_spec_i386()
#define UNREACHABLE
This should be used to mark dead code.
void set_LLP64()
int=32, long=32, pointer=64
static ost string_to_os(const std::string &)
std::size_t memory_operand_size
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
std::size_t long_int_width
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static cpp_standardt default_cpp_standard()
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool ts_18661_3_Floatn_types
static const std::size_t default_object_bits
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
static irep_idt this_architecture()
std::size_t short_int_width
void set_arch_spec_s390x()
std::size_t long_double_width
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
bool simplify(exprt &expr, const namespacet &ns)
void set_ILP64()
int=64, long=64, pointer=64
std::list< std::string > include_paths