32 if(type_id==ID_pointer)
40 else if(type_id==ID_integer ||
46 else if(type_id==ID_unsignedbv)
52 else if(type_id==ID_signedbv)
58 else if(type_id==ID_c_bool)
64 else if(type_id==ID_c_enum)
67 if(subtype.
id()==ID_signedbv)
73 else if(subtype.
id()==ID_unsignedbv)
80 else if(type_id==ID_c_bit_field)
83 const auto width = c_bit_field_type.get_width();
86 if(subtype.
id()==ID_signedbv)
91 else if(subtype.
id()==ID_unsignedbv)
96 else if(subtype.
id() == ID_c_bool)
118 uint_value = numeric_cast_v<unsigned>(i);
129 if(type_id==ID_integer)
133 else if(type_id==ID_natural)
138 else if(type_id==ID_unsignedbv)
143 else if(type_id==ID_bv)
148 else if(type_id==ID_signedbv)
153 else if(type_id==ID_c_enum)
155 const std::size_t width =
159 else if(type_id==ID_c_bool)
164 else if(type_id==ID_bool)
172 else if(type_id==ID_pointer)
177 else if(type_id==ID_c_bit_field)
182 else if(type_id==ID_fixedbv)
189 else if(type_id==ID_floatbv)
206 std::size_t result = 1;
208 for(
mp_integer x = 2; x < size; ++result, x *= 2) {}
210 INVARIANT(
power(2, result) >= size,
"address_bits(size) >= log2(size)");
227 if(base.is_long() && exponent.is_long())
229 switch(base.to_long())
234 result.setPower2(exponent.to_ulong());
251 if(exponent.is_odd())
288 std::size_t bit_index)
296 const auto nibble_index = bit_index / 4;
298 if(nibble_index >= src.
size())
301 const char nibble = src[src.
size() - 1 - nibble_index];
304 isdigit(nibble) || (nibble >=
'A' && nibble <=
'F'),
305 "bvrep is hexadecimal, upper-case");
307 const unsigned char nibble_value =
308 isdigit(nibble) ? nibble -
'0' : nibble -
'A' + 10;
310 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
319 return 'A' + nibble - 10;
329 make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f)
332 result.reserve((width + 3) / 4);
333 unsigned char nibble = 0;
335 for(std::size_t i = 0; i < width; i++)
337 const auto bit_in_nibble = i % 4;
339 nibble |= ((
unsigned char)f(i)) << bit_in_nibble;
341 if(bit_in_nibble == 3)
352 const std::size_t
pos = result.find_last_not_of(
'0');
354 if(
pos == std::string::npos)
358 result.resize(
pos + 1);
360 std::reverse(result.begin(), result.end());
376 const std::size_t width,
377 const std::function<
bool(
bool,
bool)> f)
379 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
392 const std::size_t width,
393 const std::function<
bool(
bool)> f)
395 return make_bvrep(width, [&a, &width, f](std::size_t i) {
407 if(src.is_negative())
431 const auto p =
power(2, width - 1);
434 const auto result = tmp - 2 * p;
The type of an expression, extends irept.
bool is_signed(const typet &t)
Convenience function – is the type signed?
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 signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
constant_exprt to_expr() const
const irep_idt & get_value() const
The null pointer constant.
typet & type()
Return the type of the expression.
A constant literal expression.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const irep_idt & id() const
The Boolean constant true.
void from_integer(const mp_integer &i)
API to expression classes.
#define PRECONDITION(CONDITION)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
constant_exprt to_expr() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
The Boolean constant false.
bool is_constant() const
Return whether the expression is a constant.
std::size_t get_width() const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Base class for all expressions.
void from_integer(const mp_integer &i)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
std::size_t get_size_t(const irep_namet &name) const