48 if(expr.
id()==ID_already_typechecked)
66 if(expr.
id()==ID_div ||
71 if(expr.
type().
id()==ID_floatbv &&
80 expr.
id(ID_floatbv_div);
81 else if(expr.
id()==ID_mult)
82 expr.
id(ID_floatbv_mult);
83 else if(expr.
id()==ID_plus)
84 expr.
id(ID_floatbv_plus);
85 else if(expr.
id()==ID_minus)
86 expr.
id(ID_floatbv_minus);
107 if(type1.
id()==ID_c_enum_tag)
109 else if(type2.
id()==ID_c_enum_tag)
112 if(type1.
id()==ID_c_enum)
114 if(type2.
id()==ID_c_enum)
116 else if(type2==type1.
subtype())
119 else if(type2.
id()==ID_c_enum)
124 else if(type1.
id()==ID_pointer &&
125 type2.
id()==ID_pointer)
129 else if(type1.
id()==ID_array &&
130 type2.
id()==ID_array)
135 else if(type1.
id()==ID_code &&
149 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
165 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
175 if(expr.
id()==ID_side_effect)
177 else if(expr.
id()==ID_constant)
179 else if(expr.
id()==ID_infinity)
183 else if(expr.
id()==ID_symbol)
185 else if(expr.
id()==ID_unary_plus ||
186 expr.
id()==ID_unary_minus ||
187 expr.
id()==ID_bitnot)
189 else if(expr.
id()==ID_not)
192 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
195 else if(expr.
id()==ID_address_of)
197 else if(expr.
id()==ID_dereference)
199 else if(expr.
id()==ID_member)
201 else if(expr.
id()==ID_ptrmember)
203 else if(expr.
id()==ID_equal ||
204 expr.
id()==ID_notequal ||
210 else if(expr.
id()==ID_index)
212 else if(expr.
id()==ID_typecast)
214 else if(expr.
id()==ID_sizeof)
216 else if(expr.
id()==ID_alignof)
219 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
220 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
221 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
225 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
227 else if(expr.
id()==ID_comma)
229 else if(expr.
id()==ID_if)
231 else if(expr.
id()==ID_code)
234 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
237 else if(expr.
id()==ID_gcc_builtin_va_arg)
239 else if(expr.
id()==ID_cw_va_arg_typeof)
241 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
246 assert(subtypes.size()==2);
252 subtypes[0].
remove(ID_C_constant);
253 subtypes[0].remove(ID_C_volatile);
254 subtypes[0].remove(ID_C_restricted);
255 subtypes[1].remove(ID_C_constant);
256 subtypes[1].remove(ID_C_volatile);
257 subtypes[1].remove(ID_C_restricted);
262 else if(expr.
id()==ID_clang_builtin_convertvector)
271 else if(expr.
id()==ID_builtin_offsetof)
273 else if(expr.
id()==ID_string_constant)
276 expr.
set(ID_C_lvalue,
true);
278 else if(expr.
id()==ID_arguments)
282 else if(expr.
id()==ID_designated_initializer)
284 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
288 if(it->id()==ID_index)
292 else if(expr.
id()==ID_initializer_list)
298 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
304 auto &bindings = binary_expr.op0().operands();
305 auto &where = binary_expr.op1();
307 for(
const auto &binding : bindings)
309 if(binding.get(ID_statement) != ID_decl)
312 error() <<
"expected declaration as operand of quantifier" <<
eom;
320 error() <<
"quantifier must not contain side effects" <<
eom;
325 for(
auto &binding : bindings)
328 if(expr.
id() == ID_lambda)
332 for(
auto &binding : bindings)
333 domain.push_back(binding.type());
343 else if(expr.
id()==ID_label)
347 else if(expr.
id()==ID_array)
351 else if(expr.
id()==ID_complex)
356 else if(expr.
id() == ID_complex_real)
360 if(op.
type().
id() != ID_complex)
365 error() <<
"real part retrieval expects numerical operand, "
373 expr.
swap(complex_real_expr);
381 complex_real_expr.
set(ID_C_lvalue,
true);
384 complex_real_expr.
type().
set(ID_C_constant,
true);
386 expr.
swap(complex_real_expr);
389 else if(expr.
id() == ID_complex_imag)
393 if(op.
type().
id() != ID_complex)
398 error() <<
"real part retrieval expects numerical operand, "
406 expr.
swap(complex_imag_expr);
414 complex_imag_expr.
set(ID_C_lvalue,
true);
417 complex_imag_expr.
type().
set(ID_C_constant,
true);
419 expr.
swap(complex_imag_expr);
422 else if(expr.
id()==ID_generic_selection)
432 if(op.type().id() == ID_bool)
439 for(
auto &irep : generic_associations)
441 if(irep.get(ID_type_arg) != ID_default)
443 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
454 for(
const auto &irep : generic_associations)
456 if(irep.get(ID_type_arg) == ID_default)
457 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
459 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
461 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
468 expr.
swap(default_match);
472 error() <<
"unmatched generic selection: " <<
to_string(op.type())
478 expr.
swap(assoc_match);
483 else if(expr.
id()==ID_gcc_asm_input ||
484 expr.
id()==ID_gcc_asm_output ||
485 expr.
id()==ID_gcc_asm_clobbered_register)
488 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
489 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
493 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
511 expr.
set(ID_C_lvalue,
true);
548 symbol.
name=ID_gcc_builtin_va_arg;
549 symbol.
type=symbol_type;
579 error() <<
"builtin_offsetof expects no operands" <<
eom;
594 if(m_it->id()==ID_member)
596 if(type.
id()!=ID_union && type.
id()!=ID_struct)
599 error() <<
"offsetof of member expects struct/union type, "
605 irep_idt component_name=m_it->get(ID_component_name);
609 assert(type.
id()==ID_union || type.
id()==ID_struct);
619 if(type.
id()==ID_struct)
624 if(!o_opt.has_value())
627 error() <<
"offsetof failed to determine offset of '"
628 << component_name <<
"'" <<
eom;
644 for(
const auto &c : struct_union_type.
components())
648 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
652 if(type.
id()==ID_struct)
657 if(!o_opt.has_value())
660 error() <<
"offsetof failed to determine offset of '"
661 << component_name <<
"'" <<
eom;
673 assert(type.
id()==ID_union || type.
id()==ID_struct);
683 error() <<
"offset-of of member failed to find component '"
684 << component_name <<
"' in '" <<
to_string(type) <<
"'"
691 else if(m_it->id()==ID_index)
693 if(type.
id()!=ID_array)
696 error() <<
"offsetof of index expects array type" <<
eom;
707 if(!sub_size_opt.has_value())
710 error() <<
"offsetof failed to determine array element size" <<
eom;
733 if(expr.
id()==ID_side_effect &&
734 expr.
get(ID_statement)==ID_function_call)
739 else if(expr.
id()==ID_side_effect &&
740 expr.
get(ID_statement)==ID_statement_expression)
745 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
751 auto &bindings = binary_expr.op0().operands();
753 for(
auto &binding : bindings)
762 error() <<
"forall/exists expects one declarator exactly" <<
eom;
769 symbol_tablet::symbolst::const_iterator s_it =
775 error() <<
"failed to find bound symbol `" << identifier
776 <<
"' in symbol table" <<
eom;
780 const symbolt &symbol = s_it->second;
787 error() <<
"unexpected quantified symbol" <<
eom;
811 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
815 expr.
type()=p_it->second;
816 expr.
set(ID_C_lvalue,
true);
821 asm_label_mapt::const_iterator entry=
825 identifier=entry->second;
831 if(
lookup(identifier, symbol_ptr))
834 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
838 const symbolt &symbol=*symbol_ptr;
843 error() <<
"did not expect a type symbol here, but got '"
861 if(expr.
id()==ID_constant &&
863 expr.
set(ID_C_cformat, base_name);
878 else if(identifier==
"__func__" ||
879 identifier==
"__FUNCTION__" ||
880 identifier==
"__PRETTY_FUNCTION__")
886 s.
set(ID_C_lvalue,
true);
897 expr.
set(ID_C_lvalue,
true);
899 if(expr.
type().
id()==ID_code)
902 tmp.
set(ID_C_implicit,
true);
921 if(last_statement==ID_expression)
927 if(op.
type().
id()==ID_array)
960 if(op.
type().
id() == ID_bool)
968 if(type.
id()==ID_c_bit_field)
971 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
974 else if(type.
id() == ID_bool)
977 error() <<
"sizeof cannot be applied to single bits" <<
eom;
980 else if(type.
id() == ID_empty)
989 (type.
id() == ID_struct_tag &&
991 (type.
id() == ID_union_tag &&
993 (type.
id() == ID_c_enum_tag &&
998 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1005 if(!size_of_opt.has_value())
1012 new_expr = size_of_opt.value();
1015 new_expr.
swap(expr);
1017 expr.
add(ID_C_c_sizeof_type)=type;
1025 decl_block.set_statement(ID_decl_block);
1035 exprt comma_expr(ID_comma, expr.
type());
1037 expr.
swap(comma_expr);
1043 typet argument_type;
1051 argument_type=op_type;
1075 decl_block.set_statement(ID_decl_block);
1087 op.
swap(comma_expr);
1093 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1094 op.
id() != ID_initializer_list)
1102 if(op.
type().
id() == ID_bool)
1107 for(
const auto &c : union_type.components())
1109 if(c.type() == op.
type())
1115 expr.
set(ID_C_lvalue,
true);
1123 <<
"' not found in union" <<
eom;
1130 if(op.
id()==ID_initializer_list)
1139 exprt tmp(ID_compound_literal, expr.
type());
1143 if(op.
id()==ID_array &&
1144 expr.
type().
id()==ID_array &&
1149 expr.
set(ID_C_lvalue,
true);
1154 if(expr_type.
id()==ID_empty)
1160 if(expr_type == op_type)
1165 if(expr_type.
id()==ID_vector)
1168 if(op_type.
id()==ID_vector)
1170 else if(op_type.
id()==ID_signedbv ||
1171 op_type.
id()==ID_unsignedbv)
1178 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1186 else if(op_type.
id()==ID_array)
1191 else if(op_type.
id()==ID_empty)
1193 if(expr_type.
id()!=ID_empty)
1196 error() <<
"type cast from void only permitted to void, but got '"
1201 else if(op_type.
id()==ID_vector)
1208 if((expr_type.
id()==ID_signedbv ||
1209 expr_type.
id()==ID_unsignedbv) &&
1218 <<
"' not permitted" <<
eom;
1225 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1241 if(expr_type.
id()==ID_pointer)
1242 expr.
set(ID_C_lvalue,
true);
1259 const typet &array_type = array_expr.
type();
1263 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1264 array_type.
id() != ID_vector &&
1267 std::swap(array_expr, index_expr);
1275 const typet final_array_type = array_expr.
type();
1277 if(final_array_type.
id()==ID_array ||
1278 final_array_type.
id()==ID_vector)
1282 if(array_expr.
get_bool(ID_C_lvalue))
1283 expr.
set(ID_C_lvalue,
true);
1285 if(final_array_type.
get_bool(ID_C_constant))
1286 expr.
type().
set(ID_C_constant,
true);
1288 else if(final_array_type.
id()==ID_pointer)
1294 std::swap(summands, expr.
operands());
1296 expr.
id(ID_dereference);
1297 expr.
set(ID_C_lvalue,
true);
1303 error() <<
"operator [] must take array/vector or pointer but got '"
1312 if(expr.
op0().
type().
id() == ID_floatbv)
1314 if(expr.
id()==ID_equal)
1315 expr.
id(ID_ieee_float_equal);
1316 else if(expr.
id()==ID_notequal)
1317 expr.
id(ID_ieee_float_notequal);
1330 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1338 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1342 if(o_type0.
id() != ID_array)
1363 if(type0.
id()==ID_pointer)
1365 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1368 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1369 expr.
id()==ID_ge || expr.
id()==ID_gt)
1373 if(type0.
id()==ID_string_constant)
1375 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1382 if(type0.
id()==ID_pointer &&
1389 if(type1.
id()==ID_pointer &&
1409 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1417 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1428 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1431 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1445 if(expr.
id() == ID_notequal)
1446 expr.
id(ID_vector_notequal);
1454 const typet &op0_type = op.type();
1456 if(op0_type.
id() == ID_array)
1461 index_expr.
set(ID_C_lvalue,
true);
1462 op.swap(index_expr);
1464 else if(op0_type.
id() == ID_pointer)
1470 op.swap(deref_expr);
1475 error() <<
"ptrmember operator requires pointer or array type "
1476 "on left hand side, but got '"
1492 if(type.
id()!=ID_struct &&
1493 type.
id()!=ID_union)
1496 error() <<
"member operator requires structure type "
1497 "on left hand side but got '"
1508 error() <<
"member operator got incomplete " << type.
id()
1509 <<
" type on left hand side" <<
eom;
1514 expr.
get(ID_component_name);
1530 error() <<
"member '" << component_name <<
"' not found in '"
1543 expr.
set(ID_C_lvalue,
true);
1546 expr.
type().
set(ID_C_constant,
true);
1551 if(!identifier.
empty())
1552 expr.
set(ID_C_identifier, identifier);
1556 if(access==ID_private)
1559 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1568 assert(operands.size()==3);
1571 const typet o_type0=operands[0].type();
1572 const typet o_type1=operands[1].type();
1573 const typet o_type2=operands[2].type();
1577 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1585 if(operands[1].type().
id()==ID_pointer &&
1586 operands[2].type().
id()!=ID_pointer)
1588 else if(operands[2].type().
id()==ID_pointer &&
1589 operands[1].type().
id()!=ID_pointer)
1592 if(operands[1].type().
id()==ID_pointer &&
1593 operands[2].type().
id()==ID_pointer &&
1594 operands[1].type()!=operands[2].type())
1601 if(operands[1].type().subtype().
id()==ID_empty &&
1605 else if(operands[2].type().subtype().
id()==ID_empty &&
1609 else if(operands[1].type().subtype().
id()!=ID_code ||
1610 operands[2].type().subtype().
id()!=ID_code)
1634 if(operands[1].type().
id()==ID_empty ||
1635 operands[2].type().
id()==ID_empty)
1642 operands[1].type() != operands[2].type() ||
1643 operands[1].type().
id() == ID_array)
1648 if(operands[1].type() == operands[2].type())
1650 expr.
type()=operands[1].type();
1656 if(operands[1].get_bool(ID_C_lvalue) &&
1657 operands[2].get_bool(ID_C_lvalue))
1658 expr.
set(ID_C_lvalue,
true);
1664 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1677 if(operands.size()!=2)
1680 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1686 if_exprt if_expr(operands[0], operands[0], operands[1]);
1701 if(op.
type().
id()==ID_c_bit_field)
1704 error() <<
"cannot take address of a bit field" <<
eom;
1708 if(op.
type().
id() == ID_bool)
1711 error() <<
"cannot take address of a single bit" <<
eom;
1716 if(op.
id()==ID_label)
1729 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1735 tmp.
set(ID_C_implicit,
false);
1740 if(op.
id()==ID_struct ||
1741 op.
id()==ID_union ||
1742 op.
id()==ID_array ||
1743 op.
id()==ID_string_constant)
1751 else if(op.
type().
id()==ID_code)
1758 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1772 if(op_type.
id()==ID_array)
1780 else if(op_type.
id()==ID_pointer)
1788 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1793 expr.
set(ID_C_lvalue,
true);
1804 if(expr.
type().
id()==ID_code)
1807 tmp.
set(ID_C_implicit,
true);
1817 if(statement==ID_preincrement ||
1818 statement==ID_predecrement ||
1819 statement==ID_postincrement ||
1820 statement==ID_postdecrement)
1829 <<
"' not an lvalue" <<
eom;
1840 if(type0.
id() == ID_c_enum_tag)
1846 error() <<
"operator '" << statement <<
"' given incomplete type '"
1855 else if(type0.
id() == ID_c_bit_field)
1860 expr.
type()=underlying_type;
1862 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1871 else if(type0.
id() == ID_pointer)
1879 error() <<
"operator '" << statement <<
"' not defined for type '"
1886 else if(statement==ID_function_call)
1889 else if(statement==ID_statement_expression)
1891 else if(statement==ID_gcc_conditional_expression)
1896 error() <<
"unknown side effect: " << statement <<
eom;
1907 error() <<
"function_call side effect expects two operands" <<
eom;
1916 if(f_op.
id()==ID_symbol)
1920 asm_label_mapt::const_iterator entry=
1923 identifier=entry->second;
1934 identifier ==
"__noop" &&
1948 identifier ==
"__builtin_shuffle" &&
1957 identifier ==
"__builtin_shufflevector" &&
1969 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1972 !parameters.empty(),
1973 "GCC polymorphic built-ins should have at least one parameter");
1978 if(parameters.front().type().id() == ID_pointer)
1980 identifier_with_type =
id2string(identifier) +
"_" +
1982 parameters.front().type().subtype(), *
this);
1986 identifier_with_type =
1990 gcc_polymorphic->set_identifier(identifier_with_type);
1994 for(std::size_t i = 0; i < parameters.size(); ++i)
2001 id2string(identifier_with_type) +
"::" + base_name;
2004 new_symbol.
type = parameters[i].type();
2007 new_symbol.
mode = ID_C;
2009 parameters[i].set_identifier(new_symbol.
name);
2010 parameters[i].set_base_name(new_symbol.
base_name);
2017 new_symbol.
name = identifier_with_type;
2018 new_symbol.
base_name = identifier_with_type;
2020 new_symbol.
type = gcc_polymorphic->type();
2021 new_symbol.
mode = ID_C;
2028 new_symbol.
value = implementation;
2033 f_op = std::move(*gcc_polymorphic);
2045 if(identifier==
"malloc" ||
2046 identifier==
"realloc" ||
2047 identifier==
"reallocf" ||
2048 identifier==
"valloc")
2055 new_symbol.
name=identifier;
2059 new_symbol.
type.
set(ID_C_incomplete,
true);
2067 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2077 if(f_op_type.
id() == ID_mathematical_function)
2079 const auto &mathematical_function_type =
2083 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2086 error() <<
"expected " << mathematical_function_type.domain().size()
2087 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2095 if(p.first.type() != p.second)
2108 expr.
swap(function_application);
2112 if(f_op_type.
id()!=ID_pointer)
2115 error() <<
"expected function/function pointer as argument but got '"
2121 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2128 tmp.
set(ID_C_implicit,
true);
2133 if(f_op.
type().
id()!=ID_code)
2136 error() <<
"expected code as argument" <<
eom;
2159 if(f_op.
id()!=ID_symbol)
2181 error() <<
"same_object expects two operands" <<
eom;
2187 exprt same_object_expr=
2191 return same_object_expr;
2198 error() <<
"get_must expects two operands" <<
eom;
2208 return std::move(get_must_expr);
2215 error() <<
"get_may expects two operands" <<
eom;
2225 return std::move(get_may_expr);
2232 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2241 return same_object_expr;
2248 error() <<
"buffer_size expects one operand" <<
eom;
2258 return buffer_size_expr;
2265 error() <<
"is_zero_string expects one operand" <<
eom;
2273 is_zero_string_expr.
set(ID_C_lvalue,
true);
2276 return std::move(is_zero_string_expr);
2283 error() <<
"zero_string_length expects one operand" <<
eom;
2289 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2291 zero_string_length_expr.
set(ID_C_lvalue,
true);
2294 return zero_string_length_expr;
2301 error() <<
"dynamic_object expects one argument" <<
eom;
2310 return is_dynamic_object_expr;
2317 error() <<
"pointer_offset expects one argument" <<
eom;
2333 error() <<
"object_size expects one operand" <<
eom;
2343 return std::move(object_size_expr);
2350 error() <<
"pointer_object expects one argument" <<
eom;
2361 else if(identifier==
"__builtin_bswap16" ||
2362 identifier==
"__builtin_bswap32" ||
2363 identifier==
"__builtin_bswap64")
2368 error() << identifier <<
" expects one operand" <<
eom;
2378 return std::move(bswap_expr);
2381 identifier ==
"__builtin_rotateleft8" ||
2382 identifier ==
"__builtin_rotateleft16" ||
2383 identifier ==
"__builtin_rotateleft32" ||
2384 identifier ==
"__builtin_rotateleft64" ||
2385 identifier ==
"__builtin_rotateright8" ||
2386 identifier ==
"__builtin_rotateright16" ||
2387 identifier ==
"__builtin_rotateright32" ||
2388 identifier ==
"__builtin_rotateright64")
2394 error() << identifier <<
" expects two operands" <<
eom;
2400 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2401 identifier ==
"__builtin_rotateleft16" ||
2402 identifier ==
"__builtin_rotateleft32" ||
2403 identifier ==
"__builtin_rotateleft64")
2410 return std::move(rotate_expr);
2412 else if(identifier==
"__builtin_nontemporal_load")
2417 error() << identifier <<
" expects one operand" <<
eom;
2426 if(ptr_arg.
type().
id()!=ID_pointer)
2429 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2438 identifier ==
"__builtin_fpclassify" ||
2444 error() << identifier <<
" expects six arguments" <<
eom;
2457 if(fp_value.
type().
id() != ID_floatbv)
2460 error() <<
"non-floating-point argument for " << identifier <<
eom;
2468 const auto &arguments = expr.
arguments();
2487 identifier==
"__builtin_isnan")
2492 error() <<
"isnan expects one operand" <<
eom;
2510 error() <<
"isfinite expects one operand" <<
eom;
2522 identifier==
"__builtin_inf")
2529 return std::move(inf_expr);
2538 return std::move(inff_expr);
2547 return std::move(infl_expr);
2559 error() <<
"abs-functions expect one operand" <<
eom;
2568 return std::move(abs_expr);
2578 error() <<
"fmod-functions expect two operands" <<
eom;
2592 return std::move(fmod_expr);
2602 error() <<
"remainder-functions expect two operands" <<
eom;
2616 return std::move(floatbv_rem_expr);
2623 error() <<
"allocate expects two operands" <<
eom;
2632 return std::move(malloc_expr);
2641 error() << identifier <<
" expects one or two operands" <<
eom;
2648 const auto &pointer_expr = expr.
arguments()[0];
2649 if(pointer_expr.type().id() != ID_pointer)
2652 error() << identifier <<
" expects a pointer as first argument" <<
eom;
2669 if(subtype.id() == ID_empty)
2672 error() << identifier <<
" expects a size when given a void pointer"
2678 if(!size_expr_opt.has_value())
2681 error() << identifier <<
" was given object pointer without size"
2686 size_expr = std::move(size_expr_opt.value());
2696 return std::move(ok_expr);
2705 error() << identifier <<
" expects one operand" <<
eom;
2714 return std::move(old_expr);
2719 identifier==
"__builtin_isinf")
2724 error() << identifier <<
" expects one operand" <<
eom;
2732 if(fp_value.
type().
id() != ID_floatbv)
2735 error() <<
"non-floating-point argument for " << identifier <<
eom;
2744 else if(identifier ==
"__builtin_isinf_sign")
2749 error() << identifier <<
" expects one operand" <<
eom;
2759 if(fp_value.
type().
id() != ID_floatbv)
2762 error() <<
"non-floating-point argument for " << identifier <<
eom;
2780 identifier ==
"__builtin_isnormal")
2785 error() << identifier <<
" expects one operand" <<
eom;
2793 if(fp_value.
type().
id() != ID_floatbv)
2796 error() <<
"non-floating-point argument for " << identifier <<
eom;
2808 identifier==
"__builtin_signbit" ||
2809 identifier==
"__builtin_signbitf" ||
2810 identifier==
"__builtin_signbitl")
2815 error() << identifier <<
" expects one operand" <<
eom;
2826 else if(identifier==
"__builtin_popcount" ||
2827 identifier==
"__builtin_popcountl" ||
2828 identifier==
"__builtin_popcountll" ||
2829 identifier==
"__popcnt16" ||
2830 identifier==
"__popcnt" ||
2831 identifier==
"__popcnt64")
2836 error() << identifier <<
" expects one operand" <<
eom;
2845 return std::move(popcount_expr);
2848 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2849 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2850 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2855 error() << identifier <<
" expects one operand" <<
eom;
2866 return std::move(clz);
2869 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
2870 identifier ==
"__builtin_ctzll")
2875 error() << identifier <<
" expects one operand" <<
eom;
2885 return std::move(ctz);
2892 error() <<
"equal expects two operands" <<
eom;
2905 error() <<
"equal expects two operands of same type" <<
eom;
2909 return std::move(equality_expr);
2911 else if(identifier==
"__builtin_expect")
2922 error() <<
"__builtin_expect expects two arguments" <<
eom;
2930 else if(identifier==
"__builtin_object_size")
2939 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2956 error() <<
"__builtin_object_size expects constant as second argument, "
2964 if(arg1==0 || arg1==1)
2977 else if(identifier==
"__builtin_choose_expr")
2983 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2998 else if(identifier==
"__builtin_constant_p")
3005 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3021 tmp1.
id() == ID_typecast &&
3027 .
id() == ID_string_constant)
3039 else if(identifier==
"__builtin_classify_type")
3046 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3059 if(type.
id() == ID_c_bit_field)
3062 unsigned type_number;
3064 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3075 type.
id() == ID_empty
3077 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
3079 : (type.
id() == ID_pointer || type.
id() == ID_array)
3081 : type.
id() == ID_floatbv
3083 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
3085 : type.
id() == ID_struct
3087 : type.
id() == ID_union
3108 overflow.
id(ID_minus);
3113 overflow.id(ID_mult);
3118 overflow.id(ID_plus);
3123 overflow.id(ID_shl);
3128 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
3129 of.add_source_location() = overflow.source_location();
3130 return std::move(of);
3140 overflow.add_source_location() = tmp.source_location();
3141 return std::move(overflow);
3148 std::ostringstream error_message;
3150 <<
" takes exactly 1 argument, but "
3151 << expr.
arguments().size() <<
" were provided";
3159 std::ostringstream error_message;
3161 <<
" expects enum, but (" <<
expr2c(arg1, *
this)
3162 <<
") has type `" <<
type2c(arg1.type(), *
this) <<
'`';
3171 identifier ==
"__builtin_add_overflow" ||
3172 identifier ==
"__builtin_sub_overflow" ||
3173 identifier ==
"__builtin_mul_overflow" ||
3174 identifier ==
"__builtin_add_overflow_p" ||
3175 identifier ==
"__builtin_sub_overflow_p" ||
3176 identifier ==
"__builtin_mul_overflow_p")
3181 std::ostringstream error_message;
3183 <<
" takes exactly 3 arguments, but "
3184 << expr.
arguments().size() <<
" were provided";
3197 auto const raise_wrong_argument_error =
3199 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3200 std::ostringstream error_message;
3202 << identifier <<
" has signature " << identifier
3203 <<
"(integral, integral, integral" << (_p ?
"" :
"*")
3205 <<
"but argument " << argument_number <<
" ("
3206 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3207 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3210 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3212 auto const &argument = expr.
arguments()[arg_index];
3216 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3221 (
result.type().id() != ID_pointer ||
3224 raise_wrong_argument_error(
result, 3, is__p_variant);
3257 if(code_type.
get_bool(ID_C_incomplete))
3261 else if(code_type.
is_KnR())
3266 while(parameter_types.size()>arguments.size())
3271 if(parameter_types.size()>arguments.size())
3274 error() <<
"not enough function arguments" <<
eom;
3278 else if(parameter_types.size()!=arguments.size())
3281 error() <<
"wrong number of function arguments: "
3282 <<
"expected " << parameter_types.size()
3283 <<
", but got " << arguments.size() <<
eom;
3287 for(std::size_t i=0; i<arguments.size(); i++)
3289 exprt &op=arguments[i];
3295 else if(i<parameter_types.size())
3300 const typet &op_type=parameter_type.
type();
3302 if(op_type.
id()==ID_bool &&
3303 op.
id()==ID_side_effect &&
3304 op.
get(ID_statement)==ID_assign &&
3308 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3317 if(op.
type().
id() == ID_array)
3320 dest_type.
subtype().
set(ID_C_constant,
true);
3338 if(o_type.
id()==ID_vector)
3357 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3381 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3382 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3391 if((type0.
subtype().
id()==ID_signedbv ||
3411 if(o_type0.
id()==ID_vector &&
3412 o_type1.
id()==ID_vector)
3426 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3431 expr.
type() = o_type0;
3435 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3440 expr.
type() = o_type1;
3451 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3452 expr.
id()==ID_mult || expr.
id()==ID_div)
3454 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3459 else if(type0==type1)
3468 else if(expr.
id()==ID_mod)
3472 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3480 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3481 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3490 else if(type0.
id()==ID_bool)
3492 if(expr.
id()==ID_bitand)
3494 else if(expr.
id() == ID_bitnand)
3496 else if(expr.
id()==ID_bitor)
3498 else if(expr.
id()==ID_bitxor)
3509 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3517 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3525 if(o_type0.
id()==ID_vector &&
3526 o_type1.
id()==ID_vector)
3557 if(expr.
id()==ID_shr)
3561 if(op0_type.
id()==ID_unsignedbv)
3566 else if(op0_type.
id()==ID_signedbv)
3577 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3586 assert(type.
id()==ID_pointer);
3591 subtype.
id() == ID_struct_tag &&
3595 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3599 subtype.
id() == ID_union_tag &&
3603 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3617 if(expr.
id()==ID_minus ||
3618 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3620 if(type0.
id()==ID_pointer &&
3621 type1.
id()==ID_pointer)
3631 if(type0.
id()==ID_pointer &&
3632 (type1.
id()==ID_bool ||
3633 type1.
id()==ID_c_bool ||
3634 type1.
id()==ID_unsignedbv ||
3635 type1.
id()==ID_signedbv ||
3636 type1.
id()==ID_c_bit_field ||
3637 type1.
id()==ID_c_enum_tag))
3645 else if(expr.
id()==ID_plus ||
3646 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3648 exprt *p_op, *int_op;
3650 if(type0.
id()==ID_pointer)
3655 else if(type1.
id()==ID_pointer)
3662 p_op=int_op=
nullptr;
3666 const typet &int_op_type = int_op->
type();
3668 if(int_op_type.
id()==ID_bool ||
3669 int_op_type.
id()==ID_c_bool ||
3670 int_op_type.
id()==ID_unsignedbv ||
3671 int_op_type.
id()==ID_signedbv ||
3672 int_op_type.
id()==ID_c_bit_field ||
3673 int_op_type.
id()==ID_c_enum_tag)
3684 if(expr.
id()==ID_side_effect)
3690 error() <<
"operator '" << op_name <<
"' not defined for types '"
3721 if(type0.
id()==ID_empty)
3724 error() <<
"cannot assign void" <<
eom;
3731 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3744 if(type0.
id() == ID_array)
3747 error() <<
"direct assignments to arrays not permitted" <<
eom;
3754 if(op0.
type().
id()==ID_c_bit_field)
3760 expr.
type()=o_type0;
3762 if(statement==ID_assign)
3767 else if(statement==ID_assign_shl ||
3768 statement==ID_assign_shr)
3770 if(o_type0.
id() == ID_vector)
3790 if(statement==ID_assign_shl)
3800 if(underlying_type.
id()==ID_unsignedbv ||
3801 underlying_type.
id()==ID_c_bool)
3803 expr.
set(ID_statement, ID_assign_lshr);
3806 else if(underlying_type.
id()==ID_signedbv)
3808 expr.
set(ID_statement, ID_assign_ashr);
3814 else if(statement==ID_assign_bitxor ||
3815 statement==ID_assign_bitand ||
3816 statement==ID_assign_bitor)
3819 if(o_type0.
id()==ID_bool ||
3820 o_type0.
id()==ID_c_bool)
3824 op1.
type().
id() == ID_bool || op1.
type().
id() == ID_c_bool ||
3825 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3826 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3831 else if(o_type0.
id()==ID_c_enum_tag ||
3832 o_type0.
id()==ID_unsignedbv ||
3833 o_type0.
id()==ID_signedbv ||
3834 o_type0.
id()==ID_c_bit_field)
3838 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3839 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3844 else if(o_type0.
id()==ID_vector &&
3845 o_type1.
id()==ID_vector)
3856 o_type0.
id() == ID_vector &&
3857 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
3858 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
3859 o_type1.
id() == ID_signedbv))
3868 if(o_type0.
id()==ID_pointer &&
3869 (statement==ID_assign_minus || statement==ID_assign_plus))
3874 else if(o_type0.
id()==ID_vector &&
3875 o_type1.
id()==ID_vector)
3885 else if(o_type0.
id() == ID_vector)
3891 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
3897 else if(o_type0.
id()==ID_bool ||
3898 o_type0.
id()==ID_c_bool)
3901 if(op1.
type().
id()==ID_bool ||
3902 op1.
type().
id()==ID_c_bool ||
3903 op1.
type().
id()==ID_c_enum_tag ||
3904 op1.
type().
id()==ID_unsignedbv ||
3905 op1.
type().
id()==ID_signedbv)
3913 op1.
type().
id()==ID_bool ||
3914 op1.
type().
id()==ID_c_bool ||
3915 op1.
type().
id()==ID_c_enum_tag)
3921 error() <<
"assignment '" << statement <<
"' not defined for types '"
3933 const auto rounding_mode =
3940 expr.
id()!=ID_infinity)
3943 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3956 expr.
id()!=ID_infinity)
3959 error() <<
"conversion to integer constant failed" <<
eom;
3967 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 floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_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()
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Operator to return the address of an object.
const declaratorst & declarators() const
const exprt & size() 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.
std::size_t get_width() const
The byte swap expression.
bool is_incomplete() const
enum types may be incomplete
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)
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 typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
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...
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
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
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()
constant_exprt to_expr() const
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.
irept & add(const irep_namet &name)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_namet &name, const irep_idt &value)
bool get_bool(const irep_namet &name) const
const irep_idt & id() const
void remove(const irep_namet &name)
const irep_idt & get(const irep_namet &name) const
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
mstreamt & warning() const
mstreamt & result() const
message_handlert & get_message_handler()
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.
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
The plus expression Associativity is not specified.
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.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
bool is_incomplete() const
A struct/union may be incomplete.
const componentst & components() const
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.
irep_idt base_name
Base (non-scoped) name.
const irep_idt & display_name() const
Return language specific display name if present.
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.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Type with multiple subtypes.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
source_locationt & add_source_location()
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 type2c(const typet &type, const namespacet &ns)
std::string expr2c(const exprt &expr, const namespacet &ns)
#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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< 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)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#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)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const codet & to_code(const exprt &expr)
const code_declt & to_code_decl(const codet &code)
const code_blockt & to_code_block(const codet &code)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
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 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 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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_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 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.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
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.