165 defines.push_back(
"__LITTLE_ENDIAN__");
196 defines.push_back(
"__x86_64__");
198 defines.push_back(
"__amd64__");
202 defines.push_back(
"__LITTLE_ENDIAN__");
222 if(subarch==
"powerpc")
227 if(subarch==
"ppc64le")
240 defines.push_back(
"__powerpc");
241 defines.push_back(
"__powerpc__");
242 defines.push_back(
"__POWERPC__");
246 defines.push_back(
"__BIG_ENDIAN__");
248 if(subarch!=
"powerpc")
250 defines.push_back(
"__powerpc64");
251 defines.push_back(
"__powerpc64__");
252 defines.push_back(
"__PPC64__");
253 defines.push_back(
"__ppc64__");
254 if(subarch==
"ppc64le")
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__");
303 defines.push_back(
"__aarch64__");
307 defines.push_back(
"__ARM_PCS_VFP");
311 if(subarch ==
"arm64")
338 defines.push_back(
"__alpha__");
358 if(subarch==
"mipsel" ||
360 subarch==
"mipsn32el" ||
372 if(subarch==
"mipsel" ||
373 subarch==
"mipsn32el" ||
388 "_MIPS_SZPTR="+std::to_string(
config.ansi_c.pointer_width));
471 defines.push_back(
"__s390x__");
491 if(subarch==
"sparc64")
509 defines.push_back(
"__sparc__");
510 if(subarch==
"sparc64")
511 defines.push_back(
"__arch64__");
573 defines.push_back(
"__ILP32__");
575 defines.push_back(
"__x86_64__");
576 defines.push_back(
"__amd64__");
689 defines.push_back(
"__loongarch__");
718 defines.push_back(
"__EMSCRIPTEN__");
738#if defined(__APPLE__)
741#elif defined(__FreeBSD__) || defined(__OpenBSD__)
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();
841 const std::string &argument,
842 const std::size_t pointer_width)
844 const auto throw_for_reason = [&](
const std::string &reason) {
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) +
") ",
853 throw_for_reason(
"not a valid unsigned integer");
854 if(*object_bits == 0 || *object_bits >= pointer_width)
855 throw_for_reason(
"out of range");
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"))
915 const char *CLASSPATH=getenv(
"CLASSPATH");
916 if(CLASSPATH!=
nullptr)
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;
1094 if(arch==this_arch && os==this_os)
1097 ansi_c.int_width ==
sizeof(
int) * CHAR_BIT,
1098 "int width shall be equal to the system int width");
1100 ansi_c.long_int_width ==
sizeof(
long) * CHAR_BIT,
1101 "long int width shall be equal to the system long int width");
1103 ansi_c.bool_width ==
sizeof(
bool) * CHAR_BIT,
1104 "bool width shall be equal to the system bool width");
1106 ansi_c.char_width ==
sizeof(
char) * CHAR_BIT,
1107 "char width shall be equal to the system char width");
1109 ansi_c.short_int_width ==
sizeof(
short) * CHAR_BIT,
1110 "short int width shall be equal to the system short int width");
1112 ansi_c.long_long_int_width ==
sizeof(
long long) * CHAR_BIT,
1113 "long long int width shall be equal to the system long long int width");
1115 ansi_c.pointer_width ==
sizeof(
void *) * CHAR_BIT,
1116 "pointer width shall be equal to the system pointer width");
1118 ansi_c.single_width ==
sizeof(
float) * CHAR_BIT,
1119 "float width shall be equal to the system float width");
1121 ansi_c.double_width ==
sizeof(
double) * CHAR_BIT,
1122 "double width shall be equal to the system double width");
1124 ansi_c.char_is_unsigned ==
1125 (
static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1126 "char_is_unsigned flag shall indicate system char unsignedness");
1131 ansi_c.long_double_width ==
sizeof(
long double) * CHAR_BIT,
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(
"c17"))
1244 if(cmdline.
isset(
"c23"))
1247 if(cmdline.
isset(
"cpp98"))
1250 if(cmdline.
isset(
"cpp03"))
1253 if(cmdline.
isset(
"cpp11"))
1271 const auto pointer_bits_2log =
1273 if(
ansi_c.pointer_width - pointer_bits_2log - 1 <=
ansi_c.int_width)
1276 power(2,
config.ansi_c.int_width - pointer_bits_2log - 1);
1303 else if(
os==
"macos")
1313 const std::string &what)
1318 const bool not_found = ns.
lookup(
id, symbol);
1324 tmp.
id() == ID_address_of &&
1328 "symbol table configuration entry '" +
id2string(
id) +
1329 "' must be a string constant");
1336 const std::string &what)
1341 const bool not_found = ns.
lookup(
id, symbol);
1349 "symbol table configuration entry '" +
id2string(
id) +
1350 "' must be a constant");
1357 "symbol table configuration entry '" +
id2string(
id) +
1358 "' must be convertible to mp_integer");
1433 const symbolt &entry_point_symbol=*maybe_symbol;
1435 if(entry_point_symbol.
mode==ID_java)
1437 else if(entry_point_symbol.
mode==ID_C)
1439 else if(entry_point_symbol.
mode==ID_cpp)
1443 "object_bits should fit into pointer width");
1449 return "Running with "+std::to_string(
bv_encoding.object_bits)+
1453 (
bv_encoding.is_object_bits_default ?
"default" :
"user-specified")+
1465 this_arch =
"alpha";
1466 #elif defined(__armel__)
1467 this_arch =
"armel";
1468 #elif defined(__aarch64__)
1469 this_arch =
"arm64";
1470 #elif defined(__arm__)
1471 #ifdef __ARM_PCS_VFP
1472 this_arch =
"armhf";
1476 #elif defined(_MIPSEL)
1477 #if _MIPS_SIM==_ABIO32
1478 this_arch =
"mipsel";
1479 #elif _MIPS_SIM==_ABIN32
1480 this_arch =
"mipsn32el";
1482 this_arch =
"mips64el";
1484 #elif defined(__mips__)
1485 #if _MIPS_SIM==_ABIO32
1487 #elif _MIPS_SIM==_ABIN32
1488 this_arch =
"mipsn32";
1490 this_arch =
"mips64";
1492 #elif defined(__powerpc__)
1493 #if defined(__ppc64__) || defined(__PPC64__) || \
1494 defined(__powerpc64__) || defined(__POWERPC64__)
1495 #ifdef __LITTLE_ENDIAN__
1496 this_arch =
"ppc64le";
1498 this_arch =
"ppc64";
1501 this_arch =
"powerpc";
1503 #elif defined(__riscv)
1504 this_arch =
"riscv64";
1505 #elif defined(__sparc__)
1507 this_arch =
"sparc64";
1509 this_arch =
"sparc";
1511 #elif defined(__ia64__)
1513 #elif defined(__s390x__)
1514 this_arch =
"s390x";
1515 #elif defined(__s390__)
1517 #elif defined(__x86_64__)
1521 this_arch =
"x86_64";
1523 #elif defined(__i386__)
1525 #elif defined(_WIN64)
1526 this_arch =
"x86_64";
1527 #elif defined(_WIN32)
1529 #elif defined(__hppa__)
1531 #elif defined(__sh__)
1533 #elif defined(__loongarch__)
1534 this_arch =
"loongarch64";
1535 #elif defined(__EMSCRIPTEN__)
1536 this_arch =
"emscripten";
1539 this_arch =
"unknown";
1551 const char cp_separator =
';';
1553 const char cp_separator =
':';
1556 std::vector<std::string> class_path =
1558 java.classpath.insert(
1559 java.classpath.end(), class_path.begin(), class_path.end());
1573 this_os =
"openbsd";
1583 this_os =
"emscripten";
1612 const auto bits_for_positive_offset = offset_bits - 1;
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
Base class for all expressions.
bool is_constant() const
Return whether the expression is a constant.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
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.
irep_idt mode
Language mode.
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)
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.
std::optional< T > string2optional(const std::string &str, int base=10)
convert a string to an integer, given the base of the representation works with signed and unsigned i...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::size_t long_double_width
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)
std::size_t pointer_width
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 &)
std::list< std::string > defines
void set_LLP64()
int=32, long=32, pointer=64
void set_arch_spec_arm(const irep_idt &subarch)
std::size_t wchar_t_width
@ 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
std::size_t memory_operand_size
std::size_t long_long_int_width
void set_arch_spec_s390x()
std::size_t long_int_width
void set_arch_spec_mips(const irep_idt &subarch)
void set_arch_spec_i386()
std::size_t short_int_width
void set_arch_spec_ia64()
void set_arch_spec_emscripten()
bool is_object_bits_default
static cpp_standardt default_cpp_standard()