49 if(expr.
id()==ID_already_typechecked)
67 if(expr.
id()==ID_div ||
72 if(expr.
type().
id()==ID_floatbv &&
81 expr.
id(ID_floatbv_div);
82 else if(expr.
id()==ID_mult)
83 expr.
id(ID_floatbv_mult);
84 else if(expr.
id()==ID_plus)
85 expr.
id(ID_floatbv_plus);
86 else if(expr.
id()==ID_minus)
87 expr.
id(ID_floatbv_minus);
108 if(type1.
id()==ID_c_enum_tag)
110 else if(type2.
id()==ID_c_enum_tag)
113 if(type1.
id()==ID_c_enum)
115 if(type2.
id()==ID_c_enum)
120 else if(type2.
id()==ID_c_enum)
125 else if(type1.
id()==ID_pointer &&
126 type2.
id()==ID_pointer)
131 else if(type1.
id()==ID_array &&
132 type2.
id()==ID_array)
138 else if(type1.
id()==ID_code &&
152 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
168 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
178 if(expr.
id()==ID_side_effect)
182 else if(expr.
id()==ID_infinity)
186 else if(expr.
id()==ID_symbol)
188 else if(expr.
id()==ID_unary_plus ||
189 expr.
id()==ID_unary_minus ||
190 expr.
id()==ID_bitnot)
192 else if(expr.
id()==ID_not)
195 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
198 else if(expr.
id()==ID_address_of)
200 else if(expr.
id()==ID_dereference)
202 else if(expr.
id()==ID_member)
204 else if(expr.
id()==ID_ptrmember)
206 else if(expr.
id()==ID_equal ||
207 expr.
id()==ID_notequal ||
213 else if(expr.
id()==ID_index)
215 else if(expr.
id()==ID_typecast)
217 else if(expr.
id()==ID_sizeof)
219 else if(expr.
id()==ID_alignof)
222 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
223 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
224 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
228 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
230 else if(expr.
id()==ID_comma)
232 else if(expr.
id()==ID_if)
234 else if(expr.
id()==ID_code)
237 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
240 else if(expr.
id()==ID_gcc_builtin_va_arg)
242 else if(expr.
id()==ID_cw_va_arg_typeof)
244 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
255 subtypes[0].
remove(ID_C_constant);
256 subtypes[0].remove(ID_C_volatile);
257 subtypes[0].remove(ID_C_restricted);
258 subtypes[1].remove(ID_C_constant);
259 subtypes[1].remove(ID_C_volatile);
260 subtypes[1].remove(ID_C_restricted);
265 else if(expr.
id()==ID_clang_builtin_convertvector)
274 else if(expr.
id()==ID_builtin_offsetof)
276 else if(expr.
id()==ID_string_constant)
279 expr.
set(ID_C_lvalue,
true);
281 else if(expr.
id()==ID_arguments)
285 else if(expr.
id()==ID_designated_initializer)
287 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
291 if(it->id()==ID_index)
295 else if(expr.
id()==ID_initializer_list)
301 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
307 auto &bindings = binary_expr.op0().operands();
308 auto &where = binary_expr.op1();
310 for(
const auto &binding : bindings)
312 if(binding.get(ID_statement) != ID_decl)
315 error() <<
"expected declaration as operand of quantifier" <<
eom;
323 error() <<
"quantifier must not contain side effects" <<
eom;
328 for(
auto &binding : bindings)
331 if(expr.
id() == ID_lambda)
335 for(
auto &binding : bindings)
336 domain.push_back(binding.type());
346 else if(expr.
id()==ID_label)
350 else if(expr.
id()==ID_array)
354 else if(expr.
id()==ID_complex)
359 else if(expr.
id() == ID_complex_real)
363 if(op.
type().
id() != ID_complex)
368 error() <<
"real part retrieval expects numerical operand, "
376 expr.
swap(complex_real_expr);
384 complex_real_expr.
set(ID_C_lvalue,
true);
387 complex_real_expr.
type().
set(ID_C_constant,
true);
389 expr.
swap(complex_real_expr);
392 else if(expr.
id() == ID_complex_imag)
396 if(op.
type().
id() != ID_complex)
401 error() <<
"real part retrieval expects numerical operand, "
409 expr.
swap(complex_imag_expr);
417 complex_imag_expr.
set(ID_C_lvalue,
true);
420 complex_imag_expr.
type().
set(ID_C_constant,
true);
422 expr.
swap(complex_imag_expr);
425 else if(expr.
id()==ID_generic_selection)
442 for(
auto &irep : generic_associations)
444 if(irep.get(ID_type_arg) != ID_default)
446 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
457 for(
const auto &irep : generic_associations)
459 if(irep.get(ID_type_arg) == ID_default)
460 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
462 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
464 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
471 expr.
swap(default_match);
475 error() <<
"unmatched generic selection: " <<
to_string(op.type())
481 expr.
swap(assoc_match);
486 else if(expr.
id()==ID_gcc_asm_input ||
487 expr.
id()==ID_gcc_asm_output ||
488 expr.
id()==ID_gcc_asm_clobbered_register)
491 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
492 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
497 expr.
id() == ID_C_spec_assigns || expr.
id() == ID_C_spec_frees ||
498 expr.
id() == ID_target_list)
516 expr.
set(ID_C_lvalue,
true);
551 symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C};
552 symbol.base_name=ID_gcc_builtin_va_arg;
581 error() <<
"builtin_offsetof expects no operands" <<
eom;
588 const exprt &member =
static_cast<const exprt &
>(expr.
add(ID_designator));
592 for(
const auto &op : member.
operands())
596 if(op.id() == ID_member)
598 if(type.
id()!=ID_union && type.
id()!=ID_struct)
601 error() <<
"offsetof of member expects struct/union type, "
607 irep_idt component_name = op.get(ID_component_name);
621 if(type.
id()==ID_struct)
626 if(!o_opt.has_value())
629 error() <<
"offsetof failed to determine offset of '"
630 << component_name <<
"'" <<
eom;
646 for(
const auto &c : struct_union_type.
components())
650 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
654 if(type.
id()==ID_struct)
659 if(!o_opt.has_value())
662 error() <<
"offsetof failed to determine offset of '"
663 << component_name <<
"'" <<
eom;
685 error() <<
"offset-of of member failed to find component '"
686 << component_name <<
"' in '" <<
to_string(type) <<
"'"
693 else if(op.id() == ID_index)
695 if(type.
id()!=ID_array)
698 error() <<
"offsetof of index expects array type" <<
eom;
707 auto element_size_opt =
710 if(!element_size_opt.has_value())
713 error() <<
"offsetof failed to determine array element size" <<
eom;
736 if(expr.
id()==ID_side_effect &&
737 expr.
get(ID_statement)==ID_function_call)
742 else if(expr.
id()==ID_side_effect &&
743 expr.
get(ID_statement)==ID_statement_expression)
748 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
754 auto &bindings = binary_expr.op0().operands();
756 for(
auto &binding : bindings)
765 error() <<
"forall/exists expects one declarator exactly" <<
eom;
772 symbol_table_baset::symbolst::const_iterator s_it =
778 error() <<
"failed to find bound symbol `" << identifier
779 <<
"' in symbol table" <<
eom;
783 const symbolt &symbol = s_it->second;
790 error() <<
"unexpected quantified symbol" <<
eom;
814 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
818 expr.
type()=p_it->second;
819 expr.
set(ID_C_lvalue,
true);
824 asm_label_mapt::const_iterator entry=
828 identifier=entry->second;
834 if(
lookup(identifier, symbol_ptr))
837 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
841 const symbolt &symbol=*symbol_ptr;
846 error() <<
"did not expect a type symbol here, but got '"
865 expr.
set(ID_C_cformat, base_name);
880 else if(identifier==
"__func__" ||
881 identifier==
"__FUNCTION__" ||
882 identifier==
"__PRETTY_FUNCTION__")
888 s.
set(ID_C_lvalue,
true);
899 expr.
set(ID_C_lvalue,
true);
901 if(expr.
type().
id()==ID_code)
904 tmp.
set(ID_C_implicit,
true);
923 if(last_statement==ID_expression)
929 if(op.
type().
id()==ID_array)
971 if(type.
id()==ID_c_bit_field)
974 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
977 else if(type.
id() == ID_bool)
980 error() <<
"sizeof cannot be applied to single bits" <<
eom;
983 else if(type.
id() == ID_empty)
992 (type.
id() == ID_struct_tag &&
994 (type.
id() == ID_union_tag &&
996 (type.
id() == ID_c_enum_tag &&
1001 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1008 if(!size_of_opt.has_value())
1015 new_expr = size_of_opt.value();
1018 new_expr.
swap(expr);
1020 expr.
add(ID_C_c_sizeof_type)=type;
1028 decl_block.set_statement(ID_decl_block);
1039 std::move(side_effect_expr), ID_comma, expr, expr.
type()};
1040 expr.
swap(comma_expr);
1046 typet argument_type;
1054 argument_type=op_type;
1078 decl_block.set_statement(ID_decl_block);
1089 std::move(side_effect_expr), ID_comma, op, op.
type()};
1090 op.
swap(comma_expr);
1096 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1097 op.
id() != ID_initializer_list)
1110 for(
const auto &c : union_type.components())
1112 if(c.type() == op.
type())
1118 expr.
set(ID_C_lvalue,
true);
1126 <<
"' not found in union" <<
eom;
1133 if(op.
id()==ID_initializer_list)
1142 exprt tmp(ID_compound_literal, expr.
type());
1146 if(op.
id()==ID_array &&
1147 expr.
type().
id()==ID_array &&
1152 expr.
set(ID_C_lvalue,
true);
1157 if(expr_type.
id()==ID_empty)
1163 if(expr_type == op_type)
1168 if(expr_type.
id()==ID_vector)
1171 if(op_type.
id()==ID_vector)
1173 else if(op_type.
id()==ID_signedbv ||
1174 op_type.
id()==ID_unsignedbv)
1181 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1189 else if(op_type.
id()==ID_array)
1194 if(error_opt.has_value())
1200 else if(op_type.
id()==ID_empty)
1202 if(expr_type.
id()!=ID_empty)
1205 error() <<
"type cast from void only permitted to void, but got '"
1210 else if(op_type.
id()==ID_vector)
1217 if((expr_type.
id()==ID_signedbv ||
1218 expr_type.
id()==ID_unsignedbv) &&
1227 <<
"' not permitted" <<
eom;
1234 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1250 if(expr_type.
id()==ID_pointer)
1251 expr.
set(ID_C_lvalue,
true);
1268 const typet &array_type = array_expr.
type();
1272 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1273 array_type.
id() != ID_vector &&
1276 std::swap(array_expr, index_expr);
1284 const typet final_array_type = array_expr.
type();
1286 if(final_array_type.
id()==ID_array ||
1287 final_array_type.
id()==ID_vector)
1291 if(array_expr.
get_bool(ID_C_lvalue))
1292 expr.
set(ID_C_lvalue,
true);
1294 if(final_array_type.
get_bool(ID_C_constant))
1295 expr.
type().
set(ID_C_constant,
true);
1297 else if(final_array_type.
id()==ID_pointer)
1303 std::swap(summands, expr.
operands());
1305 expr.
id(ID_dereference);
1306 expr.
set(ID_C_lvalue,
true);
1312 error() <<
"operator [] must take array/vector or pointer but got '"
1321 if(expr.
op0().
type().
id() == ID_floatbv)
1323 if(expr.
id()==ID_equal)
1324 expr.
id(ID_ieee_float_equal);
1325 else if(expr.
id()==ID_notequal)
1326 expr.
id(ID_ieee_float_notequal);
1339 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1347 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1351 if(o_type0.
id() != ID_array)
1372 if(type0.
id()==ID_pointer)
1374 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1377 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1378 expr.
id()==ID_ge || expr.
id()==ID_gt)
1382 if(type0.
id()==ID_string_constant)
1384 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1391 if(type0.
id()==ID_pointer &&
1398 if(type1.
id()==ID_pointer &&
1418 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1426 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1437 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1440 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1448 auto subtype_width =
1457 if(expr.
id() == ID_notequal)
1458 expr.
id(ID_vector_notequal);
1466 const typet &op0_type = op.type();
1468 if(op0_type.
id() == ID_array)
1473 index_expr.
set(ID_C_lvalue,
true);
1474 op.swap(index_expr);
1476 else if(op0_type.
id() == ID_pointer)
1487 error() <<
"ptrmember operator requires pointer or array type "
1488 "on left hand side, but got '"
1504 if(type.
id()!=ID_struct &&
1505 type.
id()!=ID_union)
1508 error() <<
"member operator requires structure type "
1509 "on left hand side but got '"
1520 error() <<
"member operator got incomplete " << type.
id()
1521 <<
" type on left hand side" <<
eom;
1526 expr.
get(ID_component_name);
1542 error() <<
"member '" << component_name <<
"' not found in '"
1555 expr.
set(ID_C_lvalue,
true);
1558 expr.
type().
set(ID_C_constant,
true);
1563 if(!identifier.
empty())
1564 expr.
set(ID_C_identifier, identifier);
1568 if(access==ID_private)
1571 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1583 const typet o_type0=operands[0].type();
1584 const typet o_type1=operands[1].type();
1585 const typet o_type2=operands[2].type();
1589 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1597 if(operands[1].type().
id()==ID_pointer &&
1598 operands[2].type().
id()!=ID_pointer)
1600 else if(operands[2].type().
id()==ID_pointer &&
1601 operands[1].type().
id()!=ID_pointer)
1604 if(operands[1].type().
id()==ID_pointer &&
1605 operands[2].type().
id()==ID_pointer &&
1606 operands[1].type()!=operands[2].type())
1653 if(operands[1].type().
id()==ID_empty ||
1654 operands[2].type().
id()==ID_empty)
1661 operands[1].type() != operands[2].type() ||
1662 operands[1].type().
id() == ID_array)
1667 if(operands[1].type() == operands[2].type())
1669 expr.
type()=operands[1].type();
1675 if(operands[1].get_bool(ID_C_lvalue) &&
1676 operands[2].get_bool(ID_C_lvalue))
1677 expr.
set(ID_C_lvalue,
true);
1683 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1696 if(operands.size()!=2)
1699 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1705 if_exprt if_expr(operands[0], operands[0], operands[1]);
1722 if(error_opt.has_value())
1726 if(op.
id()==ID_label)
1739 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1745 tmp.
set(ID_C_implicit,
false);
1750 if(op.
id()==ID_struct ||
1751 op.
id()==ID_union ||
1752 op.
id()==ID_array ||
1753 op.
id()==ID_string_constant)
1761 else if(op.
type().
id()==ID_code)
1768 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1782 if(op_type.
id()==ID_array)
1790 else if(op_type.
id()==ID_pointer)
1795 expr.
type().
id() == ID_empty &&
1799 error() <<
"dereferencing void pointer" <<
eom;
1807 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1812 expr.
set(ID_C_lvalue,
true);
1823 if(expr.
type().
id()==ID_code)
1826 tmp.
set(ID_C_implicit,
true);
1836 if(statement==ID_preincrement ||
1837 statement==ID_predecrement ||
1838 statement==ID_postincrement ||
1839 statement==ID_postdecrement)
1848 <<
"' not an lvalue" <<
eom;
1859 if(type0.
id() == ID_c_enum_tag)
1865 error() <<
"operator '" << statement <<
"' given incomplete type '"
1875 else if(type0.
id() == ID_c_bit_field)
1880 expr.
type()=underlying_type;
1882 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1891 else if(type0.
id() == ID_pointer)
1899 error() <<
"operator '" << statement <<
"' not defined for type '"
1906 else if(statement==ID_function_call)
1909 else if(statement==ID_statement_expression)
1911 else if(statement==ID_gcc_conditional_expression)
1916 error() <<
"unknown side effect: " << statement <<
eom;
1928 "expression must be a " CPROVER_PREFIX "typed_target function call");
1935 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
1936 std::to_string(expr.
arguments().size()),
1950 if(!size.has_value())
1954 "typed_target of type " +
1956 arg0.source_location()};
1965 arguments.push_back(size.value());
1967 if(arg0.type().id() == ID_pointer)
1983 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
1988 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
1989 std::to_string(expr.
arguments().size()),
1995 auto &function_pointer = expr.
arguments()[0];
1998 function_pointer.type().id() != ID_pointer ||
2000 !function_pointer.get_bool(ID_C_lvalue))
2004 "obeys_contract must be a function pointer lvalue expression",
2005 function_pointer.source_location());
2012 "obeys_contract must have no ternary operator",
2013 function_pointer.source_location());
2017 auto &address_of_contract = expr.
arguments()[1];
2020 address_of_contract.id() != ID_address_of ||
2022 address_of_contract.
type().
id() != ID_pointer ||
2027 "obeys_contract must must be a function symbol",
2028 address_of_contract.source_location());
2031 if(function_pointer.type() != address_of_contract.type())
2035 "obeys_contract must have the same function pointer type",
2044 return ::builtin_factory(
2057 error() <<
"function_call side effect expects two operands" <<
eom;
2066 if(f_op.
id()==ID_symbol)
2070 asm_label_mapt::const_iterator entry=
2073 identifier=entry->second;
2090 identifier ==
"__noop" &&
2104 identifier ==
"__builtin_shuffle" &&
2112 else if(identifier ==
"__builtin_shufflevector")
2133 error() <<
"equal expects two operands" <<
eom;
2144 error() <<
"equal expects two operands of same type" <<
eom;
2148 expr.
swap(equality_expr);
2162 overflow.
id(ID_minus);
2167 overflow.id(ID_mult);
2172 overflow.id(ID_plus);
2177 overflow.id(ID_shl);
2182 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
2183 of.add_source_location() = overflow.source_location();
2195 overflow.add_source_location() = tmp.source_location();
2196 expr.
swap(overflow);
2204 std::ostringstream error_message;
2205 error_message << identifier <<
" takes exactly 1 argument, but "
2206 << expr.
arguments().size() <<
" were provided";
2214 std::ostringstream error_message;
2215 error_message << identifier <<
" expects enum, but ("
2216 <<
expr2c(arg1, *
this) <<
") has type `"
2217 <<
type2c(arg1.type(), *
this) <<
'`';
2224 exprt lowered = in_range.lower(*
this);
2236 id2string(identifier) +
" expects one or two operands",
2241 auto &pointer_expr = expr.
arguments()[0];
2242 if(pointer_expr.type().id() == ID_array)
2245 dest_type.base_type().set(ID_C_constant,
true);
2248 else if(pointer_expr.type().id() != ID_pointer)
2251 id2string(identifier) +
" expects a pointer as first argument",
2267 const auto &subtype =
2269 if(subtype.id() == ID_empty)
2273 " expects a size when given a void pointer",
2279 size_expr = std::move(size_expr_opt.value());
2295 irep_idt shadow_memory_builtin_id =
2296 shadow_memory_builtin->get_identifier();
2298 const auto builtin_code_type =
2302 builtin_code_type.has_ellipsis() &&
2303 builtin_code_type.parameters().empty(),
2304 "Shadow memory builtins should be an ellipsis with 0 parameter");
2310 shadow_memory_builtin_id, shadow_memory_builtin->type(), ID_C};
2311 new_symbol.base_name = shadow_memory_builtin_id;
2322 f_op = std::move(*shadow_memory_builtin);
2328 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2331 !parameters.empty(),
2332 "GCC polymorphic built-ins should have at least one parameter");
2337 if(parameters.front().type().id() == ID_pointer)
2339 identifier_with_type =
2346 identifier_with_type =
2350 gcc_polymorphic->set_identifier(identifier_with_type);
2354 for(std::size_t i = 0; i < parameters.size(); ++i)
2356 const std::string base_name =
"p_" + std::to_string(i);
2361 id2string(identifier_with_type) +
"::" + base_name;
2364 new_symbol.
type = parameters[i].type();
2367 new_symbol.
mode = ID_C;
2369 parameters[i].set_identifier(new_symbol.
name);
2370 parameters[i].set_base_name(new_symbol.
base_name);
2376 identifier_with_type, gcc_polymorphic->type(), ID_C};
2377 new_symbol.base_name = identifier_with_type;
2385 new_symbol.value = implementation;
2390 f_op = std::move(*gcc_polymorphic);
2402 if(identifier==
"malloc" ||
2403 identifier==
"realloc" ||
2404 identifier==
"reallocf" ||
2405 identifier==
"valloc")
2412 new_symbol.base_name=identifier;
2414 new_symbol.type.
set(ID_C_incomplete,
true);
2422 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2432 if(f_op_type.
id() == ID_mathematical_function)
2434 const auto &mathematical_function_type =
2438 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2441 error() <<
"expected " << mathematical_function_type.domain().size()
2442 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2450 if(p.first.type() != p.second)
2463 expr.
swap(function_application);
2467 if(f_op_type.
id()!=ID_pointer)
2470 error() <<
"expected function/function pointer as argument but got '"
2476 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2483 tmp.
set(ID_C_implicit,
true);
2488 if(f_op.
type().
id()!=ID_code)
2491 error() <<
"expected code as argument" <<
eom;
2514 if(f_op.
id()!=ID_symbol)
2550 if(arg.type().id() != ID_pointer)
2554 "pointer_in_range_dfcc expects pointer-typed arguments",
2565 error() <<
"same_object expects two operands" <<
eom;
2571 exprt same_object_expr=
2575 return same_object_expr;
2582 error() <<
"get_must expects two operands" <<
eom;
2592 return std::move(get_must_expr);
2599 error() <<
"get_may expects two operands" <<
eom;
2609 return std::move(get_may_expr);
2616 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2625 return same_object_expr;
2632 error() <<
"buffer_size expects one operand" <<
eom;
2642 return buffer_size_expr;
2650 error() <<
"is_list expects one operand" <<
eom;
2657 expr.
arguments()[0].type().id() != ID_pointer ||
2662 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2670 return std::move(is_list_expr);
2678 error() <<
"is_dll expects one operand" <<
eom;
2685 expr.
arguments()[0].type().id() != ID_pointer ||
2690 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2698 return std::move(is_dll_expr);
2706 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2713 expr.
arguments()[0].type().id() != ID_pointer ||
2718 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2726 return std::move(is_cyclic_dll_expr);
2734 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2741 args_no_cast.reserve(expr.
arguments().size());
2742 for(
const auto &argument : expr.
arguments())
2746 args_no_cast.back().type().id() != ID_pointer ||
2751 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2758 is_sentinel_dll_expr.
operands() = args_no_cast;
2761 return std::move(is_sentinel_dll_expr);
2769 error() <<
"is_cstring expects one operand" <<
eom;
2775 if(expr.
arguments()[0].type().id() != ID_pointer)
2778 error() <<
"is_cstring expects a pointer operand" <<
eom;
2785 return std::move(is_cstring_expr);
2793 error() <<
"cstrlen expects one operand" <<
eom;
2799 if(expr.
arguments()[0].type().id() != ID_pointer)
2802 error() <<
"cstrlen expects a pointer operand" <<
eom;
2809 return std::move(cstrlen_expr);
2816 error() <<
"is_zero_string expects one operand" <<
eom;
2824 is_zero_string_expr.
set(ID_C_lvalue,
true);
2827 return std::move(is_zero_string_expr);
2834 error() <<
"zero_string_length expects one operand" <<
eom;
2840 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2842 zero_string_length_expr.
set(ID_C_lvalue,
true);
2845 return zero_string_length_expr;
2852 error() <<
"dynamic_object expects one argument" <<
eom;
2861 return is_dynamic_object_expr;
2868 error() <<
"live_object expects one argument" <<
eom;
2877 return live_object_expr;
2884 error() <<
"pointer_in_range expects three arguments" <<
eom;
2894 return pointer_in_range_expr;
2901 error() <<
"writeable_object expects one argument" <<
eom;
2910 return writeable_object_expr;
2918 error() <<
"separate expects two or more arguments" <<
eom;
2927 return separate_expr;
2934 error() <<
"pointer_offset expects one argument" <<
eom;
2950 error() <<
"object_size expects one operand" <<
eom;
2959 return std::move(object_size_expr);
2966 error() <<
"pointer_object expects one argument" <<
eom;
2977 else if(identifier==
"__builtin_bswap16" ||
2978 identifier==
"__builtin_bswap32" ||
2979 identifier==
"__builtin_bswap64")
2984 error() << identifier <<
" expects one operand" <<
eom;
2994 return std::move(bswap_expr);
2997 identifier ==
"__builtin_rotateleft8" ||
2998 identifier ==
"__builtin_rotateleft16" ||
2999 identifier ==
"__builtin_rotateleft32" ||
3000 identifier ==
"__builtin_rotateleft64" ||
3001 identifier ==
"__builtin_rotateright8" ||
3002 identifier ==
"__builtin_rotateright16" ||
3003 identifier ==
"__builtin_rotateright32" ||
3004 identifier ==
"__builtin_rotateright64")
3010 error() << identifier <<
" expects two operands" <<
eom;
3016 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
3017 identifier ==
"__builtin_rotateleft16" ||
3018 identifier ==
"__builtin_rotateleft32" ||
3019 identifier ==
"__builtin_rotateleft64")
3026 return std::move(rotate_expr);
3028 else if(identifier==
"__builtin_nontemporal_load")
3033 error() << identifier <<
" expects one operand" <<
eom;
3042 if(ptr_arg.
type().
id()!=ID_pointer)
3045 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3054 identifier ==
"__builtin_fpclassify" ||
3060 error() << identifier <<
" expects six arguments" <<
eom;
3073 if(fp_value.
type().
id() != ID_floatbv)
3076 error() <<
"non-floating-point argument for " << identifier <<
eom;
3084 const auto &arguments = expr.
arguments();
3103 identifier==
"__builtin_isnan")
3108 error() <<
"isnan expects one operand" <<
eom;
3126 error() <<
"isfinite expects one operand" <<
eom;
3138 identifier==
"__builtin_inf")
3145 return std::move(inf_expr);
3154 return std::move(inff_expr);
3163 return std::move(infl_expr);
3176 error() <<
"abs-functions expect one operand" <<
eom;
3185 return std::move(abs_expr);
3195 error() <<
"fmod-functions expect two operands" <<
eom;
3209 return std::move(fmod_expr);
3219 error() <<
"remainder-functions expect two operands" <<
eom;
3233 return std::move(floatbv_rem_expr);
3240 error() <<
"allocate expects two operands" <<
eom;
3249 return std::move(malloc_expr);
3258 error() << identifier <<
" expects one operand" <<
eom;
3262 const auto ¶m_id = expr.
arguments().front().id();
3263 if(!(param_id == ID_dereference || param_id == ID_member ||
3264 param_id == ID_symbol || param_id == ID_ptrmember ||
3265 param_id == ID_constant || param_id == ID_typecast ||
3266 param_id == ID_index))
3269 error() <<
"Tracking history of " << param_id
3270 <<
" expressions is not supported yet." <<
eom;
3279 return std::move(old_expr);
3284 identifier==
"__builtin_isinf")
3289 error() << identifier <<
" expects one operand" <<
eom;
3297 if(fp_value.
type().
id() != ID_floatbv)
3300 error() <<
"non-floating-point argument for " << identifier <<
eom;
3309 else if(identifier ==
"__builtin_isinf_sign")
3314 error() << identifier <<
" expects one operand" <<
eom;
3324 if(fp_value.
type().
id() != ID_floatbv)
3327 error() <<
"non-floating-point argument for " << identifier <<
eom;
3345 identifier ==
"__builtin_isnormal")
3350 error() << identifier <<
" expects one operand" <<
eom;
3358 if(fp_value.
type().
id() != ID_floatbv)
3361 error() <<
"non-floating-point argument for " << identifier <<
eom;
3373 identifier==
"__builtin_signbit" ||
3374 identifier==
"__builtin_signbitf" ||
3375 identifier==
"__builtin_signbitl")
3380 error() << identifier <<
" expects one operand" <<
eom;
3391 else if(identifier==
"__builtin_popcount" ||
3392 identifier==
"__builtin_popcountl" ||
3393 identifier==
"__builtin_popcountll" ||
3394 identifier==
"__popcnt16" ||
3395 identifier==
"__popcnt" ||
3396 identifier==
"__popcnt64")
3401 error() << identifier <<
" expects one operand" <<
eom;
3410 return std::move(popcount_expr);
3413 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
3414 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
3415 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
3420 error() << identifier <<
" expects one operand" <<
eom;
3431 return std::move(clz);
3434 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3435 identifier ==
"__builtin_ctzll")
3440 error() << identifier <<
" expects one operand" <<
eom;
3450 return std::move(ctz);
3453 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3454 identifier ==
"__builtin_ffsll")
3459 error() << identifier <<
" expects one operand" <<
eom;
3468 return std::move(ffs);
3470 else if(identifier==
"__builtin_expect")
3481 error() <<
"__builtin_expect expects two arguments" <<
eom;
3489 else if(identifier==
"__builtin_object_size")
3498 error() <<
"__builtin_object_size expects two arguments" <<
eom;
3515 error() <<
"__builtin_object_size expects constant as second argument, "
3523 if(arg1==0 || arg1==1)
3536 else if(identifier==
"__builtin_choose_expr")
3542 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3557 else if(identifier==
"__builtin_constant_p")
3564 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3580 tmp1.
id() == ID_typecast &&
3586 .
id() == ID_string_constant)
3598 else if(identifier==
"__builtin_classify_type")
3605 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3618 if(type.
id() == ID_c_bit_field)
3621 unsigned type_number;
3623 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3632 type.
id() == ID_empty
3634 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
3636 : (type.
id() == ID_pointer || type.
id() == ID_array)
3638 : type.
id() == ID_floatbv
3640 : (type.
id() == ID_complex &&
3643 : type.
id() == ID_struct
3645 : type.
id() == ID_union
3656 identifier ==
"__builtin_add_overflow" ||
3657 identifier ==
"__builtin_sadd_overflow" ||
3658 identifier ==
"__builtin_saddl_overflow" ||
3659 identifier ==
"__builtin_saddll_overflow" ||
3660 identifier ==
"__builtin_uadd_overflow" ||
3661 identifier ==
"__builtin_uaddl_overflow" ||
3662 identifier ==
"__builtin_uaddll_overflow" ||
3663 identifier ==
"__builtin_add_overflow_p")
3668 identifier ==
"__builtin_sub_overflow" ||
3669 identifier ==
"__builtin_ssub_overflow" ||
3670 identifier ==
"__builtin_ssubl_overflow" ||
3671 identifier ==
"__builtin_ssubll_overflow" ||
3672 identifier ==
"__builtin_usub_overflow" ||
3673 identifier ==
"__builtin_usubl_overflow" ||
3674 identifier ==
"__builtin_usubll_overflow" ||
3675 identifier ==
"__builtin_sub_overflow_p")
3680 identifier ==
"__builtin_mul_overflow" ||
3681 identifier ==
"__builtin_smul_overflow" ||
3682 identifier ==
"__builtin_smull_overflow" ||
3683 identifier ==
"__builtin_smulll_overflow" ||
3684 identifier ==
"__builtin_umul_overflow" ||
3685 identifier ==
"__builtin_umull_overflow" ||
3686 identifier ==
"__builtin_umulll_overflow" ||
3687 identifier ==
"__builtin_mul_overflow_p")
3692 identifier ==
"__builtin_bitreverse8" ||
3693 identifier ==
"__builtin_bitreverse16" ||
3694 identifier ==
"__builtin_bitreverse32" ||
3695 identifier ==
"__builtin_bitreverse64")
3700 std::ostringstream error_message;
3701 error_message <<
"error: " << identifier <<
" expects one operand";
3709 bitreverse.add_source_location() = source_location;
3711 return std::move(bitreverse);
3727 std::ostringstream error_message;
3728 error_message << identifier <<
" takes exactly 3 arguments, but "
3729 << expr.
arguments().size() <<
" were provided";
3743 auto const raise_wrong_argument_error =
3745 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3746 std::ostringstream error_message;
3747 error_message <<
"error: " << identifier <<
" has signature "
3748 << identifier <<
"(integral, integral, integral"
3749 << (_p ?
"" :
"*") <<
"), "
3750 <<
"but argument " << argument_number <<
" ("
3751 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3752 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3756 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3758 auto const &argument = expr.
arguments()[arg_index];
3762 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3766 !is__p_variant && (
result.type().id() != ID_pointer ||
3770 raise_wrong_argument_error(
result, 3, is__p_variant);
3789 std::ostringstream error_message;
3790 error_message <<
"error: " << identifier
3791 <<
" takes exactly two arguments, but "
3792 << expr.
arguments().size() <<
" were provided";
3823 if(code_type.
get_bool(ID_C_incomplete))
3827 else if(code_type.
is_KnR())
3831 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3833 arguments.push_back(
3839 if(parameters.size() > arguments.size())
3842 error() <<
"not enough function arguments" <<
eom;
3846 else if(parameters.size() != arguments.size())
3849 error() <<
"wrong number of function arguments: "
3850 <<
"expected " << parameters.size() <<
", but got "
3851 << arguments.size() <<
eom;
3855 for(std::size_t i=0; i<arguments.size(); i++)
3857 exprt &op=arguments[i];
3863 else if(i < parameters.size())
3869 op.
get(ID_statement) == ID_assign && op.
type().
id() != ID_bool)
3872 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3881 if(op.
type().
id() == ID_array)
3884 dest_type.base_type().set(ID_C_constant,
true);
3902 if(o_type.
id()==ID_vector)
3921 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3976 if(o_type0.
id()==ID_vector &&
3977 o_type1.
id()==ID_vector)
3991 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3996 expr.
type() = o_type0;
4000 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
4005 expr.
type() = o_type1;
4009 if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4022 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
4023 expr.
id()==ID_mult || expr.
id()==ID_div)
4025 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
4030 else if(type0==type1)
4039 else if(expr.
id()==ID_mod)
4043 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
4051 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
4052 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
4061 else if(type0.
id()==ID_bool)
4063 if(expr.
id()==ID_bitand)
4065 else if(expr.
id() == ID_bitnand)
4067 else if(expr.
id()==ID_bitor)
4069 else if(expr.
id()==ID_bitxor)
4078 else if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4082 (type0.
id() == ID_signedbv || type0.
id() == ID_unsignedbv))
4084 expr.
type() = type0;
4090 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4106 if(o_type0.
id()==ID_vector &&
4107 o_type1.
id()==ID_vector)
4123 o_type0.
id() == ID_vector &&
4141 if(expr.
id()==ID_shr)
4145 if(op0_type.
id()==ID_unsignedbv)
4150 else if(op0_type.
id()==ID_signedbv)
4161 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4175 base_type.
id() == ID_struct_tag &&
4179 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4183 base_type.
id() == ID_union_tag &&
4187 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4191 base_type.
id() == ID_empty &&
4195 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4198 else if(base_type.
id() == ID_empty)
4216 if(expr.
id()==ID_minus ||
4217 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
4219 if(type0.
id()==ID_pointer &&
4220 type1.
id()==ID_pointer)
4233 if(type0.
id()==ID_pointer &&
4234 (type1.
id()==ID_bool ||
4235 type1.
id()==ID_c_bool ||
4236 type1.
id()==ID_unsignedbv ||
4237 type1.
id()==ID_signedbv ||
4238 type1.
id()==ID_c_bit_field ||
4239 type1.
id()==ID_c_enum_tag))
4247 else if(expr.
id()==ID_plus ||
4248 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
4250 exprt *p_op, *int_op;
4252 if(type0.
id()==ID_pointer)
4257 else if(type1.
id()==ID_pointer)
4264 p_op=int_op=
nullptr;
4268 const typet &int_op_type = int_op->
type();
4270 if(int_op_type.
id()==ID_bool ||
4271 int_op_type.
id()==ID_c_bool ||
4272 int_op_type.
id()==ID_unsignedbv ||
4273 int_op_type.
id()==ID_signedbv ||
4274 int_op_type.
id()==ID_c_bit_field ||
4275 int_op_type.
id()==ID_c_enum_tag)
4286 if(expr.
id()==ID_side_effect)
4292 error() <<
"operator '" << op_name <<
"' not defined for types '"
4323 if(type0.
id()==ID_empty)
4326 error() <<
"cannot assign void" <<
eom;
4333 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4346 if(type0.
id() == ID_array)
4349 error() <<
"direct assignments to arrays not permitted" <<
eom;
4356 if(op0.
type().
id()==ID_c_bit_field)
4363 expr.
type()=o_type0;
4365 if(statement==ID_assign)
4370 else if(statement==ID_assign_shl ||
4371 statement==ID_assign_shr)
4373 if(o_type0.
id() == ID_vector)
4378 o_type1.
id() == ID_vector &&
4379 vector_o_type0.element_type() ==
4381 is_number(vector_o_type0.element_type()))
4397 if(statement==ID_assign_shl)
4407 if(underlying_type.
id()==ID_unsignedbv ||
4408 underlying_type.
id()==ID_c_bool)
4410 expr.
set(ID_statement, ID_assign_lshr);
4413 else if(underlying_type.
id()==ID_signedbv)
4415 expr.
set(ID_statement, ID_assign_ashr);
4421 else if(statement==ID_assign_bitxor ||
4422 statement==ID_assign_bitand ||
4423 statement==ID_assign_bitor)
4426 if(o_type0.
id()==ID_bool ||
4427 o_type0.
id()==ID_c_bool)
4432 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4433 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4438 else if(o_type0.
id()==ID_c_enum_tag ||
4439 o_type0.
id()==ID_unsignedbv ||
4440 o_type0.
id()==ID_signedbv ||
4441 o_type0.
id()==ID_c_bit_field)
4445 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4446 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4451 else if(o_type0.
id()==ID_vector &&
4452 o_type1.
id()==ID_vector)
4463 o_type0.
id() == ID_vector &&
4464 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
4465 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
4466 o_type1.
id() == ID_signedbv))
4475 if(o_type0.
id()==ID_pointer &&
4476 (statement==ID_assign_minus || statement==ID_assign_plus))
4481 else if(o_type0.
id()==ID_vector &&
4482 o_type1.
id()==ID_vector)
4492 else if(o_type0.
id() == ID_vector)
4498 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4504 else if(o_type0.
id()==ID_bool ||
4505 o_type0.
id()==ID_c_bool)
4510 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4511 op1.
type().
id() == ID_signedbv)
4522 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4530 error() <<
"assignment '" << statement <<
"' not defined for types '"
4560 if(e.
id() == ID_infinity)
4566 if(e.
id() == ID_address_of)
4571 e.
id() == ID_typecast || e.
id() == ID_array_of || e.
id() == ID_plus ||
4572 e.
id() == ID_mult || e.
id() == ID_array || e.
id() == ID_with ||
4573 e.
id() == ID_struct || e.
id() == ID_union || e.
id() == ID_empty_union ||
4574 e.
id() == ID_equal || e.
id() == ID_notequal || e.
id() == ID_lt ||
4575 e.
id() == ID_le || e.
id() == ID_gt || e.
id() == ID_ge ||
4576 e.
id() == ID_if || e.
id() == ID_not || e.
id() == ID_and ||
4577 e.
id() == ID_or || e.
id() == ID_bitnot || e.
id() == ID_bitand ||
4578 e.
id() == ID_bitor || e.
id() == ID_bitxor || e.
id() == ID_vector)
4582 return is_constant(op);
4592 if(e.
id() == ID_symbol)
4594 return e.
type().
id() == ID_code ||
4597 else if(e.
id() == ID_array && e.
get_bool(ID_C_string_constant))
4599 else if(e.
id() == ID_label)
4601 else if(e.
id() == ID_index)
4608 else if(e.
id() == ID_member)
4612 else if(e.
id() == ID_dereference)
4618 else if(e.
id() == ID_string_constant)
4630 const auto rounding_mode =
4639 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4654 error() <<
"conversion to integer constant failed" <<
eom;
4662 const std::string &message)
const
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
bitvector_typet index_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
floatbv_typet long_double_type()
bitvector_typet c_index_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
const declaratorst & declarators() const
const exprt & size() 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.
const typet & underlying_type() const
const typet & underlying_type() const
bool is_incomplete() const
enum types may be incomplete
static optionalt< std::string > check_address_can_be_taken(const typet &)
virtual void typecheck_obeys_contract_call(side_effect_expr_function_callt &expr)
Checks an obeys_contract predicate occurrence.
virtual void typecheck_expr_main(exprt &expr)
symbol_table_baset & symbol_table
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
virtual optionalt< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
exprt typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void typecheck_typed_target_call(side_effect_expr_function_callt &expr)
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.
struct configt::ansi_ct ansi_c
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
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.
The Boolean constant false.
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
IEEE-floating-point equality.
static ieee_float_spect single_precision()
static ieee_float_spect double_precision()
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt zero(const floatbv_typet &type)
The trinary if-then-else operator.
An expression denoting infinity.
Thrown when we can't handle something in an input source file.
source_locationt source_location
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.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Expression for finding the size (in bytes) of the object a pointer points to.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
The plus expression Associativity is not specified.
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
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
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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.
source_locationt & add_source_location()
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.
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_blockt & to_code_block(const codet &code)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
bool has_suffix(const std::string &s, const std::string &suffix)
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
const type_with_subtypet & to_type_with_subtype(const typet &type)