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)
119 else if(type2.
id()==ID_c_enum)
124 else if(type1.
id()==ID_pointer &&
125 type2.
id()==ID_pointer)
130 else if(type1.
id()==ID_array &&
131 type2.
id()==ID_array)
137 else if(type1.
id()==ID_code &&
151 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
167 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
177 if(expr.
id()==ID_side_effect)
181 else if(expr.
id()==ID_infinity)
185 else if(expr.
id()==ID_symbol)
187 else if(expr.
id()==ID_unary_plus ||
188 expr.
id()==ID_unary_minus ||
189 expr.
id()==ID_bitnot)
191 else if(expr.
id()==ID_not)
194 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
197 else if(expr.
id()==ID_address_of)
199 else if(expr.
id()==ID_dereference)
201 else if(expr.
id()==ID_member)
203 else if(expr.
id()==ID_ptrmember)
205 else if(expr.
id()==ID_equal ||
206 expr.
id()==ID_notequal ||
212 else if(expr.
id()==ID_index)
214 else if(expr.
id()==ID_typecast)
216 else if(expr.
id()==ID_sizeof)
218 else if(expr.
id()==ID_alignof)
221 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
222 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
223 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
227 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
229 else if(expr.
id()==ID_comma)
231 else if(expr.
id()==ID_if)
233 else if(expr.
id()==ID_code)
236 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
239 else if(expr.
id()==ID_gcc_builtin_va_arg)
241 else if(expr.
id()==ID_cw_va_arg_typeof)
243 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
254 subtypes[0].
remove(ID_C_constant);
255 subtypes[0].remove(ID_C_volatile);
256 subtypes[0].remove(ID_C_restricted);
257 subtypes[1].remove(ID_C_constant);
258 subtypes[1].remove(ID_C_volatile);
259 subtypes[1].remove(ID_C_restricted);
264 else if(expr.
id()==ID_clang_builtin_convertvector)
273 else if(expr.
id()==ID_builtin_offsetof)
275 else if(expr.
id()==ID_string_constant)
278 expr.
set(ID_C_lvalue,
true);
280 else if(expr.
id()==ID_arguments)
284 else if(expr.
id()==ID_designated_initializer)
286 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
290 if(it->id()==ID_index)
294 else if(expr.
id()==ID_initializer_list)
300 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
306 auto &bindings = binary_expr.op0().operands();
307 auto &where = binary_expr.op1();
309 for(
const auto &binding : bindings)
311 if(binding.get(ID_statement) != ID_decl)
314 error() <<
"expected declaration as operand of quantifier" <<
eom;
321 [&](
const exprt &subexpr)
328 error() <<
"quantifier must not contain function calls" <<
eom;
333 for(
auto &binding : bindings)
336 if(expr.
id() == ID_lambda)
340 for(
auto &binding : bindings)
341 domain.push_back(binding.type());
351 else if(expr.
id()==ID_label)
355 else if(expr.
id()==ID_array)
359 else if(expr.
id()==ID_complex)
364 else if(expr.
id() == ID_complex_real)
368 if(op.
type().
id() != ID_complex)
373 error() <<
"real part retrieval expects numerical operand, "
381 expr.
swap(complex_real_expr);
389 complex_real_expr.
set(ID_C_lvalue,
true);
392 complex_real_expr.
type().
set(ID_C_constant,
true);
394 expr.
swap(complex_real_expr);
397 else if(expr.
id() == ID_complex_imag)
401 if(op.
type().
id() != ID_complex)
406 error() <<
"real part retrieval expects numerical operand, "
414 expr.
swap(complex_imag_expr);
422 complex_imag_expr.
set(ID_C_lvalue,
true);
425 complex_imag_expr.
type().
set(ID_C_constant,
true);
427 expr.
swap(complex_imag_expr);
430 else if(expr.
id()==ID_generic_selection)
447 for(
auto &irep : generic_associations)
449 if(irep.get(ID_type_arg) != ID_default)
451 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
460 const typet &op_type = op.type();
462 for(
const auto &irep : generic_associations)
464 if(irep.get(ID_type_arg) == ID_default)
465 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
466 else if(op_type ==
static_cast<const typet &
>(irep.find(ID_type_arg)))
468 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
475 expr.
swap(default_match);
479 error() <<
"unmatched generic selection: " <<
to_string(op.type())
485 expr.
swap(assoc_match);
490 else if(expr.
id()==ID_gcc_asm_input ||
491 expr.
id()==ID_gcc_asm_output ||
492 expr.
id()==ID_gcc_asm_clobbered_register)
495 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
496 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
501 expr.
id() == ID_C_spec_assigns || expr.
id() == ID_C_spec_frees ||
502 expr.
id() == ID_target_list)
513 exprt tmp = bit_cast_expr->lower();
519 error() <<
"bit cast from '" <<
to_string(bit_cast_expr->op().type())
538 expr.
set(ID_C_lvalue,
true);
546 auto type_not_permitted = [
this](
const exprt &expr)
551 <<
"' not permitted for va_arg" <<
eom;
561 if(components.size() != 5)
562 type_not_permitted(expr);
564 else if(arg.
type().
id() != ID_pointer && arg.
type().
id() != ID_array)
565 type_not_permitted(expr);
589 symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C};
619 error() <<
"builtin_offsetof expects no operands" <<
eom;
626 const exprt &member =
static_cast<const exprt &
>(expr.
add(ID_designator));
630 for(
const auto &op : member.
operands())
632 if(op.id() == ID_member)
634 if(type.
id() != ID_union_tag && type.
id() != ID_struct_tag)
637 error() <<
"offsetof of member expects struct/union type, "
643 irep_idt component_name = op.get(ID_component_name);
657 if(type.
id() == ID_struct_tag)
662 if(!o_opt.has_value())
665 error() <<
"offsetof failed to determine offset of '"
666 << component_name <<
"'" <<
eom;
682 for(
const auto &c : struct_union_type.
components())
686 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
690 if(type.
id() == ID_struct_tag)
695 if(!o_opt.has_value())
698 error() <<
"offsetof failed to determine offset of '"
699 << component_name <<
"'" <<
eom;
709 typet tmp = c.type();
712 type.
id() == ID_union_tag || type.
id() == ID_struct_tag);
722 error() <<
"offset-of of member failed to find component '"
723 << component_name <<
"' in '" <<
to_string(type) <<
"'"
730 else if(op.id() == ID_index)
732 if(type.
id()!=ID_array)
735 error() <<
"offsetof of index expects array type" <<
eom;
744 auto element_size_opt =
747 if(!element_size_opt.has_value())
750 error() <<
"offsetof failed to determine array element size" <<
eom;
773 if(expr.
id()==ID_side_effect &&
774 expr.
get(ID_statement)==ID_function_call)
779 else if(expr.
id()==ID_side_effect &&
780 expr.
get(ID_statement)==ID_statement_expression)
785 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
791 auto &bindings = binary_expr.op0().operands();
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;
820 const symbolt &symbol = s_it->second;
827 error() <<
"unexpected quantified symbol" <<
eom;
851 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
855 expr.
type()=p_it->second;
856 expr.
set(ID_C_lvalue,
true);
861 asm_label_mapt::const_iterator entry=
865 identifier=entry->second;
871 if(
lookup(identifier, symbol_ptr))
874 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
878 const symbolt &symbol=*symbol_ptr;
883 error() <<
"did not expect a type symbol here, but got '"
902 expr.
set(ID_C_cformat, base_name);
917 else if(identifier==
"__func__" ||
918 identifier==
"__FUNCTION__" ||
919 identifier==
"__PRETTY_FUNCTION__")
925 s.
set(ID_C_lvalue,
true);
936 expr.
set(ID_C_lvalue,
true);
938 if(expr.
type().
id()==ID_code)
941 tmp.
set(ID_C_implicit,
true);
960 if(last_statement==ID_expression)
966 if(op.
type().
id()==ID_array)
1008 if(type.
id()==ID_c_bit_field)
1012 if(op.
id() == ID_comma || op.
id() == ID_side_effect)
1019 config.ansi_c.char_width,
1026 if(!size_of_opt.has_value())
1029 error() <<
"type has no size: "
1034 new_expr = size_of_opt.value();
1040 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
1044 else if(type.
id() == ID_bool)
1047 error() <<
"sizeof cannot be applied to single bits" <<
eom;
1050 else if(type.
id() == ID_empty)
1059 (type.
id() == ID_struct_tag &&
1061 (type.
id() == ID_union_tag &&
1063 (type.
id() == ID_c_enum_tag &&
1068 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1075 if(!size_of_opt.has_value())
1082 new_expr = size_of_opt.value();
1086 new_expr.
swap(expr);
1088 expr.
add(ID_C_c_sizeof_type)=type;
1094 ID_statement_expression,
void_type(), location);
1096 decl_block.set_statement(ID_decl_block);
1109 expr.
swap(comma_expr);
1115 typet argument_type;
1123 argument_type=op_type;
1147 decl_block.set_statement(ID_decl_block);
1158 std::move(side_effect_expr), ID_comma, op, op.
type()};
1159 op.
swap(comma_expr);
1165 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1166 op.
id() != ID_initializer_list)
1179 for(
const auto &c : union_type.components())
1181 if(c.type() == op.
type())
1187 expr.
set(ID_C_lvalue,
true);
1195 <<
"' not found in union" <<
eom;
1202 if(op.
id()==ID_initializer_list)
1211 exprt tmp(ID_compound_literal, expr.
type());
1215 if(op.
id()==ID_array &&
1216 expr.
type().
id()==ID_array &&
1221 expr.
set(ID_C_lvalue,
true);
1226 if(expr_type.
id()==ID_empty)
1232 if(expr_type == op_type)
1237 if(expr_type.
id()==ID_vector)
1240 if(op_type.
id()==ID_vector)
1242 else if(op_type.
id()==ID_signedbv ||
1243 op_type.
id()==ID_unsignedbv)
1250 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1258 else if(op_type.
id()==ID_array)
1263 if(error_opt.has_value())
1269 else if(op_type.
id()==ID_empty)
1271 if(expr_type.
id()!=ID_empty)
1274 error() <<
"type cast from void only permitted to void, but got '"
1279 else if(op_type.
id()==ID_vector)
1286 if((expr_type.
id()==ID_signedbv ||
1287 expr_type.
id()==ID_unsignedbv) &&
1296 <<
"' not permitted" <<
eom;
1303 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1319 if(expr_type.
id()==ID_pointer)
1320 expr.
set(ID_C_lvalue,
true);
1337 const typet &array_type = array_expr.
type();
1338 const typet &index_type = index_expr.
type();
1341 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1342 array_type.
id() != ID_vector &&
1343 (index_type.
id() == ID_array || index_type.
id() == ID_pointer ||
1344 index_type.
id() == ID_vector))
1345 std::swap(array_expr, index_expr);
1353 const typet final_array_type = array_expr.
type();
1355 if(final_array_type.
id()==ID_array ||
1356 final_array_type.
id()==ID_vector)
1360 if(array_expr.
get_bool(ID_C_lvalue))
1361 expr.
set(ID_C_lvalue,
true);
1363 if(final_array_type.
get_bool(ID_C_constant))
1364 expr.
type().
set(ID_C_constant,
true);
1366 else if(final_array_type.
id()==ID_pointer)
1372 std::swap(summands, expr.
operands());
1374 expr.
id(ID_dereference);
1375 expr.
set(ID_C_lvalue,
true);
1381 error() <<
"operator [] must take array/vector or pointer but got '"
1390 if(expr.
op0().
type().
id() == ID_floatbv)
1392 if(expr.
id()==ID_equal)
1393 expr.
id(ID_ieee_float_equal);
1394 else if(expr.
id()==ID_notequal)
1395 expr.
id(ID_ieee_float_notequal);
1408 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1416 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1418 if(o_type0 == o_type1)
1420 if(o_type0.
id() != ID_array)
1441 if(type0.
id()==ID_pointer)
1443 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1446 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1447 expr.
id()==ID_ge || expr.
id()==ID_gt)
1451 if(type0.
id()==ID_string_constant)
1453 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1460 if(type0.
id()==ID_pointer &&
1467 if(type1.
id()==ID_pointer &&
1487 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1495 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1506 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1509 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1517 auto subtype_width =
1526 if(expr.
id() == ID_notequal)
1527 expr.
id(ID_vector_notequal);
1535 const typet &op0_type = op.type();
1537 if(op0_type.
id() == ID_array)
1542 index_expr.
set(ID_C_lvalue,
true);
1543 op.swap(index_expr);
1545 else if(op0_type.
id() == ID_pointer)
1556 error() <<
"ptrmember operator requires pointer or array type "
1557 "on left hand side, but got '"
1571 if(type.
id() != ID_struct_tag && type.
id() != ID_union_tag)
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;
1592 expr.
get(ID_component_name);
1608 error() <<
"member '" << component_name <<
"' not found in '"
1621 expr.
set(ID_C_lvalue,
true);
1625 struct_union_type.
get_bool(ID_C_constant))
1627 expr.
type().
set(ID_C_constant,
true);
1633 if(!identifier.
empty())
1634 expr.
set(ID_C_identifier, identifier);
1638 if(access==ID_private)
1641 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1653 const typet o_type0=operands[0].type();
1654 const typet o_type1=operands[1].type();
1655 const typet o_type2=operands[2].type();
1659 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1679 if(operands[1].type().
id()==ID_pointer &&
1680 operands[2].type().
id()!=ID_pointer)
1682 else if(operands[2].type().
id()==ID_pointer &&
1683 operands[1].type().
id()!=ID_pointer)
1686 if(operands[1].type().
id()==ID_pointer &&
1687 operands[2].type().
id()==ID_pointer &&
1688 operands[1].type()!=operands[2].type())
1735 if(operands[1].type().
id()==ID_empty ||
1736 operands[2].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();
1757 if(operands[1].get_bool(ID_C_lvalue) &&
1758 operands[2].get_bool(ID_C_lvalue))
1759 expr.
set(ID_C_lvalue,
true);
1765 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1778 if(operands.size()!=2)
1781 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1787 if_exprt if_expr(operands[0], operands[0], operands[1]);
1804 if(error_opt.has_value())
1808 if(op.
id()==ID_label)
1821 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1827 tmp.
set(ID_C_implicit,
false);
1832 if(op.
id()==ID_struct ||
1833 op.
id()==ID_union ||
1834 op.
id()==ID_array ||
1835 op.
id()==ID_string_constant)
1843 else if(op.
type().
id()==ID_code)
1850 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1864 if(op_type.
id()==ID_array)
1872 else if(op_type.
id()==ID_pointer)
1877 expr.
type().
id() == ID_empty &&
1881 error() <<
"dereferencing void pointer" <<
eom;
1889 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1894 expr.
set(ID_C_lvalue,
true);
1905 if(expr.
type().
id()==ID_code)
1908 tmp.
set(ID_C_implicit,
true);
1918 if(statement==ID_preincrement ||
1919 statement==ID_predecrement ||
1920 statement==ID_postincrement ||
1921 statement==ID_postdecrement)
1930 <<
"' not an lvalue" <<
eom;
1941 if(type0.
id() == ID_c_enum_tag)
1947 error() <<
"operator '" << statement <<
"' given incomplete type '"
1957 else if(type0.
id() == ID_c_bit_field)
1961 typet type_before{type0};
1963 expr.
type()=underlying_type;
1967 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1976 else if(type0.
id() == ID_pointer)
1984 error() <<
"operator '" << statement <<
"' not defined for type '"
1991 else if(statement==ID_function_call)
1994 else if(statement==ID_statement_expression)
1996 else if(statement==ID_gcc_conditional_expression)
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());
2052 if(arg0.type().id() == ID_pointer)
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()),
2080 auto &function_pointer = expr.
arguments()[0];
2083 function_pointer.type().id() != ID_pointer ||
2084 to_pointer_type(function_pointer.type()).base_type().id() != ID_code ||
2085 !function_pointer.get_bool(ID_C_lvalue))
2089 "obeys_contract must be a function pointer lvalue expression",
2090 function_pointer.source_location());
2097 "obeys_contract must have no ternary operator",
2098 function_pointer.source_location());
2102 auto &address_of_contract = expr.
arguments()[1];
2105 address_of_contract.id() != ID_address_of ||
2107 address_of_contract.type().id() != ID_pointer ||
2108 to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
2112 "obeys_contract must must be a function symbol",
2113 address_of_contract.source_location());
2116 if(function_pointer.type() != address_of_contract.type())
2120 "obeys_contract must have the same function pointer type",
2129 return ::builtin_factory(
2131 config.ansi_c.float16_type,
2142 error() <<
"function_call side effect expects two operands" <<
eom;
2151 if(f_op.
id()==ID_symbol)
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;
2235 expr.
swap(equality_expr);
2249 overflow.
id(ID_minus);
2254 overflow.
id(ID_mult);
2259 overflow.
id(ID_plus);
2264 overflow.
id(ID_shl);
2283 expr.
swap(overflow);
2291 std::ostringstream error_message;
2292 error_message << identifier <<
" takes exactly 1 argument, but "
2293 << expr.
arguments().size() <<
" were provided";
2301 std::ostringstream error_message;
2302 error_message << identifier <<
" expects enum, but ("
2303 <<
expr2c(arg1, *
this) <<
") has type `"
2304 <<
type2c(arg1.type(), *
this) <<
'`';
2323 id2string(identifier) +
" expects one or two operands",
2328 auto &pointer_expr = expr.
arguments()[0];
2329 if(pointer_expr.type().id() == ID_array)
2332 dest_type.base_type().set(ID_C_constant,
true);
2335 else if(pointer_expr.type().id() != ID_pointer)
2338 id2string(identifier) +
" expects a pointer as first argument",
2354 const auto &subtype =
2356 if(subtype.id() == ID_empty)
2360 " expects a size when given a void pointer",
2366 size_expr = std::move(size_expr_opt.value());
2382 irep_idt shadow_memory_builtin_id =
2383 shadow_memory_builtin->get_identifier();
2385 const auto builtin_code_type =
2389 builtin_code_type.has_ellipsis() &&
2390 builtin_code_type.parameters().empty(),
2391 "Shadow memory builtins should be an ellipsis with 0 parameter");
2397 shadow_memory_builtin_id, shadow_memory_builtin->type(), ID_C};
2398 new_symbol.
base_name = shadow_memory_builtin_id;
2409 f_op = std::move(*shadow_memory_builtin);
2415 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2418 !parameters.empty(),
2419 "GCC polymorphic built-ins should have at least one parameter");
2424 if(parameters.front().type().id() == ID_pointer)
2426 identifier_with_type =
2433 identifier_with_type =
2437 gcc_polymorphic->set_identifier(identifier_with_type);
2441 for(std::size_t i = 0; i < parameters.size(); ++i)
2443 const std::string base_name =
"p_" + std::to_string(i);
2448 id2string(identifier_with_type) +
"::" + base_name;
2451 new_symbol.
type = parameters[i].type();
2454 new_symbol.
mode = ID_C;
2456 parameters[i].set_identifier(new_symbol.
name);
2457 parameters[i].set_base_name(new_symbol.
base_name);
2463 identifier_with_type, gcc_polymorphic->type(), ID_C};
2464 new_symbol.
base_name = identifier_with_type;
2472 new_symbol.
value = implementation;
2477 f_op = std::move(*gcc_polymorphic);
2489 if(identifier==
"malloc" ||
2490 identifier==
"realloc" ||
2491 identifier==
"reallocf" ||
2492 identifier==
"valloc")
2501 new_symbol.
type.
set(ID_C_incomplete,
true);
2513 debug() <<
"builtin '" << identifier <<
"' is unknown" <<
eom;
2518 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2529 if(f_op_type.
id() == ID_mathematical_function)
2531 const auto &mathematical_function_type =
2535 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2538 error() <<
"expected " << mathematical_function_type.domain().size()
2539 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2547 if(p.first.type() != p.second)
2560 expr.
swap(function_application);
2564 if(f_op_type.
id()!=ID_pointer)
2567 error() <<
"expected function/function pointer as argument but got '"
2573 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2580 tmp.
set(ID_C_implicit,
true);
2585 if(f_op.
type().
id()!=ID_code)
2588 error() <<
"expected code as argument" <<
eom;
2611 if(f_op.
id()!=ID_symbol)
2659 if(arg.type().id() != ID_pointer)
2663 "pointer_in_range_dfcc expects pointer-typed arguments",
2664 arg.source_location()};
2674 error() <<
"same_object expects two operands" <<
eom;
2680 exprt same_object_expr=
2684 return same_object_expr;
2691 error() <<
"get_must expects two operands" <<
eom;
2701 return std::move(get_must_expr);
2708 error() <<
"get_may expects two operands" <<
eom;
2718 return std::move(get_may_expr);
2725 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2734 return same_object_expr;
2741 error() <<
"buffer_size expects one operand" <<
eom;
2751 return buffer_size_expr;
2759 error() <<
"is_list expects one operand" <<
eom;
2766 expr.
arguments()[0].type().id() != ID_pointer ||
2771 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2779 return std::move(is_list_expr);
2787 error() <<
"is_dll expects one operand" <<
eom;
2794 expr.
arguments()[0].type().id() != ID_pointer ||
2799 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2807 return std::move(is_dll_expr);
2815 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2822 expr.
arguments()[0].type().id() != ID_pointer ||
2827 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2835 return std::move(is_cyclic_dll_expr);
2843 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2850 args_no_cast.reserve(expr.
arguments().size());
2851 for(
const auto &argument : expr.
arguments())
2855 args_no_cast.back().type().id() != ID_pointer ||
2860 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2867 is_sentinel_dll_expr.
operands() = args_no_cast;
2870 return std::move(is_sentinel_dll_expr);
2878 error() <<
"is_cstring expects one operand" <<
eom;
2884 if(expr.
arguments()[0].type().id() != ID_pointer)
2887 error() <<
"is_cstring expects a pointer operand" <<
eom;
2894 return std::move(is_cstring_expr);
2902 error() <<
"cstrlen expects one operand" <<
eom;
2908 if(expr.
arguments()[0].type().id() != ID_pointer)
2911 error() <<
"cstrlen expects a pointer operand" <<
eom;
2918 return std::move(cstrlen_expr);
2925 error() <<
"is_zero_string expects one operand" <<
eom;
2933 is_zero_string_expr.
set(ID_C_lvalue,
true);
2936 return std::move(is_zero_string_expr);
2943 error() <<
"zero_string_length expects one operand" <<
eom;
2949 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2951 zero_string_length_expr.
set(ID_C_lvalue,
true);
2954 return zero_string_length_expr;
2961 error() <<
"dynamic_object expects one argument" <<
eom;
2970 return is_dynamic_object_expr;
2977 error() <<
"live_object expects one argument" <<
eom;
2986 return live_object_expr;
2993 error() <<
"pointer_in_range expects three arguments" <<
eom;
3003 return pointer_in_range_expr;
3010 error() <<
"writeable_object expects one argument" <<
eom;
3019 return writeable_object_expr;
3027 error() <<
"separate expects two or more arguments" <<
eom;
3036 return separate_expr;
3043 error() <<
"pointer_offset expects one argument" <<
eom;
3059 error() <<
"object_size expects one operand" <<
eom;
3068 return std::move(object_size_expr);
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;
3103 return std::move(bswap_expr);
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")
3135 return std::move(rotate_expr);
3137 else if(identifier==
"__builtin_nontemporal_load")
3142 error() << identifier <<
" expects one operand" <<
eom;
3151 if(ptr_arg.
type().
id()!=ID_pointer)
3154 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3163 identifier ==
"__builtin_fpclassify" ||
3169 error() << identifier <<
" expects six arguments" <<
eom;
3182 if(fp_value.
type().
id() != ID_floatbv)
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;
3235 error() <<
"isfinite expects one operand" <<
eom;
3247 identifier==
"__builtin_inf")
3254 return std::move(inf_expr);
3263 return std::move(inff_expr);
3272 return std::move(infl_expr);
3282 error() << identifier <<
" expects two arguments" <<
eom;
3286 auto round_to_integral_expr =
3290 return std::move(round_to_integral_expr);
3303 error() <<
"abs-functions expect one operand" <<
eom;
3312 return std::move(abs_expr);
3322 error() <<
"fmod-functions expect two operands" <<
eom;
3336 return std::move(fmod_expr);
3346 error() <<
"remainder-functions expect two operands" <<
eom;
3360 return std::move(floatbv_rem_expr);
3367 error() <<
"allocate expects two operands" <<
eom;
3376 return std::move(malloc_expr);
3385 error() << identifier <<
" expects one operand" <<
eom;
3389 const auto ¶m_id = expr.
arguments().front().id();
3390 if(!(param_id == ID_dereference || param_id == ID_member ||
3391 param_id == ID_symbol || param_id == ID_ptrmember ||
3392 param_id == ID_constant || param_id == ID_typecast ||
3393 param_id == ID_index))
3396 error() <<
"Tracking history of " << param_id
3397 <<
" expressions is not supported yet." <<
eom;
3406 return std::move(old_expr);
3411 identifier==
"__builtin_isinf")
3416 error() << identifier <<
" expects one operand" <<
eom;
3424 if(fp_value.
type().
id() != ID_floatbv)
3427 error() <<
"non-floating-point argument for " << identifier <<
eom;
3436 else if(identifier ==
"__builtin_isinf_sign")
3441 error() << identifier <<
" expects one operand" <<
eom;
3451 if(fp_value.
type().
id() != ID_floatbv)
3454 error() <<
"non-floating-point argument for " << identifier <<
eom;
3472 identifier ==
"__builtin_isnormal")
3477 error() << identifier <<
" expects one operand" <<
eom;
3485 if(fp_value.
type().
id() != ID_floatbv)
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;
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;
3537 return std::move(popcount_expr);
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;
3557 return std::move(clz);
3560 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3561 identifier ==
"__builtin_ctzll")
3566 error() << identifier <<
" expects one operand" <<
eom;
3576 return std::move(ctz);
3579 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3580 identifier ==
"__builtin_ffsll")
3585 error() << identifier <<
" expects one operand" <<
eom;
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, "
3653 if(arg1==0 || arg1==1)
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;
3710 tmp1.
id() == ID_typecast &&
3716 .
id() == ID_string_constant)
3728 else if(identifier==
"__builtin_classify_type")
3735 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3746 const typet &type =
object.type().
id() == ID_c_bit_field
3750 unsigned type_number;
3752 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3760 type_number = type.
id() == ID_empty ? 0u
3761 : (type.
id() == ID_bool || type.
id() == ID_c_bool) ? 4u
3762 : (type.
id() == ID_pointer || type.
id() == ID_array) ? 5u
3763 : type.
id() == ID_floatbv ? 8u
3764 : (type.
id() == ID_complex &&
3767 : type.
id() == ID_struct_tag ? 12u
3768 : type.
id() == ID_union_tag
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")
3823 std::ostringstream error_message;
3824 error_message <<
"error: " << identifier <<
" expects one operand";
3834 return std::move(bitreverse);
3850 std::ostringstream error_message;
3851 error_message << identifier <<
" takes exactly 3 arguments, but "
3852 << expr.
arguments().size() <<
" were provided";
3866 auto const raise_wrong_argument_error =
3868 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3869 std::ostringstream error_message;
3870 error_message <<
"error: " << identifier <<
" has signature "
3871 << identifier <<
"(integral, integral, integral"
3872 << (_p ?
"" :
"*") <<
"), "
3873 <<
"but argument " << argument_number <<
" ("
3874 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3875 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3879 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3881 auto const &argument = expr.
arguments()[arg_index];
3885 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3889 !is__p_variant && (
result.type().id() != ID_pointer ||
3893 raise_wrong_argument_error(
result, 3, is__p_variant);
3912 std::ostringstream error_message;
3913 error_message <<
"error: " << identifier
3914 <<
" takes exactly two arguments, but "
3915 << expr.
arguments().size() <<
" were provided";
3923 identifier ==
"__builtin_elementwise_sub_sat")
3929 identifier ==
"__builtin_elementwise_add_sat")
3954 if(code_type.
get_bool(ID_C_incomplete))
3958 else if(code_type.
is_KnR())
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())
4000 op.
get(ID_statement) == ID_assign && op.
type().
id() != ID_bool)
4003 warning() <<
"assignment where Boolean argument is expected" <<
eom;
4012 if(op.
type().
id() == ID_array)
4015 dest_type.base_type().set(ID_C_constant,
true);
4033 if(o_type.
id()==ID_vector)
4052 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
4107 if(o_type0.
id()==ID_vector &&
4108 o_type1.
id()==ID_vector)
4122 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
4127 expr.
type() = o_type0;
4131 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
4136 expr.
type() = o_type1;
4140 if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4153 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
4154 expr.
id()==ID_mult || expr.
id()==ID_div)
4156 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
4161 else if(type0==type1)
4170 else if(expr.
id()==ID_mod)
4174 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
4182 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
4183 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
4192 else if(type0.
id()==ID_bool)
4194 if(expr.
id()==ID_bitand)
4196 else if(expr.
id() == ID_bitnand)
4198 else if(expr.
id()==ID_bitor)
4200 else if(expr.
id()==ID_bitxor)
4209 else if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4213 (type0.
id() == ID_signedbv || type0.
id() == ID_unsignedbv))
4215 expr.
type() = type0;
4221 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4237 if(o_type0.
id()==ID_vector &&
4238 o_type1.
id()==ID_vector)
4254 o_type0.
id() == ID_vector &&
4272 if(expr.
id()==ID_shr)
4276 if(op0_type.
id()==ID_unsignedbv)
4281 else if(op0_type.
id()==ID_signedbv)
4292 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4306 base_type.
id() == ID_struct_tag &&
4310 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4314 base_type.
id() == ID_union_tag &&
4318 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4322 base_type.
id() == ID_empty &&
4326 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4329 else if(base_type.
id() == ID_empty)
4347 if(expr.
id()==ID_minus ||
4348 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
4350 if(type0.
id()==ID_pointer &&
4351 type1.
id()==ID_pointer)
4364 if(type0.
id()==ID_pointer &&
4365 (type1.
id()==ID_bool ||
4366 type1.
id()==ID_c_bool ||
4367 type1.
id()==ID_unsignedbv ||
4368 type1.
id()==ID_signedbv ||
4369 type1.
id()==ID_c_bit_field ||
4370 type1.
id()==ID_c_enum_tag))
4378 else if(expr.
id()==ID_plus ||
4379 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
4381 exprt *p_op, *int_op;
4383 if(type0.
id()==ID_pointer)
4388 else if(type1.
id()==ID_pointer)
4395 p_op=int_op=
nullptr;
4399 const typet &int_op_type = int_op->
type();
4401 if(int_op_type.
id()==ID_bool ||
4402 int_op_type.
id()==ID_c_bool ||
4403 int_op_type.
id()==ID_unsignedbv ||
4404 int_op_type.
id()==ID_signedbv ||
4405 int_op_type.
id()==ID_c_bit_field ||
4406 int_op_type.
id()==ID_c_enum_tag)
4417 if(expr.
id()==ID_side_effect)
4423 error() <<
"operator '" << op_name <<
"' not defined for types '"
4454 if(type0.
id()==ID_empty)
4457 error() <<
"cannot assign void" <<
eom;
4464 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4477 if(type0.
id() == ID_array)
4480 error() <<
"direct assignments to arrays not permitted" <<
eom;
4486 if(op0.
type() != op1.
type() && op0.
type().
id() == ID_c_bit_field)
4495 expr.
type()=o_type0;
4497 if(statement==ID_assign)
4502 else if(statement==ID_assign_shl ||
4503 statement==ID_assign_shr)
4505 if(o_type0.
id() == ID_vector)
4510 o_type1.
id() == ID_vector &&
4511 vector_o_type0.element_type() ==
4513 is_number(vector_o_type0.element_type()))
4529 if(statement==ID_assign_shl)
4539 if(underlying_type.
id()==ID_unsignedbv ||
4540 underlying_type.
id()==ID_c_bool)
4542 expr.
set(ID_statement, ID_assign_lshr);
4545 else if(underlying_type.
id()==ID_signedbv)
4547 expr.
set(ID_statement, ID_assign_ashr);
4553 else if(statement==ID_assign_bitxor ||
4554 statement==ID_assign_bitand ||
4555 statement==ID_assign_bitor)
4558 if(o_type0.
id()==ID_bool ||
4559 o_type0.
id()==ID_c_bool)
4564 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4565 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4570 else if(o_type0.
id()==ID_c_enum_tag ||
4571 o_type0.
id()==ID_unsignedbv ||
4572 o_type0.
id()==ID_signedbv ||
4573 o_type0.
id()==ID_c_bit_field)
4577 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4578 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4583 else if(o_type0.
id()==ID_vector &&
4584 o_type1.
id()==ID_vector)
4595 o_type0.
id() == ID_vector &&
4596 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
4597 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
4598 o_type1.
id() == ID_signedbv))
4607 if(o_type0.
id()==ID_pointer &&
4608 (statement==ID_assign_minus || statement==ID_assign_plus))
4613 else if(o_type0.
id()==ID_vector &&
4614 o_type1.
id()==ID_vector)
4624 else if(o_type0.
id() == ID_vector)
4630 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4636 else if(o_type0.
id()==ID_bool ||
4637 o_type0.
id()==ID_c_bool)
4642 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4643 op1.
type().
id() == ID_signedbv)
4654 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4662 error() <<
"assignment '" << statement <<
"' not defined for types '"
4692 if(e.
id() == ID_infinity)
4698 if(e.
id() == ID_address_of)
4703 e.
id() == ID_typecast || e.
id() == ID_array_of || e.
id() == ID_plus ||
4704 e.
id() == ID_mult || e.
id() == ID_array || e.
id() == ID_with ||
4705 e.
id() == ID_struct || e.
id() == ID_union || e.
id() == ID_empty_union ||
4706 e.
id() == ID_equal || e.
id() == ID_notequal || e.
id() == ID_lt ||
4707 e.
id() == ID_le || e.
id() == ID_gt || e.
id() == ID_ge ||
4708 e.
id() == ID_if || e.
id() == ID_not || e.
id() == ID_and ||
4709 e.
id() == ID_or || e.
id() == ID_bitnot || e.
id() == ID_bitand ||
4710 e.
id() == ID_bitor || e.
id() == ID_bitxor || e.
id() == ID_vector)
4714 return is_constant(op);
4724 if(e.
id() == ID_symbol)
4726 return e.
type().
id() == ID_code ||
4729 else if(e.
id() == ID_array && e.
get_bool(ID_C_string_constant))
4731 else if(e.
id() == ID_label)
4733 else if(e.
id() == ID_index)
4740 else if(e.
id() == ID_member)
4744 else if(e.
id() == ID_dereference)
4750 else if(e.
id() == ID_string_constant)
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()
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.
const declaratorst & declarators() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
The byte swap expression.
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
const typet & underlying_type() const
const typet & underlying_type() const
bool is_incomplete() const
enum types may be incomplete
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)
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)
codet & find_last_statement()
A codet representing the declaration of a local variable.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
bool has_ellipsis() 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.
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.
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...
exprt lower(const namespacet &ns) const
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.
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.
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
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()
constant_exprt to_expr() const
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 remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
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)) ∧...
const typet & base_type() const
The type of the data what we point to.
The popcount (counting the number of bits set to 1) expression.
A base class for 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.
const componentst & components() const
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.
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
irep_idt base_name
Base (non-scoped) name.
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.
const irep_idt & display_name() const
Return language specific display name if present.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The Boolean constant true.
Type with multiple subtypes.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
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.
const constant_exprt & size() const
typet index_type() const
The type of any index expression into an instance of this type.
const typet & element_type() const
The type of the elements of the vector.
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)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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)