151 for(std::size_t
i=0;
i<
c_type1.parameters().size();
i++)
236 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
248 assert(subtypes.size()==2);
314 error() <<
"expected declaration as operand of quantifier" <<
eom;
322 error() <<
"quantifier must not contain side effects" <<
eom;
335 domain.push_back(binding.type());
367 error() <<
"real part retrieval expects numerical operand, "
400 error() <<
"real part retrieval expects numerical operand, "
474 error() <<
"unmatched generic selection: " <<
to_string(op.type())
581 error() <<
"builtin_offsetof expects no operands" <<
eom;
601 error() <<
"offsetof of member expects struct/union type, "
626 if(!
o_opt.has_value())
629 error() <<
"offsetof failed to determine offset of '"
630 << component_name <<
"'" <<
eom;
659 if(!
o_opt.has_value())
662 error() <<
"offsetof failed to determine offset of '"
663 << component_name <<
"'" <<
eom;
685 error() <<
"offset-of of member failed to find component '"
686 << component_name <<
"' in '" <<
to_string(type) <<
"'"
698 error() <<
"offsetof of index expects array type" <<
eom;
713 error() <<
"offsetof failed to determine array element size" <<
eom;
765 error() <<
"forall/exists expects one declarator exactly" <<
eom;
772 symbol_tablet::symbolst::const_iterator
s_it =
778 error() <<
"failed to find bound symbol `" << identifier
779 <<
"' in symbol table" <<
eom;
790 error() <<
"unexpected quantified symbol" <<
eom;
824 asm_label_mapt::const_iterator entry=
828 identifier=entry->second;
837 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
846 error() <<
"did not expect a type symbol here, but got '"
881 else if(identifier==
"__func__" ||
882 identifier==
"__FUNCTION__" ||
883 identifier==
"__PRETTY_FUNCTION__")
974 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
980 error() <<
"sizeof cannot be applied to single bits" <<
eom;
1001 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1112 if(
c.type() == op.
type())
1126 <<
"' not found in union" <<
eom;
1143 tmp.copy_to_operands(op);
1199 error() <<
"type cast from void only permitted to void, but got '"
1221 <<
"' not permitted" <<
eom;
1306 error() <<
"operator [] must take array/vector or pointer but got '"
1420 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1434 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1479 error() <<
"ptrmember operator requires pointer or array type "
1480 "on left hand side, but got '"
1500 error() <<
"member operator requires structure type "
1501 "on left hand side but got '"
1512 error() <<
"member operator got incomplete " << type.
id()
1513 <<
" type on left hand side" <<
eom;
1534 error() <<
"member '" << component_name <<
"' not found in '"
1555 if(!identifier.
empty())
1563 error() <<
"member '" << component_name <<
"' is " <<
access <<
eom;
1572 assert(operands.size()==3);
1592 else if(operands[2].type().
id()==
ID_pointer &&
1598 operands[1].type()!=operands[2].type())
1605 if(operands[1].type().subtype().
id()==
ID_empty &&
1606 tmp1.is_constant() &&
1609 else if(operands[2].type().subtype().
id()==
ID_empty &&
1610 tmp2.is_constant() &&
1613 else if(operands[1].type().subtype().
id()!=
ID_code ||
1614 operands[2].type().subtype().
id()!=
ID_code)
1638 if(operands[1].type().
id()==
ID_empty ||
1646 operands[1].type() != operands[2].type() ||
1647 operands[1].type().
id() ==
ID_array)
1652 if(operands[1].type() == operands[2].type())
1654 expr.
type()=operands[1].type();
1681 if(operands.size()!=2)
1684 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1696 operands[0] =
if_expr.true_case();
1697 operands[1] =
if_expr.false_case();
1708 error() <<
"cannot take address of a bit field" <<
eom;
1715 error() <<
"cannot take address of a single bit" <<
eom;
1762 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1833 <<
"' not an lvalue" <<
eom;
1850 error() <<
"operator '" << statement <<
"' given incomplete type '"
1865 expr.
type()=underlying_type;
1884 error() <<
"operator '" << statement <<
"' not defined for type '"
1901 error() <<
"unknown side effect: " << statement <<
eom;
1912 error() <<
"function_call side effect expects two operands" <<
eom;
1925 asm_label_mapt::const_iterator entry=
1928 identifier=entry->second;
1939 identifier ==
"__noop" &&
1953 identifier ==
"__builtin_shuffle" &&
1962 identifier ==
"__builtin_shufflevector" &&
1977 !parameters.empty(),
1978 "GCC polymorphic built-ins should have at least one parameter");
1983 if(parameters.front().type().id() ==
ID_pointer)
1987 parameters.front().type().subtype(), *
this);
1999 for(std::size_t
i = 0;
i < parameters.size(); ++
i)
2001 const std::string base_name =
"p_" + std::to_string(
i);
2009 new_symbol.
type = parameters[
i].type();
2014 parameters[
i].set_identifier(new_symbol.
name);
2015 parameters[
i].set_base_name(new_symbol.
base_name);
2050 if(identifier==
"malloc" ||
2051 identifier==
"realloc" ||
2052 identifier==
"reallocf" ||
2053 identifier==
"valloc")
2060 new_symbol.
name=identifier;
2072 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2092 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2100 if(p.first.type() != p.second)
2113 expr.
swap(function_application);
2120 error() <<
"expected function/function pointer as argument but got '"
2134 tmp.add_source_location()=
f_op.source_location();
2141 error() <<
"expected code as argument" <<
eom;
2151 if(
tmp.is_not_nil())
2186 error() <<
"same_object expects two operands" <<
eom;
2203 error() <<
"get_must expects two operands" <<
eom;
2220 error() <<
"get_may expects two operands" <<
eom;
2237 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2253 error() <<
"buffer_size expects one operand" <<
eom;
2270 error() <<
"is_zero_string expects one operand" <<
eom;
2288 error() <<
"zero_string_length expects one operand" <<
eom;
2306 error() <<
"dynamic_object expects one argument" <<
eom;
2322 error() <<
"pointer_offset expects one argument" <<
eom;
2338 error() <<
"object_size expects one operand" <<
eom;
2355 error() <<
"pointer_object expects one argument" <<
eom;
2366 else if(identifier==
"__builtin_bswap16" ||
2367 identifier==
"__builtin_bswap32" ||
2368 identifier==
"__builtin_bswap64")
2373 error() << identifier <<
" expects one operand" <<
eom;
2381 bswap_expr.add_source_location()=source_location;
2386 identifier ==
"__builtin_rotateleft8" ||
2387 identifier ==
"__builtin_rotateleft16" ||
2388 identifier ==
"__builtin_rotateleft32" ||
2389 identifier ==
"__builtin_rotateleft64" ||
2390 identifier ==
"__builtin_rotateright8" ||
2391 identifier ==
"__builtin_rotateright16" ||
2392 identifier ==
"__builtin_rotateright32" ||
2393 identifier ==
"__builtin_rotateright64")
2399 error() << identifier <<
" expects two operands" <<
eom;
2405 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2406 identifier ==
"__builtin_rotateleft16" ||
2407 identifier ==
"__builtin_rotateleft32" ||
2408 identifier ==
"__builtin_rotateleft64")
2413 rotate_expr.add_source_location() = source_location;
2417 else if(identifier==
"__builtin_nontemporal_load")
2422 error() << identifier <<
" expects one operand" <<
eom;
2434 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2443 identifier ==
"__builtin_fpclassify" ||
2449 error() << identifier <<
" expects six arguments" <<
eom;
2465 error() <<
"non-floating-point argument for " << identifier <<
eom;
2473 const auto &arguments = expr.
arguments();
2492 identifier==
"__builtin_isnan")
2497 error() <<
"isnan expects one operand" <<
eom;
2504 isnan_expr.add_source_location()=source_location;
2515 error() <<
"isfinite expects one operand" <<
eom;
2527 identifier==
"__builtin_inf")
2532 inf_expr.add_source_location()=source_location;
2541 inff_expr.add_source_location()=source_location;
2550 infl_expr.add_source_location()=source_location;
2564 error() <<
"abs-functions expect one operand" <<
eom;
2571 abs_expr.add_source_location()=source_location;
2583 error() <<
"fmod-functions expect two operands" <<
eom;
2595 fmod_expr.add_source_location() = source_location;
2607 error() <<
"remainder-functions expect two operands" <<
eom;
2628 error() <<
"allocate expects two operands" <<
eom;
2646 error() << identifier <<
" expects one or two operands" <<
eom;
2653 const auto &pointer_expr = expr.
arguments()[0];
2657 error() << identifier <<
" expects a pointer as first argument" <<
eom;
2677 error() << identifier <<
" expects a size when given a void pointer"
2686 error() << identifier <<
" was given object pointer without size"
2699 ok_expr.add_source_location() = source_location;
2710 error() << identifier <<
" expects one operand" <<
eom;
2717 old_expr.add_source_location() = source_location;
2724 identifier==
"__builtin_isinf")
2729 error() << identifier <<
" expects one operand" <<
eom;
2740 error() <<
"non-floating-point argument for " << identifier <<
eom;
2745 isinf_expr.add_source_location()=source_location;
2749 else if(identifier ==
"__builtin_isinf_sign")
2754 error() << identifier <<
" expects one operand" <<
eom;
2767 error() <<
"non-floating-point argument for " << identifier <<
eom;
2772 isinf_expr.add_source_location() = source_location;
2785 identifier ==
"__builtin_isnormal")
2790 error() << identifier <<
" expects one operand" <<
eom;
2801 error() <<
"non-floating-point argument for " << identifier <<
eom;
2813 identifier==
"__builtin_signbit" ||
2814 identifier==
"__builtin_signbitf" ||
2815 identifier==
"__builtin_signbitl")
2820 error() << identifier <<
" expects one operand" <<
eom;
2827 sign_expr.add_source_location()=source_location;
2831 else if(identifier==
"__builtin_popcount" ||
2832 identifier==
"__builtin_popcountl" ||
2833 identifier==
"__builtin_popcountll" ||
2834 identifier==
"__popcnt16" ||
2835 identifier==
"__popcnt" ||
2836 identifier==
"__popcnt64")
2841 error() << identifier <<
" expects one operand" <<
eom;
2853 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2854 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2855 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2860 error() << identifier <<
" expects one operand" <<
eom;
2869 clz.add_source_location() = source_location;
2871 return std::move(
clz);
2874 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
2875 identifier ==
"__builtin_ctzll")
2880 error() << identifier <<
" expects one operand" <<
eom;
2888 ctz.add_source_location() = source_location;
2890 return std::move(
ctz);
2897 error() <<
"equal expects two operands" <<
eom;
2910 error() <<
"equal expects two operands of same type" <<
eom;
2916 else if(identifier==
"__builtin_expect")
2927 error() <<
"__builtin_expect expects two arguments" <<
eom;
2935 else if(identifier==
"__builtin_object_size")
2944 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2961 error() <<
"__builtin_object_size expects constant as second argument, "
2972 tmp.add_source_location()=
f_op.source_location();
2977 tmp.add_source_location()=
f_op.source_location();
2982 else if(identifier==
"__builtin_choose_expr")
2988 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3003 else if(identifier==
"__builtin_constant_p")
3010 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3040 tmp2.add_source_location()=source_location;
3044 else if(identifier==
"__builtin_classify_type")
3051 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3098 tmp.add_source_location()=source_location;
3109 overflow.add_source_location() =
f_op.source_location();
3134 of.add_source_location() =
overflow.source_location();
3135 return std::move(
of);
3140 tmp.add_source_location() =
f_op.source_location();
3145 overflow.add_source_location() =
tmp.source_location();
3155 <<
" takes exactly 1 argument, but "
3156 << expr.
arguments().size() <<
" were provided";
3166 <<
" expects enum, but (" <<
expr2c(
arg1, *
this)
3167 <<
") has type `" <<
type2c(
arg1.type(), *
this) <<
'`';
3176 identifier ==
"__builtin_add_overflow" ||
3177 identifier ==
"__builtin_sadd_overflow" ||
3178 identifier ==
"__builtin_saddl_overflow" ||
3179 identifier ==
"__builtin_saddll_overflow" ||
3180 identifier ==
"__builtin_uadd_overflow" ||
3181 identifier ==
"__builtin_uaddl_overflow" ||
3182 identifier ==
"__builtin_uaddll_overflow" ||
3183 identifier ==
"__builtin_add_overflow_p")
3188 identifier ==
"__builtin_sub_overflow" ||
3189 identifier ==
"__builtin_ssub_overflow" ||
3190 identifier ==
"__builtin_ssubl_overflow" ||
3191 identifier ==
"__builtin_ssubll_overflow" ||
3192 identifier ==
"__builtin_usub_overflow" ||
3193 identifier ==
"__builtin_usubl_overflow" ||
3194 identifier ==
"__builtin_usubll_overflow" ||
3195 identifier ==
"__builtin_sub_overflow_p")
3200 identifier ==
"__builtin_mul_overflow" ||
3201 identifier ==
"__builtin_smul_overflow" ||
3202 identifier ==
"__builtin_smull_overflow" ||
3203 identifier ==
"__builtin_smulll_overflow" ||
3204 identifier ==
"__builtin_umul_overflow" ||
3205 identifier ==
"__builtin_umull_overflow" ||
3206 identifier ==
"__builtin_umulll_overflow" ||
3207 identifier ==
"__builtin_mul_overflow_p")
3212 identifier ==
"__builtin_bitreverse8" ||
3213 identifier ==
"__builtin_bitreverse16" ||
3214 identifier ==
"__builtin_bitreverse32" ||
3215 identifier ==
"__builtin_bitreverse64")
3222 <<
": error: " << identifier <<
" expects one operand";
3229 bitreverse.add_source_location() = source_location;
3249 <<
" takes exactly 3 arguments, but "
3250 << expr.
arguments().size() <<
" were provided";
3268 << identifier <<
" has signature " << identifier
3269 <<
"(integral, integral, integral" << (
_p ?
"" :
"*")
3331 error() <<
"not enough function arguments" <<
eom;
3338 error() <<
"wrong number of function arguments: "
3340 <<
", but got " << arguments.size() <<
eom;
3344 for(std::size_t
i=0;
i<arguments.size();
i++)
3365 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3414 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3457 return type0.element_type() ==
type1.element_type();
3567 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3638 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3656 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3664 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3751 error() <<
"operator '" << op_name <<
"' not defined for types '"
3785 error() <<
"cannot assign void" <<
eom;
3792 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3808 error() <<
"direct assignments to arrays not permitted" <<
eom;
3986 error() <<
"assignment '" << statement <<
"' not defined for types '"
4030 const auto rounding_mode =
4039 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4054 error() <<
"conversion to integer constant failed" <<
eom;
4062 const std::string &message)
const
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void base_type(typet &type, const namespacet &ns)
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
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.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
bitvector_typet index_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
floatbv_typet long_double_type()
bitvector_typet c_index_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_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_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_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.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
The byte swap expression.
const typet & underlying_type() const
virtual void typecheck_expr_main(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
symbol_tablet & symbol_table
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void make_constant_index(exprt &expr)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
A codet representing sequential composition of program statements.
static code_blockt from_list(const std::list< codet > &_list)
codet & find_last_statement()
A codet representing the declaration of a local variable.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
Data structure for representing an arbitrary statement in a program.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
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 & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
IEEE-floating-point equality.
static ieee_float_spect single_precision()
static ieee_float_spect double_precision()
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt zero(const floatbv_typet &type)
The trinary if-then-else operator.
An expression denoting infinity.
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) 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
irept & add(const irep_idt &name)
bool is_constant(const exprt &e) const override
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const override
this function determines which reference-typed expressions are constant
is_compile_time_constantt(const namespacet &ns)
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & warning() const
mstreamt & result() const
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
The plus expression Associativity is not specified.
const typet & base_type() const
The type of the data what we point to.
The popcount (counting the number of bits set to 1) expression.
A base class for a predicate that indicates that an address range is ok to read or write or both.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
An expression containing a side effect.
const irep_idt & get_statement() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
std::string as_string() const
Base type for structs and unions.
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
const irep_idt & display_name() const
Return language specific display name if present.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Type with multiple subtypes.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
const constant_exprt & size() const
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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'.
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_blockt & to_code_block(const codet &code)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
bool has_suffix(const std::string &s, const std::string &suffix)
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
const type_with_subtypet & to_type_with_subtype(const typet &type)