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;
322 error() <<
"quantifier must not contain side effects" <<
eom;
327 for(
auto &binding : bindings)
330 if(expr.
id() == ID_lambda)
334 for(
auto &binding : bindings)
335 domain.push_back(binding.type());
345 else if(expr.
id()==ID_label)
349 else if(expr.
id()==ID_array)
353 else if(expr.
id()==ID_complex)
358 else if(expr.
id() == ID_complex_real)
362 if(op.
type().
id() != ID_complex)
367 error() <<
"real part retrieval expects numerical operand, "
375 expr.
swap(complex_real_expr);
383 complex_real_expr.
set(ID_C_lvalue,
true);
386 complex_real_expr.
type().
set(ID_C_constant,
true);
388 expr.
swap(complex_real_expr);
391 else if(expr.
id() == ID_complex_imag)
395 if(op.
type().
id() != ID_complex)
400 error() <<
"real part retrieval expects numerical operand, "
408 expr.
swap(complex_imag_expr);
416 complex_imag_expr.
set(ID_C_lvalue,
true);
419 complex_imag_expr.
type().
set(ID_C_constant,
true);
421 expr.
swap(complex_imag_expr);
424 else if(expr.
id()==ID_generic_selection)
441 for(
auto &irep : generic_associations)
443 if(irep.get(ID_type_arg) != ID_default)
445 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
454 const typet &op_type = op.type();
456 for(
const auto &irep : generic_associations)
458 if(irep.get(ID_type_arg) == ID_default)
459 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
460 else if(op_type ==
static_cast<const typet &
>(irep.find(ID_type_arg)))
462 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
469 expr.
swap(default_match);
473 error() <<
"unmatched generic selection: " <<
to_string(op.type())
479 expr.
swap(assoc_match);
484 else if(expr.
id()==ID_gcc_asm_input ||
485 expr.
id()==ID_gcc_asm_output ||
486 expr.
id()==ID_gcc_asm_clobbered_register)
489 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
490 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
495 expr.
id() == ID_C_spec_assigns || expr.
id() == ID_C_spec_frees ||
496 expr.
id() == ID_target_list)
514 expr.
set(ID_C_lvalue,
true);
549 symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C};
550 symbol.base_name=ID_gcc_builtin_va_arg;
579 error() <<
"builtin_offsetof expects no operands" <<
eom;
586 const exprt &member =
static_cast<const exprt &
>(expr.
add(ID_designator));
590 for(
const auto &op : member.
operands())
592 if(op.id() == ID_member)
594 if(type.
id() != ID_union_tag && type.
id() != ID_struct_tag)
597 error() <<
"offsetof of member expects struct/union type, "
603 irep_idt component_name = op.get(ID_component_name);
617 if(type.
id() == ID_struct_tag)
622 if(!o_opt.has_value())
625 error() <<
"offsetof failed to determine offset of '"
626 << component_name <<
"'" <<
eom;
642 for(
const auto &c : struct_union_type.
components())
646 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
650 if(type.
id() == ID_struct_tag)
655 if(!o_opt.has_value())
658 error() <<
"offsetof failed to determine offset of '"
659 << component_name <<
"'" <<
eom;
669 typet tmp = c.type();
672 type.
id() == ID_union_tag || type.
id() == ID_struct_tag);
682 error() <<
"offset-of of member failed to find component '"
683 << component_name <<
"' in '" <<
to_string(type) <<
"'"
690 else if(op.id() == ID_index)
692 if(type.
id()!=ID_array)
695 error() <<
"offsetof of index expects array type" <<
eom;
704 auto element_size_opt =
707 if(!element_size_opt.has_value())
710 error() <<
"offsetof failed to determine array element size" <<
eom;
733 if(expr.
id()==ID_side_effect &&
734 expr.
get(ID_statement)==ID_function_call)
739 else if(expr.
id()==ID_side_effect &&
740 expr.
get(ID_statement)==ID_statement_expression)
745 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
751 auto &bindings = binary_expr.op0().operands();
753 for(
auto &binding : bindings)
762 error() <<
"forall/exists expects one declarator exactly" <<
eom;
769 symbol_table_baset::symbolst::const_iterator s_it =
775 error() <<
"failed to find bound symbol `" << identifier
776 <<
"' in symbol table" <<
eom;
780 const symbolt &symbol = s_it->second;
787 error() <<
"unexpected quantified symbol" <<
eom;
811 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
815 expr.
type()=p_it->second;
816 expr.
set(ID_C_lvalue,
true);
821 asm_label_mapt::const_iterator entry=
825 identifier=entry->second;
831 if(
lookup(identifier, symbol_ptr))
834 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
838 const symbolt &symbol=*symbol_ptr;
843 error() <<
"did not expect a type symbol here, but got '"
862 expr.
set(ID_C_cformat, base_name);
877 else if(identifier==
"__func__" ||
878 identifier==
"__FUNCTION__" ||
879 identifier==
"__PRETTY_FUNCTION__")
885 s.
set(ID_C_lvalue,
true);
896 expr.
set(ID_C_lvalue,
true);
898 if(expr.
type().
id()==ID_code)
901 tmp.
set(ID_C_implicit,
true);
920 if(last_statement==ID_expression)
926 if(op.
type().
id()==ID_array)
968 if(type.
id()==ID_c_bit_field)
972 if(op.
id() == ID_comma || op.
id() == ID_side_effect)
986 if(!size_of_opt.has_value())
989 error() <<
"type has no size: "
994 new_expr = size_of_opt.value();
1000 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
1004 else if(type.
id() == ID_bool)
1007 error() <<
"sizeof cannot be applied to single bits" <<
eom;
1010 else if(type.
id() == ID_empty)
1019 (type.
id() == ID_struct_tag &&
1021 (type.
id() == ID_union_tag &&
1023 (type.
id() == ID_c_enum_tag &&
1028 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1035 if(!size_of_opt.has_value())
1042 new_expr = size_of_opt.value();
1046 new_expr.
swap(expr);
1048 expr.
add(ID_C_c_sizeof_type)=type;
1054 ID_statement_expression,
void_type(), location);
1056 decl_block.set_statement(ID_decl_block);
1069 expr.
swap(comma_expr);
1075 typet argument_type;
1083 argument_type=op_type;
1107 decl_block.set_statement(ID_decl_block);
1118 std::move(side_effect_expr), ID_comma, op, op.
type()};
1119 op.
swap(comma_expr);
1125 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1126 op.
id() != ID_initializer_list)
1139 for(
const auto &c : union_type.components())
1141 if(c.type() == op.
type())
1147 expr.
set(ID_C_lvalue,
true);
1155 <<
"' not found in union" <<
eom;
1162 if(op.
id()==ID_initializer_list)
1171 exprt tmp(ID_compound_literal, expr.
type());
1175 if(op.
id()==ID_array &&
1176 expr.
type().
id()==ID_array &&
1181 expr.
set(ID_C_lvalue,
true);
1186 if(expr_type.
id()==ID_empty)
1192 if(expr_type == op_type)
1197 if(expr_type.
id()==ID_vector)
1200 if(op_type.
id()==ID_vector)
1202 else if(op_type.
id()==ID_signedbv ||
1203 op_type.
id()==ID_unsignedbv)
1210 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1218 else if(op_type.
id()==ID_array)
1223 if(error_opt.has_value())
1229 else if(op_type.
id()==ID_empty)
1231 if(expr_type.
id()!=ID_empty)
1234 error() <<
"type cast from void only permitted to void, but got '"
1239 else if(op_type.
id()==ID_vector)
1246 if((expr_type.
id()==ID_signedbv ||
1247 expr_type.
id()==ID_unsignedbv) &&
1256 <<
"' not permitted" <<
eom;
1263 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1279 if(expr_type.
id()==ID_pointer)
1280 expr.
set(ID_C_lvalue,
true);
1297 const typet &array_type = array_expr.
type();
1298 const typet &index_type = index_expr.
type();
1301 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1302 array_type.
id() != ID_vector &&
1303 (index_type.
id() == ID_array || index_type.
id() == ID_pointer ||
1304 index_type.
id() == ID_vector))
1305 std::swap(array_expr, index_expr);
1313 const typet final_array_type = array_expr.
type();
1315 if(final_array_type.
id()==ID_array ||
1316 final_array_type.
id()==ID_vector)
1320 if(array_expr.
get_bool(ID_C_lvalue))
1321 expr.
set(ID_C_lvalue,
true);
1323 if(final_array_type.
get_bool(ID_C_constant))
1324 expr.
type().
set(ID_C_constant,
true);
1326 else if(final_array_type.
id()==ID_pointer)
1332 std::swap(summands, expr.
operands());
1334 expr.
id(ID_dereference);
1335 expr.
set(ID_C_lvalue,
true);
1341 error() <<
"operator [] must take array/vector or pointer but got '"
1350 if(expr.
op0().
type().
id() == ID_floatbv)
1352 if(expr.
id()==ID_equal)
1353 expr.
id(ID_ieee_float_equal);
1354 else if(expr.
id()==ID_notequal)
1355 expr.
id(ID_ieee_float_notequal);
1368 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1376 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1378 if(o_type0 == o_type1)
1380 if(o_type0.
id() != ID_array)
1401 if(type0.
id()==ID_pointer)
1403 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1406 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1407 expr.
id()==ID_ge || expr.
id()==ID_gt)
1411 if(type0.
id()==ID_string_constant)
1413 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1420 if(type0.
id()==ID_pointer &&
1427 if(type1.
id()==ID_pointer &&
1447 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1455 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1466 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1469 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1477 auto subtype_width =
1486 if(expr.
id() == ID_notequal)
1487 expr.
id(ID_vector_notequal);
1495 const typet &op0_type = op.type();
1497 if(op0_type.
id() == ID_array)
1502 index_expr.
set(ID_C_lvalue,
true);
1503 op.swap(index_expr);
1505 else if(op0_type.
id() == ID_pointer)
1516 error() <<
"ptrmember operator requires pointer or array type "
1517 "on left hand side, but got '"
1531 if(type.
id() != ID_struct_tag && type.
id() != ID_union_tag)
1534 error() <<
"member operator requires structure type "
1535 "on left hand side but got '"
1546 error() <<
"member operator got incomplete " << type.
id()
1547 <<
" type on left hand side" <<
eom;
1552 expr.
get(ID_component_name);
1568 error() <<
"member '" << component_name <<
"' not found in '"
1581 expr.
set(ID_C_lvalue,
true);
1585 struct_union_type.
get_bool(ID_C_constant))
1587 expr.
type().
set(ID_C_constant,
true);
1593 if(!identifier.
empty())
1594 expr.
set(ID_C_identifier, identifier);
1598 if(access==ID_private)
1601 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1613 const typet o_type0=operands[0].type();
1614 const typet o_type1=operands[1].type();
1615 const typet o_type2=operands[2].type();
1619 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1627 if(operands[1].type().
id()==ID_pointer &&
1628 operands[2].type().
id()!=ID_pointer)
1630 else if(operands[2].type().
id()==ID_pointer &&
1631 operands[1].type().
id()!=ID_pointer)
1634 if(operands[1].type().
id()==ID_pointer &&
1635 operands[2].type().
id()==ID_pointer &&
1636 operands[1].type()!=operands[2].type())
1683 if(operands[1].type().
id()==ID_empty ||
1684 operands[2].type().
id()==ID_empty)
1691 operands[1].type() != operands[2].type() ||
1692 operands[1].type().
id() == ID_array)
1697 if(operands[1].type() == operands[2].type())
1699 expr.
type()=operands[1].type();
1705 if(operands[1].get_bool(ID_C_lvalue) &&
1706 operands[2].get_bool(ID_C_lvalue))
1707 expr.
set(ID_C_lvalue,
true);
1713 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1726 if(operands.size()!=2)
1729 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1735 if_exprt if_expr(operands[0], operands[0], operands[1]);
1752 if(error_opt.has_value())
1756 if(op.
id()==ID_label)
1769 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1775 tmp.
set(ID_C_implicit,
false);
1780 if(op.
id()==ID_struct ||
1781 op.
id()==ID_union ||
1782 op.
id()==ID_array ||
1783 op.
id()==ID_string_constant)
1791 else if(op.
type().
id()==ID_code)
1798 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1812 if(op_type.
id()==ID_array)
1820 else if(op_type.
id()==ID_pointer)
1825 expr.
type().
id() == ID_empty &&
1829 error() <<
"dereferencing void pointer" <<
eom;
1837 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1842 expr.
set(ID_C_lvalue,
true);
1853 if(expr.
type().
id()==ID_code)
1856 tmp.
set(ID_C_implicit,
true);
1866 if(statement==ID_preincrement ||
1867 statement==ID_predecrement ||
1868 statement==ID_postincrement ||
1869 statement==ID_postdecrement)
1878 <<
"' not an lvalue" <<
eom;
1889 if(type0.
id() == ID_c_enum_tag)
1895 error() <<
"operator '" << statement <<
"' given incomplete type '"
1905 else if(type0.
id() == ID_c_bit_field)
1909 typet type_before{type0};
1911 expr.
type()=underlying_type;
1915 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1924 else if(type0.
id() == ID_pointer)
1932 error() <<
"operator '" << statement <<
"' not defined for type '"
1939 else if(statement==ID_function_call)
1942 else if(statement==ID_statement_expression)
1944 else if(statement==ID_gcc_conditional_expression)
1949 error() <<
"unknown side effect: " << statement <<
eom;
1961 "expression must be a " CPROVER_PREFIX "typed_target function call");
1968 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
1979 arg0.source_location()};
1983 if(!size.has_value())
1987 "typed_target of type " +
1989 arg0.source_location()};
1998 arguments.push_back(size.value());
2000 if(arg0.type().id() == ID_pointer)
2016 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
2021 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
2028 auto &function_pointer = expr.
arguments()[0];
2031 function_pointer.type().id() != ID_pointer ||
2033 !function_pointer.get_bool(ID_C_lvalue))
2037 "obeys_contract must be a function pointer lvalue expression",
2038 function_pointer.source_location());
2045 "obeys_contract must have no ternary operator",
2046 function_pointer.source_location());
2050 auto &address_of_contract = expr.
arguments()[1];
2053 address_of_contract.id() != ID_address_of ||
2055 address_of_contract.
type().
id() != ID_pointer ||
2060 "obeys_contract must must be a function symbol",
2061 address_of_contract.source_location());
2064 if(function_pointer.type() != address_of_contract.type())
2068 "obeys_contract must have the same function pointer type",
2090 error() <<
"function_call side effect expects two operands" <<
eom;
2099 if(f_op.
id()==ID_symbol)
2103 asm_label_mapt::const_iterator entry=
2106 identifier=entry->second;
2123 identifier ==
"__noop" &&
2137 identifier ==
"__builtin_shuffle" &&
2145 else if(identifier ==
"__builtin_shufflevector")
2166 error() <<
"equal expects two operands" <<
eom;
2177 error() <<
"equal expects two operands of same type" <<
eom;
2181 expr.
swap(equality_expr);
2195 overflow.
id(ID_minus);
2200 overflow.id(ID_mult);
2205 overflow.id(ID_plus);
2210 overflow.id(ID_shl);
2215 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
2216 of.add_source_location() = overflow.source_location();
2228 overflow.add_source_location() = tmp.source_location();
2229 expr.
swap(overflow);
2237 std::ostringstream error_message;
2238 error_message << identifier <<
" takes exactly 1 argument, but "
2239 << expr.
arguments().size() <<
" were provided";
2247 std::ostringstream error_message;
2248 error_message << identifier <<
" expects enum, but ("
2249 <<
expr2c(arg1, *
this) <<
") has type `"
2250 <<
type2c(arg1.type(), *
this) <<
'`';
2257 exprt lowered = in_range.lower(*
this);
2269 id2string(identifier) +
" expects one or two operands",
2274 auto &pointer_expr = expr.
arguments()[0];
2275 if(pointer_expr.type().id() == ID_array)
2278 dest_type.base_type().set(ID_C_constant,
true);
2281 else if(pointer_expr.type().id() != ID_pointer)
2284 id2string(identifier) +
" expects a pointer as first argument",
2300 const auto &subtype =
2302 if(subtype.id() == ID_empty)
2306 " expects a size when given a void pointer",
2312 size_expr = std::move(size_expr_opt.value());
2328 irep_idt shadow_memory_builtin_id =
2329 shadow_memory_builtin->get_identifier();
2331 const auto builtin_code_type =
2335 builtin_code_type.has_ellipsis() &&
2336 builtin_code_type.parameters().empty(),
2337 "Shadow memory builtins should be an ellipsis with 0 parameter");
2343 shadow_memory_builtin_id, shadow_memory_builtin->type(), ID_C};
2344 new_symbol.base_name = shadow_memory_builtin_id;
2355 f_op = std::move(*shadow_memory_builtin);
2361 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2364 !parameters.empty(),
2365 "GCC polymorphic built-ins should have at least one parameter");
2370 if(parameters.front().type().id() == ID_pointer)
2372 identifier_with_type =
2379 identifier_with_type =
2383 gcc_polymorphic->set_identifier(identifier_with_type);
2387 for(std::size_t i = 0; i < parameters.size(); ++i)
2394 id2string(identifier_with_type) +
"::" + base_name;
2397 new_symbol.
type = parameters[i].type();
2400 new_symbol.
mode = ID_C;
2402 parameters[i].set_identifier(new_symbol.
name);
2403 parameters[i].set_base_name(new_symbol.
base_name);
2409 identifier_with_type, gcc_polymorphic->type(), ID_C};
2410 new_symbol.base_name = identifier_with_type;
2418 new_symbol.value = implementation;
2423 f_op = std::move(*gcc_polymorphic);
2435 if(identifier==
"malloc" ||
2436 identifier==
"realloc" ||
2437 identifier==
"reallocf" ||
2438 identifier==
"valloc")
2445 new_symbol.base_name=identifier;
2447 new_symbol.type.
set(ID_C_incomplete,
true);
2455 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2465 if(f_op_type.
id() == ID_mathematical_function)
2467 const auto &mathematical_function_type =
2471 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2474 error() <<
"expected " << mathematical_function_type.domain().size()
2475 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2483 if(p.first.type() != p.second)
2496 expr.
swap(function_application);
2500 if(f_op_type.
id()!=ID_pointer)
2503 error() <<
"expected function/function pointer as argument but got '"
2509 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2516 tmp.
set(ID_C_implicit,
true);
2521 if(f_op.
type().
id()!=ID_code)
2524 error() <<
"expected code as argument" <<
eom;
2547 if(f_op.
id()!=ID_symbol)
2583 if(arg.type().id() != ID_pointer)
2587 "pointer_in_range_dfcc expects pointer-typed arguments",
2588 arg.source_location()};
2598 error() <<
"same_object expects two operands" <<
eom;
2604 exprt same_object_expr=
2608 return same_object_expr;
2615 error() <<
"get_must expects two operands" <<
eom;
2625 return std::move(get_must_expr);
2632 error() <<
"get_may expects two operands" <<
eom;
2642 return std::move(get_may_expr);
2649 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2658 return same_object_expr;
2665 error() <<
"buffer_size expects one operand" <<
eom;
2675 return buffer_size_expr;
2683 error() <<
"is_list expects one operand" <<
eom;
2690 expr.
arguments()[0].type().id() != ID_pointer ||
2695 error() <<
"is_list expects a struct-pointer operand" <<
eom;
2703 return std::move(is_list_expr);
2711 error() <<
"is_dll expects one operand" <<
eom;
2718 expr.
arguments()[0].type().id() != ID_pointer ||
2723 error() <<
"is_dll expects a struct-pointer operand" <<
eom;
2731 return std::move(is_dll_expr);
2739 error() <<
"is_cyclic_dll expects one operand" <<
eom;
2746 expr.
arguments()[0].type().id() != ID_pointer ||
2751 error() <<
"is_cyclic_dll expects a struct-pointer operand" <<
eom;
2759 return std::move(is_cyclic_dll_expr);
2767 error() <<
"is_sentinel_dll expects two or three operands" <<
eom;
2774 args_no_cast.reserve(expr.
arguments().size());
2775 for(
const auto &argument : expr.
arguments())
2779 args_no_cast.back().type().id() != ID_pointer ||
2784 error() <<
"is_sentinel_dll_node expects struct-pointer operands"
2791 is_sentinel_dll_expr.
operands() = args_no_cast;
2794 return std::move(is_sentinel_dll_expr);
2802 error() <<
"is_cstring expects one operand" <<
eom;
2808 if(expr.
arguments()[0].type().id() != ID_pointer)
2811 error() <<
"is_cstring expects a pointer operand" <<
eom;
2818 return std::move(is_cstring_expr);
2826 error() <<
"cstrlen expects one operand" <<
eom;
2832 if(expr.
arguments()[0].type().id() != ID_pointer)
2835 error() <<
"cstrlen expects a pointer operand" <<
eom;
2842 return std::move(cstrlen_expr);
2849 error() <<
"is_zero_string expects one operand" <<
eom;
2857 is_zero_string_expr.
set(ID_C_lvalue,
true);
2860 return std::move(is_zero_string_expr);
2867 error() <<
"zero_string_length expects one operand" <<
eom;
2873 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2875 zero_string_length_expr.
set(ID_C_lvalue,
true);
2878 return zero_string_length_expr;
2885 error() <<
"dynamic_object expects one argument" <<
eom;
2894 return is_dynamic_object_expr;
2901 error() <<
"live_object expects one argument" <<
eom;
2910 return live_object_expr;
2917 error() <<
"pointer_in_range expects three arguments" <<
eom;
2927 return pointer_in_range_expr;
2934 error() <<
"writeable_object expects one argument" <<
eom;
2943 return writeable_object_expr;
2951 error() <<
"separate expects two or more arguments" <<
eom;
2960 return separate_expr;
2967 error() <<
"pointer_offset expects one argument" <<
eom;
2983 error() <<
"object_size expects one operand" <<
eom;
2992 return std::move(object_size_expr);
2999 error() <<
"pointer_object expects one argument" <<
eom;
3010 else if(identifier==
"__builtin_bswap16" ||
3011 identifier==
"__builtin_bswap32" ||
3012 identifier==
"__builtin_bswap64")
3017 error() << identifier <<
" expects one operand" <<
eom;
3027 return std::move(bswap_expr);
3030 identifier ==
"__builtin_rotateleft8" ||
3031 identifier ==
"__builtin_rotateleft16" ||
3032 identifier ==
"__builtin_rotateleft32" ||
3033 identifier ==
"__builtin_rotateleft64" ||
3034 identifier ==
"__builtin_rotateright8" ||
3035 identifier ==
"__builtin_rotateright16" ||
3036 identifier ==
"__builtin_rotateright32" ||
3037 identifier ==
"__builtin_rotateright64")
3043 error() << identifier <<
" expects two operands" <<
eom;
3049 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
3050 identifier ==
"__builtin_rotateleft16" ||
3051 identifier ==
"__builtin_rotateleft32" ||
3052 identifier ==
"__builtin_rotateleft64")
3059 return std::move(rotate_expr);
3061 else if(identifier==
"__builtin_nontemporal_load")
3066 error() << identifier <<
" expects one operand" <<
eom;
3075 if(ptr_arg.
type().
id()!=ID_pointer)
3078 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
3087 identifier ==
"__builtin_fpclassify" ||
3093 error() << identifier <<
" expects six arguments" <<
eom;
3106 if(fp_value.
type().
id() != ID_floatbv)
3109 error() <<
"non-floating-point argument for " << identifier <<
eom;
3117 const auto &arguments = expr.
arguments();
3136 identifier==
"__builtin_isnan")
3141 error() <<
"isnan expects one operand" <<
eom;
3159 error() <<
"isfinite expects one operand" <<
eom;
3171 identifier==
"__builtin_inf")
3178 return std::move(inf_expr);
3187 return std::move(inff_expr);
3196 return std::move(infl_expr);
3209 error() <<
"abs-functions expect one operand" <<
eom;
3218 return std::move(abs_expr);
3228 error() <<
"fmod-functions expect two operands" <<
eom;
3242 return std::move(fmod_expr);
3252 error() <<
"remainder-functions expect two operands" <<
eom;
3266 return std::move(floatbv_rem_expr);
3273 error() <<
"allocate expects two operands" <<
eom;
3282 return std::move(malloc_expr);
3291 error() << identifier <<
" expects one operand" <<
eom;
3295 const auto ¶m_id = expr.
arguments().front().id();
3296 if(!(param_id == ID_dereference || param_id == ID_member ||
3297 param_id == ID_symbol || param_id == ID_ptrmember ||
3298 param_id == ID_constant || param_id == ID_typecast ||
3299 param_id == ID_index))
3302 error() <<
"Tracking history of " << param_id
3303 <<
" expressions is not supported yet." <<
eom;
3312 return std::move(old_expr);
3317 identifier==
"__builtin_isinf")
3322 error() << identifier <<
" expects one operand" <<
eom;
3330 if(fp_value.
type().
id() != ID_floatbv)
3333 error() <<
"non-floating-point argument for " << identifier <<
eom;
3342 else if(identifier ==
"__builtin_isinf_sign")
3347 error() << identifier <<
" expects one operand" <<
eom;
3357 if(fp_value.
type().
id() != ID_floatbv)
3360 error() <<
"non-floating-point argument for " << identifier <<
eom;
3378 identifier ==
"__builtin_isnormal")
3383 error() << identifier <<
" expects one operand" <<
eom;
3391 if(fp_value.
type().
id() != ID_floatbv)
3394 error() <<
"non-floating-point argument for " << identifier <<
eom;
3406 identifier==
"__builtin_signbit" ||
3407 identifier==
"__builtin_signbitf" ||
3408 identifier==
"__builtin_signbitl")
3413 error() << identifier <<
" expects one operand" <<
eom;
3424 else if(identifier==
"__builtin_popcount" ||
3425 identifier==
"__builtin_popcountl" ||
3426 identifier==
"__builtin_popcountll" ||
3427 identifier==
"__popcnt16" ||
3428 identifier==
"__popcnt" ||
3429 identifier==
"__popcnt64")
3434 error() << identifier <<
" expects one operand" <<
eom;
3443 return std::move(popcount_expr);
3446 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
3447 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
3448 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
3453 error() << identifier <<
" expects one operand" <<
eom;
3463 return std::move(clz);
3466 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
3467 identifier ==
"__builtin_ctzll")
3472 error() << identifier <<
" expects one operand" <<
eom;
3482 return std::move(ctz);
3485 identifier ==
"__builtin_ffs" || identifier ==
"__builtin_ffsl" ||
3486 identifier ==
"__builtin_ffsll")
3491 error() << identifier <<
" expects one operand" <<
eom;
3500 return std::move(ffs);
3502 else if(identifier==
"__builtin_expect")
3513 error() <<
"__builtin_expect expects two arguments" <<
eom;
3522 identifier ==
"__builtin_object_size" ||
3523 identifier ==
"__builtin_dynamic_object_size")
3534 error() <<
"__builtin_object_size expects two arguments" <<
eom;
3551 error() <<
"__builtin_object_size expects constant as second argument, "
3559 if(arg1==0 || arg1==1)
3572 else if(identifier==
"__builtin_choose_expr")
3578 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3593 else if(identifier==
"__builtin_constant_p")
3600 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3616 tmp1.
id() == ID_typecast &&
3622 .
id() == ID_string_constant)
3634 else if(identifier==
"__builtin_classify_type")
3641 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3652 const typet &type =
object.type().
id() == ID_c_bit_field
3656 unsigned type_number;
3658 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3666 type_number = type.
id() == ID_empty ? 0u
3667 : (type.
id() == ID_bool || type.
id() == ID_c_bool) ? 4u
3668 : (type.
id() == ID_pointer || type.
id() == ID_array) ? 5u
3669 : type.
id() == ID_floatbv ? 8u
3670 : (type.
id() == ID_complex &&
3673 : type.
id() == ID_struct_tag ? 12u
3674 : type.
id() == ID_union_tag
3685 identifier ==
"__builtin_add_overflow" ||
3686 identifier ==
"__builtin_sadd_overflow" ||
3687 identifier ==
"__builtin_saddl_overflow" ||
3688 identifier ==
"__builtin_saddll_overflow" ||
3689 identifier ==
"__builtin_uadd_overflow" ||
3690 identifier ==
"__builtin_uaddl_overflow" ||
3691 identifier ==
"__builtin_uaddll_overflow" ||
3692 identifier ==
"__builtin_add_overflow_p")
3697 identifier ==
"__builtin_sub_overflow" ||
3698 identifier ==
"__builtin_ssub_overflow" ||
3699 identifier ==
"__builtin_ssubl_overflow" ||
3700 identifier ==
"__builtin_ssubll_overflow" ||
3701 identifier ==
"__builtin_usub_overflow" ||
3702 identifier ==
"__builtin_usubl_overflow" ||
3703 identifier ==
"__builtin_usubll_overflow" ||
3704 identifier ==
"__builtin_sub_overflow_p")
3709 identifier ==
"__builtin_mul_overflow" ||
3710 identifier ==
"__builtin_smul_overflow" ||
3711 identifier ==
"__builtin_smull_overflow" ||
3712 identifier ==
"__builtin_smulll_overflow" ||
3713 identifier ==
"__builtin_umul_overflow" ||
3714 identifier ==
"__builtin_umull_overflow" ||
3715 identifier ==
"__builtin_umulll_overflow" ||
3716 identifier ==
"__builtin_mul_overflow_p")
3721 identifier ==
"__builtin_bitreverse8" ||
3722 identifier ==
"__builtin_bitreverse16" ||
3723 identifier ==
"__builtin_bitreverse32" ||
3724 identifier ==
"__builtin_bitreverse64")
3729 std::ostringstream error_message;
3730 error_message <<
"error: " << identifier <<
" expects one operand";
3738 bitreverse.add_source_location() = source_location;
3740 return std::move(bitreverse);
3756 std::ostringstream error_message;
3757 error_message << identifier <<
" takes exactly 3 arguments, but "
3758 << expr.
arguments().size() <<
" were provided";
3772 auto const raise_wrong_argument_error =
3774 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3775 std::ostringstream error_message;
3776 error_message <<
"error: " << identifier <<
" has signature "
3777 << identifier <<
"(integral, integral, integral"
3778 << (_p ?
"" :
"*") <<
"), "
3779 <<
"but argument " << argument_number <<
" ("
3780 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3781 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3785 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3787 auto const &argument = expr.
arguments()[arg_index];
3791 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3795 !is__p_variant && (
result.type().id() != ID_pointer ||
3799 raise_wrong_argument_error(
result, 3, is__p_variant);
3818 std::ostringstream error_message;
3819 error_message <<
"error: " << identifier
3820 <<
" takes exactly two arguments, but "
3821 << expr.
arguments().size() <<
" were provided";
3852 if(code_type.
get_bool(ID_C_incomplete))
3856 else if(code_type.
is_KnR())
3860 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3862 arguments.push_back(
3868 if(parameters.size() > arguments.size())
3871 error() <<
"not enough function arguments" <<
eom;
3875 else if(parameters.size() != arguments.size())
3878 error() <<
"wrong number of function arguments: "
3879 <<
"expected " << parameters.size() <<
", but got "
3880 << arguments.size() <<
eom;
3884 for(std::size_t i=0; i<arguments.size(); i++)
3886 exprt &op=arguments[i];
3892 else if(i < parameters.size())
3898 op.
get(ID_statement) == ID_assign && op.
type().
id() != ID_bool)
3901 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3910 if(op.
type().
id() == ID_array)
3913 dest_type.base_type().set(ID_C_constant,
true);
3931 if(o_type.
id()==ID_vector)
3950 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3974 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3975 const auto s1 = numeric_cast<mp_integer>(type1.
size());
4005 if(o_type0.
id()==ID_vector &&
4006 o_type1.
id()==ID_vector)
4020 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
4025 expr.
type() = o_type0;
4029 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
4034 expr.
type() = o_type1;
4038 if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4051 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
4052 expr.
id()==ID_mult || expr.
id()==ID_div)
4054 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
4059 else if(type0==type1)
4068 else if(expr.
id()==ID_mod)
4072 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
4080 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
4081 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
4090 else if(type0.
id()==ID_bool)
4092 if(expr.
id()==ID_bitand)
4094 else if(expr.
id() == ID_bitnand)
4096 else if(expr.
id()==ID_bitor)
4098 else if(expr.
id()==ID_bitxor)
4107 else if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
4111 (type0.
id() == ID_signedbv || type0.
id() == ID_unsignedbv))
4113 expr.
type() = type0;
4119 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4135 if(o_type0.
id()==ID_vector &&
4136 o_type1.
id()==ID_vector)
4152 o_type0.
id() == ID_vector &&
4170 if(expr.
id()==ID_shr)
4174 if(op0_type.
id()==ID_unsignedbv)
4179 else if(op0_type.
id()==ID_signedbv)
4190 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
4204 base_type.
id() == ID_struct_tag &&
4208 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4212 base_type.
id() == ID_union_tag &&
4216 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4220 base_type.
id() == ID_empty &&
4224 error() <<
"pointer arithmetic with unknown object size" <<
eom;
4227 else if(base_type.
id() == ID_empty)
4245 if(expr.
id()==ID_minus ||
4246 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
4248 if(type0.
id()==ID_pointer &&
4249 type1.
id()==ID_pointer)
4262 if(type0.
id()==ID_pointer &&
4263 (type1.
id()==ID_bool ||
4264 type1.
id()==ID_c_bool ||
4265 type1.
id()==ID_unsignedbv ||
4266 type1.
id()==ID_signedbv ||
4267 type1.
id()==ID_c_bit_field ||
4268 type1.
id()==ID_c_enum_tag))
4276 else if(expr.
id()==ID_plus ||
4277 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
4279 exprt *p_op, *int_op;
4281 if(type0.
id()==ID_pointer)
4286 else if(type1.
id()==ID_pointer)
4293 p_op=int_op=
nullptr;
4297 const typet &int_op_type = int_op->
type();
4299 if(int_op_type.
id()==ID_bool ||
4300 int_op_type.
id()==ID_c_bool ||
4301 int_op_type.
id()==ID_unsignedbv ||
4302 int_op_type.
id()==ID_signedbv ||
4303 int_op_type.
id()==ID_c_bit_field ||
4304 int_op_type.
id()==ID_c_enum_tag)
4315 if(expr.
id()==ID_side_effect)
4321 error() <<
"operator '" << op_name <<
"' not defined for types '"
4352 if(type0.
id()==ID_empty)
4355 error() <<
"cannot assign void" <<
eom;
4362 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
4375 if(type0.
id() == ID_array)
4378 error() <<
"direct assignments to arrays not permitted" <<
eom;
4384 if(op0.
type() != op1.
type() && op0.
type().
id() == ID_c_bit_field)
4393 expr.
type()=o_type0;
4395 if(statement==ID_assign)
4400 else if(statement==ID_assign_shl ||
4401 statement==ID_assign_shr)
4403 if(o_type0.
id() == ID_vector)
4408 o_type1.
id() == ID_vector &&
4409 vector_o_type0.element_type() ==
4411 is_number(vector_o_type0.element_type()))
4427 if(statement==ID_assign_shl)
4437 if(underlying_type.
id()==ID_unsignedbv ||
4438 underlying_type.
id()==ID_c_bool)
4440 expr.
set(ID_statement, ID_assign_lshr);
4443 else if(underlying_type.
id()==ID_signedbv)
4445 expr.
set(ID_statement, ID_assign_ashr);
4451 else if(statement==ID_assign_bitxor ||
4452 statement==ID_assign_bitand ||
4453 statement==ID_assign_bitor)
4456 if(o_type0.
id()==ID_bool ||
4457 o_type0.
id()==ID_c_bool)
4462 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4463 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4468 else if(o_type0.
id()==ID_c_enum_tag ||
4469 o_type0.
id()==ID_unsignedbv ||
4470 o_type0.
id()==ID_signedbv ||
4471 o_type0.
id()==ID_c_bit_field)
4475 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4476 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
4481 else if(o_type0.
id()==ID_vector &&
4482 o_type1.
id()==ID_vector)
4493 o_type0.
id() == ID_vector &&
4494 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
4495 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
4496 o_type1.
id() == ID_signedbv))
4505 if(o_type0.
id()==ID_pointer &&
4506 (statement==ID_assign_minus || statement==ID_assign_plus))
4511 else if(o_type0.
id()==ID_vector &&
4512 o_type1.
id()==ID_vector)
4522 else if(o_type0.
id() == ID_vector)
4528 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4534 else if(o_type0.
id()==ID_bool ||
4535 o_type0.
id()==ID_c_bool)
4540 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
4541 op1.
type().
id() == ID_signedbv)
4552 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
4560 error() <<
"assignment '" << statement <<
"' not defined for types '"
4590 if(e.
id() == ID_infinity)
4596 if(e.
id() == ID_address_of)
4601 e.
id() == ID_typecast || e.
id() == ID_array_of || e.
id() == ID_plus ||
4602 e.
id() == ID_mult || e.
id() == ID_array || e.
id() == ID_with ||
4603 e.
id() == ID_struct || e.
id() == ID_union || e.
id() == ID_empty_union ||
4604 e.
id() == ID_equal || e.
id() == ID_notequal || e.
id() == ID_lt ||
4605 e.
id() == ID_le || e.
id() == ID_gt || e.
id() == ID_ge ||
4606 e.
id() == ID_if || e.
id() == ID_not || e.
id() == ID_and ||
4607 e.
id() == ID_or || e.
id() == ID_bitnot || e.
id() == ID_bitand ||
4608 e.
id() == ID_bitor || e.
id() == ID_bitxor || e.
id() == ID_vector)
4612 return is_constant(op);
4622 if(e.
id() == ID_symbol)
4624 return e.
type().
id() == ID_code ||
4627 else if(e.
id() == ID_array && e.
get_bool(ID_C_string_constant))
4629 else if(e.
id() == ID_label)
4631 else if(e.
id() == ID_index)
4638 else if(e.
id() == ID_member)
4642 else if(e.
id() == ID_dereference)
4648 else if(e.
id() == ID_string_constant)
4662 const auto rounding_mode =
4672 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4689 error() <<
"conversion to integer constant failed" <<
eom;
4697 const std::string &message)
const
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool builtin_factory(const irep_idt &identifier, bool support_float16_type, symbol_table_baset &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
unsignedbv_typet unsigned_int_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
bitvector_typet char_type()
floatbv_typet long_double_type()
bitvector_typet c_index_type()
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 c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Operator to return the address of an object.
const declaratorst & declarators() const
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
A base class for relations, i.e., binary predicates whose two operands have the same type.
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 typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
bool is_boolean() const
Return whether the expression represents a Boolean.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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.
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
mstreamt & warning() const
mstreamt & result() const
message_handlert & get_message_handler()
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...
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
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 componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
bool is_incomplete() const
A struct/union may be incomplete.
const componentst & components() const
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
const irep_idt & display_name() const
Return language specific display name if present.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
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.
typet && with_source_location(source_locationt location) &&
This is a 'fluent style' method for creating a new type with an added-on source location.
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
const typet & element_type() const
The type of the elements of the vector.
typet index_type() const
The type of any index expression into an instance of this type.
A predicate that indicates that the object pointed to is writeable.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_frontend_declt & to_code_frontend_decl(const codet &code)
const code_blockt & to_code_block(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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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)