Go to the documentation of this file.
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)
116 else if(type2==type1.
subtype())
119 else if(type2.
id()==ID_c_enum)
124 else if(type1.
id()==ID_pointer &&
125 type2.
id()==ID_pointer)
129 else if(type1.
id()==ID_array &&
130 type2.
id()==ID_array)
135 else if(type1.
id()==ID_code &&
149 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
165 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
175 if(expr.
id()==ID_side_effect)
177 else if(expr.
id()==ID_constant)
179 else if(expr.
id()==ID_infinity)
183 else if(expr.
id()==ID_symbol)
185 else if(expr.
id()==ID_unary_plus ||
186 expr.
id()==ID_unary_minus ||
187 expr.
id()==ID_bitnot)
189 else if(expr.
id()==ID_not)
192 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
195 else if(expr.
id()==ID_address_of)
197 else if(expr.
id()==ID_dereference)
199 else if(expr.
id()==ID_member)
201 else if(expr.
id()==ID_ptrmember)
203 else if(expr.
id()==ID_equal ||
204 expr.
id()==ID_notequal ||
210 else if(expr.
id()==ID_index)
212 else if(expr.
id()==ID_typecast)
214 else if(expr.
id()==ID_sizeof)
216 else if(expr.
id()==ID_alignof)
219 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
220 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
221 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
225 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
227 else if(expr.
id()==ID_comma)
229 else if(expr.
id()==ID_if)
231 else if(expr.
id()==ID_code)
234 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
237 else if(expr.
id()==ID_gcc_builtin_va_arg)
239 else if(expr.
id()==ID_cw_va_arg_typeof)
241 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
246 assert(subtypes.size()==2);
252 subtypes[0].
remove(ID_C_constant);
253 subtypes[0].remove(ID_C_volatile);
254 subtypes[0].remove(ID_C_restricted);
255 subtypes[1].remove(ID_C_constant);
256 subtypes[1].remove(ID_C_volatile);
257 subtypes[1].remove(ID_C_restricted);
262 else if(expr.
id()==ID_clang_builtin_convertvector)
271 else if(expr.
id()==ID_builtin_offsetof)
273 else if(expr.
id()==ID_string_constant)
276 expr.
set(ID_C_lvalue,
true);
278 else if(expr.
id()==ID_arguments)
282 else if(expr.
id()==ID_designated_initializer)
284 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
288 if(it->id()==ID_index)
292 else if(expr.
id()==ID_initializer_list)
298 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
304 auto &bindings = binary_expr.op0().operands();
305 auto &where = binary_expr.op1();
307 for(
const auto &binding : bindings)
309 if(binding.get(ID_statement) != ID_decl)
312 error() <<
"expected declaration as operand of quantifier" <<
eom;
320 error() <<
"quantifier must not contain side effects" <<
eom;
325 for(
auto &binding : bindings)
328 if(expr.
id() == ID_lambda)
332 for(
auto &binding : bindings)
333 domain.push_back(binding.type());
343 else if(expr.
id()==ID_label)
347 else if(expr.
id()==ID_array)
351 else if(expr.
id()==ID_complex)
356 else if(expr.
id() == ID_complex_real)
360 if(op.
type().
id() != ID_complex)
365 error() <<
"real part retrieval expects numerical operand, "
373 expr.
swap(complex_real_expr);
381 complex_real_expr.
set(ID_C_lvalue,
true);
384 complex_real_expr.
type().
set(ID_C_constant,
true);
386 expr.
swap(complex_real_expr);
389 else if(expr.
id() == ID_complex_imag)
393 if(op.
type().
id() != ID_complex)
398 error() <<
"real part retrieval expects numerical operand, "
406 expr.
swap(complex_imag_expr);
414 complex_imag_expr.
set(ID_C_lvalue,
true);
417 complex_imag_expr.
type().
set(ID_C_constant,
true);
419 expr.
swap(complex_imag_expr);
422 else if(expr.
id()==ID_generic_selection)
432 if(op.type().id() == ID_bool)
439 for(
auto &irep : generic_associations)
441 if(irep.get(ID_type_arg) != ID_default)
443 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
454 for(
const auto &irep : generic_associations)
456 if(irep.get(ID_type_arg) == ID_default)
457 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
459 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
461 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
468 expr.
swap(default_match);
472 error() <<
"unmatched generic selection: " <<
to_string(op.type())
478 expr.
swap(assoc_match);
483 else if(expr.
id()==ID_gcc_asm_input ||
484 expr.
id()==ID_gcc_asm_output ||
485 expr.
id()==ID_gcc_asm_clobbered_register)
488 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
489 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
493 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
511 expr.
set(ID_C_lvalue,
true);
548 symbol.
name=ID_gcc_builtin_va_arg;
549 symbol.
type=symbol_type;
579 error() <<
"builtin_offsetof expects no operands" <<
eom;
594 if(m_it->id()==ID_member)
596 if(type.
id()!=ID_union && type.
id()!=ID_struct)
599 error() <<
"offsetof of member expects struct/union type, "
605 irep_idt component_name=m_it->get(ID_component_name);
609 assert(type.
id()==ID_union || type.
id()==ID_struct);
619 if(type.
id()==ID_struct)
624 if(!o_opt.has_value())
627 error() <<
"offsetof failed to determine offset of '"
628 << component_name <<
"'" <<
eom;
644 for(
const auto &c : struct_union_type.
components())
648 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
652 if(type.
id()==ID_struct)
657 if(!o_opt.has_value())
660 error() <<
"offsetof failed to determine offset of '"
661 << component_name <<
"'" <<
eom;
673 assert(type.
id()==ID_union || type.
id()==ID_struct);
683 error() <<
"offset-of of member failed to find component '"
684 << component_name <<
"' in '" <<
to_string(type) <<
"'"
691 else if(m_it->id()==ID_index)
693 if(type.
id()!=ID_array)
696 error() <<
"offsetof of index expects array type" <<
eom;
707 if(!sub_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_tablet::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 '"
861 if(expr.
id()==ID_constant &&
863 expr.
set(ID_C_cformat, base_name);
878 else if(identifier==
"__func__" ||
879 identifier==
"__FUNCTION__" ||
880 identifier==
"__PRETTY_FUNCTION__")
886 s.
set(ID_C_lvalue,
true);
897 expr.
set(ID_C_lvalue,
true);
899 if(expr.
type().
id()==ID_code)
902 tmp.
set(ID_C_implicit,
true);
921 if(last_statement==ID_expression)
927 if(op.
type().
id()==ID_array)
960 if(op.
type().
id() == ID_bool)
968 if(type.
id()==ID_c_bit_field)
971 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
974 else if(type.
id() == ID_bool)
977 error() <<
"sizeof cannot be applied to single bits" <<
eom;
980 else if(type.
id() == ID_empty)
989 (type.
id() == ID_struct_tag &&
991 (type.
id() == ID_union_tag &&
993 (type.
id() == ID_c_enum_tag &&
998 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1005 if(!size_of_opt.has_value())
1012 new_expr = size_of_opt.value();
1015 new_expr.
swap(expr);
1017 expr.
add(ID_C_c_sizeof_type)=type;
1025 decl_block.set_statement(ID_decl_block);
1035 exprt comma_expr(ID_comma, expr.
type());
1037 expr.
swap(comma_expr);
1043 typet argument_type;
1051 argument_type=op_type;
1075 decl_block.set_statement(ID_decl_block);
1087 op.
swap(comma_expr);
1093 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1094 op.
id() != ID_initializer_list)
1102 if(op.
type().
id() == ID_bool)
1107 for(
const auto &c : union_type.components())
1109 if(c.type() == op.
type())
1115 expr.
set(ID_C_lvalue,
true);
1123 <<
"' not found in union" <<
eom;
1130 if(op.
id()==ID_initializer_list)
1139 exprt tmp(ID_compound_literal, expr.
type());
1143 if(op.
id()==ID_array &&
1144 expr.
type().
id()==ID_array &&
1149 expr.
set(ID_C_lvalue,
true);
1154 if(expr_type.
id()==ID_empty)
1160 if(expr_type == op_type)
1165 if(expr_type.
id()==ID_vector)
1168 if(op_type.
id()==ID_vector)
1170 else if(op_type.
id()==ID_signedbv ||
1171 op_type.
id()==ID_unsignedbv)
1178 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1186 else if(op_type.
id()==ID_array)
1191 else if(op_type.
id()==ID_empty)
1193 if(expr_type.
id()!=ID_empty)
1196 error() <<
"type cast from void only permitted to void, but got '"
1201 else if(op_type.
id()==ID_vector)
1208 if((expr_type.
id()==ID_signedbv ||
1209 expr_type.
id()==ID_unsignedbv) &&
1218 <<
"' not permitted" <<
eom;
1225 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1241 if(expr_type.
id()==ID_pointer)
1242 expr.
set(ID_C_lvalue,
true);
1259 const typet &array_type = array_expr.
type();
1263 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1264 array_type.
id() != ID_vector &&
1267 std::swap(array_expr, index_expr);
1275 const typet final_array_type = array_expr.
type();
1277 if(final_array_type.
id()==ID_array ||
1278 final_array_type.
id()==ID_vector)
1282 if(array_expr.
get_bool(ID_C_lvalue))
1283 expr.
set(ID_C_lvalue,
true);
1285 if(final_array_type.
get_bool(ID_C_constant))
1286 expr.
type().
set(ID_C_constant,
true);
1288 else if(final_array_type.
id()==ID_pointer)
1294 std::swap(summands, expr.
operands());
1296 expr.
id(ID_dereference);
1297 expr.
set(ID_C_lvalue,
true);
1303 error() <<
"operator [] must take array/vector or pointer but got '"
1312 if(expr.
op0().
type().
id() == ID_floatbv)
1314 if(expr.
id()==ID_equal)
1315 expr.
id(ID_ieee_float_equal);
1316 else if(expr.
id()==ID_notequal)
1317 expr.
id(ID_ieee_float_notequal);
1330 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1338 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1342 if(o_type0.
id() != ID_array)
1363 if(type0.
id()==ID_pointer)
1365 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1368 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1369 expr.
id()==ID_ge || expr.
id()==ID_gt)
1373 if(type0.
id()==ID_string_constant)
1375 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1382 if(type0.
id()==ID_pointer &&
1389 if(type1.
id()==ID_pointer &&
1409 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1417 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1428 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1431 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1445 if(expr.
id() == ID_notequal)
1446 expr.
id(ID_vector_notequal);
1454 const typet &op0_type = op.type();
1456 if(op0_type.
id() == ID_array)
1461 index_expr.
set(ID_C_lvalue,
true);
1462 op.swap(index_expr);
1464 else if(op0_type.
id() == ID_pointer)
1470 op.swap(deref_expr);
1475 error() <<
"ptrmember operator requires pointer or array type "
1476 "on left hand side, but got '"
1492 if(type.
id()!=ID_struct &&
1493 type.
id()!=ID_union)
1496 error() <<
"member operator requires structure type "
1497 "on left hand side but got '"
1508 error() <<
"member operator got incomplete " << type.
id()
1509 <<
" type on left hand side" <<
eom;
1514 expr.
get(ID_component_name);
1530 error() <<
"member '" << component_name <<
"' not found in '"
1543 expr.
set(ID_C_lvalue,
true);
1546 expr.
type().
set(ID_C_constant,
true);
1551 if(!identifier.
empty())
1552 expr.
set(ID_C_identifier, identifier);
1556 if(access==ID_private)
1559 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1568 assert(operands.size()==3);
1571 const typet o_type0=operands[0].type();
1572 const typet o_type1=operands[1].type();
1573 const typet o_type2=operands[2].type();
1577 if(o_type1.
id() == ID_empty || o_type2.
id() == ID_empty)
1585 if(operands[1].type().
id()==ID_pointer &&
1586 operands[2].type().
id()!=ID_pointer)
1588 else if(operands[2].type().
id()==ID_pointer &&
1589 operands[1].type().
id()!=ID_pointer)
1592 if(operands[1].type().
id()==ID_pointer &&
1593 operands[2].type().
id()==ID_pointer &&
1594 operands[1].type()!=operands[2].type())
1601 if(operands[1].type().subtype().
id()==ID_empty &&
1605 else if(operands[2].type().subtype().
id()==ID_empty &&
1609 else if(operands[1].type().subtype().
id()!=ID_code ||
1610 operands[2].type().subtype().
id()!=ID_code)
1634 if(operands[1].type().
id()==ID_empty ||
1635 operands[2].type().
id()==ID_empty)
1642 operands[1].type() != operands[2].type() ||
1643 operands[1].type().
id() == ID_array)
1648 if(operands[1].type() == operands[2].type())
1650 expr.
type()=operands[1].type();
1656 if(operands[1].get_bool(ID_C_lvalue) &&
1657 operands[2].get_bool(ID_C_lvalue))
1658 expr.
set(ID_C_lvalue,
true);
1664 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1677 if(operands.size()!=2)
1680 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1686 if_exprt if_expr(operands[0], operands[0], operands[1]);
1701 if(op.
type().
id()==ID_c_bit_field)
1704 error() <<
"cannot take address of a bit field" <<
eom;
1708 if(op.
type().
id() == ID_bool)
1711 error() <<
"cannot take address of a single bit" <<
eom;
1716 if(op.
id()==ID_label)
1729 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1735 tmp.
set(ID_C_implicit,
false);
1740 if(op.
id()==ID_struct ||
1741 op.
id()==ID_union ||
1742 op.
id()==ID_array ||
1743 op.
id()==ID_string_constant)
1751 else if(op.
type().
id()==ID_code)
1758 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1772 if(op_type.
id()==ID_array)
1780 else if(op_type.
id()==ID_pointer)
1788 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1793 expr.
set(ID_C_lvalue,
true);
1804 if(expr.
type().
id()==ID_code)
1807 tmp.
set(ID_C_implicit,
true);
1817 if(statement==ID_preincrement ||
1818 statement==ID_predecrement ||
1819 statement==ID_postincrement ||
1820 statement==ID_postdecrement)
1829 <<
"' not an lvalue" <<
eom;
1840 if(type0.
id() == ID_c_enum_tag)
1846 error() <<
"operator '" << statement <<
"' given incomplete type '"
1855 else if(type0.
id() == ID_c_bit_field)
1860 expr.
type()=underlying_type;
1862 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1871 else if(type0.
id() == ID_pointer)
1879 error() <<
"operator '" << statement <<
"' not defined for type '"
1886 else if(statement==ID_function_call)
1889 else if(statement==ID_statement_expression)
1891 else if(statement==ID_gcc_conditional_expression)
1896 error() <<
"unknown side effect: " << statement <<
eom;
1907 error() <<
"function_call side effect expects two operands" <<
eom;
1916 if(f_op.
id()==ID_symbol)
1920 asm_label_mapt::const_iterator entry=
1923 identifier=entry->second;
1934 identifier ==
"__noop" &&
1948 identifier ==
"__builtin_shuffle" &&
1957 identifier ==
"__builtin_shufflevector" &&
1969 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1972 !parameters.empty(),
1973 "GCC polymorphic built-ins should have at least one parameter");
1978 if(parameters.front().type().id() == ID_pointer)
1980 identifier_with_type =
id2string(identifier) +
"_" +
1982 parameters.front().type().subtype(), *
this);
1986 identifier_with_type =
1990 gcc_polymorphic->set_identifier(identifier_with_type);
1994 for(std::size_t i = 0; i < parameters.size(); ++i)
2001 id2string(identifier_with_type) +
"::" + base_name;
2004 new_symbol.
type = parameters[i].type();
2007 new_symbol.
mode = ID_C;
2009 parameters[i].set_identifier(new_symbol.
name);
2010 parameters[i].set_base_name(new_symbol.
base_name);
2017 new_symbol.
name = identifier_with_type;
2018 new_symbol.
base_name = identifier_with_type;
2020 new_symbol.
type = gcc_polymorphic->type();
2021 new_symbol.
mode = ID_C;
2028 new_symbol.
value = implementation;
2033 f_op = std::move(*gcc_polymorphic);
2045 if(identifier==
"malloc" ||
2046 identifier==
"realloc" ||
2047 identifier==
"reallocf" ||
2048 identifier==
"valloc")
2055 new_symbol.
name=identifier;
2059 new_symbol.
type.
set(ID_C_incomplete,
true);
2067 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2077 if(f_op_type.
id() == ID_mathematical_function)
2079 const auto &mathematical_function_type =
2083 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2086 error() <<
"expected " << mathematical_function_type.domain().size()
2087 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2095 if(p.first.type() != p.second)
2108 expr.
swap(function_application);
2112 if(f_op_type.
id()!=ID_pointer)
2115 error() <<
"expected function/function pointer as argument but got '"
2121 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2128 tmp.
set(ID_C_implicit,
true);
2133 if(f_op.
type().
id()!=ID_code)
2136 error() <<
"expected code as argument" <<
eom;
2159 if(f_op.
id()!=ID_symbol)
2181 error() <<
"same_object expects two operands" <<
eom;
2187 exprt same_object_expr=
2191 return same_object_expr;
2198 error() <<
"get_must expects two operands" <<
eom;
2208 return std::move(get_must_expr);
2215 error() <<
"get_may expects two operands" <<
eom;
2225 return std::move(get_may_expr);
2232 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2241 return same_object_expr;
2248 error() <<
"buffer_size expects one operand" <<
eom;
2258 return buffer_size_expr;
2265 error() <<
"is_zero_string expects one operand" <<
eom;
2273 is_zero_string_expr.
set(ID_C_lvalue,
true);
2276 return std::move(is_zero_string_expr);
2283 error() <<
"zero_string_length expects one operand" <<
eom;
2289 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2291 zero_string_length_expr.
set(ID_C_lvalue,
true);
2294 return zero_string_length_expr;
2301 error() <<
"dynamic_object expects one argument" <<
eom;
2310 return is_dynamic_object_expr;
2317 error() <<
"pointer_offset expects one argument" <<
eom;
2333 error() <<
"object_size expects one operand" <<
eom;
2343 return std::move(object_size_expr);
2350 error() <<
"pointer_object expects one argument" <<
eom;
2361 else if(identifier==
"__builtin_bswap16" ||
2362 identifier==
"__builtin_bswap32" ||
2363 identifier==
"__builtin_bswap64")
2368 error() << identifier <<
" expects one operand" <<
eom;
2378 return std::move(bswap_expr);
2381 identifier ==
"__builtin_rotateleft8" ||
2382 identifier ==
"__builtin_rotateleft16" ||
2383 identifier ==
"__builtin_rotateleft32" ||
2384 identifier ==
"__builtin_rotateleft64" ||
2385 identifier ==
"__builtin_rotateright8" ||
2386 identifier ==
"__builtin_rotateright16" ||
2387 identifier ==
"__builtin_rotateright32" ||
2388 identifier ==
"__builtin_rotateright64")
2394 error() << identifier <<
" expects two operands" <<
eom;
2400 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2401 identifier ==
"__builtin_rotateleft16" ||
2402 identifier ==
"__builtin_rotateleft32" ||
2403 identifier ==
"__builtin_rotateleft64")
2410 return std::move(rotate_expr);
2412 else if(identifier==
"__builtin_nontemporal_load")
2417 error() << identifier <<
" expects one operand" <<
eom;
2426 if(ptr_arg.
type().
id()!=ID_pointer)
2429 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2438 identifier ==
"__builtin_fpclassify" ||
2444 error() << identifier <<
" expects six arguments" <<
eom;
2457 if(fp_value.
type().
id() != ID_floatbv)
2460 error() <<
"non-floating-point argument for " << identifier <<
eom;
2468 const auto &arguments = expr.
arguments();
2487 identifier==
"__builtin_isnan")
2492 error() <<
"isnan expects one operand" <<
eom;
2510 error() <<
"isfinite expects one operand" <<
eom;
2522 identifier==
"__builtin_inf")
2529 return std::move(inf_expr);
2538 return std::move(inff_expr);
2547 return std::move(infl_expr);
2559 error() <<
"abs-functions expect one operand" <<
eom;
2568 return std::move(abs_expr);
2578 error() <<
"fmod-functions expect two operands" <<
eom;
2592 return std::move(fmod_expr);
2602 error() <<
"remainder-functions expect two operands" <<
eom;
2616 return std::move(floatbv_rem_expr);
2623 error() <<
"allocate expects two operands" <<
eom;
2632 return std::move(malloc_expr);
2641 error() << identifier <<
" expects one or two operands" <<
eom;
2648 const auto &pointer_expr = expr.
arguments()[0];
2649 if(pointer_expr.type().id() != ID_pointer)
2652 error() << identifier <<
" expects a pointer as first argument" <<
eom;
2669 if(subtype.id() == ID_empty)
2672 error() << identifier <<
" expects a size when given a void pointer"
2678 if(!size_expr_opt.has_value())
2681 error() << identifier <<
" was given object pointer without size"
2686 size_expr = std::move(size_expr_opt.value());
2696 return std::move(ok_expr);
2705 error() << identifier <<
" expects one operand" <<
eom;
2714 return std::move(old_expr);
2719 identifier==
"__builtin_isinf")
2724 error() << identifier <<
" expects one operand" <<
eom;
2732 if(fp_value.
type().
id() != ID_floatbv)
2735 error() <<
"non-floating-point argument for " << identifier <<
eom;
2744 else if(identifier ==
"__builtin_isinf_sign")
2749 error() << identifier <<
" expects one operand" <<
eom;
2759 if(fp_value.
type().
id() != ID_floatbv)
2762 error() <<
"non-floating-point argument for " << identifier <<
eom;
2780 identifier ==
"__builtin_isnormal")
2785 error() << identifier <<
" expects one operand" <<
eom;
2793 if(fp_value.
type().
id() != ID_floatbv)
2796 error() <<
"non-floating-point argument for " << identifier <<
eom;
2808 identifier==
"__builtin_signbit" ||
2809 identifier==
"__builtin_signbitf" ||
2810 identifier==
"__builtin_signbitl")
2815 error() << identifier <<
" expects one operand" <<
eom;
2826 else if(identifier==
"__builtin_popcount" ||
2827 identifier==
"__builtin_popcountl" ||
2828 identifier==
"__builtin_popcountll" ||
2829 identifier==
"__popcnt16" ||
2830 identifier==
"__popcnt" ||
2831 identifier==
"__popcnt64")
2836 error() << identifier <<
" expects one operand" <<
eom;
2845 return std::move(popcount_expr);
2848 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2849 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2850 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2855 error() << identifier <<
" expects one operand" <<
eom;
2866 return std::move(clz);
2869 identifier ==
"__builtin_ctz" || identifier ==
"__builtin_ctzl" ||
2870 identifier ==
"__builtin_ctzll")
2875 error() << identifier <<
" expects one operand" <<
eom;
2885 return std::move(ctz);
2892 error() <<
"equal expects two operands" <<
eom;
2905 error() <<
"equal expects two operands of same type" <<
eom;
2909 return std::move(equality_expr);
2911 else if(identifier==
"__builtin_expect")
2922 error() <<
"__builtin_expect expects two arguments" <<
eom;
2930 else if(identifier==
"__builtin_object_size")
2939 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2956 error() <<
"__builtin_object_size expects constant as second argument, "
2964 if(arg1==0 || arg1==1)
2977 else if(identifier==
"__builtin_choose_expr")
2983 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2998 else if(identifier==
"__builtin_constant_p")
3005 error() <<
"__builtin_constant_p expects one argument" <<
eom;
3021 tmp1.
id() == ID_typecast &&
3027 .
id() == ID_string_constant)
3039 else if(identifier==
"__builtin_classify_type")
3046 error() <<
"__builtin_classify_type expects one argument" <<
eom;
3059 if(type.
id() == ID_c_bit_field)
3062 unsigned type_number;
3064 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
3075 type.
id() == ID_empty
3077 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
3079 : (type.
id() == ID_pointer || type.
id() == ID_array)
3081 : type.
id() == ID_floatbv
3083 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
3085 : type.
id() == ID_struct
3087 : type.
id() == ID_union
3108 overflow.
id(ID_minus);
3113 overflow.id(ID_mult);
3118 overflow.id(ID_plus);
3123 overflow.id(ID_shl);
3128 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
3129 of.add_source_location() = overflow.source_location();
3130 return std::move(of);
3140 overflow.add_source_location() = tmp.source_location();
3141 return std::move(overflow);
3148 std::ostringstream error_message;
3150 <<
" takes exactly 1 argument, but "
3151 << expr.
arguments().size() <<
" were provided";
3159 std::ostringstream error_message;
3161 <<
" expects enum, but (" <<
expr2c(arg1, *
this)
3162 <<
") has type `" <<
type2c(arg1.type(), *
this) <<
'`';
3171 identifier ==
"__builtin_add_overflow" ||
3172 identifier ==
"__builtin_sub_overflow" ||
3173 identifier ==
"__builtin_mul_overflow" ||
3174 identifier ==
"__builtin_add_overflow_p" ||
3175 identifier ==
"__builtin_sub_overflow_p" ||
3176 identifier ==
"__builtin_mul_overflow_p")
3181 std::ostringstream error_message;
3183 <<
" takes exactly 3 arguments, but "
3184 << expr.
arguments().size() <<
" were provided";
3197 auto const raise_wrong_argument_error =
3199 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3200 std::ostringstream error_message;
3202 << identifier <<
" has signature " << identifier
3203 <<
"(integral, integral, integral" << (_p ?
"" :
"*")
3205 <<
"but argument " << argument_number <<
" ("
3206 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3207 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3210 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3212 auto const &argument = expr.
arguments()[arg_index];
3216 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3221 (
result.type().id() != ID_pointer ||
3224 raise_wrong_argument_error(
result, 3, is__p_variant);
3257 if(code_type.
get_bool(ID_C_incomplete))
3261 else if(code_type.
is_KnR())
3266 while(parameter_types.size()>arguments.size())
3271 if(parameter_types.size()>arguments.size())
3274 error() <<
"not enough function arguments" <<
eom;
3278 else if(parameter_types.size()!=arguments.size())
3281 error() <<
"wrong number of function arguments: "
3282 <<
"expected " << parameter_types.size()
3283 <<
", but got " << arguments.size() <<
eom;
3287 for(std::size_t i=0; i<arguments.size(); i++)
3289 exprt &op=arguments[i];
3295 else if(i<parameter_types.size())
3300 const typet &op_type=parameter_type.
type();
3302 if(op_type.
id()==ID_bool &&
3303 op.
id()==ID_side_effect &&
3304 op.
get(ID_statement)==ID_assign &&
3308 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3317 if(op.
type().
id() == ID_array)
3320 dest_type.
subtype().
set(ID_C_constant,
true);
3338 if(o_type.
id()==ID_vector)
3357 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3381 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3382 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3391 if((type0.
subtype().
id()==ID_signedbv ||
3411 if(o_type0.
id()==ID_vector &&
3412 o_type1.
id()==ID_vector)
3426 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3431 expr.
type() = o_type0;
3435 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3440 expr.
type() = o_type1;
3451 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3452 expr.
id()==ID_mult || expr.
id()==ID_div)
3454 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3459 else if(type0==type1)
3468 else if(expr.
id()==ID_mod)
3472 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3480 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3481 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3490 else if(type0.
id()==ID_bool)
3492 if(expr.
id()==ID_bitand)
3494 else if(expr.
id() == ID_bitnand)
3496 else if(expr.
id()==ID_bitor)
3498 else if(expr.
id()==ID_bitxor)
3509 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3517 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3525 if(o_type0.
id()==ID_vector &&
3526 o_type1.
id()==ID_vector)
3557 if(expr.
id()==ID_shr)
3561 if(op0_type.
id()==ID_unsignedbv)
3566 else if(op0_type.
id()==ID_signedbv)
3577 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3586 assert(type.
id()==ID_pointer);
3591 subtype.
id() == ID_struct_tag &&
3595 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3599 subtype.
id() == ID_union_tag &&
3603 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3617 if(expr.
id()==ID_minus ||
3618 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3620 if(type0.
id()==ID_pointer &&
3621 type1.
id()==ID_pointer)
3631 if(type0.
id()==ID_pointer &&
3632 (type1.
id()==ID_bool ||
3633 type1.
id()==ID_c_bool ||
3634 type1.
id()==ID_unsignedbv ||
3635 type1.
id()==ID_signedbv ||
3636 type1.
id()==ID_c_bit_field ||
3637 type1.
id()==ID_c_enum_tag))
3645 else if(expr.
id()==ID_plus ||
3646 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3648 exprt *p_op, *int_op;
3650 if(type0.
id()==ID_pointer)
3655 else if(type1.
id()==ID_pointer)
3662 p_op=int_op=
nullptr;
3666 const typet &int_op_type = int_op->
type();
3668 if(int_op_type.
id()==ID_bool ||
3669 int_op_type.
id()==ID_c_bool ||
3670 int_op_type.
id()==ID_unsignedbv ||
3671 int_op_type.
id()==ID_signedbv ||
3672 int_op_type.
id()==ID_c_bit_field ||
3673 int_op_type.
id()==ID_c_enum_tag)
3684 if(expr.
id()==ID_side_effect)
3690 error() <<
"operator '" << op_name <<
"' not defined for types '"
3721 if(type0.
id()==ID_empty)
3724 error() <<
"cannot assign void" <<
eom;
3731 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3744 if(type0.
id() == ID_array)
3747 error() <<
"direct assignments to arrays not permitted" <<
eom;
3754 if(op0.
type().
id()==ID_c_bit_field)
3760 expr.
type()=o_type0;
3762 if(statement==ID_assign)
3767 else if(statement==ID_assign_shl ||
3768 statement==ID_assign_shr)
3770 if(o_type0.
id() == ID_vector)
3790 if(statement==ID_assign_shl)
3800 if(underlying_type.
id()==ID_unsignedbv ||
3801 underlying_type.
id()==ID_c_bool)
3803 expr.
set(ID_statement, ID_assign_lshr);
3806 else if(underlying_type.
id()==ID_signedbv)
3808 expr.
set(ID_statement, ID_assign_ashr);
3814 else if(statement==ID_assign_bitxor ||
3815 statement==ID_assign_bitand ||
3816 statement==ID_assign_bitor)
3819 if(o_type0.
id()==ID_bool ||
3820 o_type0.
id()==ID_c_bool)
3824 op1.
type().
id() == ID_bool || op1.
type().
id() == ID_c_bool ||
3825 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3826 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3831 else if(o_type0.
id()==ID_c_enum_tag ||
3832 o_type0.
id()==ID_unsignedbv ||
3833 o_type0.
id()==ID_signedbv ||
3834 o_type0.
id()==ID_c_bit_field)
3838 op1.
type().
id() == ID_c_enum_tag || op1.
type().
id() == ID_unsignedbv ||
3839 op1.
type().
id() == ID_signedbv || op1.
type().
id() == ID_c_bit_field)
3844 else if(o_type0.
id()==ID_vector &&
3845 o_type1.
id()==ID_vector)
3856 o_type0.
id() == ID_vector &&
3857 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
3858 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
3859 o_type1.
id() == ID_signedbv))
3868 if(o_type0.
id()==ID_pointer &&
3869 (statement==ID_assign_minus || statement==ID_assign_plus))
3874 else if(o_type0.
id()==ID_vector &&
3875 o_type1.
id()==ID_vector)
3885 else if(o_type0.
id() == ID_vector)
3891 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
3897 else if(o_type0.
id()==ID_bool ||
3898 o_type0.
id()==ID_c_bool)
3901 if(op1.
type().
id()==ID_bool ||
3902 op1.
type().
id()==ID_c_bool ||
3903 op1.
type().
id()==ID_c_enum_tag ||
3904 op1.
type().
id()==ID_unsignedbv ||
3905 op1.
type().
id()==ID_signedbv)
3913 op1.
type().
id()==ID_bool ||
3914 op1.
type().
id()==ID_c_bool ||
3915 op1.
type().
id()==ID_c_enum_tag)
3921 error() <<
"assignment '" << statement <<
"' not defined for types '"
3933 const auto rounding_mode =
3940 expr.
id()!=ID_infinity)
3943 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3956 expr.
id()!=ID_infinity)
3959 error() <<
"conversion to integer constant failed" <<
eom;
3967 const std::string &message)
const
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_function() const
bool has_ellipsis() const
A codet representing sequential composition of program statements.
static exprt conditional_cast(const exprt &expr, const typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
const typet & subtype() const
ANSI-CC Language Type Checking.
Type with multiple subtypes.
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
static code_blockt from_list(const std::list< codet > &_list)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt pointer_object(const exprt &p)
const declaratorst & declarators() const
std::string as_string() const
bool is_incomplete() const
enum types may be incomplete
#define Forall_operands(it, expr)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
virtual void typecheck_expr_shifts(shift_exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_declt & to_code_decl(const codet &code)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
std::vector< parametert > parameterst
ANSI-C Language Type Checking.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_declaration(ansi_c_declarationt &)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
std::string expr2c(const exprt &expr, const namespacet &ns)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
virtual std::string to_string(const exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
Base type for structs and unions.
typet type
Type of symbol.
floatbv_typet long_double_type()
Operator to dereference a pointer.
A side_effect_exprt representation of a function call side effect.
The trinary if-then-else operator.
static void add_rounding_mode(exprt &)
irept & add(const irep_namet &name)
Evaluates to true if the operand is a pointer to a dynamic object.
Fixed-width bit-vector with IEEE floating-point interpretation.
Various predicates over pointers in programs.
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...
Real part of the expression describing a complex number.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
A codet representing the declaration of a local variable.
Union constructor from single element.
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
The plus expression Associativity is not specified.
virtual void typecheck_expr_symbol(exprt &expr)
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
Generic base class for unary expressions.
A base class for binary expressions.
irep_idt base_name
Base (non-scoped) name.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Complex numbers made of pair of given subtype.
Sign of an expression Predicate is true if _op is negative, false otherwise.
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
Thrown when we can't handle something in an input source file.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_type(typet &type)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
bool is_true() const
Return whether the expression is a constant representing true.
side_effect_exprt & to_side_effect_expr(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
struct configt::ansi_ct ansi_c
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
bitvector_typet index_type()
virtual void typecheck_expr_binary_boolean(exprt &expr)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
An expression denoting infinity.
Evaluates to true if the operand is finite.
std::list< codet > clean_code
virtual void make_constant(exprt &expr)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
virtual void typecheck_expr_operands(exprt &expr)
const exprt & size() const
virtual void typecheck_expr_member(exprt &expr)
std::string type2c(const typet &type, const namespacet &ns)
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
typet & type()
Return the type of the expression.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
bool get_bool(const irep_namet &name) const
asm_label_mapt asm_label_map
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
irep_idt mode
Language mode.
mstreamt & result() const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
static ieee_float_spect double_precision()
signedbv_typet signed_int_type()
bool has_prefix(const std::string &s, const std::string &prefix)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual void implicit_typecast_bool(exprt &expr)
const std::string & id2string(const irep_idt &d)
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
preprocessort preprocessor
source_locationt source_location
virtual void typecheck_expr_function_identifier(exprt &expr)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define forall_operands(it, expr)
virtual void typecheck_expr_dereference(exprt &expr)
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...
API to expression classes that are internal to the C frontend.
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
virtual bool is_complete_type(const typet &type) const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Fixed-width bit-vector with two's complement interpretation.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
API to expression classes for Pointers.
bool simplify(exprt &expr, const namespacet &ns)
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
std::vector< typet > domaint
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
symbol_tablet & symbol_table
virtual bool gcc_types_compatible_p(const typet &, const typet &)
mp_integer alignment(const typet &type, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_int_type()
virtual void typecheck_code(codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
bool has_component(const irep_idt &component_name) const
virtual void make_constant_index(exprt &expr)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
const irep_idt & id() const
virtual void typecheck_expr_trinary(if_exprt &expr)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void remove(const irep_namet &name)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
API to expression classes for floating-point arithmetic.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() const
source_locationt & add_source_location()
const constant_exprt & size() const
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
id_type_mapt parameter_map
exprt pointer_offset(const exprt &pointer)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
std::map< irep_idt, source_locationt > labels_used
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const irep_idt & get_statement() const
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr(exprt &expr)
std::size_t get_width() const
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Deprecated expression utility functions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
A base class for shift and rotate operators.
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
static bool is_numeric_type(const typet &src)
A class for an expression that indicates a history variable.
virtual void typecheck_expr_main(exprt &expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is infinite.
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
exprt::operandst & arguments()
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Imaginary part of the expression describing a complex number.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
exprt same_object(const exprt &p1, const exprt &p2)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
virtual void typecheck_expr_constant(exprt &expr)
A base class for a predicate that indicates that an address range is ok to read or write or both.
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
static ieee_floatt zero(const floatbv_typet &type)
const typet & return_type() const
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const code_blockt & to_code_block(const codet &code)
The byte swap expression.
C Language Type Checking.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
constant_exprt to_expr() const
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
codet & find_last_statement()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
signedbv_typet pointer_diff_type()
unsignedbv_typet size_type()
const irep_idt & get_statement() const
A constant literal expression.
IEEE-floating-point equality.
mstreamt & warning() const
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
virtual void typecheck_expr_sizeof(exprt &expr)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
static ieee_float_spect single_precision()
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
ranget< iteratort > make_range(iteratort begin, iteratort end)
A type for mathematical functions (do not confuse with functions/methods in code)
Evaluates to true if the operand is a normal number.
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
An expression containing a side effect.
API to expression classes for bitvectors.
virtual void typecheck_expr_index(exprt &expr)
virtual void make_index_type(exprt &expr)
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
Evaluates to true if the operand is NaN.
API to expression classes for 'mathematical' expressions.
ANSI-C Language Type Checking.
Data structure for representing an arbitrary statement in a program.
virtual void typecheck_expr_comma(exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.