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")
796 if(cmdline.
isset(
"function"))
799 if(cmdline.
isset(
'D'))
802 if(cmdline.
isset(
'I'))
805 if(cmdline.
isset(
"classpath"))
811 else if(cmdline.
isset(
"cp"))
820 const char *CLASSPATH=getenv(
"CLASSPATH");
821 if(CLASSPATH!=
nullptr)
827 if(cmdline.
isset(
"main-class"))
830 if(cmdline.
isset(
"include"))
842 if(cmdline.
isset(
"i386-linux"))
847 else if(cmdline.
isset(
"i386-win32") ||
848 cmdline.
isset(
"win32"))
853 else if(cmdline.
isset(
"winx64"))
858 else if(cmdline.
isset(
"i386-macos"))
863 else if(cmdline.
isset(
"ppc-macos"))
869 if(cmdline.
isset(
"arch"))
874 if(cmdline.
isset(
"os"))
886 if(cmdline.
isset(
"gcc"))
929 else if(os==
"linux" || os==
"solaris")
936 else if(os==
"freebsd")
970 if(arch==
"x64_64" && cmdline.
isset(
"gcc"))
978 if(arch==this_arch && os==this_os)
982 "int width shall be equal to the system int width");
985 "long int width shall be equal to the system long int width");
988 "bool width shall be equal to the system bool width");
991 "char width shall be equal to the system char width");
994 "short int width shall be equal to the system short int width");
997 "long long int width shall be equal to the system long long int width");
1000 "pointer width shall be equal to the system pointer width");
1003 "float width shall be equal to the system float width");
1006 "double width shall be equal to the system double width");
1009 "char_is_unsigned flag shall indicate system char unsignedness");
1015 "long double width shall be equal to the system long double width");
1021 if(cmdline.
isset(
"16"))
1024 if(cmdline.
isset(
"32"))
1027 if(cmdline.
isset(
"64"))
1030 if(cmdline.
isset(
"LP64"))
1033 if(cmdline.
isset(
"ILP64"))
1036 if(cmdline.
isset(
"LLP64"))
1039 if(cmdline.
isset(
"ILP32"))
1042 if(cmdline.
isset(
"LP32"))
1045 if(cmdline.
isset(
"string-abstraction"))
1050 if(cmdline.
isset(
"no-library"))
1053 if(cmdline.
isset(
"little-endian"))
1056 if(cmdline.
isset(
"big-endian"))
1059 if(cmdline.
isset(
"little-endian") &&
1060 cmdline.
isset(
"big-endian"))
1063 if(cmdline.
isset(
"unsigned-char"))
1066 if(cmdline.
isset(
"round-to-even") ||
1067 cmdline.
isset(
"round-to-nearest"))
1070 if(cmdline.
isset(
"round-to-plus-inf"))
1073 if(cmdline.
isset(
"round-to-minus-inf"))
1076 if(cmdline.
isset(
"round-to-zero"))
1079 if(cmdline.
isset(
"object-bits"))
1088 "object-bits must be positive and less than the pointer width (" +
1104 case ost::OS_LINUX:
return "linux";
1105 case ost::OS_MACOS:
return "macos";
1106 case ost::OS_WIN:
return "win";
1107 case ost::NO_OS:
return "none";
1117 return ost::OS_LINUX;
1118 else if(os==
"macos")
1119 return ost::OS_MACOS;
1128 const std::string &what)
1133 const bool not_found = ns.
lookup(
id, symbol);
1139 tmp.
id() == ID_address_of &&
1143 "symbol table configuration entry '" +
id2string(
id) +
1144 "' must be a string constant");
1151 const std::string &what)
1156 const bool not_found = ns.
lookup(
id, symbol);
1163 tmp.
id() == ID_constant,
1164 "symbol table configuration entry '" +
id2string(
id) +
1165 "' must be a constant");
1172 "symbol table configuration entry '" +
id2string(
id) +
1173 "' must be convertible to mp_integer");
1175 return numeric_cast_v<unsigned>(int_value);
1250 const symbolt &entry_point_symbol=*maybe_symbol;
1252 if(entry_point_symbol.
mode==ID_java)
1254 else if(entry_point_symbol.
mode==ID_C)
1256 else if(entry_point_symbol.
mode==ID_cpp)
1260 "object_bits should fit into pointer width");
1282 this_arch =
"alpha";
1283 #elif defined(__armel__)
1284 this_arch =
"armel";
1285 #elif defined(__aarch64__)
1286 this_arch =
"arm64";
1287 #elif defined(__arm__)
1288 #ifdef __ARM_PCS_VFP
1289 this_arch =
"armhf";
1293 #elif defined(__mipsel__)
1294 #if _MIPS_SIM==_ABIO32
1295 this_arch =
"mipsel";
1296 #elif _MIPS_SIM==_ABIN32
1297 this_arch =
"mipsn32el";
1299 this_arch =
"mips64el";
1301 #elif defined(__mips__)
1302 #if _MIPS_SIM==_ABIO32
1304 #elif _MIPS_SIM==_ABIN32
1305 this_arch =
"mipsn32";
1307 this_arch =
"mips64";
1309 #elif defined(__powerpc__)
1310 #if defined(__ppc64__) || defined(__PPC64__) || \
1311 defined(__powerpc64__) || defined(__POWERPC64__)
1312 #ifdef __LITTLE_ENDIAN__
1313 this_arch =
"ppc64le";
1315 this_arch =
"ppc64";
1318 this_arch =
"powerpc";
1320 #elif defined(__riscv)
1321 this_arch =
"riscv64";
1322 #elif defined(__sparc__)
1324 this_arch =
"sparc64";
1326 this_arch =
"sparc";
1328 #elif defined(__ia64__)
1330 #elif defined(__s390x__)
1331 this_arch =
"s390x";
1332 #elif defined(__s390__)
1334 #elif defined(__x86_64__)
1338 this_arch =
"x86_64";
1340 #elif defined(__i386__)
1342 #elif defined(_WIN64)
1343 this_arch =
"x86_64";
1344 #elif defined(_WIN32)
1346 #elif defined(__hppa__)
1348 #elif defined(__sh__)
1352 this_arch =
"unknown";
1364 const char cp_separator =
';';
1366 const char cp_separator =
':';
1369 std::vector<std::string> class_path =
1372 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
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.
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)
#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
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
unsigned unsafe_string2unsigned(const std::string &str, int base)
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()
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
enum configt::cppt::cpp_standardt cpp_standard
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.