151 for(std::size_t i=0; i<
c_type1.parameters().size(); i++)
153 c_type1.parameters()[i].type(),
154 c_type2.parameters()[i].type()))
236 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
309 for(
const auto &binding : bindings)
314 error() <<
"expected declaration as operand of quantifier" <<
eom;
328 error() <<
"quantifier must not contain function calls" <<
eom;
333 for(
auto &binding : bindings)
340 for(
auto &binding : bindings)
341 domain.push_back(binding.type());
373 error() <<
"real part retrieval expects numerical operand, "
406 error() <<
"real part retrieval expects numerical operand, "
479 error() <<
"unmatched generic selection: " <<
to_string(op.type())
551 <<
"' not permitted for va_arg" <<
eom;
560 const auto &components =
follow_tag(*struct_tag_type).components();
561 if(components.size() != 5)
619 error() <<
"builtin_offsetof expects no operands" <<
eom;
630 for(
const auto &op : member.
operands())
637 error() <<
"offsetof of member expects struct/union type, "
662 if(!
o_opt.has_value())
665 error() <<
"offsetof failed to determine offset of '"
666 << component_name <<
"'" <<
eom;
695 if(!
o_opt.has_value())
698 error() <<
"offsetof failed to determine offset of '"
699 << component_name <<
"'" <<
eom;
722 error() <<
"offset-of of member failed to find component '"
723 << component_name <<
"' in '" <<
to_string(type) <<
"'"
735 error() <<
"offsetof of index expects array type" <<
eom;
750 error() <<
"offsetof failed to determine array element size" <<
eom;
793 for(
auto &binding : bindings)
802 error() <<
"forall/exists expects one declarator exactly" <<
eom;
809 symbol_table_baset::symbolst::const_iterator
s_it =
815 error() <<
"failed to find bound symbol `" << identifier
816 <<
"' in symbol table" <<
eom;
827 error() <<
"unexpected quantified symbol" <<
eom;
861 asm_label_mapt::const_iterator entry=
865 identifier=entry->second;
874 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
883 error() <<
"did not expect a type symbol here, but got '"
917 else if(identifier==
"__func__" ||
918 identifier==
"__FUNCTION__" ||
919 identifier==
"__PRETTY_FUNCTION__")
1029 error() <<
"type has no size: "
1040 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
1047 error() <<
"sizeof cannot be applied to single bits" <<
eom;
1068 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1108 .with_source_location(location);
1181 if(
c.type() == op.
type())
1195 <<
"' not found in union" <<
eom;
1212 tmp.copy_to_operands(op);
1274 error() <<
"type cast from void only permitted to void, but got '"
1296 <<
"' not permitted" <<
eom;
1381 error() <<
"operator [] must take array/vector or pointer but got '"
1495 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1509 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1556 error() <<
"ptrmember operator requires pointer or array type "
1557 "on left hand side, but got '"
1574 error() <<
"member operator requires structure type "
1575 "on left hand side but got '"
1586 error() <<
"member operator got incomplete " << type.
id()
1587 <<
" type on left hand side" <<
eom;
1608 error() <<
"member '" << component_name <<
"' not found in '"
1633 if(!identifier.
empty())
1641 error() <<
"member '" << component_name <<
"' is " <<
access <<
eom;
1682 else if(operands[2].type().
id()==
ID_pointer &&
1688 operands[1].type()!=operands[2].type())
1735 if(operands[1].type().
id()==
ID_empty ||
1743 operands[1].type() != operands[2].type() ||
1744 operands[1].type().
id() ==
ID_array)
1749 if(operands[1].type() == operands[2].type())
1751 expr.
type()=operands[1].type();
1778 if(operands.size()!=2)
1781 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1793 operands[0] =
if_expr.true_case();
1794 operands[1] =
if_expr.false_case();
1850 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1881 error() <<
"dereferencing void pointer" <<
eom;
1930 <<
"' not an lvalue" <<
eom;
1947 error() <<
"operator '" << statement <<
"' given incomplete type '"
1963 expr.
type()=underlying_type;
1984 error() <<
"operator '" << statement <<
"' not defined for type '"
2001 error() <<
"unknown side effect: " << statement <<
eom;
2013 "expression must be a " CPROVER_PREFIX "typed_target function call");
2020 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
2021 std::to_string(expr.
arguments().size()),
2031 arg0.source_location()};
2035 if(!size.has_value())
2039 "typed_target of type " +
2041 arg0.source_location()};
2050 arguments.push_back(size.value());
2068 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
2073 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
2074 std::to_string(expr.
arguments().size()),
2089 "obeys_contract must be a function pointer lvalue expression",
2097 "obeys_contract must have no ternary operator",
2112 "obeys_contract must must be a function symbol",
2120 "obeys_contract must have the same function pointer type",
2129 return ::builtin_factory(
2142 error() <<
"function_call side effect expects two operands" <<
eom;
2155 asm_label_mapt::const_iterator entry=
2158 identifier=entry->second;
2175 identifier ==
"__noop" &&
2189 identifier ==
"__builtin_shuffle" &&
2197 else if(identifier ==
"__builtin_shufflevector")
2207 identifier ==
"__builtin_elementwise_add_sat" ||
2208 identifier ==
"__builtin_elementwise_sub_sat")
2220 error() <<
"equal expects two operands" <<
eom;
2231 error() <<
"equal expects two operands of same type" <<
eom;
2245 overflow.add_source_location() =
f_op.source_location();
2270 of.add_source_location() =
overflow.source_location();
2277 tmp.add_source_location() =
f_op.source_location();
2282 overflow.add_source_location() =
tmp.source_location();
2292 error_message << identifier <<
" takes exactly 1 argument, but "
2293 << expr.
arguments().size() <<
" were provided";
2323 id2string(identifier) +
" expects one or two operands",
2324 f_op.source_location()};
2328 auto &pointer_expr = expr.
arguments()[0];
2329 if(pointer_expr.type().id() ==
ID_array)
2335 else if(pointer_expr.type().id() !=
ID_pointer)
2338 id2string(identifier) +
" expects a pointer as first argument",
2339 f_op.source_location()};
2354 const auto &subtype =
2360 " expects a size when given a void pointer",
2361 f_op.source_location()};
2391 "Shadow memory builtins should be an ellipsis with 0 parameter");
2399 new_symbol.location =
f_op.source_location();
2418 !parameters.empty(),
2419 "GCC polymorphic built-ins should have at least one parameter");
2424 if(parameters.front().type().id() ==
ID_pointer)
2441 for(std::size_t i = 0; i < parameters.size(); ++i)
2443 const std::string base_name =
"p_" + std::to_string(i);
2451 new_symbol.
type = parameters[i].type();
2456 parameters[i].set_identifier(new_symbol.
name);
2457 parameters[i].set_base_name(new_symbol.
base_name);
2465 new_symbol.location =
f_op.source_location();
2472 new_symbol.value = implementation;
2489 if(identifier==
"malloc" ||
2490 identifier==
"realloc" ||
2491 identifier==
"reallocf" ||
2492 identifier==
"valloc")
2499 new_symbol.base_name=identifier;
2513 debug() <<
"builtin '" << identifier <<
"' is unknown" <<
eom;
2518 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2539 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2547 if(p.first.type() != p.second)
2560 expr.
swap(function_application);
2567 error() <<
"expected function/function pointer as argument but got '"
2581 tmp.add_source_location()=
f_op.source_location();
2588 error() <<
"expected code as argument" <<
eom;
2598 if(
tmp.is_not_nil())
2663 "pointer_in_range_dfcc expects pointer-typed arguments",
2664 arg.source_location()};
2674 error() <<
"same_object expects two operands" <<
eom;
2691 error() <<
"get_must expects two operands" <<
eom;
2708 error() <<
"get_may expects two operands" <<
eom;
2725 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2741 error() <<
"buffer_size expects one operand" <<
eom;
2759 error() <<
"is_list expects one operand" <<
eom;
2771 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2787 error() <<
"is_dll expects one operand" <<
eom;
2799 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2805 is_dll_expr.add_source_location() = source_location;
2815 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2827 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2843 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2860 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2878 error() <<
"is_cstring expects one operand" <<
eom;
2887 error() <<
"is_cstring expects a pointer operand" <<
eom;
2902 error() <<
"cstrlen expects one operand" <<
eom;
2911 error() <<
"cstrlen expects a pointer operand" <<
eom;
2925 error() <<
"is_zero_string expects one operand" <<
eom;
2943 error() <<
"zero_string_length expects one operand" <<
eom;
2961 error() <<
"dynamic_object expects one argument" <<
eom;
2977 error() <<
"live_object expects one argument" <<
eom;
2993 error() <<
"pointer_in_range expects three arguments" <<
eom;
3010 error() <<
"writeable_object expects one argument" <<
eom;
3027 error() <<
"separate expects two or more arguments" <<
eom;
3043 error() <<
"pointer_offset expects one argument" <<
eom;
3059 error() <<
"object_size expects one operand" <<
eom;
3075 error() <<
"pointer_object expects one argument" <<
eom;
3086 else if(identifier==
"__builtin_bswap16" ||
3087 identifier==
"__builtin_bswap32" ||
3088 identifier==
"__builtin_bswap64")
3093 error() << identifier <<
" expects one operand" <<
eom;
3101 bswap_expr.add_source_location()=source_location;
3106 identifier ==
"__builtin_rotateleft8" ||
3107 identifier ==
"__builtin_rotateleft16" ||
3108 identifier ==
"__builtin_rotateleft32" ||
3109 identifier ==
"__builtin_rotateleft64" ||
3110 identifier ==
"__builtin_rotateright8" ||
3111 identifier ==
"__builtin_rotateright16" ||
3112 identifier ==
"__builtin_rotateright32" ||
3113 identifier ==
"__builtin_rotateright64")
3119 error() << identifier <<
" expects two operands" <<
eom;
3125 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
3126 identifier ==
"__builtin_rotateleft16" ||
3127 identifier ==
"__builtin_rotateleft32" ||
3128 identifier ==
"__builtin_rotateleft64")
3133 rotate_expr.add_source_location() = source_location;
3137 else if(identifier==
"__builtin_nontemporal_load")
3142 error() << identifier <<
" expects one operand" <<
eom;
3154 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3163 identifier ==
"__builtin_fpclassify" ||
3169 error() << identifier <<
" expects six arguments" <<
eom;
3185 error() <<
"non-floating-point argument for " << identifier <<
eom;
3193 const auto &arguments = expr.
arguments();
3212 identifier==
"__builtin_isnan")
3217 error() <<
"isnan expects one operand" <<
eom;
3224 isnan_expr.add_source_location()=source_location;
3235 error() <<
"isfinite expects one operand" <<
eom;
3247 identifier==
"__builtin_inf")
3252 inf_expr.add_source_location()=source_location;
3261 inff_expr.add_source_location()=source_location;
3270 infl_expr.add_source_location()=source_location;
3282 error() << identifier <<
" expects two arguments" <<
eom;
3303 error() <<
"abs-functions expect one operand" <<
eom;
3310 abs_expr.add_source_location()=source_location;
3322 error() <<
"fmod-functions expect two operands" <<
eom;
3334 fmod_expr.add_source_location() = source_location;
3346 error() <<
"remainder-functions expect two operands" <<
eom;
3367 error() <<
"allocate expects two operands" <<
eom;
3385 error() << identifier <<
" expects one operand" <<
eom;
3397 <<
" expressions is not supported yet." <<
eom;
3404 old_expr.add_source_location() = source_location;
3411 identifier==
"__builtin_isinf")
3416 error() << identifier <<
" expects one operand" <<
eom;
3427 error() <<
"non-floating-point argument for " << identifier <<
eom;
3432 isinf_expr.add_source_location()=source_location;
3436 else if(identifier ==
"__builtin_isinf_sign")
3441 error() << identifier <<
" expects one operand" <<
eom;
3454 error() <<
"non-floating-point argument for " << identifier <<
eom;
3459 isinf_expr.add_source_location() = source_location;
3472 identifier ==
"__builtin_isnormal")
3477 error() << identifier <<
" expects one operand" <<
eom;
3488 error() <<
"non-floating-point argument for " << identifier <<
eom;
3500 identifier==
"__builtin_signbit" ||
3501 identifier==
"__builtin_signbitf" ||
3502 identifier==
"__builtin_signbitl")
3507 error() << identifier <<
" expects one operand" <<
eom;
3514 sign_expr.add_source_location()=source_location;
3518 else if(identifier==
"__builtin_popcount" ||
3519 identifier==
"__builtin_popcountl" ||
3520 identifier==
"__builtin_popcountll" ||
3521 identifier==
"__popcnt16" ||
3522 identifier==
"__popcnt" ||
3523 identifier==
"__popcnt64")
3528 error() << identifier <<
" expects one operand" <<
eom;
3540 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
3541 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
3542 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
3547 error() << identifier <<
" expects one operand" <<
eom;
3555 clz.add_source_location() = source_location;
3557 return std::move(
clz);
3560 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3561 identifier ==
"__builtin_ctzll")
3566 error() << identifier <<
" expects one operand" <<
eom;
3574 ctz.add_source_location() = source_location;
3576 return std::move(
ctz);
3579 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3580 identifier ==
"__builtin_ffsll")
3585 error() << identifier <<
" expects one operand" <<
eom;
3592 ffs.add_source_location() = source_location;
3594 return std::move(
ffs);
3596 else if(identifier==
"__builtin_expect")
3607 error() <<
"__builtin_expect expects two arguments" <<
eom;
3616 identifier ==
"__builtin_object_size" ||
3617 identifier ==
"__builtin_dynamic_object_size")
3628 error() <<
"__builtin_object_size expects two arguments" <<
eom;
3645 error() <<
"__builtin_object_size expects constant as second argument, "
3656 tmp.add_source_location()=
f_op.source_location();
3661 tmp.add_source_location()=
f_op.source_location();
3666 else if(identifier==
"__builtin_choose_expr")
3672 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3687 else if(identifier==
"__builtin_constant_p")
3694 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3724 tmp2.add_source_location()=source_location;
3728 else if(identifier==
"__builtin_classify_type")
3735 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3774 tmp.add_source_location()=source_location;
3779 identifier ==
"__builtin_add_overflow" ||
3780 identifier ==
"__builtin_sadd_overflow" ||
3781 identifier ==
"__builtin_saddl_overflow" ||
3782 identifier ==
"__builtin_saddll_overflow" ||
3783 identifier ==
"__builtin_uadd_overflow" ||
3784 identifier ==
"__builtin_uaddl_overflow" ||
3785 identifier ==
"__builtin_uaddll_overflow" ||
3786 identifier ==
"__builtin_add_overflow_p")
3791 identifier ==
"__builtin_sub_overflow" ||
3792 identifier ==
"__builtin_ssub_overflow" ||
3793 identifier ==
"__builtin_ssubl_overflow" ||
3794 identifier ==
"__builtin_ssubll_overflow" ||
3795 identifier ==
"__builtin_usub_overflow" ||
3796 identifier ==
"__builtin_usubl_overflow" ||
3797 identifier ==
"__builtin_usubll_overflow" ||
3798 identifier ==
"__builtin_sub_overflow_p")
3803 identifier ==
"__builtin_mul_overflow" ||
3804 identifier ==
"__builtin_smul_overflow" ||
3805 identifier ==
"__builtin_smull_overflow" ||
3806 identifier ==
"__builtin_smulll_overflow" ||
3807 identifier ==
"__builtin_umul_overflow" ||
3808 identifier ==
"__builtin_umull_overflow" ||
3809 identifier ==
"__builtin_umulll_overflow" ||
3810 identifier ==
"__builtin_mul_overflow_p")
3815 identifier ==
"__builtin_bitreverse8" ||
3816 identifier ==
"__builtin_bitreverse16" ||
3817 identifier ==
"__builtin_bitreverse32" ||
3818 identifier ==
"__builtin_bitreverse64")
3824 error_message <<
"error: " << identifier <<
" expects one operand";
3832 bitreverse.add_source_location() = source_location;
3851 error_message << identifier <<
" takes exactly 3 arguments, but "
3852 << expr.
arguments().size() <<
" were provided";
3870 error_message <<
"error: " << identifier <<
" has signature "
3871 << identifier <<
"(integral, integral, integral"
3872 << (
_p ?
"" :
"*") <<
"), "
3914 <<
" takes exactly two arguments, but "
3915 << expr.
arguments().size() <<
" were provided";
3923 identifier ==
"__builtin_elementwise_sub_sat")
3929 identifier ==
"__builtin_elementwise_add_sat")
3962 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3964 arguments.push_back(
3970 if(parameters.size() > arguments.size())
3973 error() <<
"not enough function arguments" <<
eom;
3977 else if(parameters.size() != arguments.size())
3980 error() <<
"wrong number of function arguments: "
3981 <<
"expected " << parameters.size() <<
", but got "
3982 << arguments.size() <<
eom;
3986 for(std::size_t i=0; i<arguments.size(); i++)
3988 exprt &op=arguments[i];
3994 else if(i < parameters.size())
4003 warning() <<
"assignment where Boolean argument is expected" <<
eom;
4052 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
4095 return type0.element_type() ==
type1.element_type();
4221 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4292 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4310 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4318 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4326 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4423 error() <<
"operator '" << op_name <<
"' not defined for types '"
4457 error() <<
"cannot assign void" <<
eom;
4464 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4480 error() <<
"direct assignments to arrays not permitted" <<
eom;
4662 error() <<
"assignment '" << statement <<
"' not defined for types '"
4714 return is_constant(op);
4764 const auto rounding_mode =
4774 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4791 error() <<
"conversion to integer constant failed" <<
eom;
4799 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)
unsignedbv_typet unsigned_int_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.
virtual void clear()
Reset the abstract state.
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.
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
static std::optional< 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)
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 std::optional< 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.
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 void typecheck_expr_operands(exprt &expr)
virtual std::optional< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
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.
const irep_idt & get_statement() const
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.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
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.
Round a floating-point number to an integral value considering the given rounding mode.
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_float_valuet zero(const floatbv_typet &type)
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
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.
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.
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
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.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, 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)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
const code_blockt & to_code_block(const codet &code)
bool can_cast_expr< side_effect_exprt >(const exprt &base)
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_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 struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_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)