26 if(type_id==ID_pointer)
34 else if(type_id == ID_integer || type_id == ID_natural || type_id == ID_range)
39 else if(type_id==ID_unsignedbv)
45 else if(type_id==ID_signedbv)
51 else if(type_id==ID_c_bool)
57 else if(type_id==ID_c_enum)
60 if(underlying_type.
id() == ID_signedbv)
66 else if(underlying_type.
id() == ID_unsignedbv)
73 else if(type_id==ID_c_bit_field)
76 const auto width = c_bit_field_type.get_width();
77 const typet &underlying_type = c_bit_field_type.underlying_type();
79 if(underlying_type.
id() == ID_signedbv)
84 else if(underlying_type.
id() == ID_unsignedbv)
89 else if(underlying_type.
id() == ID_c_bool)
105 if(type_id==ID_integer)
109 else if(type_id==ID_natural)
114 else if(type_id == ID_range)
121 else if(type_id==ID_unsignedbv)
126 else if(type_id==ID_bv)
131 else if(type_id==ID_signedbv)
136 else if(type_id==ID_c_enum)
138 const std::size_t width =
142 else if(type_id==ID_c_bool)
147 else if(type_id==ID_bool)
155 else if(type_id==ID_pointer)
160 else if(type_id==ID_c_bit_field)
165 else if(type_id==ID_fixedbv)
172 else if(type_id==ID_floatbv)
191 std::size_t result = 1;
193 for(
mp_integer x = 2; x < size; ++result, x *= 2) {}
195 INVARIANT(
power(2, result) >= size,
"address_bits(size) >= log2(size)");
212 if(base.is_long() && exponent.is_long())
214 switch(base.to_long())
236 if(exponent.is_odd())
273 std::size_t bit_index)
281 const auto nibble_index = bit_index / 4;
283 if(nibble_index >= src.
size())
286 const char nibble = src[src.
size() - 1 - nibble_index];
289 isdigit(nibble) || (nibble >=
'A' && nibble <=
'F'),
290 "bvrep is hexadecimal, upper-case");
292 const unsigned char nibble_value =
293 isdigit(nibble) ? nibble -
'0' : nibble -
'A' + 10;
295 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
304 return 'A' + nibble - 10;
314make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f)
317 result.reserve((width + 3) / 4);
318 unsigned char nibble = 0;
320 for(std::size_t i = 0; i < width; i++)
322 const auto bit_in_nibble = i % 4;
324 nibble |= ((
unsigned char)f(i)) << bit_in_nibble;
326 if(bit_in_nibble == 3)
337 const std::size_t
pos = result.find_last_not_of(
'0');
339 if(
pos == std::string::npos)
343 result.resize(
pos + 1);
345 std::reverse(result.begin(), result.end());
361 const std::size_t width,
362 const std::function<
bool(
bool,
bool)> f)
364 return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
377 const std::size_t width,
378 const std::function<
bool(
bool)> f)
380 return make_bvrep(width, [&a, &width, f](std::size_t i) {
392 if(src.is_negative())
416 const auto p =
power(2, width - 1);
419 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.
std::size_t get_width() const
const typet & underlying_type() const
A constant literal expression.
const irep_idt & get_value() const
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
typet & type()
Return the type of the expression.
The Boolean constant false.
void from_integer(const mp_integer &i)
constant_exprt to_expr() const
constant_exprt to_expr() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
void from_integer(const mp_integer &i)
const irep_idt & id() const
The null pointer constant.
The Boolean constant true.
The type of an expression, extends irept.
Deprecated expression utility functions.
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.
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
bool is_signed(const typet &t)
Convenience function – is the type signed?