Go to the documentation of this file.
25 if(type_id==ID_pointer)
33 else if(type_id==ID_integer ||
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(subtype.
id()==ID_signedbv)
66 else if(subtype.
id()==ID_unsignedbv)
73 else if(type_id==ID_c_bit_field)
76 const auto width = c_bit_field_type.get_width();
79 if(subtype.
id()==ID_signedbv)
84 else if(subtype.
id()==ID_unsignedbv)
89 else if(subtype.
id() == ID_c_bool)
105 if(type_id==ID_integer)
109 else if(type_id==ID_natural)
114 else if(type_id==ID_unsignedbv)
119 else if(type_id==ID_bv)
124 else if(type_id==ID_signedbv)
129 else if(type_id==ID_c_enum)
131 const std::size_t width =
135 else if(type_id==ID_c_bool)
140 else if(type_id==ID_bool)
148 else if(type_id==ID_pointer)
153 else if(type_id==ID_c_bit_field)
158 else if(type_id==ID_fixedbv)
165 else if(type_id==ID_floatbv)
182 std::size_t result = 1;
184 for(
mp_integer x = 2; x < size; ++result, x *= 2) {}
186 INVARIANT(
power(2, result) >= size,
"address_bits(size) >= log2(size)");
203 if(base.is_long() && exponent.is_long())
205 switch(base.to_long())
210 result.setPower2(numeric_cast_v<unsigned>(exponent));
227 if(exponent.is_odd())
264 std::size_t bit_index)
272 const auto nibble_index = bit_index / 4;
274 if(nibble_index >= src.
size())
277 const char nibble = src[src.
size() - 1 - nibble_index];
280 isdigit(nibble) || (nibble >=
'A' && nibble <=
'F'),
281 "bvrep is hexadecimal, upper-case");
283 const unsigned char nibble_value =
284 isdigit(nibble) ? nibble -
'0' : nibble -
'A' + 10;
286 return ((nibble_value >> (bit_index % 4)) & 1) != 0;
295 return 'A' + nibble - 10;
305 make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f)
308 result.reserve((width + 3) / 4);
309 unsigned char nibble = 0;
311 for(std::size_t i = 0; i < width; i++)
313 const auto bit_in_nibble = i % 4;
315 nibble |= ((
unsigned char)f(i)) << bit_in_nibble;
317 if(bit_in_nibble == 3)
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 c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
void from_integer(const mp_integer &i)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
bool is_signed(const typet &t)
Convenience function – is the type signed?
const mp_integer string2integer(const std::string &n, unsigned base)
constant_exprt to_expr() const
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
typet & type()
Return the type of the expression.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
The null pointer constant.
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const irep_idt & id() const
The Boolean constant false.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void from_integer(const mp_integer &i)
std::size_t get_width() const
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
constant_exprt to_expr() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
The Boolean constant true.
A constant literal expression.
API to expression classes.
const irep_idt & get_value() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const std::string integer2string(const mp_integer &n, unsigned base)