127 if(expr.
type()!=type)
582 code1.parameters().erase(
code1.parameters().begin());
588 code2.parameters().erase(
code2.parameters().begin());
952 if(parameters.size() != 2)
1071 comp_type.parameters().size() == 1,
"expected exactly one parameter");
1076 exprt this_expr(expr);
1175 unsigned &
rank)
const
1320 component_type.
parameters().size() == 1,
"exactly one parameter");
1326 exprt this_expr(expr);
1362 "the returned value must be pointer to reference");
1407 tmp.add_source_location()=
new_expr.source_location();
1430 tmp.add_source_location()=
new_expr.source_location();
1553 str <<
"\n " << type.
pretty() <<
'\n';
1616 error() <<
"bad reference initializer" <<
eom;
1637 std::vector<typet>
snt1;
1640 while(
snt1.back().has_subtype())
1653 std::vector<typet>
snt2;
1655 while(
snt2.back().has_subtype())
1670 for(std::size_t i=k; i > 1; i--)
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.
floatbv_typet float_type()
reference_typet reference_type(const typet &subtype)
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_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...
static void make_already_typechecked(exprt &expr)
const parameterst & parameters() const
const typet & return_type() const
struct configt::ansi_ct ansi_c
bool reference_compatible(const exprt &expr, const reference_typet &type, unsigned &rank) const
Reference-compatible.
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
void implicit_typecast(exprt &expr, const typet &type) override
bool reference_related(const exprt &expr, const reference_typet &type) const
Reference-related.
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void show_instantiation_stack(std::ostream &)
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
bool cast_away_constness(const typet &t1, const typet &t2) const
void add_implicit_dereference(exprt &)
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type)
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
std::string to_string(const typet &) override
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
void reference_initializer(exprt &expr, const reference_typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
bool reference_binding(exprt expr, const reference_typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
Operator to dereference a pointer.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
bool get_bool(const irep_idt &name) const
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 remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
source_locationt source_location
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
A side_effect_exprt representation of a function call side effect.
An expression containing a side effect.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#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'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
const type_with_subtypet & to_type_with_subtype(const typet &type)