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:
312 defines.push_back(
"_M_ARM64");
314 defines.push_back(
"_M_ARM");
317 case flavourt::CODEWARRIOR:
330 endianness=endiannesst::IS_LITTLE_ENDIAN;
331 long_double_width=16*8;
332 char_is_unsigned=
false;
338 defines.push_back(
"__alpha__");
341 case flavourt::VISUAL_STUDIO:
342 defines.push_back(
"_M_ALPHA");
345 case flavourt::CLANG:
346 case flavourt::CODEWARRIOR:
364 long_double_width=8*8;
369 long_double_width=16*8;
375 endianness=endiannesst::IS_LITTLE_ENDIAN;
377 endianness=endiannesst::IS_BIG_ENDIAN;
379 char_is_unsigned=
false;
385 defines.push_back(
"__mips__");
386 defines.push_back(
"mips");
388 "_MIPS_SZPTR="+std::to_string(
config.
ansi_c.pointer_width));
391 case flavourt::VISUAL_STUDIO:
395 case flavourt::CLANG:
396 case flavourt::CODEWARRIOR:
409 endianness = endiannesst::IS_LITTLE_ENDIAN;
410 long_double_width = 16 * 8;
411 char_is_unsigned =
true;
417 defines.push_back(
"__riscv");
420 case flavourt::VISUAL_STUDIO:
421 case flavourt::CLANG:
422 case flavourt::CODEWARRIOR:
435 endianness=endiannesst::IS_BIG_ENDIAN;
436 long_double_width=16*8;
437 char_is_unsigned=
true;
443 defines.push_back(
"__s390__");
446 case flavourt::VISUAL_STUDIO:
450 case flavourt::CLANG:
451 case flavourt::CODEWARRIOR:
464 endianness=endiannesst::IS_BIG_ENDIAN;
465 char_is_unsigned=
true;
471 defines.push_back(
"__s390x__");
474 case flavourt::VISUAL_STUDIO:
478 case flavourt::CLANG:
479 case flavourt::CODEWARRIOR:
494 long_double_width=16*8;
499 long_double_width=16*8;
502 endianness=endiannesst::IS_BIG_ENDIAN;
503 char_is_unsigned=
false;
509 defines.push_back(
"__sparc__");
511 defines.push_back(
"__arch64__");
514 case flavourt::VISUAL_STUDIO:
518 case flavourt::CLANG:
519 case flavourt::CODEWARRIOR:
532 long_double_width=16*8;
533 endianness=endiannesst::IS_LITTLE_ENDIAN;
534 char_is_unsigned=
false;
540 defines.push_back(
"__ia64__");
541 defines.push_back(
"_IA64");
542 defines.push_back(
"__IA64__");
545 case flavourt::VISUAL_STUDIO:
546 defines.push_back(
"_M_IA64");
549 case flavourt::CLANG:
550 case flavourt::CODEWARRIOR:
565 long_double_width=16*8;
566 endianness=endiannesst::IS_LITTLE_ENDIAN;
567 char_is_unsigned=
false;
573 defines.push_back(
"__ILP32__");
574 defines.push_back(
"__x86_64");
575 defines.push_back(
"__x86_64__");
576 defines.push_back(
"__amd64__");
577 defines.push_back(
"__amd64");
580 case flavourt::VISUAL_STUDIO:
584 case flavourt::CLANG:
585 case flavourt::CODEWARRIOR:
609 long_double_width=8*8;
610 endianness=endiannesst::IS_LITTLE_ENDIAN;
613 char_is_unsigned=
false;
622 long_double_width=8*8;
623 endianness=endiannesst::IS_BIG_ENDIAN;
624 char_is_unsigned=
false;
630 defines.push_back(
"__hppa__");
633 case flavourt::VISUAL_STUDIO:
637 case flavourt::CLANG:
638 case flavourt::CODEWARRIOR:
651 long_double_width=8*8;
652 endianness=endiannesst::IS_LITTLE_ENDIAN;
653 char_is_unsigned=
false;
659 defines.push_back(
"__sh__");
660 defines.push_back(
"__SH4__");
663 case flavourt::VISUAL_STUDIO:
667 case flavourt::CLANG:
668 case flavourt::CODEWARRIOR:
681 endianness = endiannesst::IS_LITTLE_ENDIAN;
682 long_double_width = 16 * 8;
683 char_is_unsigned =
false;
689 defines.push_back(
"__loongarch__");
692 case flavourt::VISUAL_STUDIO:
696 case flavourt::CODEWARRIOR:
697 case flavourt::CLANG:
710 endianness = endiannesst::IS_LITTLE_ENDIAN;
711 long_double_width = 16 * 8;
712 char_is_unsigned =
false;
717 case flavourt::CLANG:
718 defines.push_back(
"__EMSCRIPTEN__");
721 case flavourt::VISUAL_STUDIO:
726 case flavourt::CODEWARRIOR:
738#if defined(__APPLE__)
740 return c_standardt::C11;
741#elif defined(__FreeBSD__) || defined(__OpenBSD__)
744 return c_standardt::C99;
747 return c_standardt::C11;
757 return cpp_standardt::CPP14;
759 return cpp_standardt::CPP98;
772 ansi_c.NULL_is_zero=
false;
774 if(
sizeof(
long int)==8)
779 else if(arch==
"alpha")
780 ansi_c.set_arch_spec_alpha();
781 else if(arch==
"arm64" ||
785 ansi_c.set_arch_spec_arm(arch);
786 else if(arch==
"mips64el" ||
792 ansi_c.set_arch_spec_mips(arch);
793 else if(arch==
"powerpc" ||
796 ansi_c.set_arch_spec_power(arch);
797 else if(arch ==
"riscv64")
798 ansi_c.set_arch_spec_riscv64();
799 else if(arch==
"sparc" ||
801 ansi_c.set_arch_spec_sparc(arch);
802 else if(arch==
"ia64")
803 ansi_c.set_arch_spec_ia64();
804 else if(arch==
"s390x")
805 ansi_c.set_arch_spec_s390x();
806 else if(arch==
"s390")
807 ansi_c.set_arch_spec_s390();
809 ansi_c.set_arch_spec_x32();
810 else if(arch==
"v850")
811 ansi_c.set_arch_spec_v850();
812 else if(arch==
"hppa")
813 ansi_c.set_arch_spec_hppa();
815 ansi_c.set_arch_spec_sh4();
816 else if(arch==
"x86_64")
817 ansi_c.set_arch_spec_x86_64();
818 else if(arch==
"i386")
819 ansi_c.set_arch_spec_i386();
820 else if(arch ==
"loongarch64")
821 ansi_c.set_arch_spec_loongarch64();
822 else if(arch ==
"emscripten")
823 ansi_c.set_arch_spec_emscripten();
828 ansi_c.set_arch_spec_i386();
842 const std::size_t pointer_width)
846 "Value of \"" +
argument +
"\" given for object-bits is " + reason +
847 ". object-bits must be positive and less than the pointer width (" +
848 std::to_string(pointer_width) +
") ",
854 if(*object_bits == 0 || *object_bits >= pointer_width)
869 ansi_c.single_precision_constant=
false;
870 ansi_c.for_has_scope=
true;
871 ansi_c.ts_18661_3_Floatn_types=
false;
872 ansi_c.__float128_is_keyword =
false;
873 ansi_c.float16_type =
false;
882 ansi_c.NULL_is_zero=
reinterpret_cast<size_t>(
nullptr)==0;
891 if(cmdline.
isset(
"function"))
894 if(cmdline.
isset(
'D'))
897 if(cmdline.
isset(
'I'))
900 if(cmdline.
isset(
"classpath"))
906 else if(cmdline.
isset(
"cp"))
922 if(cmdline.
isset(
"main-class"))
925 if(cmdline.
isset(
"include"))
937 if(cmdline.
isset(
"i386-linux"))
942 else if(cmdline.
isset(
"i386-win32") ||
943 cmdline.
isset(
"win32"))
948 else if(cmdline.
isset(
"winx64"))
953 else if(cmdline.
isset(
"i386-macos"))
958 else if(cmdline.
isset(
"ppc-macos"))
964 if(cmdline.
isset(
"arch"))
969 if(cmdline.
isset(
"os"))
981 if(cmdline.
isset(
"gcc"))
990 ansi_c.defines.push_back(
"__CYGWIN__");
994 ansi_c.defines.push_back(
"__int64=long long");
1006#elif defined(__FreeBSD__) || defined(__OpenBSD__)
1017 else if(os==
"macos")
1026 ansi_c.__float128_is_keyword =
true;
1027 ansi_c.float16_type =
true;
1031 else if(os ==
"linux" || os ==
"solaris" || os ==
"netbsd" || os ==
"hurd")
1038 else if(os ==
"freebsd" || os ==
"openbsd")
1047 ansi_c.__float128_is_keyword =
true;
1048 ansi_c.float16_type =
true;
1062 ansi_c.gcc__float128_type =
true;
1074 ansi_c.wchar_t_width=2*8;
1075 ansi_c.wchar_t_is_unsigned=
true;
1079 if(arch ==
"x86_64" && cmdline.
isset(
"gcc"))
1080 ansi_c.long_double_width=16*8;
1082 ansi_c.long_double_width=8*8;
1084 else if(os ==
"macos" && arch ==
"arm64")
1088 ansi_c.char_is_unsigned =
false;
1089 ansi_c.long_double_width = 8 * 8;
1098 "int width shall be equal to the system int width");
1101 "long int width shall be equal to the system long int width");
1104 "bool width shall be equal to the system bool width");
1107 "char width shall be equal to the system char width");
1110 "short int width shall be equal to the system short int width");
1113 "long long int width shall be equal to the system long long int width");
1116 "pointer width shall be equal to the system pointer width");
1119 "float width shall be equal to the system float width");
1122 "double width shall be equal to the system double width");
1124 ansi_c.char_is_unsigned ==
1126 "char_is_unsigned flag shall indicate system char unsignedness");
1132 "long double width shall be equal to the system long double width");
1138 if(cmdline.
isset(
"16"))
1141 if(cmdline.
isset(
"32"))
1144 if(cmdline.
isset(
"64"))
1147 if(cmdline.
isset(
"LP64"))
1150 if(cmdline.
isset(
"ILP64"))
1153 if(cmdline.
isset(
"LLP64"))
1156 if(cmdline.
isset(
"ILP32"))
1159 if(cmdline.
isset(
"LP32"))
1162 if(cmdline.
isset(
"string-abstraction"))
1163 ansi_c.string_abstraction=
true;
1165 ansi_c.string_abstraction=
false;
1167 if(cmdline.
isset(
"dfcc-debug-lib"))
1168 ansi_c.dfcc_debug_lib =
true;
1170 ansi_c.dfcc_debug_lib =
false;
1172 if(cmdline.
isset(
"dfcc-simple-invalid-pointer-model"))
1173 ansi_c.simple_invalid_pointer_model =
true;
1175 ansi_c.simple_invalid_pointer_model =
false;
1177 if(cmdline.
isset(
"no-library"))
1180 if(cmdline.
isset(
"little-endian"))
1183 if(cmdline.
isset(
"big-endian"))
1186 if(cmdline.
isset(
"little-endian") &&
1187 cmdline.
isset(
"big-endian"))
1190 if(cmdline.
isset(
"unsigned-char"))
1191 ansi_c.char_is_unsigned=
true;
1193 if(cmdline.
isset(
"round-to-even") ||
1194 cmdline.
isset(
"round-to-nearest"))
1197 if(cmdline.
isset(
"round-to-plus-inf"))
1200 if(cmdline.
isset(
"round-to-minus-inf"))
1203 if(cmdline.
isset(
"round-to-zero"))
1206 if(cmdline.
isset(
"object-bits"))
1212 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1215 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1217 if(cmdline.
isset(
"malloc-fail-null"))
1218 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_return_null;
1219 if(cmdline.
isset(
"malloc-fail-assert"))
1220 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_assert_then_assume;
1222 if(cmdline.
isset(
"malloc-may-fail"))
1224 ansi_c.malloc_may_fail =
true;
1226 if(cmdline.
isset(
"no-malloc-may-fail"))
1228 ansi_c.malloc_may_fail =
false;
1232 if(cmdline.
isset(
"c89"))
1235 if(cmdline.
isset(
"c99"))
1238 if(cmdline.
isset(
"c11"))
1241 if(cmdline.
isset(
"cpp98"))
1244 if(cmdline.
isset(
"cpp03"))
1247 if(cmdline.
isset(
"cpp11"))
1283 case ost::OS_LINUX:
return "linux";
1284 case ost::OS_MACOS:
return "macos";
1285 case ost::OS_WIN:
return "win";
1286 case ost::NO_OS:
return "none";
1296 return ost::OS_LINUX;
1297 else if(os==
"macos")
1298 return ost::OS_MACOS;
1307 const std::string &what)
1322 "symbol table configuration entry '" +
id2string(
id) +
1323 "' must be a string constant");
1330 const std::string &what)
1343 "symbol table configuration entry '" +
id2string(
id) +
1344 "' must be a constant");
1351 "symbol table configuration entry '" +
id2string(
id) +
1352 "' must be convertible to mp_integer");
1437 "object_bits should fit into pointer width");
1443 return "Running with "+std::to_string(
bv_encoding.object_bits)+
1447 (
bv_encoding.is_object_bits_default ?
"default" :
"user-specified")+
1460 #elif defined(__armel__)
1462 #elif defined(__aarch64__)
1464 #elif defined(__arm__)
1465 #ifdef __ARM_PCS_VFP
1470 #elif defined(_MIPSEL)
1471 #if _MIPS_SIM==_ABIO32
1473 #elif _MIPS_SIM==_ABIN32
1478 #elif defined(__mips__)
1479 #if _MIPS_SIM==_ABIO32
1481 #elif _MIPS_SIM==_ABIN32
1486 #elif defined(__powerpc__)
1487 #if defined(__ppc64__) || defined(__PPC64__) || \
1488 defined(__powerpc64__) || defined(__POWERPC64__)
1489 #ifdef __LITTLE_ENDIAN__
1497 #elif defined(__riscv)
1499 #elif defined(__sparc__)
1505 #elif defined(__ia64__)
1507 #elif defined(__s390x__)
1509 #elif defined(__s390__)
1511 #elif defined(__x86_64__)
1517 #elif defined(__i386__)
1519 #elif defined(_WIN64)
1521 #elif defined(_WIN32)
1523 #elif defined(__hppa__)
1525 #elif defined(__sh__)
1527 #elif defined(__loongarch__)
1529 #elif defined(__EMSCRIPTEN__)
1552 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)
std::string object_bits_info()
void set_classpath(const std::string &cp)
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
void set_from_symbol_table(const symbol_table_baset &)
static irep_idt this_architecture()
std::optional< std::string > main
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 PRECONDITION(CONDITION)
#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.
char * getenv(const char *name)
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_arch_spec_loongarch64()
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)
@ malloc_failure_mode_none
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()
void set_arch_spec_emscripten()
static cpp_standardt default_cpp_standard()