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);
573 symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C};
603 error() <<
"builtin_offsetof expects no operands" <<
eom;
610 const exprt &member =
static_cast<const exprt &
>(expr.
add(ID_designator));
614 for(
const auto &op : member.
operands())
616 if(op.id() == ID_member)
618 if(type.
id() != ID_union_tag && type.
id() != ID_struct_tag)
621 error() <<
"offsetof of member expects struct/union type, "
627 irep_idt component_name = op.get(ID_component_name);
641 if(type.
id() == ID_struct_tag)
646 if(!o_opt.has_value())
649 error() <<
"offsetof failed to determine offset of '"
650 << component_name <<
"'" <<
eom;
666 for(
const auto &c : struct_union_type.
components())
670 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
674 if(type.
id() == ID_struct_tag)
679 if(!o_opt.has_value())
682 error() <<
"offsetof failed to determine offset of '"
683 << component_name <<
"'" <<
eom;
693 typet tmp = c.type();
696 type.
id() == ID_union_tag || type.
id() == ID_struct_tag);
706 error() <<
"offset-of of member failed to find component '"
707 << component_name <<
"' in '" <<
to_string(type) <<
"'"
714 else if(op.id() == ID_index)
716 if(type.
id()!=ID_array)
719 error() <<
"offsetof of index expects array type" <<
eom;
728 auto element_size_opt =
731 if(!element_size_opt.has_value())
734 error() <<
"offsetof failed to determine array element size" <<
eom;
757 if(expr.
id()==ID_side_effect &&
758 expr.
get(ID_statement)==ID_function_call)
763 else if(expr.
id()==ID_side_effect &&
764 expr.
get(ID_statement)==ID_statement_expression)
769 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
775 auto &bindings = binary_expr.op0().operands();
777 for(
auto &binding : bindings)
786 error() <<
"forall/exists expects one declarator exactly" <<
eom;
793 symbol_table_baset::symbolst::const_iterator s_it =
799 error() <<
"failed to find bound symbol `" << identifier
800 <<
"' in symbol table" <<
eom;
804 const symbolt &symbol = s_it->second;
811 error() <<
"unexpected quantified symbol" <<
eom;
835 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
839 expr.
type()=p_it->second;
840 expr.
set(ID_C_lvalue,
true);
845 asm_label_mapt::const_iterator entry=
849 identifier=entry->second;
855 if(
lookup(identifier, symbol_ptr))
858 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
862 const symbolt &symbol=*symbol_ptr;
867 error() <<
"did not expect a type symbol here, but got '"
886 expr.
set(ID_C_cformat, base_name);
901 else if(identifier==
"__func__" ||
902 identifier==
"__FUNCTION__" ||
903 identifier==
"__PRETTY_FUNCTION__")
909 s.
set(ID_C_lvalue,
true);
920 expr.
set(ID_C_lvalue,
true);
922 if(expr.
type().
id()==ID_code)
925 tmp.
set(ID_C_implicit,
true);
944 if(last_statement==ID_expression)
950 if(op.
type().
id()==ID_array)
992 if(type.
id()==ID_c_bit_field)
996 if(op.
id() == ID_comma || op.
id() == ID_side_effect)
1003 config.ansi_c.char_width,
1010 if(!size_of_opt.has_value())
1013 error() <<
"type has no size: "
1018 new_expr = size_of_opt.value();
1024 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
1028 else if(type.
id() == ID_bool)
1031 error() <<
"sizeof cannot be applied to single bits" <<
eom;
1034 else if(type.
id() == ID_empty)
1043 (type.
id() == ID_struct_tag &&
1045 (type.
id() == ID_union_tag &&
1047 (type.
id() == ID_c_enum_tag &&
1052 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1059 if(!size_of_opt.has_value())
1066 new_expr = size_of_opt.value();
1070 new_expr.
swap(expr);
1072 expr.
add(ID_C_c_sizeof_type)=type;
1078 ID_statement_expression,
void_type(), location);
1080 decl_block.set_statement(ID_decl_block);
1093 expr.
swap(comma_expr);
1099 typet argument_type;
1107 argument_type=op_type;
1131 decl_block.set_statement(ID_decl_block);
1142 std::move(side_effect_expr), ID_comma, op, op.
type()};
1143 op.
swap(comma_expr);
1149 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1150 op.
id() != ID_initializer_list)
1163 for(
const auto &c : union_type.components())
1165 if(c.type() == op.
type())
1171 expr.
set(ID_C_lvalue,
true);
1179 <<
"' not found in union" <<
eom;
1186 if(op.
id()==ID_initializer_list)
1195 exprt tmp(ID_compound_literal, expr.
type());
1199 if(op.
id()==ID_array &&
1200 expr.
type().
id()==ID_array &&
1205 expr.
set(ID_C_lvalue,
true);
1210 if(expr_type.
id()==ID_empty)
1216 if(expr_type == op_type)
1221 if(expr_type.
id()==ID_vector)
1224 if(op_type.
id()==ID_vector)
1226 else if(op_type.
id()==ID_signedbv ||
1227 op_type.
id()==ID_unsignedbv)
1234 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1242 else if(op_type.
id()==ID_array)
1247 if(error_opt.has_value())
1253 else if(op_type.
id()==ID_empty)
1255 if(expr_type.
id()!=ID_empty)
1258 error() <<
"type cast from void only permitted to void, but got '"
1263 else if(op_type.
id()==ID_vector)
1270 if((expr_type.
id()==ID_signedbv ||
1271 expr_type.
id()==ID_unsignedbv) &&
1280 <<
"' not permitted" <<
eom;
1287 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1303 if(expr_type.
id()==ID_pointer)
1304 expr.
set(ID_C_lvalue,
true);
1321 const typet &array_type = array_expr.
type();
1322 const typet &index_type = index_expr.
type();
1325 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1326 array_type.
id() != ID_vector &&
1327 (index_type.
id() == ID_array || index_type.
id() == ID_pointer ||
1328 index_type.
id() == ID_vector))
1329 std::swap(array_expr, index_expr);
1337 const typet final_array_type = array_expr.
type();
1339 if(final_array_type.
id()==ID_array ||
1340 final_array_type.
id()==ID_vector)
1344 if(array_expr.
get_bool(ID_C_lvalue))
1345 expr.
set(ID_C_lvalue,
true);
1347 if(final_array_type.
get_bool(ID_C_constant))
1348 expr.
type().
set(ID_C_constant,
true);
1350 else if(final_array_type.
id()==ID_pointer)
1356 std::swap(summands, expr.
operands());
1358 expr.
id(ID_dereference);
1359 expr.
set(ID_C_lvalue,
true);
1365 error() <<
"operator [] must take array/vector or pointer but got '"
1374 if(expr.
op0().
type().
id() == ID_floatbv)
1376 if(expr.
id()==ID_equal)
1377 expr.
id(ID_ieee_float_equal);
1378 else if(expr.
id()==ID_notequal)
1379 expr.
id(ID_ieee_float_notequal);
1392 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1400 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1402 if(o_type0 == o_type1)
1404 if(o_type0.
id() != ID_array)
1425 if(type0.
id()==ID_pointer)
1427 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1430 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1431 expr.
id()==ID_ge || expr.
id()==ID_gt)
1435 if(type0.
id()==ID_string_constant)
1437 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1444 if(type0.
id()==ID_pointer &&
1451 if(type1.
id()==ID_pointer &&
1471 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1479 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1490 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1493 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1501 auto subtype_width =
1510 if(expr.
id() == ID_notequal)
1511 expr.
id(ID_vector_notequal);
1519 const typet &op0_type = op.type();
1521 if(op0_type.
id() == ID_array)
1526 index_expr.
set(ID_C_lvalue,
true);
1527 op.swap(index_expr);
1529 else if(op0_type.
id() == ID_pointer)
1540 error() <<
"ptrmember operator requires pointer or array type "
1541 "on left hand side, but got '"
1555 if(type.
id() != ID_struct_tag && type.
id() != ID_union_tag)
1558 error() <<
"member operator requires structure type "
1559 "on left hand side but got '"
1570 error() <<
"member operator got incomplete " << type.
id()
1571 <<
" type on left hand side" <<
eom;
1576 expr.
get(ID_component_name);
1592 error() <<
"member '" << component_name <<
"' not found in '"
1605 expr.
set(ID_C_lvalue,
true);
1609 struct_union_type.
get_bool(ID_C_constant))
1611 expr.
type().
set(ID_C_constant,
true);
1617 if(!identifier.
empty())
1618 expr.
set(ID_C_identifier, identifier);
1622 if(access==ID_private)
1625 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1637 const typet o_type0=operands[0].type();
1638 const typet o_type1=operands[1].type();
1639 const typet o_type2=operands[2].type();
1643 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1663 if(operands[1].type().
id()==ID_pointer &&
1664 operands[2].type().
id()!=ID_pointer)
1666 else if(operands[2].type().
id()==ID_pointer &&
1667 operands[1].type().
id()!=ID_pointer)
1670 if(operands[1].type().
id()==ID_pointer &&
1671 operands[2].type().
id()==ID_pointer &&
1672 operands[1].type()!=operands[2].type())
1719 if(operands[1].type().
id()==ID_empty ||
1720 operands[2].type().
id()==ID_empty)
1727 operands[1].type() != operands[2].type() ||
1728 operands[1].type().
id() == ID_array)
1733 if(operands[1].type() == operands[2].type())
1735 expr.
type()=operands[1].type();
1741 if(operands[1].get_bool(ID_C_lvalue) &&
1742 operands[2].get_bool(ID_C_lvalue))
1743 expr.
set(ID_C_lvalue,
true);
1749 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1762 if(operands.size()!=2)
1765 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1771 if_exprt if_expr(operands[0], operands[0], operands[1]);
1788 if(error_opt.has_value())
1792 if(op.
id()==ID_label)
1805 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1811 tmp.
set(ID_C_implicit,
false);
1816 if(op.
id()==ID_struct ||
1817 op.
id()==ID_union ||
1818 op.
id()==ID_array ||
1819 op.
id()==ID_string_constant)
1827 else if(op.
type().
id()==ID_code)
1834 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1848 if(op_type.
id()==ID_array)
1856 else if(op_type.
id()==ID_pointer)
1861 expr.
type().
id() == ID_empty &&
1865 error() <<
"dereferencing void pointer" <<
eom;
1873 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1878 expr.
set(ID_C_lvalue,
true);
1889 if(expr.
type().
id()==ID_code)
1892 tmp.
set(ID_C_implicit,
true);
1902 if(statement==ID_preincrement ||
1903 statement==ID_predecrement ||
1904 statement==ID_postincrement ||
1905 statement==ID_postdecrement)
1914 <<
"' not an lvalue" <<
eom;
1925 if(type0.
id() == ID_c_enum_tag)
1931 error() <<
"operator '" << statement <<
"' given incomplete type '"
1941 else if(type0.
id() == ID_c_bit_field)
1945 typet type_before{type0};
1947 expr.
type()=underlying_type;
1951 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1960 else if(type0.
id() == ID_pointer)
1968 error() <<
"operator '" << statement <<
"' not defined for type '"
1975 else if(statement==ID_function_call)
1978 else if(statement==ID_statement_expression)
1980 else if(statement==ID_gcc_conditional_expression)
1985 error() <<
"unknown side effect: " << statement <<
eom;
1997 "expression must be a " CPROVER_PREFIX "typed_target function call");
2004 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
2005 std::to_string(expr.
arguments().size()),
2015 arg0.source_location()};
2019 if(!size.has_value())
2023 "typed_target of type " +
2025 arg0.source_location()};
2034 arguments.push_back(size.value());
2036 if(arg0.type().id() == ID_pointer)
2052 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
2057 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
2058 std::to_string(expr.
arguments().size()),
2064 auto &function_pointer = expr.
arguments()[0];
2067 function_pointer.type().id() != ID_pointer ||
2068 to_pointer_type(function_pointer.type()).base_type().id() != ID_code ||
2069 !function_pointer.get_bool(ID_C_lvalue))
2073 "obeys_contract must be a function pointer lvalue expression",
2074 function_pointer.source_location());
2081 "obeys_contract must have no ternary operator",
2082 function_pointer.source_location());
2086 auto &address_of_contract = expr.
arguments()[1];
2089 address_of_contract.id() != ID_address_of ||
2091 address_of_contract.type().id() != ID_pointer ||
2092 to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
2096 "obeys_contract must must be a function symbol",
2097 address_of_contract.source_location());
2100 if(function_pointer.type() != address_of_contract.type())
2104 "obeys_contract must have the same function pointer type",
2113 return ::builtin_factory(
2115 config.ansi_c.float16_type,
2126 error() <<
"function_call side effect expects two operands" <<
eom;
2135 if(f_op.
id()==ID_symbol)
2139 asm_label_mapt::const_iterator entry=
2142 identifier=entry->second;
2159 identifier ==
"__noop" &&
2173 identifier ==
"__builtin_shuffle" &&
2181 else if(identifier ==
"__builtin_shufflevector")
2191 identifier ==
"__builtin_elementwise_add_sat" ||
2192 identifier ==
"__builtin_elementwise_sub_sat")
2204 error() <<
"equal expects two operands" <<
eom;
2215 error() <<
"equal expects two operands of same type" <<
eom;
2219 expr.
swap(equality_expr);
2233 overflow.id(ID_minus);
2238 overflow.id(ID_mult);
2243 overflow.id(ID_plus);
2248 overflow.id(ID_shl);
2253 overflow.operands()[0], overflow.id(), overflow.operands()[1]};
2267 expr.
swap(overflow);
2275 std::ostringstream error_message;
2276 error_message << identifier <<
" takes exactly 1 argument, but "
2277 << expr.
arguments().size() <<
" were provided";
2285 std::ostringstream error_message;
2286 error_message << identifier <<
" expects enum, but ("
2287 <<
expr2c(arg1, *
this) <<
") has type `"
2288 <<
type2c(arg1.type(), *
this) <<
'`';
2295 exprt lowered = in_range.lower(*
this);
2307 id2string(identifier) +
" expects one or two operands",
2312 auto &pointer_expr = expr.
arguments()[0];
2313 if(pointer_expr.type().id() == ID_array)
2316 dest_type.base_type().set(ID_C_constant,
true);
2319 else if(pointer_expr.type().id() != ID_pointer)
2322 id2string(identifier) +
" expects a pointer as first argument",
2338 const auto &subtype =
2340 if(subtype.id() == ID_empty)
2344 " expects a size when given a void pointer",
2350 size_expr = std::move(size_expr_opt.value());
2366 irep_idt shadow_memory_builtin_id =
2367 shadow_memory_builtin->get_identifier();
2369 const auto builtin_code_type =
2373 builtin_code_type.has_ellipsis() &&
2374 builtin_code_type.parameters().empty(),
2375 "Shadow memory builtins should be an ellipsis with 0 parameter");
2381 shadow_memory_builtin_id, shadow_memory_builtin->type(), ID_C};
2382 new_symbol.
base_name = shadow_memory_builtin_id;
2393 f_op = std::move(*shadow_memory_builtin);
2399 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2402 !parameters.empty(),
2403 "GCC polymorphic built-ins should have at least one parameter");
2408 if(parameters.front().type().id() == ID_pointer)
2410 identifier_with_type =
2417 identifier_with_type =
2421 gcc_polymorphic->set_identifier(identifier_with_type);
2425 for(std::size_t i = 0; i < parameters.size(); ++i)
2427 const std::string base_name =
"p_" + std::to_string(i);
2432 id2string(identifier_with_type) +
"::" + base_name;
2435 new_symbol.
type = parameters[i].type();
2438 new_symbol.
mode = ID_C;
2440 parameters[i].set_identifier(new_symbol.
name);
2441 parameters[i].set_base_name(new_symbol.
base_name);
2447 identifier_with_type, gcc_polymorphic->type(), ID_C};
2448 new_symbol.
base_name = identifier_with_type;
2456 new_symbol.value = implementation;
2461 f_op = std::move(*gcc_polymorphic);
2473 if(identifier==
"malloc" ||
2474 identifier==
"realloc" ||
2475 identifier==
"reallocf" ||
2476 identifier==
"valloc")
2485 new_symbol.type.
set(ID_C_incomplete,
true);
2497 debug() <<
"builtin '" << identifier <<
"' is unknown" <<
eom;
2502 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2513 if(f_op_type.
id() == ID_mathematical_function)
2515 const auto &mathematical_function_type =
2519 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2522 error() <<
"expected " << mathematical_function_type.domain().size()
2523 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2531 if(p.first.type() != p.second)
2544 expr.
swap(function_application);
2548 if(f_op_type.
id()!=ID_pointer)
2551 error() <<
"expected function/function pointer as argument but got '"
2557 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2564 tmp.
set(ID_C_implicit,
true);
2569 if(f_op.
type().
id()!=ID_code)
2572 error() <<
"expected code as argument" <<
eom;
2595 if(f_op.
id()!=ID_symbol)
2643 if(arg.type().id() != ID_pointer)
2647 "pointer_in_range_dfcc expects pointer-typed arguments",
2648 arg.source_location()};
2658 error() <<
"same_object expects two operands" <<
eom;
2664 exprt same_object_expr=
2668 return same_object_expr;
2675 error() <<
"get_must expects two operands" <<
eom;
2685 return std::move(get_must_expr);
2692 error() <<
"get_may expects two operands" <<
eom;
2702 return std::move(get_may_expr);
2709 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2718 return same_object_expr;
2725 error() <<
"buffer_size expects one operand" <<
eom;
2735 return buffer_size_expr;
2743 error() <<
"is_list expects one operand" <<
eom;
2750 expr.
arguments()[0].type().id() != ID_pointer ||
2755 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2763 return std::move(is_list_expr);
2771 error() <<
"is_dll expects one operand" <<
eom;
2778 expr.
arguments()[0].type().id() != ID_pointer ||
2783 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2791 return std::move(is_dll_expr);
2799 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2806 expr.
arguments()[0].type().id() != ID_pointer ||
2811 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2819 return std::move(is_cyclic_dll_expr);
2827 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2834 args_no_cast.reserve(expr.
arguments().size());
2835 for(
const auto &argument : expr.
arguments())
2839 args_no_cast.back().type().id() != ID_pointer ||
2844 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2851 is_sentinel_dll_expr.
operands() = args_no_cast;
2854 return std::move(is_sentinel_dll_expr);
2862 error() <<
"is_cstring expects one operand" <<
eom;
2868 if(expr.
arguments()[0].type().id() != ID_pointer)
2871 error() <<
"is_cstring expects a pointer operand" <<
eom;
2878 return std::move(is_cstring_expr);
2886 error() <<
"cstrlen expects one operand" <<
eom;
2892 if(expr.
arguments()[0].type().id() != ID_pointer)
2895 error() <<
"cstrlen expects a pointer operand" <<
eom;
2902 return std::move(cstrlen_expr);
2909 error() <<
"is_zero_string expects one operand" <<
eom;
2917 is_zero_string_expr.
set(ID_C_lvalue,
true);
2920 return std::move(is_zero_string_expr);
2927 error() <<
"zero_string_length expects one operand" <<
eom;
2933 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2935 zero_string_length_expr.
set(ID_C_lvalue,
true);
2938 return zero_string_length_expr;
2945 error() <<
"dynamic_object expects one argument" <<
eom;
2954 return is_dynamic_object_expr;
2961 error() <<
"live_object expects one argument" <<
eom;
2970 return live_object_expr;
2977 error() <<
"pointer_in_range expects three arguments" <<
eom;
2987 return pointer_in_range_expr;
2994 error() <<
"writeable_object expects one argument" <<
eom;
3003 return writeable_object_expr;
3011 error() <<
"separate expects two or more arguments" <<
eom;
3020 return separate_expr;
3027 error() <<
"pointer_offset expects one argument" <<
eom;
3043 error() <<
"object_size expects one operand" <<
eom;
3052 return std::move(object_size_expr);
3059 error() <<
"pointer_object expects one argument" <<
eom;
3070 else if(identifier==
"__builtin_bswap16" ||
3071 identifier==
"__builtin_bswap32" ||
3072 identifier==
"__builtin_bswap64")
3077 error() << identifier <<
" expects one operand" <<
eom;
3087 return std::move(bswap_expr);
3090 identifier ==
"__builtin_rotateleft8" ||
3091 identifier ==
"__builtin_rotateleft16" ||
3092 identifier ==
"__builtin_rotateleft32" ||
3093 identifier ==
"__builtin_rotateleft64" ||
3094 identifier ==
"__builtin_rotateright8" ||
3095 identifier ==
"__builtin_rotateright16" ||
3096 identifier ==
"__builtin_rotateright32" ||
3097 identifier ==
"__builtin_rotateright64")
3103 error() << identifier <<
" expects two operands" <<
eom;
3109 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
3110 identifier ==
"__builtin_rotateleft16" ||
3111 identifier ==
"__builtin_rotateleft32" ||
3112 identifier ==
"__builtin_rotateleft64")
3119 return std::move(rotate_expr);
3121 else if(identifier==
"__builtin_nontemporal_load")
3126 error() << identifier <<
" expects one operand" <<
eom;
3135 if(ptr_arg.
type().
id()!=ID_pointer)
3138 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3147 identifier ==
"__builtin_fpclassify" ||
3153 error() << identifier <<
" expects six arguments" <<
eom;
3166 if(fp_value.
type().
id() != ID_floatbv)
3169 error() <<
"non-floating-point argument for " << identifier <<
eom;
3177 const auto &arguments = expr.
arguments();
3196 identifier==
"__builtin_isnan")
3201 error() <<
"isnan expects one operand" <<
eom;
3219 error() <<
"isfinite expects one operand" <<
eom;
3231 identifier==
"__builtin_inf")
3238 return std::move(inf_expr);
3247 return std::move(inff_expr);
3256 return std::move(infl_expr);
3266 error() << identifier <<
" expects two arguments" <<
eom;
3270 auto round_to_integral_expr =
3274 return std::move(round_to_integral_expr);
3287 error() <<
"abs-functions expect one operand" <<
eom;
3296 return std::move(abs_expr);
3306 error() <<
"fmod-functions expect two operands" <<
eom;
3320 return std::move(fmod_expr);
3330 error() <<
"remainder-functions expect two operands" <<
eom;
3344 return std::move(floatbv_rem_expr);
3351 error() <<
"allocate expects two operands" <<
eom;
3360 return std::move(malloc_expr);
3369 error() << identifier <<
" expects one operand" <<
eom;
3373 const auto ¶m_id = expr.
arguments().front().id();
3374 if(!(param_id == ID_dereference || param_id == ID_member ||
3375 param_id == ID_symbol || param_id == ID_ptrmember ||
3376 param_id == ID_constant || param_id == ID_typecast ||
3377 param_id == ID_index))
3380 error() <<
"Tracking history of " << param_id
3381 <<
" expressions is not supported yet." <<
eom;
3390 return std::move(old_expr);
3395 identifier==
"__builtin_isinf")
3400 error() << identifier <<
" expects one operand" <<
eom;
3408 if(fp_value.
type().
id() != ID_floatbv)
3411 error() <<
"non-floating-point argument for " << identifier <<
eom;
3420 else if(identifier ==
"__builtin_isinf_sign")
3425 error() << identifier <<
" expects one operand" <<
eom;
3435 if(fp_value.
type().
id() != ID_floatbv)
3438 error() <<
"non-floating-point argument for " << identifier <<
eom;
3456 identifier ==
"__builtin_isnormal")
3461 error() << identifier <<
" expects one operand" <<
eom;
3469 if(fp_value.
type().
id() != ID_floatbv)
3472 error() <<
"non-floating-point argument for " << identifier <<
eom;
3484 identifier==
"__builtin_signbit" ||
3485 identifier==
"__builtin_signbitf" ||
3486 identifier==
"__builtin_signbitl")
3491 error() << identifier <<
" expects one operand" <<
eom;
3502 else if(identifier==
"__builtin_popcount" ||
3503 identifier==
"__builtin_popcountl" ||
3504 identifier==
"__builtin_popcountll" ||
3505 identifier==
"__popcnt16" ||
3506 identifier==
"__popcnt" ||
3507 identifier==
"__popcnt64")
3512 error() << identifier <<
" expects one operand" <<
eom;
3521 return std::move(popcount_expr);
3524 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
3525 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
3526 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
3531 error() << identifier <<
" expects one operand" <<
eom;
3541 return std::move(clz);
3544 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3545 identifier ==
"__builtin_ctzll")
3550 error() << identifier <<
" expects one operand" <<
eom;
3560 return std::move(ctz);
3563 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3564 identifier ==
"__builtin_ffsll")
3569 error() << identifier <<
" expects one operand" <<
eom;
3578 return std::move(ffs);
3580 else if(identifier==
"__builtin_expect")
3591 error() <<
"__builtin_expect expects two arguments" <<
eom;
3600 identifier ==
"__builtin_object_size" ||
3601 identifier ==
"__builtin_dynamic_object_size")
3612 error() <<
"__builtin_object_size expects two arguments" <<
eom;
3629 error() <<
"__builtin_object_size expects constant as second argument, "
3637 if(arg1==0 || arg1==1)
3650 else if(identifier==
"__builtin_choose_expr")
3656 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3671 else if(identifier==
"__builtin_constant_p")
3678 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3694 tmp1.
id() == ID_typecast &&
3700 .
id() == ID_string_constant)
3712 else if(identifier==
"__builtin_classify_type")
3719 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3730 const typet &type =
object.type().
id() == ID_c_bit_field
3734 unsigned type_number;
3736 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3744 type_number = type.
id() == ID_empty ? 0u
3745 : (type.
id() == ID_bool || type.
id() == ID_c_bool) ? 4u
3746 : (type.
id() == ID_pointer || type.
id() == ID_array) ? 5u
3747 : type.
id() == ID_floatbv ? 8u
3748 : (type.
id() == ID_complex &&
3751 : type.
id() == ID_struct_tag ? 12u
3752 : type.
id() == ID_union_tag
3763 identifier ==
"__builtin_add_overflow" ||
3764 identifier ==
"__builtin_sadd_overflow" ||
3765 identifier ==
"__builtin_saddl_overflow" ||
3766 identifier ==
"__builtin_saddll_overflow" ||
3767 identifier ==
"__builtin_uadd_overflow" ||
3768 identifier ==
"__builtin_uaddl_overflow" ||
3769 identifier ==
"__builtin_uaddll_overflow" ||
3770 identifier ==
"__builtin_add_overflow_p")
3775 identifier ==
"__builtin_sub_overflow" ||
3776 identifier ==
"__builtin_ssub_overflow" ||
3777 identifier ==
"__builtin_ssubl_overflow" ||
3778 identifier ==
"__builtin_ssubll_overflow" ||
3779 identifier ==
"__builtin_usub_overflow" ||
3780 identifier ==
"__builtin_usubl_overflow" ||
3781 identifier ==
"__builtin_usubll_overflow" ||
3782 identifier ==
"__builtin_sub_overflow_p")
3787 identifier ==
"__builtin_mul_overflow" ||
3788 identifier ==
"__builtin_smul_overflow" ||
3789 identifier ==
"__builtin_smull_overflow" ||
3790 identifier ==
"__builtin_smulll_overflow" ||
3791 identifier ==
"__builtin_umul_overflow" ||
3792 identifier ==
"__builtin_umull_overflow" ||
3793 identifier ==
"__builtin_umulll_overflow" ||
3794 identifier ==
"__builtin_mul_overflow_p")
3799 identifier ==
"__builtin_bitreverse8" ||
3800 identifier ==
"__builtin_bitreverse16" ||
3801 identifier ==
"__builtin_bitreverse32" ||
3802 identifier ==
"__builtin_bitreverse64")
3807 std::ostringstream error_message;
3808 error_message <<
"error: " << identifier <<
" expects one operand";
3818 return std::move(bitreverse);
3834 std::ostringstream error_message;
3835 error_message << identifier <<
" takes exactly 3 arguments, but "
3836 << expr.
arguments().size() <<
" were provided";
3850 auto const raise_wrong_argument_error =
3852 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3853 std::ostringstream error_message;
3854 error_message <<
"error: " << identifier <<
" has signature "
3855 << identifier <<
"(integral, integral, integral"
3856 << (_p ?
"" :
"*") <<
"), "
3857 <<
"but argument " << argument_number <<
" ("
3858 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3859 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3863 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3865 auto const &argument = expr.
arguments()[arg_index];
3869 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3873 !is__p_variant && (
result.type().id() != ID_pointer ||
3877 raise_wrong_argument_error(
result, 3, is__p_variant);
3896 std::ostringstream error_message;
3897 error_message <<
"error: " << identifier
3898 <<
" takes exactly two arguments, but "
3899 << expr.
arguments().size() <<
" were provided";
3907 identifier ==
"__builtin_elementwise_sub_sat")
3913 identifier ==
"__builtin_elementwise_add_sat")
3938 if(code_type.
get_bool(ID_C_incomplete))
3942 else if(code_type.
is_KnR())
3946 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3948 arguments.push_back(
3954 if(parameters.size() > arguments.size())
3957 error() <<
"not enough function arguments" <<
eom;
3961 else if(parameters.size() != arguments.size())
3964 error() <<
"wrong number of function arguments: "
3965 <<
"expected " << parameters.size() <<
", but got "
3966 << arguments.size() <<
eom;
3970 for(std::size_t i=0; i<arguments.size(); i++)
3972 exprt &op=arguments[i];
3978 else if(i < parameters.size())
3984 op.
get(ID_statement) == ID_assign && op.
type().
id() != ID_bool)
3987 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3996 if(op.
type().
id() == ID_array)
3999 dest_type.base_type().set(ID_C_constant,
true);
4017 if(o_type.
id()==ID_vector)
4036 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
4091 if(o_type0.
id()==ID_vector &&
4092 o_type1.
id()==ID_vector)
4106 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
4111 expr.
type() = o_type0;
4115 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
4120 expr.
type() = o_type1;
4124 if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4137 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
4138 expr.
id()==ID_mult || expr.
id()==ID_div)
4140 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
4145 else if(type0==type1)
4154 else if(expr.
id()==ID_mod)
4158 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
4166 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
4167 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
4176 else if(type0.
id()==ID_bool)
4178 if(expr.
id()==ID_bitand)
4180 else if(expr.
id() == ID_bitnand)
4182 else if(expr.
id()==ID_bitor)
4184 else if(expr.
id()==ID_bitxor)
4193 else if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4197 (type0.
id() == ID_signedbv || type0.
id() == ID_unsignedbv))
4199 expr.
type() = type0;
4205 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4221 if(o_type0.
id()==ID_vector &&
4222 o_type1.
id()==ID_vector)
4238 o_type0.
id() == ID_vector &&
4256 if(expr.
id()==ID_shr)
4260 if(op0_type.
id()==ID_unsignedbv)
4265 else if(op0_type.
id()==ID_signedbv)
4276 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4290 base_type.
id() == ID_struct_tag &&
4294 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4298 base_type.
id() == ID_union_tag &&
4302 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4306 base_type.
id() == ID_empty &&
4310 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4313 else if(base_type.
id() == ID_empty)
4331 if(expr.
id()==ID_minus ||
4332 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
4334 if(type0.
id()==ID_pointer &&
4335 type1.
id()==ID_pointer)
4348 if(type0.
id()==ID_pointer &&
4349 (type1.
id()==ID_bool ||
4350 type1.
id()==ID_c_bool ||
4351 type1.
id()==ID_unsignedbv ||
4352 type1.
id()==ID_signedbv ||
4353 type1.
id()==ID_c_bit_field ||
4354 type1.
id()==ID_c_enum_tag))
4362 else if(expr.
id()==ID_plus ||
4363 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
4365 exprt *p_op, *int_op;
4367 if(type0.
id()==ID_pointer)
4372 else if(type1.
id()==ID_pointer)
4379 p_op=int_op=
nullptr;
4383 const typet &int_op_type = int_op->
type();
4385 if(int_op_type.
id()==ID_bool ||
4386 int_op_type.
id()==ID_c_bool ||
4387 int_op_type.
id()==ID_unsignedbv ||
4388 int_op_type.
id()==ID_signedbv ||
4389 int_op_type.
id()==ID_c_bit_field ||
4390 int_op_type.
id()==ID_c_enum_tag)
4401 if(expr.
id()==ID_side_effect)
4407 error() <<
"operator '" << op_name <<
"' not defined for types '"
4438 if(type0.
id()==ID_empty)
4441 error() <<
"cannot assign void" <<
eom;
4448 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4461 if(type0.
id() == ID_array)
4464 error() <<
"direct assignments to arrays not permitted" <<
eom;
4470 if(op0.
type() != op1.
type() && op0.
type().
id() == ID_c_bit_field)
4479 expr.
type()=o_type0;
4481 if(statement==ID_assign)
4486 else if(statement==ID_assign_shl ||
4487 statement==ID_assign_shr)
4489 if(o_type0.
id() == ID_vector)
4494 o_type1.
id() == ID_vector &&
4495 vector_o_type0.element_type() ==
4497 is_number(vector_o_type0.element_type()))
4513 if(statement==ID_assign_shl)
4523 if(underlying_type.
id()==ID_unsignedbv ||
4524 underlying_type.
id()==ID_c_bool)
4526 expr.
set(ID_statement, ID_assign_lshr);
4529 else if(underlying_type.
id()==ID_signedbv)
4531 expr.
set(ID_statement, ID_assign_ashr);
4537 else if(statement==ID_assign_bitxor ||
4538 statement==ID_assign_bitand ||
4539 statement==ID_assign_bitor)
4542 if(o_type0.
id()==ID_bool ||
4543 o_type0.
id()==ID_c_bool)
4548 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4549 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4554 else if(o_type0.
id()==ID_c_enum_tag ||
4555 o_type0.
id()==ID_unsignedbv ||
4556 o_type0.
id()==ID_signedbv ||
4557 o_type0.
id()==ID_c_bit_field)
4561 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4562 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4567 else if(o_type0.
id()==ID_vector &&
4568 o_type1.
id()==ID_vector)
4579 o_type0.
id() == ID_vector &&
4580 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
4581 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
4582 o_type1.
id() == ID_signedbv))
4591 if(o_type0.
id()==ID_pointer &&
4592 (statement==ID_assign_minus || statement==ID_assign_plus))
4597 else if(o_type0.
id()==ID_vector &&
4598 o_type1.
id()==ID_vector)
4608 else if(o_type0.
id() == ID_vector)
4614 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4620 else if(o_type0.
id()==ID_bool ||
4621 o_type0.
id()==ID_c_bool)
4626 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4627 op1.
type().
id() == ID_signedbv)
4638 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4646 error() <<
"assignment '" << statement <<
"' not defined for types '"
4676 if(e.
id() == ID_infinity)
4682 if(e.
id() == ID_address_of)
4687 e.
id() == ID_typecast || e.
id() == ID_array_of || e.
id() == ID_plus ||
4688 e.
id() == ID_mult || e.
id() == ID_array || e.
id() == ID_with ||
4689 e.
id() == ID_struct || e.
id() == ID_union || e.
id() == ID_empty_union ||
4690 e.
id() == ID_equal || e.
id() == ID_notequal || e.
id() == ID_lt ||
4691 e.
id() == ID_le || e.
id() == ID_gt || e.
id() == ID_ge ||
4692 e.
id() == ID_if || e.
id() == ID_not || e.
id() == ID_and ||
4693 e.
id() == ID_or || e.
id() == ID_bitnot || e.
id() == ID_bitand ||
4694 e.
id() == ID_bitor || e.
id() == ID_bitxor || e.
id() == ID_vector)
4698 return is_constant(op);
4708 if(e.
id() == ID_symbol)
4710 return e.
type().
id() == ID_code ||
4713 else if(e.
id() == ID_array && e.
get_bool(ID_C_string_constant))
4715 else if(e.
id() == ID_label)
4717 else if(e.
id() == ID_index)
4724 else if(e.
id() == ID_member)
4728 else if(e.
id() == ID_dereference)
4734 else if(e.
id() == ID_string_constant)
4748 const auto rounding_mode =
4758 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4775 error() <<
"conversion to integer constant failed" <<
eom;
4783 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...
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.
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)
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
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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)