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;
813 ansi_c.NULL_is_zero=
reinterpret_cast<size_t>(
nullptr)==0;
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"))
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"))
921 ansi_c.defines.push_back(
"__CYGWIN__");
925 ansi_c.defines.push_back(
"__int64=long long");
955 else if(os==
"linux" || os==
"solaris")
962 else if(os==
"freebsd")
979 ansi_c.gcc__float128_type =
true;
992 ansi_c.wchar_t_is_unsigned=
true;
996 if(arch ==
"x86_64" && cmdline.
isset(
"gcc"))
997 ansi_c.long_double_width=16*8;
999 ansi_c.long_double_width=8*8;
1001 else if(os ==
"macos" && arch ==
"arm64")
1005 ansi_c.char_is_unsigned =
false;
1006 ansi_c.long_double_width = 8 * 8;
1015 "int width shall be equal to the system int width");
1018 "long int width shall be equal to the system long int width");
1021 "bool width shall be equal to the system bool width");
1024 "char width shall be equal to the system char width");
1027 "short int width shall be equal to the system short int width");
1030 "long long int width shall be equal to the system long long int width");
1033 "pointer width shall be equal to the system pointer width");
1036 "float width shall be equal to the system float width");
1039 "double width shall be equal to the system double width");
1041 ansi_c.char_is_unsigned ==
1043 "char_is_unsigned flag shall indicate system char unsignedness");
1049 "long double width shall be equal to the system long double width");
1055 if(cmdline.
isset(
"16"))
1058 if(cmdline.
isset(
"32"))
1061 if(cmdline.
isset(
"64"))
1064 if(cmdline.
isset(
"LP64"))
1067 if(cmdline.
isset(
"ILP64"))
1070 if(cmdline.
isset(
"LLP64"))
1073 if(cmdline.
isset(
"ILP32"))
1076 if(cmdline.
isset(
"LP32"))
1079 if(cmdline.
isset(
"string-abstraction"))
1080 ansi_c.string_abstraction=
true;
1082 ansi_c.string_abstraction=
false;
1084 if(cmdline.
isset(
"no-library"))
1087 if(cmdline.
isset(
"little-endian"))
1090 if(cmdline.
isset(
"big-endian"))
1093 if(cmdline.
isset(
"little-endian") &&
1094 cmdline.
isset(
"big-endian"))
1097 if(cmdline.
isset(
"unsigned-char"))
1098 ansi_c.char_is_unsigned=
true;
1100 if(cmdline.
isset(
"round-to-even") ||
1101 cmdline.
isset(
"round-to-nearest"))
1104 if(cmdline.
isset(
"round-to-plus-inf"))
1107 if(cmdline.
isset(
"round-to-minus-inf"))
1110 if(cmdline.
isset(
"round-to-zero"))
1113 if(cmdline.
isset(
"object-bits"))
1119 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1122 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1124 if(cmdline.
isset(
"malloc-fail-null"))
1125 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_return_null;
1126 if(cmdline.
isset(
"malloc-fail-assert"))
1127 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_assert_then_assume;
1129 ansi_c.malloc_may_fail = cmdline.
isset(
"malloc-may-fail");
1131 if(cmdline.
isset(
"c89"))
1134 if(cmdline.
isset(
"c99"))
1137 if(cmdline.
isset(
"c11"))
1140 if(cmdline.
isset(
"cpp98"))
1143 if(cmdline.
isset(
"cpp03"))
1146 if(cmdline.
isset(
"cpp11"))
1182 case ost::OS_LINUX:
return "linux";
1183 case ost::OS_MACOS:
return "macos";
1184 case ost::OS_WIN:
return "win";
1185 case ost::NO_OS:
return "none";
1195 return ost::OS_LINUX;
1196 else if(os==
"macos")
1197 return ost::OS_MACOS;
1206 const std::string &what)
1221 "symbol table configuration entry '" +
id2string(
id) +
1222 "' must be a string constant");
1229 const std::string &what)
1242 "symbol table configuration entry '" +
id2string(
id) +
1243 "' must be a constant");
1250 "symbol table configuration entry '" +
id2string(
id) +
1251 "' must be convertible to mp_integer");
1336 "object_bits should fit into pointer width");
1342 return "Running with "+std::to_string(
bv_encoding.object_bits)+
1346 (
bv_encoding.is_object_bits_default ?
"default" :
"user-specified")+
1359 #elif defined(__armel__)
1361 #elif defined(__aarch64__)
1363 #elif defined(__arm__)
1364 #ifdef __ARM_PCS_VFP
1369 #elif defined(_MIPSEL)
1370 #if _MIPS_SIM==_ABIO32
1372 #elif _MIPS_SIM==_ABIN32
1377 #elif defined(__mips__)
1378 #if _MIPS_SIM==_ABIO32
1380 #elif _MIPS_SIM==_ABIN32
1385 #elif defined(__powerpc__)
1386 #if defined(__ppc64__) || defined(__PPC64__) || \
1387 defined(__powerpc64__) || defined(__POWERPC64__)
1388 #ifdef __LITTLE_ENDIAN__
1396 #elif defined(__riscv)
1398 #elif defined(__sparc__)
1404 #elif defined(__ia64__)
1406 #elif defined(__s390x__)
1408 #elif defined(__s390__)
1410 #elif defined(__x86_64__)
1416 #elif defined(__i386__)
1418 #elif defined(_WIN64)
1420 #elif defined(_WIN32)
1422 #elif defined(__hppa__)
1424 #elif defined(__sh__)
1447 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()