54 long_long_int_width=8*8;
58 long_double_width=16*8;
59 char_is_unsigned=
false;
60 wchar_t_is_unsigned=
false;
63 memory_operand_size=int_width/8;
78 long_long_int_width=8*8;
82 long_double_width=8*8;
83 char_is_unsigned=
false;
84 wchar_t_is_unsigned=
false;
87 memory_operand_size=int_width/8;
98 long_long_int_width=8*8;
102 long_double_width=8*8;
103 char_is_unsigned=
false;
104 wchar_t_is_unsigned=
false;
107 memory_operand_size=int_width/8;
118 long_long_int_width=8*8;
122 long_double_width=12*8;
123 char_is_unsigned=
false;
124 wchar_t_is_unsigned=
false;
127 memory_operand_size=int_width/8;
138 long_long_int_width=8*8;
142 long_double_width=8*8;
143 char_is_unsigned=
false;
144 wchar_t_is_unsigned=
false;
147 memory_operand_size=int_width/8;
153 endianness=endiannesst::IS_LITTLE_ENDIAN;
154 char_is_unsigned=
false;
160 case flavourt::CLANG:
161 defines.push_back(
"i386");
162 defines.push_back(
"__i386");
163 defines.push_back(
"__i386__");
164 if(mode == flavourt::CLANG)
165 defines.push_back(
"__LITTLE_ENDIAN__");
168 case flavourt::VISUAL_STUDIO:
169 defines.push_back(
"_M_IX86");
172 case flavourt::CODEWARRIOR:
185 endianness=endiannesst::IS_LITTLE_ENDIAN;
186 long_double_width=16*8;
187 char_is_unsigned=
false;
193 case flavourt::CLANG:
194 defines.push_back(
"__LP64__");
195 defines.push_back(
"__x86_64");
196 defines.push_back(
"__x86_64__");
197 defines.push_back(
"_LP64");
198 defines.push_back(
"__amd64__");
199 defines.push_back(
"__amd64");
201 if(os == ost::OS_MACOS)
202 defines.push_back(
"__LITTLE_ENDIAN__");
205 case flavourt::VISUAL_STUDIO:
206 defines.push_back(
"_M_X64");
207 defines.push_back(
"_M_AMD64");
210 case flavourt::CODEWARRIOR:
228 endianness=endiannesst::IS_LITTLE_ENDIAN;
230 endianness=endiannesst::IS_BIG_ENDIAN;
232 long_double_width=16*8;
233 char_is_unsigned=
true;
239 case flavourt::CLANG:
240 defines.push_back(
"__powerpc");
241 defines.push_back(
"__powerpc__");
242 defines.push_back(
"__POWERPC__");
243 defines.push_back(
"__ppc__");
245 if(os == ost::OS_MACOS)
246 defines.push_back(
"__BIG_ENDIAN__");
250 defines.push_back(
"__powerpc64");
251 defines.push_back(
"__powerpc64__");
252 defines.push_back(
"__PPC64__");
253 defines.push_back(
"__ppc64__");
256 defines.push_back(
"_CALL_ELF=2");
257 defines.push_back(
"__LITTLE_ENDIAN__");
261 defines.push_back(
"_CALL_ELF=1");
262 defines.push_back(
"__BIG_ENDIAN__");
267 case flavourt::VISUAL_STUDIO:
268 defines.push_back(
"_M_PPC");
271 case flavourt::CODEWARRIOR:
286 long_double_width=16*8;
291 long_double_width=8*8;
294 endianness=endiannesst::IS_LITTLE_ENDIAN;
295 char_is_unsigned=
true;
301 case flavourt::CLANG:
303 defines.push_back(
"__aarch64__");
305 defines.push_back(
"__arm__");
307 defines.push_back(
"__ARM_PCS_VFP");
310 case flavourt::VISUAL_STUDIO:
311 defines.push_back(
"_M_ARM");
314 case flavourt::CODEWARRIOR:
327 endianness=endiannesst::IS_LITTLE_ENDIAN;
328 long_double_width=16*8;
329 char_is_unsigned=
false;
335 defines.push_back(
"__alpha__");
338 case flavourt::VISUAL_STUDIO:
339 defines.push_back(
"_M_ALPHA");
342 case flavourt::CLANG:
343 case flavourt::CODEWARRIOR:
361 long_double_width=8*8;
366 long_double_width=16*8;
372 endianness=endiannesst::IS_LITTLE_ENDIAN;
374 endianness=endiannesst::IS_BIG_ENDIAN;
376 char_is_unsigned=
false;
382 defines.push_back(
"__mips__");
383 defines.push_back(
"mips");
385 "_MIPS_SZPTR="+std::to_string(
config.
ansi_c.pointer_width));
388 case flavourt::VISUAL_STUDIO:
392 case flavourt::CLANG:
393 case flavourt::CODEWARRIOR:
406 endianness = endiannesst::IS_LITTLE_ENDIAN;
407 long_double_width = 16 * 8;
408 char_is_unsigned =
true;
414 defines.push_back(
"__riscv");
417 case flavourt::VISUAL_STUDIO:
418 case flavourt::CLANG:
419 case flavourt::CODEWARRIOR:
432 endianness=endiannesst::IS_BIG_ENDIAN;
433 long_double_width=16*8;
434 char_is_unsigned=
true;
440 defines.push_back(
"__s390__");
443 case flavourt::VISUAL_STUDIO:
447 case flavourt::CLANG:
448 case flavourt::CODEWARRIOR:
461 endianness=endiannesst::IS_BIG_ENDIAN;
462 char_is_unsigned=
true;
468 defines.push_back(
"__s390x__");
471 case flavourt::VISUAL_STUDIO:
475 case flavourt::CLANG:
476 case flavourt::CODEWARRIOR:
491 long_double_width=16*8;
496 long_double_width=16*8;
499 endianness=endiannesst::IS_BIG_ENDIAN;
500 char_is_unsigned=
false;
506 defines.push_back(
"__sparc__");
508 defines.push_back(
"__arch64__");
511 case flavourt::VISUAL_STUDIO:
515 case flavourt::CLANG:
516 case flavourt::CODEWARRIOR:
529 long_double_width=16*8;
530 endianness=endiannesst::IS_LITTLE_ENDIAN;
531 char_is_unsigned=
false;
537 defines.push_back(
"__ia64__");
538 defines.push_back(
"_IA64");
539 defines.push_back(
"__IA64__");
542 case flavourt::VISUAL_STUDIO:
543 defines.push_back(
"_M_IA64");
546 case flavourt::CLANG:
547 case flavourt::CODEWARRIOR:
562 long_double_width=16*8;
563 endianness=endiannesst::IS_LITTLE_ENDIAN;
564 char_is_unsigned=
false;
570 defines.push_back(
"__ILP32__");
571 defines.push_back(
"__x86_64");
572 defines.push_back(
"__x86_64__");
573 defines.push_back(
"__amd64__");
574 defines.push_back(
"__amd64");
577 case flavourt::VISUAL_STUDIO:
581 case flavourt::CLANG:
582 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;
711 ansi_c.NULL_is_zero=
false;
713 if(
sizeof(
long int)==8)
718 else if(arch==
"alpha")
719 ansi_c.set_arch_spec_alpha();
720 else if(arch==
"arm64" ||
724 ansi_c.set_arch_spec_arm(arch);
725 else if(arch==
"mips64el" ||
731 ansi_c.set_arch_spec_mips(arch);
732 else if(arch==
"powerpc" ||
735 ansi_c.set_arch_spec_power(arch);
736 else if(arch ==
"riscv64")
737 ansi_c.set_arch_spec_riscv64();
738 else if(arch==
"sparc" ||
740 ansi_c.set_arch_spec_sparc(arch);
741 else if(arch==
"ia64")
742 ansi_c.set_arch_spec_ia64();
743 else if(arch==
"s390x")
744 ansi_c.set_arch_spec_s390x();
745 else if(arch==
"s390")
746 ansi_c.set_arch_spec_s390();
748 ansi_c.set_arch_spec_x32();
749 else if(arch==
"v850")
750 ansi_c.set_arch_spec_v850();
751 else if(arch==
"hppa")
752 ansi_c.set_arch_spec_hppa();
754 ansi_c.set_arch_spec_sh4();
755 else if(arch==
"x86_64")
756 ansi_c.set_arch_spec_x86_64();
757 else if(arch==
"i386")
758 ansi_c.set_arch_spec_i386();
763 ansi_c.set_arch_spec_i386();
777 const std::size_t pointer_width)
781 "Value of \"" +
argument +
"\" given for object-bits is " + reason +
782 ". object-bits must be positive and less than the pointer width (" +
783 std::to_string(pointer_width) +
") ",
789 if(*object_bits == 0 || *object_bits >= pointer_width)
804 ansi_c.single_precision_constant=
false;
805 ansi_c.for_has_scope=
true;
806 ansi_c.ts_18661_3_Floatn_types=
false;
807 ansi_c.float16_type =
false;
815 ansi_c.NULL_is_zero=
reinterpret_cast<size_t>(
nullptr)==0;
824 if(cmdline.
isset(
"function"))
827 if(cmdline.
isset(
'D'))
830 if(cmdline.
isset(
'I'))
833 if(cmdline.
isset(
"classpath"))
839 else if(cmdline.
isset(
"cp"))
855 if(cmdline.
isset(
"main-class"))
858 if(cmdline.
isset(
"include"))
870 if(cmdline.
isset(
"i386-linux"))
875 else if(cmdline.
isset(
"i386-win32") ||
876 cmdline.
isset(
"win32"))
881 else if(cmdline.
isset(
"winx64"))
886 else if(cmdline.
isset(
"i386-macos"))
891 else if(cmdline.
isset(
"ppc-macos"))
897 if(cmdline.
isset(
"arch"))
902 if(cmdline.
isset(
"os"))
914 if(cmdline.
isset(
"gcc"))
923 ansi_c.defines.push_back(
"__CYGWIN__");
927 ansi_c.defines.push_back(
"__int64=long long");
957 else if(os==
"linux" || os==
"solaris")
964 else if(os==
"freebsd")
981 ansi_c.gcc__float128_type =
true;
994 ansi_c.wchar_t_is_unsigned=
true;
998 if(arch ==
"x86_64" && cmdline.
isset(
"gcc"))
999 ansi_c.long_double_width=16*8;
1001 ansi_c.long_double_width=8*8;
1003 else if(os ==
"macos" && arch ==
"arm64")
1007 ansi_c.char_is_unsigned =
false;
1008 ansi_c.long_double_width = 8 * 8;
1017 "int width shall be equal to the system int width");
1020 "long int width shall be equal to the system long int width");
1023 "bool width shall be equal to the system bool width");
1026 "char width shall be equal to the system char width");
1029 "short int width shall be equal to the system short int width");
1032 "long long int width shall be equal to the system long long int width");
1035 "pointer width shall be equal to the system pointer width");
1038 "float width shall be equal to the system float width");
1041 "double width shall be equal to the system double width");
1043 ansi_c.char_is_unsigned ==
1045 "char_is_unsigned flag shall indicate system char unsignedness");
1051 "long double width shall be equal to the system long double width");
1057 if(cmdline.
isset(
"16"))
1060 if(cmdline.
isset(
"32"))
1063 if(cmdline.
isset(
"64"))
1066 if(cmdline.
isset(
"LP64"))
1069 if(cmdline.
isset(
"ILP64"))
1072 if(cmdline.
isset(
"LLP64"))
1075 if(cmdline.
isset(
"ILP32"))
1078 if(cmdline.
isset(
"LP32"))
1081 if(cmdline.
isset(
"string-abstraction"))
1082 ansi_c.string_abstraction=
true;
1084 ansi_c.string_abstraction=
false;
1086 if(cmdline.
isset(
"no-library"))
1089 if(cmdline.
isset(
"little-endian"))
1092 if(cmdline.
isset(
"big-endian"))
1095 if(cmdline.
isset(
"little-endian") &&
1096 cmdline.
isset(
"big-endian"))
1099 if(cmdline.
isset(
"unsigned-char"))
1100 ansi_c.char_is_unsigned=
true;
1102 if(cmdline.
isset(
"round-to-even") ||
1103 cmdline.
isset(
"round-to-nearest"))
1106 if(cmdline.
isset(
"round-to-plus-inf"))
1109 if(cmdline.
isset(
"round-to-minus-inf"))
1112 if(cmdline.
isset(
"round-to-zero"))
1115 if(cmdline.
isset(
"object-bits"))
1121 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1124 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1126 if(cmdline.
isset(
"malloc-fail-null"))
1127 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_return_null;
1128 if(cmdline.
isset(
"malloc-fail-assert"))
1129 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_assert_then_assume;
1131 ansi_c.malloc_may_fail = cmdline.
isset(
"malloc-may-fail");
1133 if(cmdline.
isset(
"c89"))
1136 if(cmdline.
isset(
"c99"))
1139 if(cmdline.
isset(
"c11"))
1142 if(cmdline.
isset(
"cpp98"))
1145 if(cmdline.
isset(
"cpp03"))
1148 if(cmdline.
isset(
"cpp11"))
1184 case ost::OS_LINUX:
return "linux";
1185 case ost::OS_MACOS:
return "macos";
1186 case ost::OS_WIN:
return "win";
1187 case ost::NO_OS:
return "none";
1197 return ost::OS_LINUX;
1198 else if(os==
"macos")
1199 return ost::OS_MACOS;
1208 const std::string &what)
1223 "symbol table configuration entry '" +
id2string(
id) +
1224 "' must be a string constant");
1231 const std::string &what)
1244 "symbol table configuration entry '" +
id2string(
id) +
1245 "' must be a constant");
1252 "symbol table configuration entry '" +
id2string(
id) +
1253 "' must be convertible to mp_integer");
1338 "object_bits should fit into pointer width");
1344 return "Running with "+std::to_string(
bv_encoding.object_bits)+
1348 (
bv_encoding.is_object_bits_default ?
"default" :
"user-specified")+
1361 #elif defined(__armel__)
1363 #elif defined(__aarch64__)
1365 #elif defined(__arm__)
1366 #ifdef __ARM_PCS_VFP
1371 #elif defined(_MIPSEL)
1372 #if _MIPS_SIM==_ABIO32
1374 #elif _MIPS_SIM==_ABIN32
1379 #elif defined(__mips__)
1380 #if _MIPS_SIM==_ABIO32
1382 #elif _MIPS_SIM==_ABIN32
1387 #elif defined(__powerpc__)
1388 #if defined(__ppc64__) || defined(__PPC64__) || \
1389 defined(__powerpc64__) || defined(__POWERPC64__)
1390 #ifdef __LITTLE_ENDIAN__
1398 #elif defined(__riscv)
1400 #elif defined(__sparc__)
1406 #elif defined(__ia64__)
1408 #elif defined(__s390x__)
1410 #elif defined(__s390__)
1412 #elif defined(__x86_64__)
1418 #elif defined(__i386__)
1420 #elif defined(_WIN64)
1422 #elif defined(_WIN32)
1424 #elif defined(__hppa__)
1426 #elif defined(__sh__)
1449 java.classpath.insert(
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
Globally accessible architectural configuration.
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
void set_arch(const irep_idt &)
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
optionalt< std::string > main
std::string object_bits_info()
void set_classpath(const std::string &cp)
void set_from_symbol_table(const symbol_table_baset &)
static irep_idt this_architecture()
struct configt::javat java
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
exprt value
Initial value of symbol.
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.
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
const std::string & id2string(const irep_idt &d)
mp_integer alignment(const typet &type, const namespacet &ns)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool simplify(exprt &expr, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
void set_arch_spec_riscv64()
void set_ILP32()
int=32, long=32, pointer=32
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
void set_arch_spec_hppa()
static std::string os_to_string(ost)
void set_ILP64()
int=64, long=64, pointer=64
void set_arch_spec_sparc(const irep_idt &subarch)
static ost string_to_os(const std::string &)
void set_LLP64()
int=32, long=32, pointer=64
void set_arch_spec_arm(const irep_idt &subarch)
static c_standardt default_c_standard()
void set_arch_spec_alpha()
void set_arch_spec_power(const irep_idt &subarch)
void set_arch_spec_s390()
void set_LP64()
int=32, long=64, pointer=64
void set_arch_spec_x86_64()
void set_LP32()
int=16, long=32, pointer=32
void set_arch_spec_s390x()
void set_arch_spec_mips(const irep_idt &subarch)
void set_arch_spec_i386()
void set_arch_spec_ia64()
static cpp_standardt default_cpp_standard()