152 for(std::size_t i=0; i<
c_type1.parameters().size(); i++)
154 c_type1.parameters()[i].type(),
155 c_type2.parameters()[i].type()))
237 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
310 for(
const auto &binding : bindings)
315 error() <<
"expected declaration as operand of quantifier" <<
eom;
323 error() <<
"quantifier must not contain side effects" <<
eom;
328 for(
auto &binding : bindings)
335 for(
auto &binding : bindings)
336 domain.push_back(binding.type());
368 error() <<
"real part retrieval expects numerical operand, "
401 error() <<
"real part retrieval expects numerical operand, "
475 error() <<
"unmatched generic selection: " <<
to_string(op.type())
581 error() <<
"builtin_offsetof expects no operands" <<
eom;
592 for(
const auto &op : member.
operands())
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;
756 for(
auto &binding : bindings)
765 error() <<
"forall/exists expects one declarator exactly" <<
eom;
772 symbol_table_baset::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 '"
880 else if(identifier==
"__func__" ||
881 identifier==
"__FUNCTION__" ||
882 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);
1205 error() <<
"type cast from void only permitted to void, but got '"
1227 <<
"' not permitted" <<
eom;
1312 error() <<
"operator [] must take array/vector or pointer but got '"
1426 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1440 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1487 error() <<
"ptrmember operator requires pointer or array type "
1488 "on left hand side, but got '"
1508 error() <<
"member operator requires structure type "
1509 "on left hand side but got '"
1520 error() <<
"member operator got incomplete " << type.
id()
1521 <<
" type on left hand side" <<
eom;
1542 error() <<
"member '" << component_name <<
"' not found in '"
1563 if(!identifier.
empty())
1571 error() <<
"member '" << component_name <<
"' is " <<
access <<
eom;
1600 else if(operands[2].type().
id()==
ID_pointer &&
1606 operands[1].type()!=operands[2].type())
1653 if(operands[1].type().
id()==
ID_empty ||
1661 operands[1].type() != operands[2].type() ||
1662 operands[1].type().
id() ==
ID_array)
1667 if(operands[1].type() == operands[2].type())
1669 expr.
type()=operands[1].type();
1696 if(operands.size()!=2)
1699 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1711 operands[0] =
if_expr.true_case();
1712 operands[1] =
if_expr.false_case();
1768 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1799 error() <<
"dereferencing void pointer" <<
eom;
1848 <<
"' not an lvalue" <<
eom;
1865 error() <<
"operator '" << statement <<
"' given incomplete type '"
1880 expr.
type()=underlying_type;
1899 error() <<
"operator '" << statement <<
"' not defined for type '"
1916 error() <<
"unknown side effect: " << statement <<
eom;
1928 "expression must be a " CPROVER_PREFIX "typed_target function call");
1935 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
1936 std::to_string(expr.
arguments().size()),
1946 arg0.source_location()};
1950 if(!size.has_value())
1954 "typed_target of type " +
1956 arg0.source_location()};
1965 arguments.push_back(size.value());
1983 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
1988 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
1989 std::to_string(expr.
arguments().size()),
2004 "obeys_contract must be a function pointer lvalue expression",
2012 "obeys_contract must have no ternary operator",
2027 "obeys_contract must must be a function symbol",
2035 "obeys_contract must have the same function pointer type",
2044 return ::builtin_factory(
2057 error() <<
"function_call side effect expects two operands" <<
eom;
2070 asm_label_mapt::const_iterator entry=
2073 identifier=entry->second;
2090 identifier ==
"__noop" &&
2104 identifier ==
"__builtin_shuffle" &&
2112 else if(identifier ==
"__builtin_shufflevector")
2133 error() <<
"equal expects two operands" <<
eom;
2144 error() <<
"equal expects two operands of same type" <<
eom;
2158 overflow.add_source_location() =
f_op.source_location();
2183 of.add_source_location() =
overflow.source_location();
2190 tmp.add_source_location() =
f_op.source_location();
2195 overflow.add_source_location() =
tmp.source_location();
2205 error_message << identifier <<
" takes exactly 1 argument, but "
2206 << expr.
arguments().size() <<
" were provided";
2236 id2string(identifier) +
" expects one or two operands",
2237 f_op.source_location()};
2241 auto &pointer_expr = expr.
arguments()[0];
2242 if(pointer_expr.type().id() ==
ID_array)
2248 else if(pointer_expr.type().id() !=
ID_pointer)
2251 id2string(identifier) +
" expects a pointer as first argument",
2252 f_op.source_location()};
2267 const auto &subtype =
2273 " expects a size when given a void pointer",
2274 f_op.source_location()};
2304 "Shadow memory builtins should be an ellipsis with 0 parameter");
2312 new_symbol.location =
f_op.source_location();
2331 !parameters.empty(),
2332 "GCC polymorphic built-ins should have at least one parameter");
2337 if(parameters.front().type().id() ==
ID_pointer)
2354 for(std::size_t i = 0; i < parameters.size(); ++i)
2356 const std::string base_name =
"p_" + std::to_string(i);
2364 new_symbol.
type = parameters[i].type();
2369 parameters[i].set_identifier(new_symbol.
name);
2370 parameters[i].set_base_name(new_symbol.
base_name);
2378 new_symbol.location =
f_op.source_location();
2385 new_symbol.value = implementation;
2402 if(identifier==
"malloc" ||
2403 identifier==
"realloc" ||
2404 identifier==
"reallocf" ||
2405 identifier==
"valloc")
2412 new_symbol.base_name=identifier;
2422 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2442 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2450 if(p.first.type() != p.second)
2463 expr.
swap(function_application);
2470 error() <<
"expected function/function pointer as argument but got '"
2484 tmp.add_source_location()=
f_op.source_location();
2491 error() <<
"expected code as argument" <<
eom;
2501 if(
tmp.is_not_nil())
2554 "pointer_in_range_dfcc expects pointer-typed arguments",
2555 arg.source_location()};
2565 error() <<
"same_object expects two operands" <<
eom;
2582 error() <<
"get_must expects two operands" <<
eom;
2599 error() <<
"get_may expects two operands" <<
eom;
2616 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2632 error() <<
"buffer_size expects one operand" <<
eom;
2650 error() <<
"is_list expects one operand" <<
eom;
2662 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2678 error() <<
"is_dll expects one operand" <<
eom;
2690 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2696 is_dll_expr.add_source_location() = source_location;
2706 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2718 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2734 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2751 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2769 error() <<
"is_cstring expects one operand" <<
eom;
2778 error() <<
"is_cstring expects a pointer operand" <<
eom;
2793 error() <<
"cstrlen expects one operand" <<
eom;
2802 error() <<
"cstrlen expects a pointer operand" <<
eom;
2816 error() <<
"is_zero_string expects one operand" <<
eom;
2834 error() <<
"zero_string_length expects one operand" <<
eom;
2852 error() <<
"dynamic_object expects one argument" <<
eom;
2868 error() <<
"live_object expects one argument" <<
eom;
2884 error() <<
"pointer_in_range expects three arguments" <<
eom;
2901 error() <<
"writeable_object expects one argument" <<
eom;
2918 error() <<
"separate expects two or more arguments" <<
eom;
2934 error() <<
"pointer_offset expects one argument" <<
eom;
2950 error() <<
"object_size expects one operand" <<
eom;
2966 error() <<
"pointer_object expects one argument" <<
eom;
2977 else if(identifier==
"__builtin_bswap16" ||
2978 identifier==
"__builtin_bswap32" ||
2979 identifier==
"__builtin_bswap64")
2984 error() << identifier <<
" expects one operand" <<
eom;
2992 bswap_expr.add_source_location()=source_location;
2997 identifier ==
"__builtin_rotateleft8" ||
2998 identifier ==
"__builtin_rotateleft16" ||
2999 identifier ==
"__builtin_rotateleft32" ||
3000 identifier ==
"__builtin_rotateleft64" ||
3001 identifier ==
"__builtin_rotateright8" ||
3002 identifier ==
"__builtin_rotateright16" ||
3003 identifier ==
"__builtin_rotateright32" ||
3004 identifier ==
"__builtin_rotateright64")
3010 error() << identifier <<
" expects two operands" <<
eom;
3016 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
3017 identifier ==
"__builtin_rotateleft16" ||
3018 identifier ==
"__builtin_rotateleft32" ||
3019 identifier ==
"__builtin_rotateleft64")
3024 rotate_expr.add_source_location() = source_location;
3028 else if(identifier==
"__builtin_nontemporal_load")
3033 error() << identifier <<
" expects one operand" <<
eom;
3045 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3054 identifier ==
"__builtin_fpclassify" ||
3060 error() << identifier <<
" expects six arguments" <<
eom;
3076 error() <<
"non-floating-point argument for " << identifier <<
eom;
3084 const auto &arguments = expr.
arguments();
3103 identifier==
"__builtin_isnan")
3108 error() <<
"isnan expects one operand" <<
eom;
3115 isnan_expr.add_source_location()=source_location;
3126 error() <<
"isfinite expects one operand" <<
eom;
3138 identifier==
"__builtin_inf")
3143 inf_expr.add_source_location()=source_location;
3152 inff_expr.add_source_location()=source_location;
3161 infl_expr.add_source_location()=source_location;
3176 error() <<
"abs-functions expect one operand" <<
eom;
3183 abs_expr.add_source_location()=source_location;
3195 error() <<
"fmod-functions expect two operands" <<
eom;
3207 fmod_expr.add_source_location() = source_location;
3219 error() <<
"remainder-functions expect two operands" <<
eom;
3240 error() <<
"allocate expects two operands" <<
eom;
3258 error() << identifier <<
" expects one operand" <<
eom;
3270 <<
" expressions is not supported yet." <<
eom;
3277 old_expr.add_source_location() = source_location;
3284 identifier==
"__builtin_isinf")
3289 error() << identifier <<
" expects one operand" <<
eom;
3300 error() <<
"non-floating-point argument for " << identifier <<
eom;
3305 isinf_expr.add_source_location()=source_location;
3309 else if(identifier ==
"__builtin_isinf_sign")
3314 error() << identifier <<
" expects one operand" <<
eom;
3327 error() <<
"non-floating-point argument for " << identifier <<
eom;
3332 isinf_expr.add_source_location() = source_location;
3345 identifier ==
"__builtin_isnormal")
3350 error() << identifier <<
" expects one operand" <<
eom;
3361 error() <<
"non-floating-point argument for " << identifier <<
eom;
3373 identifier==
"__builtin_signbit" ||
3374 identifier==
"__builtin_signbitf" ||
3375 identifier==
"__builtin_signbitl")
3380 error() << identifier <<
" expects one operand" <<
eom;
3387 sign_expr.add_source_location()=source_location;
3391 else if(identifier==
"__builtin_popcount" ||
3392 identifier==
"__builtin_popcountl" ||
3393 identifier==
"__builtin_popcountll" ||
3394 identifier==
"__popcnt16" ||
3395 identifier==
"__popcnt" ||
3396 identifier==
"__popcnt64")
3401 error() << identifier <<
" expects one operand" <<
eom;
3413 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
3414 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
3415 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
3420 error() << identifier <<
" expects one operand" <<
eom;
3429 clz.add_source_location() = source_location;
3431 return std::move(
clz);
3434 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3435 identifier ==
"__builtin_ctzll")
3440 error() << identifier <<
" expects one operand" <<
eom;
3448 ctz.add_source_location() = source_location;
3450 return std::move(
ctz);
3453 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3454 identifier ==
"__builtin_ffsll")
3459 error() << identifier <<
" expects one operand" <<
eom;
3466 ffs.add_source_location() = source_location;
3468 return std::move(
ffs);
3470 else if(identifier==
"__builtin_expect")
3481 error() <<
"__builtin_expect expects two arguments" <<
eom;
3489 else if(identifier==
"__builtin_object_size")
3498 error() <<
"__builtin_object_size expects two arguments" <<
eom;
3515 error() <<
"__builtin_object_size expects constant as second argument, "
3526 tmp.add_source_location()=
f_op.source_location();
3531 tmp.add_source_location()=
f_op.source_location();
3536 else if(identifier==
"__builtin_choose_expr")
3542 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3557 else if(identifier==
"__builtin_constant_p")
3564 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3594 tmp2.add_source_location()=source_location;
3598 else if(identifier==
"__builtin_classify_type")
3605 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3651 tmp.add_source_location()=source_location;
3656 identifier ==
"__builtin_add_overflow" ||
3657 identifier ==
"__builtin_sadd_overflow" ||
3658 identifier ==
"__builtin_saddl_overflow" ||
3659 identifier ==
"__builtin_saddll_overflow" ||
3660 identifier ==
"__builtin_uadd_overflow" ||
3661 identifier ==
"__builtin_uaddl_overflow" ||
3662 identifier ==
"__builtin_uaddll_overflow" ||
3663 identifier ==
"__builtin_add_overflow_p")
3668 identifier ==
"__builtin_sub_overflow" ||
3669 identifier ==
"__builtin_ssub_overflow" ||
3670 identifier ==
"__builtin_ssubl_overflow" ||
3671 identifier ==
"__builtin_ssubll_overflow" ||
3672 identifier ==
"__builtin_usub_overflow" ||
3673 identifier ==
"__builtin_usubl_overflow" ||
3674 identifier ==
"__builtin_usubll_overflow" ||
3675 identifier ==
"__builtin_sub_overflow_p")
3680 identifier ==
"__builtin_mul_overflow" ||
3681 identifier ==
"__builtin_smul_overflow" ||
3682 identifier ==
"__builtin_smull_overflow" ||
3683 identifier ==
"__builtin_smulll_overflow" ||
3684 identifier ==
"__builtin_umul_overflow" ||
3685 identifier ==
"__builtin_umull_overflow" ||
3686 identifier ==
"__builtin_umulll_overflow" ||
3687 identifier ==
"__builtin_mul_overflow_p")
3692 identifier ==
"__builtin_bitreverse8" ||
3693 identifier ==
"__builtin_bitreverse16" ||
3694 identifier ==
"__builtin_bitreverse32" ||
3695 identifier ==
"__builtin_bitreverse64")
3701 error_message <<
"error: " << identifier <<
" expects one operand";
3709 bitreverse.add_source_location() = source_location;
3728 error_message << identifier <<
" takes exactly 3 arguments, but "
3729 << expr.
arguments().size() <<
" were provided";
3747 error_message <<
"error: " << identifier <<
" has signature "
3748 << identifier <<
"(integral, integral, integral"
3749 << (
_p ?
"" :
"*") <<
"), "
3791 <<
" takes exactly two arguments, but "
3792 << expr.
arguments().size() <<
" were provided";
3831 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3833 arguments.push_back(
3839 if(parameters.size() > arguments.size())
3842 error() <<
"not enough function arguments" <<
eom;
3846 else if(parameters.size() != arguments.size())
3849 error() <<
"wrong number of function arguments: "
3850 <<
"expected " << parameters.size() <<
", but got "
3851 << arguments.size() <<
eom;
3855 for(std::size_t i=0; i<arguments.size(); i++)
3857 exprt &op=arguments[i];
3863 else if(i < parameters.size())
3872 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3921 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3964 return type0.element_type() ==
type1.element_type();
4090 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4161 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4179 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4187 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4195 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4292 error() <<
"operator '" << op_name <<
"' not defined for types '"
4326 error() <<
"cannot assign void" <<
eom;
4333 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4349 error() <<
"direct assignments to arrays not permitted" <<
eom;
4530 error() <<
"assignment '" << statement <<
"' not defined for types '"
4582 return is_constant(op);
4630 const auto rounding_mode =
4639 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4654 error() <<
"conversion to integer constant failed" <<
eom;
4662 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.
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.
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()
bitvector_typet char_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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const declaratorst & declarators() const
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.
The byte swap expression.
static optionalt< std::string > check_address_can_be_taken(const typet &)
virtual void typecheck_obeys_contract_call(side_effect_expr_function_callt &expr)
Checks an obeys_contract predicate occurrence.
virtual void typecheck_expr_main(exprt &expr)
symbol_table_baset & symbol_table
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)
virtual optionalt< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
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)
exprt typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr)
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 typecheck_typed_target_call(side_effect_expr_function_callt &expr)
const irep_idt const irep_idt mode
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_arithmetic_pointer(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_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)
virtual bool builtin_factory(const irep_idt &)
A codet representing sequential composition of program statements.
static code_blockt from_list(const std::list< codet > &_list)
A codet representing the declaration of a local variable.
std::vector< parametert > parameterst
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...
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
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.
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
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
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 set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
Architecturally similar to can_forward_propagatet, but specialized for what is a constexpr,...
is_compile_time_constantt(const namespacet &ns)
bool is_constant(const exprt &e) const
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const
this function determines which reference-typed expressions are constant
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
A predicate that indicates that a zero-terminated string starts at the given address.
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 predicate that indicates that the object pointed to is live.
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.
Expression for finding the size (in bytes) of the object a pointer points to.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
The plus expression Associativity is not specified.
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
The popcount (counting the number of bits set to 1) expression.
A base class for expressions that are predicates, i.e., Boolean-typed.
A base class for a predicate that indicates that an address range is ok to read or write or both.
Saturating subtraction expression.
The saturating plus expression.
A predicate that indicates that the objects pointed to are distinct.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
A side_effect_exprt that returns a non-deterministically chosen value.
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
Base type for structs and unions.
Expression to hold a symbol (variable)
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
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.
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.
irep_idt mode
Language mode.
The Boolean constant true.
Type with multiple subtypes.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Union constructor from single element.
A predicate that indicates that the object pointed to is writeable.
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)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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 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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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)
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
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'.
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_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 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 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)