131 const std::size_t width =
182 std::size_t result = 1;
186 INVARIANT(
power(2, result) >= size,
"address_bits(size) >= log2(size)");
203 if(base.is_long() && exponent.is_long())
205 switch(base.to_long())
227 if(exponent.is_odd())
281 "bvrep is hexadecimal, upper-case");
305make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f)
308 result.reserve((width + 3) / 4);
311 for(std::size_t
i = 0;
i < width;
i++)
328 const std::size_t
pos = result.find_last_not_of(
'0');
330 if(
pos == std::string::npos)
334 result.resize(
pos + 1);
336 std::reverse(result.begin(), result.end());
352 const std::size_t width,
353 const std::function<
bool(
bool,
bool)> f)
355 return make_bvrep(width, [&
a, &
b, &width, f](std::size_t
i) {
368 const std::size_t width,
369 const std::function<
bool(
bool)> f)
371 return make_bvrep(width, [&
a, &width, f](std::size_t
i) {
383 if(src.is_negative())
407 const auto p =
power(2, width - 1);
410 const auto result =
tmp - 2 * p;
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::size_t get_width() const
const typet & underlying_type() const
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & id() const
The null pointer constant.
The Boolean constant true.
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#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'.
API to expression classes.
bool is_signed(const typet &t)
Convenience function – is the type signed?