310 const typet &type)
const
394 typet underlying_type;
403 underlying_type =
followed.underlying_type();
473 const typet &type)
const
621 warnings.push_back(
"incompatible pointer types");
629 warnings.push_back(
"disregarding volatile");
644 errors.push_back(
"implicit conversion not permitted");
735 errors.push_back(
"implicit arithmetic conversion not permitted");
787 if(op1.has_value() && op2.has_value())
809std::optional<std::string>
813 return std::string(
"cannot take address of a bit field");
816 return std::string(
"cannot take address of a proper Boolean");
825 "bitvector must have width that is a multiple of CHAR_BIT");
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.
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
bool has_a_void_pointer(const typet &type)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
floatbv_typet float_type()
signedbv_typet signed_long_int_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_long_long_int_type()
floatbv_typet long_double_type()
bitvector_typet c_index_type()
floatbv_typet double_type()
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_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class of fixed-width bit-vector types.
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
virtual void implicit_typecast(exprt &expr, const typet &type)
c_typet get_c_type(const typet &type) const
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< std::string > warnings
static std::optional< std::string > check_address_can_be_taken(const typet &)
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
static ieee_float_spect quadruple_precision()
Unbounded, signed integers (mathematical integers, not bitvectors)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Natural numbers including zero (mathematical integers, not bitvectors)
The null pointer constant.
const typet & base_type() const
The type of the data what we point to.
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Union constructor from single element.
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Deprecated expression utility functions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const type_with_subtypet & to_type_with_subtype(const typet &type)