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)
179 else if(expr.
id()==ID_constant)
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)
248 assert(subtypes.size()==2);
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)
434 if(op.type().id() == ID_bool)
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));
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));
461 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
463 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
470 expr.
swap(default_match);
474 error() <<
"unmatched generic selection: " <<
to_string(op.type())
480 expr.
swap(assoc_match);
485 else if(expr.
id()==ID_gcc_asm_input ||
486 expr.
id()==ID_gcc_asm_output ||
487 expr.
id()==ID_gcc_asm_clobbered_register)
490 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
491 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
495 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
513 expr.
set(ID_C_lvalue,
true);
550 symbol.
name=ID_gcc_builtin_va_arg;
551 symbol.
type=symbol_type;
581 error() <<
"builtin_offsetof expects no operands" <<
eom;
596 if(m_it->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=m_it->get(ID_component_name);
611 assert(type.
id()==ID_union || type.
id()==ID_struct);
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;
675 assert(type.
id()==ID_union || type.
id()==ID_struct);
685 error() <<
"offset-of of member failed to find component '"
686 << component_name <<
"' in '" <<
to_string(type) <<
"'"
693 else if(m_it->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_tablet::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 '"
864 if(expr.
id()==ID_constant &&
866 expr.
set(ID_C_cformat, base_name);
881 else if(identifier==
"__func__" ||
882 identifier==
"__FUNCTION__" ||
883 identifier==
"__PRETTY_FUNCTION__")
889 s.
set(ID_C_lvalue,
true);
900 expr.
set(ID_C_lvalue,
true);
902 if(expr.
type().
id()==ID_code)
905 tmp.
set(ID_C_implicit,
true);
924 if(last_statement==ID_expression)
930 if(op.
type().
id()==ID_array)
963 if(op.
type().
id() == ID_bool)
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);
1038 exprt comma_expr(ID_comma, expr.
type());
1040 expr.
swap(comma_expr);
1046 typet argument_type;
1054 argument_type=op_type;
1078 decl_block.set_statement(ID_decl_block);
1090 op.
swap(comma_expr);
1096 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1097 op.
id() != ID_initializer_list)
1105 if(op.
type().
id() == ID_bool)
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 else if(op_type.
id()==ID_empty)
1196 if(expr_type.
id()!=ID_empty)
1199 error() <<
"type cast from void only permitted to void, but got '"
1204 else if(op_type.
id()==ID_vector)
1211 if((expr_type.
id()==ID_signedbv ||
1212 expr_type.
id()==ID_unsignedbv) &&
1221 <<
"' not permitted" <<
eom;
1228 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1244 if(expr_type.
id()==ID_pointer)
1245 expr.
set(ID_C_lvalue,
true);
1262 const typet &array_type = array_expr.
type();
1266 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1267 array_type.
id() != ID_vector &&
1270 std::swap(array_expr, index_expr);
1278 const typet final_array_type = array_expr.
type();
1280 if(final_array_type.
id()==ID_array ||
1281 final_array_type.
id()==ID_vector)
1285 if(array_expr.
get_bool(ID_C_lvalue))
1286 expr.
set(ID_C_lvalue,
true);
1288 if(final_array_type.
get_bool(ID_C_constant))
1289 expr.
type().
set(ID_C_constant,
true);
1291 else if(final_array_type.
id()==ID_pointer)
1297 std::swap(summands, expr.
operands());
1299 expr.
id(ID_dereference);
1300 expr.
set(ID_C_lvalue,
true);
1306 error() <<
"operator [] must take array/vector or pointer but got '"
1315 if(expr.
op0().
type().
id() == ID_floatbv)
1317 if(expr.
id()==ID_equal)
1318 expr.
id(ID_ieee_float_equal);
1319 else if(expr.
id()==ID_notequal)
1320 expr.
id(ID_ieee_float_notequal);
1333 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1341 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1345 if(o_type0.
id() != ID_array)
1366 if(type0.
id()==ID_pointer)
1368 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1371 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1372 expr.
id()==ID_ge || expr.
id()==ID_gt)
1376 if(type0.
id()==ID_string_constant)
1378 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1385 if(type0.
id()==ID_pointer &&
1392 if(type1.
id()==ID_pointer &&
1412 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1420 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1431 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1434 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1442 auto subtype_width =
1449 if(expr.
id() == ID_notequal)
1450 expr.
id(ID_vector_notequal);
1458 const typet &op0_type = op.type();
1460 if(op0_type.
id() == ID_array)
1465 index_expr.
set(ID_C_lvalue,
true);
1466 op.swap(index_expr);
1468 else if(op0_type.
id() == ID_pointer)
1474 op.swap(deref_expr);
1479 error() <<
"ptrmember operator requires pointer or array type "
1480 "on left hand side, but got '"
1496 if(type.
id()!=ID_struct &&
1497 type.
id()!=ID_union)
1500 error() <<
"member operator requires structure type "
1501 "on left hand side but got '"
1512 error() <<
"member operator got incomplete " << type.
id()
1513 <<
" type on left hand side" <<
eom;
1518 expr.
get(ID_component_name);
1534 error() <<
"member '" << component_name <<
"' not found in '"
1547 expr.
set(ID_C_lvalue,
true);
1550 expr.
type().
set(ID_C_constant,
true);
1555 if(!identifier.
empty())
1556 expr.
set(ID_C_identifier, identifier);
1560 if(access==ID_private)
1563 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1572 assert(operands.size()==3);
1575 const typet o_type0=operands[0].type();
1576 const typet o_type1=operands[1].type();
1577 const typet o_type2=operands[2].type();
1581 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1589 if(operands[1].type().
id()==ID_pointer &&
1590 operands[2].type().
id()!=ID_pointer)
1592 else if(operands[2].type().
id()==ID_pointer &&
1593 operands[1].type().
id()!=ID_pointer)
1596 if(operands[1].type().
id()==ID_pointer &&
1597 operands[2].type().
id()==ID_pointer &&
1598 operands[1].type()!=operands[2].type())
1605 if(operands[1].type().subtype().
id()==ID_empty &&
1609 else if(operands[2].type().subtype().
id()==ID_empty &&
1613 else if(operands[1].type().subtype().
id()!=ID_code ||
1614 operands[2].type().subtype().
id()!=ID_code)
1638 if(operands[1].type().
id()==ID_empty ||
1639 operands[2].type().
id()==ID_empty)
1646 operands[1].type() != operands[2].type() ||
1647 operands[1].type().
id() == ID_array)
1652 if(operands[1].type() == operands[2].type())
1654 expr.
type()=operands[1].type();
1660 if(operands[1].get_bool(ID_C_lvalue) &&
1661 operands[2].get_bool(ID_C_lvalue))
1662 expr.
set(ID_C_lvalue,
true);
1668 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1681 if(operands.size()!=2)
1684 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1690 if_exprt if_expr(operands[0], operands[0], operands[1]);
1705 if(op.
type().
id()==ID_c_bit_field)
1708 error() <<
"cannot take address of a bit field" <<
eom;
1712 if(op.
type().
id() == ID_bool)
1715 error() <<
"cannot take address of a single bit" <<
eom;
1720 if(op.
id()==ID_label)
1733 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1739 tmp.
set(ID_C_implicit,
false);
1744 if(op.
id()==ID_struct ||
1745 op.
id()==ID_union ||
1746 op.
id()==ID_array ||
1747 op.
id()==ID_string_constant)
1755 else if(op.
type().
id()==ID_code)
1762 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1776 if(op_type.
id()==ID_array)
1784 else if(op_type.
id()==ID_pointer)
1792 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1797 expr.
set(ID_C_lvalue,
true);
1808 if(expr.
type().
id()==ID_code)
1811 tmp.
set(ID_C_implicit,
true);
1821 if(statement==ID_preincrement ||
1822 statement==ID_predecrement ||
1823 statement==ID_postincrement ||
1824 statement==ID_postdecrement)
1833 <<
"' not an lvalue" <<
eom;
1844 if(type0.
id() == ID_c_enum_tag)
1850 error() <<
"operator '" << statement <<
"' given incomplete type '"
1860 else if(type0.
id() == ID_c_bit_field)
1865 expr.
type()=underlying_type;
1867 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1876 else if(type0.
id() == ID_pointer)
1884 error() <<
"operator '" << statement <<
"' not defined for type '"
1891 else if(statement==ID_function_call)
1894 else if(statement==ID_statement_expression)
1896 else if(statement==ID_gcc_conditional_expression)
1901 error() <<
"unknown side effect: " << statement <<
eom;
1912 error() <<
"function_call side effect expects two operands" <<
eom;
1921 if(f_op.
id()==ID_symbol)
1925 asm_label_mapt::const_iterator entry=
1928 identifier=entry->second;
1939 identifier ==
"__noop" &&
1953 identifier ==
"__builtin_shuffle" &&
1962 identifier ==
"__builtin_shufflevector" &&
1974 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1977 !parameters.empty(),
1978 "GCC polymorphic built-ins should have at least one parameter");
1983 if(parameters.front().type().id() == ID_pointer)
1985 identifier_with_type =
id2string(identifier) +
"_" +
1987 parameters.front().type().subtype(), *
this);
1991 identifier_with_type =
1995 gcc_polymorphic->set_identifier(identifier_with_type);
1999 for(std::size_t i = 0; i < parameters.size(); ++i)
2006 id2string(identifier_with_type) +
"::" + base_name;
2009 new_symbol.
type = parameters[i].type();
2012 new_symbol.
mode = ID_C;
2014 parameters[i].set_identifier(new_symbol.
name);
2015 parameters[i].set_base_name(new_symbol.
base_name);
2022 new_symbol.
name = identifier_with_type;
2023 new_symbol.
base_name = identifier_with_type;
2025 new_symbol.
type = gcc_polymorphic->type();
2026 new_symbol.
mode = ID_C;
2033 new_symbol.
value = implementation;
2038 f_op = std::move(*gcc_polymorphic);
2050 if(identifier==
"malloc" ||
2051 identifier==
"realloc" ||
2052 identifier==
"reallocf" ||
2053 identifier==
"valloc")
2060 new_symbol.
name=identifier;
2064 new_symbol.
type.
set(ID_C_incomplete,
true);
2072 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2082 if(f_op_type.
id() == ID_mathematical_function)
2084 const auto &mathematical_function_type =
2088 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2091 error() <<
"expected " << mathematical_function_type.domain().size()
2092 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2100 if(p.first.type() != p.second)
2113 expr.
swap(function_application);
2117 if(f_op_type.
id()!=ID_pointer)
2120 error() <<
"expected function/function pointer as argument but got '"
2126 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2133 tmp.
set(ID_C_implicit,
true);
2138 if(f_op.
type().
id()!=ID_code)
2141 error() <<
"expected code as argument" <<
eom;
2164 if(f_op.
id()!=ID_symbol)
2186 error() <<
"same_object expects two operands" <<
eom;
2192 exprt same_object_expr=
2196 return same_object_expr;
2203 error() <<
"get_must expects two operands" <<
eom;
2213 return std::move(get_must_expr);
2220 error() <<
"get_may expects two operands" <<
eom;
2230 return std::move(get_may_expr);
2237 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2246 return same_object_expr;
2253 error() <<
"buffer_size expects one operand" <<
eom;
2263 return buffer_size_expr;
2270 error() <<
"is_zero_string expects one operand" <<
eom;
2278 is_zero_string_expr.
set(ID_C_lvalue,
true);
2281 return std::move(is_zero_string_expr);
2288 error() <<
"zero_string_length expects one operand" <<
eom;
2294 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2296 zero_string_length_expr.
set(ID_C_lvalue,
true);
2299 return zero_string_length_expr;
2306 error() <<
"dynamic_object expects one argument" <<
eom;
2315 return is_dynamic_object_expr;
2322 error() <<
"pointer_offset expects one argument" <<
eom;
2338 error() <<
"object_size expects one operand" <<
eom;
2348 return std::move(object_size_expr);
2355 error() <<
"pointer_object expects one argument" <<
eom;
2366 else if(identifier==
"__builtin_bswap16" ||
2367 identifier==
"__builtin_bswap32" ||
2368 identifier==
"__builtin_bswap64")
2373 error() << identifier <<
" expects one operand" <<
eom;
2383 return std::move(bswap_expr);
2386 identifier ==
"__builtin_rotateleft8" ||
2387 identifier ==
"__builtin_rotateleft16" ||
2388 identifier ==
"__builtin_rotateleft32" ||
2389 identifier ==
"__builtin_rotateleft64" ||
2390 identifier ==
"__builtin_rotateright8" ||
2391 identifier ==
"__builtin_rotateright16" ||
2392 identifier ==
"__builtin_rotateright32" ||
2393 identifier ==
"__builtin_rotateright64")
2399 error() << identifier <<
" expects two operands" <<
eom;
2405 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2406 identifier ==
"__builtin_rotateleft16" ||
2407 identifier ==
"__builtin_rotateleft32" ||
2408 identifier ==
"__builtin_rotateleft64")
2415 return std::move(rotate_expr);
2417 else if(identifier==
"__builtin_nontemporal_load")
2422 error() << identifier <<
" expects one operand" <<
eom;
2431 if(ptr_arg.
type().
id()!=ID_pointer)
2434 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2443 identifier ==
"__builtin_fpclassify" ||
2449 error() << identifier <<
" expects six arguments" <<
eom;
2462 if(fp_value.
type().
id() != ID_floatbv)
2465 error() <<
"non-floating-point argument for " << identifier <<
eom;
2473 const auto &arguments = expr.
arguments();
2492 identifier==
"__builtin_isnan")
2497 error() <<
"isnan expects one operand" <<
eom;
2515 error() <<
"isfinite expects one operand" <<
eom;
2527 identifier==
"__builtin_inf")
2534 return std::move(inf_expr);
2543 return std::move(inff_expr);
2552 return std::move(infl_expr);
2564 error() <<
"abs-functions expect one operand" <<
eom;
2573 return std::move(abs_expr);
2583 error() <<
"fmod-functions expect two operands" <<
eom;
2597 return std::move(fmod_expr);
2607 error() <<
"remainder-functions expect two operands" <<
eom;
2621 return std::move(floatbv_rem_expr);
2628 error() <<
"allocate expects two operands" <<
eom;
2637 return std::move(malloc_expr);
2646 error() << identifier <<
" expects one or two operands" <<
eom;
2653 const auto &pointer_expr = expr.
arguments()[0];
2654 if(pointer_expr.type().id() != ID_pointer)
2657 error() << identifier <<
" expects a pointer as first argument" <<
eom;
2674 if(subtype.id() == ID_empty)
2677 error() << identifier <<
" expects a size when given a void pointer"
2683 if(!size_expr_opt.has_value())
2686 error() << identifier <<
" was given object pointer without size"
2691 size_expr = std::move(size_expr_opt.value());
2701 return std::move(ok_expr);
2710 error() << identifier <<
" expects one operand" <<
eom;
2719 return std::move(old_expr);
2724 identifier==
"__builtin_isinf")
2729 error() << identifier <<
" expects one operand" <<
eom;
2737 if(fp_value.
type().
id() != ID_floatbv)
2740 error() <<
"non-floating-point argument for " << identifier <<
eom;
2749 else if(identifier ==
"__builtin_isinf_sign")
2754 error() << identifier <<
" expects one operand" <<
eom;
2764 if(fp_value.
type().
id() != ID_floatbv)
2767 error() <<
"non-floating-point argument for " << identifier <<
eom;
2785 identifier ==
"__builtin_isnormal")
2790 error() << identifier <<
" expects one operand" <<
eom;
2798 if(fp_value.
type().
id() != ID_floatbv)
2801 error() <<
"non-floating-point argument for " << identifier <<
eom;
2813 identifier==
"__builtin_signbit" ||
2814 identifier==
"__builtin_signbitf" ||
2815 identifier==
"__builtin_signbitl")
2820 error() << identifier <<
" expects one operand" <<
eom;
2831 else if(identifier==
"__builtin_popcount" ||
2832 identifier==
"__builtin_popcountl" ||
2833 identifier==
"__builtin_popcountll" ||
2834 identifier==
"__popcnt16" ||
2835 identifier==
"__popcnt" ||
2836 identifier==
"__popcnt64")
2841 error() << identifier <<
" expects one operand" <<
eom;
2850 return std::move(popcount_expr);
2853 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2854 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2855 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2860 error() << identifier <<
" expects one operand" <<
eom;
2871 return std::move(clz);
2874 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
2875 identifier ==
"__builtin_ctzll")
2880 error() << identifier <<
" expects one operand" <<
eom;
2890 return std::move(ctz);
2897 error() <<
"equal expects two operands" <<
eom;
2910 error() <<
"equal expects two operands of same type" <<
eom;
2914 return std::move(equality_expr);
2916 else if(identifier==
"__builtin_expect")
2927 error() <<
"__builtin_expect expects two arguments" <<
eom;
2935 else if(identifier==
"__builtin_object_size")
2944 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2961 error() <<
"__builtin_object_size expects constant as second argument, "
2969 if(arg1==0 || arg1==1)
2982 else if(identifier==
"__builtin_choose_expr")
2988 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
3003 else if(identifier==
"__builtin_constant_p")
3010 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3026 tmp1.
id() == ID_typecast &&
3032 .
id() == ID_string_constant)
3044 else if(identifier==
"__builtin_classify_type")
3051 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3064 if(type.
id() == ID_c_bit_field)
3067 unsigned type_number;
3069 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3080 type.
id() == ID_empty
3082 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
3084 : (type.
id() == ID_pointer || type.
id() == ID_array)
3086 : type.
id() == ID_floatbv
3088 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
3090 : type.
id() == ID_struct
3092 : type.
id() == ID_union
3113 overflow.
id(ID_minus);
3118 overflow.id(ID_mult);
3123 overflow.id(ID_plus);
3128 overflow.id(ID_shl);
3133 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
3134 of.add_source_location() = overflow.source_location();
3135 return std::move(of);
3145 overflow.add_source_location() = tmp.source_location();
3146 return std::move(overflow);
3153 std::ostringstream error_message;
3155 <<
" takes exactly 1 argument, but "
3156 << expr.
arguments().size() <<
" were provided";
3164 std::ostringstream error_message;
3166 <<
" expects enum, but (" <<
expr2c(arg1, *
this)
3167 <<
") has type `" <<
type2c(arg1.type(), *
this) <<
'`';
3176 identifier ==
"__builtin_add_overflow" ||
3177 identifier ==
"__builtin_sadd_overflow" ||
3178 identifier ==
"__builtin_saddl_overflow" ||
3179 identifier ==
"__builtin_saddll_overflow" ||
3180 identifier ==
"__builtin_uadd_overflow" ||
3181 identifier ==
"__builtin_uaddl_overflow" ||
3182 identifier ==
"__builtin_uaddll_overflow" ||
3183 identifier ==
"__builtin_add_overflow_p")
3188 identifier ==
"__builtin_sub_overflow" ||
3189 identifier ==
"__builtin_ssub_overflow" ||
3190 identifier ==
"__builtin_ssubl_overflow" ||
3191 identifier ==
"__builtin_ssubll_overflow" ||
3192 identifier ==
"__builtin_usub_overflow" ||
3193 identifier ==
"__builtin_usubl_overflow" ||
3194 identifier ==
"__builtin_usubll_overflow" ||
3195 identifier ==
"__builtin_sub_overflow_p")
3200 identifier ==
"__builtin_mul_overflow" ||
3201 identifier ==
"__builtin_smul_overflow" ||
3202 identifier ==
"__builtin_smull_overflow" ||
3203 identifier ==
"__builtin_smulll_overflow" ||
3204 identifier ==
"__builtin_umul_overflow" ||
3205 identifier ==
"__builtin_umull_overflow" ||
3206 identifier ==
"__builtin_umulll_overflow" ||
3207 identifier ==
"__builtin_mul_overflow_p")
3212 identifier ==
"__builtin_bitreverse8" ||
3213 identifier ==
"__builtin_bitreverse16" ||
3214 identifier ==
"__builtin_bitreverse32" ||
3215 identifier ==
"__builtin_bitreverse64")
3220 std::ostringstream error_message;
3222 <<
": error: " << identifier <<
" expects one operand";
3229 bitreverse.add_source_location() = source_location;
3231 return std::move(bitreverse);
3247 std::ostringstream error_message;
3249 <<
" takes exactly 3 arguments, but "
3250 << expr.
arguments().size() <<
" were provided";
3263 auto const raise_wrong_argument_error =
3265 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3266 std::ostringstream error_message;
3268 << identifier <<
" has signature " << identifier
3269 <<
"(integral, integral, integral" << (_p ?
"" :
"*")
3271 <<
"but argument " << argument_number <<
" ("
3272 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3273 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3276 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3278 auto const &argument = expr.
arguments()[arg_index];
3282 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3287 (
result.type().id() != ID_pointer ||
3290 raise_wrong_argument_error(
result, 3, is__p_variant);
3314 if(code_type.
get_bool(ID_C_incomplete))
3318 else if(code_type.
is_KnR())
3323 while(parameter_types.size()>arguments.size())
3328 if(parameter_types.size()>arguments.size())
3331 error() <<
"not enough function arguments" <<
eom;
3335 else if(parameter_types.size()!=arguments.size())
3338 error() <<
"wrong number of function arguments: "
3339 <<
"expected " << parameter_types.size()
3340 <<
", but got " << arguments.size() <<
eom;
3344 for(std::size_t i=0; i<arguments.size(); i++)
3346 exprt &op=arguments[i];
3352 else if(i<parameter_types.size())
3357 const typet &op_type=parameter_type.
type();
3359 if(op_type.
id()==ID_bool &&
3360 op.
id()==ID_side_effect &&
3361 op.
get(ID_statement)==ID_assign &&
3365 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3374 if(op.
type().
id() == ID_array)
3377 dest_type.
subtype().
set(ID_C_constant,
true);
3395 if(o_type.
id()==ID_vector)
3414 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3438 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3439 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3469 if(o_type0.
id()==ID_vector &&
3470 o_type1.
id()==ID_vector)
3484 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3489 expr.
type() = o_type0;
3493 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3498 expr.
type() = o_type1;
3509 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3510 expr.
id()==ID_mult || expr.
id()==ID_div)
3512 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3517 else if(type0==type1)
3526 else if(expr.
id()==ID_mod)
3530 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3538 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3539 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3548 else if(type0.
id()==ID_bool)
3550 if(expr.
id()==ID_bitand)
3552 else if(expr.
id() == ID_bitnand)
3554 else if(expr.
id()==ID_bitor)
3556 else if(expr.
id()==ID_bitxor)
3567 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3575 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3583 if(o_type0.
id()==ID_vector &&
3584 o_type1.
id()==ID_vector)
3600 o_type0.
id() == ID_vector &&
3618 if(expr.
id()==ID_shr)
3622 if(op0_type.
id()==ID_unsignedbv)
3627 else if(op0_type.
id()==ID_signedbv)
3638 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3656 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3664 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3678 if(expr.
id()==ID_minus ||
3679 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3681 if(type0.
id()==ID_pointer &&
3682 type1.
id()==ID_pointer)
3692 if(type0.
id()==ID_pointer &&
3693 (type1.
id()==ID_bool ||
3694 type1.
id()==ID_c_bool ||
3695 type1.
id()==ID_unsignedbv ||
3696 type1.
id()==ID_signedbv ||
3697 type1.
id()==ID_c_bit_field ||
3698 type1.
id()==ID_c_enum_tag))
3706 else if(expr.
id()==ID_plus ||
3707 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3709 exprt *p_op, *int_op;
3711 if(type0.
id()==ID_pointer)
3716 else if(type1.
id()==ID_pointer)
3723 p_op=int_op=
nullptr;
3727 const typet &int_op_type = int_op->
type();
3729 if(int_op_type.
id()==ID_bool ||
3730 int_op_type.
id()==ID_c_bool ||
3731 int_op_type.
id()==ID_unsignedbv ||
3732 int_op_type.
id()==ID_signedbv ||
3733 int_op_type.
id()==ID_c_bit_field ||
3734 int_op_type.
id()==ID_c_enum_tag)
3745 if(expr.
id()==ID_side_effect)
3751 error() <<
"operator '" << op_name <<
"' not defined for types '"
3782 if(type0.
id()==ID_empty)
3785 error() <<
"cannot assign void" <<
eom;
3792 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3805 if(type0.
id() == ID_array)
3808 error() <<
"direct assignments to arrays not permitted" <<
eom;
3815 if(op0.
type().
id()==ID_c_bit_field)
3821 expr.
type()=o_type0;
3823 if(statement==ID_assign)
3828 else if(statement==ID_assign_shl ||
3829 statement==ID_assign_shr)
3831 if(o_type0.
id() == ID_vector)
3836 o_type1.
id() == ID_vector &&
3837 vector_o_type0.element_type() ==
3839 is_number(vector_o_type0.element_type()))
3855 if(statement==ID_assign_shl)
3865 if(underlying_type.
id()==ID_unsignedbv ||
3866 underlying_type.
id()==ID_c_bool)
3868 expr.
set(ID_statement, ID_assign_lshr);
3871 else if(underlying_type.
id()==ID_signedbv)
3873 expr.
set(ID_statement, ID_assign_ashr);
3879 else if(statement==ID_assign_bitxor ||
3880 statement==ID_assign_bitand ||
3881 statement==ID_assign_bitor)
3884 if(o_type0.
id()==ID_bool ||
3885 o_type0.
id()==ID_c_bool)
3889 op1.
type().
id() == ID_bool || op1.
type().
id() == ID_c_bool ||
3890 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3891 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3896 else if(o_type0.
id()==ID_c_enum_tag ||
3897 o_type0.
id()==ID_unsignedbv ||
3898 o_type0.
id()==ID_signedbv ||
3899 o_type0.
id()==ID_c_bit_field)
3903 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3904 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3909 else if(o_type0.
id()==ID_vector &&
3910 o_type1.
id()==ID_vector)
3921 o_type0.
id() == ID_vector &&
3922 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
3923 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
3924 o_type1.
id() == ID_signedbv))
3933 if(o_type0.
id()==ID_pointer &&
3934 (statement==ID_assign_minus || statement==ID_assign_plus))
3939 else if(o_type0.
id()==ID_vector &&
3940 o_type1.
id()==ID_vector)
3950 else if(o_type0.
id() == ID_vector)
3956 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
3962 else if(o_type0.
id()==ID_bool ||
3963 o_type0.
id()==ID_c_bool)
3966 if(op1.
type().
id()==ID_bool ||
3967 op1.
type().
id()==ID_c_bool ||
3968 op1.
type().
id()==ID_c_enum_tag ||
3969 op1.
type().
id()==ID_unsignedbv ||
3970 op1.
type().
id()==ID_signedbv)
3978 op1.
type().
id()==ID_bool ||
3979 op1.
type().
id()==ID_c_bool ||
3980 op1.
type().
id()==ID_c_enum_tag)
3986 error() <<
"assignment '" << statement <<
"' not defined for types '"
4005 if(e.
id() == ID_infinity)
4013 if(e.
id() == ID_symbol)
4015 return e.
type().
id() == ID_code ||
4018 else if(e.
id() == ID_array && e.
get_bool(ID_C_string_constant))
4030 const auto rounding_mode =
4039 error() <<
"expected constant expression, but got '" <<
to_string(expr)
4054 error() <<
"conversion to integer constant failed" <<
eom;
4062 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.
void base_type(typet &type, const namespacet &ns)
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
bitvector_typet index_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet pointer_diff_type()
floatbv_typet long_double_type()
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.
const typet & underlying_type() const
const typet & underlying_type() const
bool is_incomplete() const
enum types may be incomplete
virtual void typecheck_expr_main(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
symbol_tablet & symbol_table
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
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 make_constant_index(exprt &expr)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
A codet representing sequential composition of program statements.
static code_blockt from_list(const std::list< codet > &_list)
codet & find_last_statement()
A codet representing the declaration of a local variable.
std::vector< parametert > parameterst
const typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
A constant literal expression.
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
IEEE-floating-point equality.
static ieee_float_spect single_precision()
static ieee_float_spect double_precision()
constant_exprt to_expr() const
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
static ieee_floatt zero(const floatbv_typet &type)
The trinary if-then-else operator.
An expression denoting infinity.
Thrown when we can't handle something in an input source file.
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)
bool is_constant(const exprt &e) const override
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const override
this function determines which reference-typed expressions are constant
is_compile_time_constantt(const namespacet &ns)
Determine whether an expression is constant.
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
mstreamt & warning() const
mstreamt & result() const
message_handlert & get_message_handler()
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
The plus expression Associativity is not specified.
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 a predicate that indicates that an address range is ok to read or write or both.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
An expression containing a side effect.
const irep_idt & get_statement() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
std::string as_string() const
Base type for structs and unions.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
bool is_incomplete() const
A struct/union may be incomplete.
const componentst & components() const
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
const irep_idt & display_name() const
Return language specific display name if present.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Type with multiple subtypes.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
source_locationt & add_source_location()
Generic base class for unary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
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)
#define Forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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 unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
bool has_suffix(const std::string &s, const std::string &suffix)
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
const type_with_subtypet & to_type_with_subtype(const typet &type)