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(
"no-library"))
1170 if(cmdline.
isset(
"little-endian"))
1173 if(cmdline.
isset(
"big-endian"))
1176 if(cmdline.
isset(
"little-endian") &&
1177 cmdline.
isset(
"big-endian"))
1180 if(cmdline.
isset(
"unsigned-char"))
1181 ansi_c.char_is_unsigned=
true;
1183 if(cmdline.
isset(
"round-to-even") ||
1184 cmdline.
isset(
"round-to-nearest"))
1187 if(cmdline.
isset(
"round-to-plus-inf"))
1190 if(cmdline.
isset(
"round-to-minus-inf"))
1193 if(cmdline.
isset(
"round-to-zero"))
1196 if(cmdline.
isset(
"object-bits"))
1202 if(cmdline.
isset(
"malloc-fail-assert") && cmdline.
isset(
"malloc-fail-null"))
1205 "at most one malloc failure mode is acceptable",
"--malloc-fail-null"};
1207 if(cmdline.
isset(
"malloc-fail-null"))
1208 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_return_null;
1209 if(cmdline.
isset(
"malloc-fail-assert"))
1210 ansi_c.malloc_failure_mode =
ansi_c.malloc_failure_mode_assert_then_assume;
1212 if(cmdline.
isset(
"malloc-may-fail"))
1214 ansi_c.malloc_may_fail =
true;
1216 if(cmdline.
isset(
"no-malloc-may-fail"))
1218 ansi_c.malloc_may_fail =
false;
1222 if(cmdline.
isset(
"c89"))
1225 if(cmdline.
isset(
"c99"))
1228 if(cmdline.
isset(
"c11"))
1231 if(cmdline.
isset(
"cpp98"))
1234 if(cmdline.
isset(
"cpp03"))
1237 if(cmdline.
isset(
"cpp11"))
1255 const auto pointer_bits_2log =
1257 if(
ansi_c.pointer_width - pointer_bits_2log - 1 <=
ansi_c.int_width)
1260 power(2,
config.ansi_c.int_width - pointer_bits_2log - 1);
1287 else if(
os==
"macos")
1297 const std::string &what)
1302 const bool not_found = ns.
lookup(
id, symbol);
1308 tmp.
id() == ID_address_of &&
1312 "symbol table configuration entry '" +
id2string(
id) +
1313 "' must be a string constant");
1320 const std::string &what)
1325 const bool not_found = ns.
lookup(
id, symbol);
1333 "symbol table configuration entry '" +
id2string(
id) +
1334 "' must be a constant");
1341 "symbol table configuration entry '" +
id2string(
id) +
1342 "' must be convertible to mp_integer");
1417 const symbolt &entry_point_symbol=*maybe_symbol;
1419 if(entry_point_symbol.
mode==ID_java)
1421 else if(entry_point_symbol.
mode==ID_C)
1423 else if(entry_point_symbol.
mode==ID_cpp)
1427 "object_bits should fit into pointer width");
1433 return "Running with "+std::to_string(
bv_encoding.object_bits)+
1437 (
bv_encoding.is_object_bits_default ?
"default" :
"user-specified")+
1449 this_arch =
"alpha";
1450 #elif defined(__armel__)
1451 this_arch =
"armel";
1452 #elif defined(__aarch64__)
1453 this_arch =
"arm64";
1454 #elif defined(__arm__)
1455 #ifdef __ARM_PCS_VFP
1456 this_arch =
"armhf";
1460 #elif defined(_MIPSEL)
1461 #if _MIPS_SIM==_ABIO32
1462 this_arch =
"mipsel";
1463 #elif _MIPS_SIM==_ABIN32
1464 this_arch =
"mipsn32el";
1466 this_arch =
"mips64el";
1468 #elif defined(__mips__)
1469 #if _MIPS_SIM==_ABIO32
1471 #elif _MIPS_SIM==_ABIN32
1472 this_arch =
"mipsn32";
1474 this_arch =
"mips64";
1476 #elif defined(__powerpc__)
1477 #if defined(__ppc64__) || defined(__PPC64__) || \
1478 defined(__powerpc64__) || defined(__POWERPC64__)
1479 #ifdef __LITTLE_ENDIAN__
1480 this_arch =
"ppc64le";
1482 this_arch =
"ppc64";
1485 this_arch =
"powerpc";
1487 #elif defined(__riscv)
1488 this_arch =
"riscv64";
1489 #elif defined(__sparc__)
1491 this_arch =
"sparc64";
1493 this_arch =
"sparc";
1495 #elif defined(__ia64__)
1497 #elif defined(__s390x__)
1498 this_arch =
"s390x";
1499 #elif defined(__s390__)
1501 #elif defined(__x86_64__)
1505 this_arch =
"x86_64";
1507 #elif defined(__i386__)
1509 #elif defined(_WIN64)
1510 this_arch =
"x86_64";
1511 #elif defined(_WIN32)
1513 #elif defined(__hppa__)
1515 #elif defined(__sh__)
1517 #elif defined(__loongarch__)
1518 this_arch =
"loongarch64";
1519 #elif defined(__EMSCRIPTEN__)
1520 this_arch =
"emscripten";
1523 this_arch =
"unknown";
1535 const char cp_separator =
';';
1537 const char cp_separator =
':';
1540 std::vector<std::string> class_path =
1542 java.classpath.insert(
1543 java.classpath.end(), class_path.begin(), class_path.end());
1557 this_os =
"openbsd";
1567 this_os =
"emscripten";
1596 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()