109 const exprt &as_expr=
110 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
209 const exprt &as_expr=
210 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
258 const exprt &as_expr =
259 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
264 const exprt &as_expr =
265 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
272 const exprt &as_expr =
273 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
277 other.push_back(type);
299 error() <<
"illegal type modifier for defined type" <<
eom;
315 error() <<
"illegal combination of defined types" <<
eom;
322 if(!
requires.empty())
336 error() <<
"combining constructor and destructor not supported"
348 error() <<
"constructor and destructor required to be type void, "
359 error() <<
"constructor and destructor required to be type void, "
374 error() <<
"cannot combine integer type with floating-point type" <<
eom;
385 error() <<
"conflicting type modifiers" <<
eom;
415 error() <<
"cannot combine integer type with floating-point type" <<
eom;
422 error() <<
"conflicting type modifiers" <<
eom;
440 error() <<
"conflicting type modifiers" <<
eom;
447 error() <<
"illegal type modifier for float" <<
eom;
459 error() <<
"illegal type modifier for C boolean type" <<
eom;
473 error() <<
"illegal type modifier for proper boolean type" <<
eom;
492 error() <<
"illegal type modifier for char type" <<
eom;
499 error() <<
"conflicting type modifiers" <<
eom;
518 error() <<
"conflicting type modifiers" <<
eom;
531 error() <<
"conflicting type modifiers" <<
eom;
588 error() <<
"conflicting type modifiers" <<
eom;
621 error() <<
"illegal type modifier for integer type" <<
eom;
ANSI-C Language Conversion.
floatbv_typet float_type()
signedbv_typet signed_long_int_type()
signedbv_typet signed_char_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_int_type()
unsignedbv_typet unsigned_char_type()
bitvector_typet char_type()
signedbv_typet signed_long_long_int_type()
floatbv_typet long_double_type()
floatbv_typet double_type()
signedbv_typet signed_short_int_type()
unsignedbv_typet unsigned_short_int_type()
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual void read_rec(const typet &type)
exprt::operandst c_storage_spect c_storage_spec
virtual void read(const typet &type)
virtual void write(typet &type)
unsigned gcc_float128x_cnt
unsigned gcc_float32x_cnt
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
unsigned gcc_float64x_cnt
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
c_qualifierst c_qualifiers
unsigned gcc_float128_cnt
virtual void write(typet &src) const override
bool is_transparent_union
const typet & return_type() const
const exprt::operandst & assigns() const
exprt::operandst &const exprt::operandst & ensures() const
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
source_locationt source_location
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const irep_idt & get_value() const
Type with a single subtype.
The type of an expression, extends irept.
const source_locationt & source_location() const
#define forall_operands(it, expr)
floatbv_typet gcc_float32_type()
floatbv_typet gcc_float16_type()
floatbv_typet gcc_float64_type()
signedbv_typet gcc_signed_int128_type()
floatbv_typet gcc_float32x_type()
floatbv_typet gcc_float64x_type()
floatbv_typet gcc_float128x_type()
unsignedbv_typet gcc_unsigned_int128_type()
floatbv_typet gcc_float128_type()
#define UNREACHABLE
This should be used to mark dead code.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)
bool is_signed(const typet &t)
Convenience function – is the type signed?