Go to the documentation of this file.
47 if(expr.
id()==ID_already_typechecked)
65 if(expr.
id()==ID_div ||
70 if(expr.
type().
id()==ID_floatbv &&
79 expr.
id(ID_floatbv_div);
80 else if(expr.
id()==ID_mult)
81 expr.
id(ID_floatbv_mult);
82 else if(expr.
id()==ID_plus)
83 expr.
id(ID_floatbv_plus);
84 else if(expr.
id()==ID_minus)
85 expr.
id(ID_floatbv_minus);
106 if(type1.
id()==ID_c_enum_tag)
108 else if(type2.
id()==ID_c_enum_tag)
111 if(type1.
id()==ID_c_enum)
113 if(type2.
id()==ID_c_enum)
115 else if(type2==type1.
subtype())
118 else if(type2.
id()==ID_c_enum)
123 else if(type1.
id()==ID_pointer &&
124 type2.
id()==ID_pointer)
128 else if(type1.
id()==ID_array &&
129 type2.
id()==ID_array)
134 else if(type1.
id()==ID_code &&
148 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
164 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
174 if(expr.
id()==ID_side_effect)
176 else if(expr.
id()==ID_constant)
178 else if(expr.
id()==ID_infinity)
182 else if(expr.
id()==ID_symbol)
184 else if(expr.
id()==ID_unary_plus ||
185 expr.
id()==ID_unary_minus ||
186 expr.
id()==ID_bitnot)
188 else if(expr.
id()==ID_not)
191 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
194 else if(expr.
id()==ID_address_of)
196 else if(expr.
id()==ID_dereference)
198 else if(expr.
id()==ID_member)
200 else if(expr.
id()==ID_ptrmember)
202 else if(expr.
id()==ID_equal ||
203 expr.
id()==ID_notequal ||
209 else if(expr.
id()==ID_index)
211 else if(expr.
id()==ID_typecast)
213 else if(expr.
id()==ID_sizeof)
215 else if(expr.
id()==ID_alignof)
218 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
219 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
220 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
224 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
226 else if(expr.
id()==ID_comma)
228 else if(expr.
id()==ID_if)
230 else if(expr.
id()==ID_code)
233 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
236 else if(expr.
id()==ID_gcc_builtin_va_arg)
238 else if(expr.
id()==ID_cw_va_arg_typeof)
240 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
245 assert(subtypes.size()==2);
251 subtypes[0].
remove(ID_C_constant);
252 subtypes[0].remove(ID_C_volatile);
253 subtypes[0].remove(ID_C_restricted);
254 subtypes[1].remove(ID_C_constant);
255 subtypes[1].remove(ID_C_volatile);
256 subtypes[1].remove(ID_C_restricted);
261 else if(expr.
id()==ID_clang_builtin_convertvector)
270 else if(expr.
id()==ID_builtin_offsetof)
272 else if(expr.
id()==ID_string_constant)
275 expr.
set(ID_C_lvalue,
true);
277 else if(expr.
id()==ID_arguments)
281 else if(expr.
id()==ID_designated_initializer)
283 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
287 if(it->id()==ID_index)
291 else if(expr.
id()==ID_initializer_list)
297 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
303 auto &bindings = binary_expr.op0().operands();
304 auto &where = binary_expr.op1();
306 for(
const auto &binding : bindings)
308 if(binding.get(ID_statement) != ID_decl)
311 error() <<
"expected declaration as operand of quantifier" <<
eom;
319 error() <<
"quantifier must not contain side effects" <<
eom;
324 for(
auto &binding : bindings)
327 if(expr.
id() == ID_lambda)
331 for(
auto &binding : bindings)
332 domain.push_back(binding.type());
342 else if(expr.
id()==ID_label)
346 else if(expr.
id()==ID_array)
350 else if(expr.
id()==ID_complex)
355 else if(expr.
id() == ID_complex_real)
359 if(op.
type().
id() != ID_complex)
364 error() <<
"real part retrieval expects numerical operand, "
372 expr.
swap(complex_real_expr);
380 complex_real_expr.
set(ID_C_lvalue,
true);
383 complex_real_expr.
type().
set(ID_C_constant,
true);
385 expr.
swap(complex_real_expr);
388 else if(expr.
id() == ID_complex_imag)
392 if(op.
type().
id() != ID_complex)
397 error() <<
"real part retrieval expects numerical operand, "
405 expr.
swap(complex_imag_expr);
413 complex_imag_expr.
set(ID_C_lvalue,
true);
416 complex_imag_expr.
type().
set(ID_C_constant,
true);
418 expr.
swap(complex_imag_expr);
421 else if(expr.
id()==ID_generic_selection)
431 if(op.type().id() == ID_bool)
438 for(
auto &irep : generic_associations)
440 if(irep.get(ID_type_arg) != ID_default)
442 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
453 for(
const auto &irep : generic_associations)
455 if(irep.get(ID_type_arg) == ID_default)
456 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
458 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
460 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
467 expr.
swap(default_match);
471 error() <<
"unmatched generic selection: " <<
to_string(op.type())
477 expr.
swap(assoc_match);
482 else if(expr.
id()==ID_gcc_asm_input ||
483 expr.
id()==ID_gcc_asm_output ||
484 expr.
id()==ID_gcc_asm_clobbered_register)
487 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
488 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
492 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
510 expr.
set(ID_C_lvalue,
true);
547 symbol.
name=ID_gcc_builtin_va_arg;
548 symbol.
type=symbol_type;
578 error() <<
"builtin_offsetof expects no operands" <<
eom;
593 if(m_it->id()==ID_member)
595 if(type.
id()!=ID_union && type.
id()!=ID_struct)
598 error() <<
"offsetof of member expects struct/union type, "
604 irep_idt component_name=m_it->get(ID_component_name);
608 assert(type.
id()==ID_union || type.
id()==ID_struct);
618 if(type.
id()==ID_struct)
623 if(!o_opt.has_value())
626 error() <<
"offsetof failed to determine offset of '"
627 << component_name <<
"'" <<
eom;
643 for(
const auto &c : struct_union_type.
components())
647 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
651 if(type.
id()==ID_struct)
656 if(!o_opt.has_value())
659 error() <<
"offsetof failed to determine offset of '"
660 << component_name <<
"'" <<
eom;
672 assert(type.
id()==ID_union || type.
id()==ID_struct);
682 error() <<
"offset-of of member failed to find component '"
683 << component_name <<
"' in '" <<
to_string(type) <<
"'"
690 else if(m_it->id()==ID_index)
692 if(type.
id()!=ID_array)
695 error() <<
"offsetof of index expects array type" <<
eom;
706 if(!sub_size_opt.has_value())
709 error() <<
"offsetof failed to determine array element size" <<
eom;
732 if(expr.
id()==ID_side_effect &&
733 expr.
get(ID_statement)==ID_function_call)
738 else if(expr.
id()==ID_side_effect &&
739 expr.
get(ID_statement)==ID_statement_expression)
744 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
750 auto &bindings = binary_expr.op0().operands();
752 for(
auto &binding : bindings)
761 error() <<
"forall/exists expects one declarator exactly" <<
eom;
768 symbol_tablet::symbolst::const_iterator s_it =
774 error() <<
"failed to find bound symbol `" << identifier
775 <<
"' in symbol table" <<
eom;
779 const symbolt &symbol = s_it->second;
786 error() <<
"unexpected quantified symbol" <<
eom;
810 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
814 expr.
type()=p_it->second;
815 expr.
set(ID_C_lvalue,
true);
820 asm_label_mapt::const_iterator entry=
824 identifier=entry->second;
830 if(
lookup(identifier, symbol_ptr))
833 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
837 const symbolt &symbol=*symbol_ptr;
842 error() <<
"did not expect a type symbol here, but got '"
860 if(expr.
id()==ID_constant &&
862 expr.
set(ID_C_cformat, base_name);
877 else if(identifier==
"__func__" ||
878 identifier==
"__FUNCTION__" ||
879 identifier==
"__PRETTY_FUNCTION__")
885 s.
set(ID_C_lvalue,
true);
896 expr.
set(ID_C_lvalue,
true);
898 if(expr.
type().
id()==ID_code)
901 tmp.
set(ID_C_implicit,
true);
920 if(last_statement==ID_expression)
926 if(op.
type().
id()==ID_array)
959 if(op.
type().
id() == ID_bool)
967 if(type.
id()==ID_c_bit_field)
970 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
973 else if(type.
id() == ID_bool)
976 error() <<
"sizeof cannot be applied to single bits" <<
eom;
979 else if(type.
id() == ID_empty)
988 (type.
id() == ID_struct_tag &&
990 (type.
id() == ID_union_tag &&
992 (type.
id() == ID_c_enum_tag &&
997 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
1004 if(!size_of_opt.has_value())
1011 new_expr = size_of_opt.value();
1014 new_expr.
swap(expr);
1016 expr.
add(ID_C_c_sizeof_type)=type;
1024 decl_block.set_statement(ID_decl_block);
1034 exprt comma_expr(ID_comma, expr.
type());
1036 expr.
swap(comma_expr);
1042 typet argument_type;
1050 argument_type=op_type;
1074 decl_block.set_statement(ID_decl_block);
1086 op.
swap(comma_expr);
1092 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1093 op.
id() != ID_initializer_list)
1101 if(op.
type().
id() == ID_bool)
1106 for(
const auto &c : union_type.components())
1108 if(c.type() == op.
type())
1114 expr.
set(ID_C_lvalue,
true);
1122 <<
"' not found in union" <<
eom;
1129 if(op.
id()==ID_initializer_list)
1138 exprt tmp(ID_compound_literal, expr.
type());
1142 if(op.
id()==ID_array &&
1143 expr.
type().
id()==ID_array &&
1148 expr.
set(ID_C_lvalue,
true);
1153 if(expr_type.
id()==ID_empty)
1159 if(expr_type == op_type)
1164 if(expr_type.
id()==ID_vector)
1167 if(op_type.
id()==ID_vector)
1169 else if(op_type.
id()==ID_signedbv ||
1170 op_type.
id()==ID_unsignedbv)
1177 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1185 else if(op_type.
id()==ID_array)
1190 else if(op_type.
id()==ID_empty)
1192 if(expr_type.
id()!=ID_empty)
1195 error() <<
"type cast from void only permitted to void, but got '"
1200 else if(op_type.
id()==ID_vector)
1207 if((expr_type.
id()==ID_signedbv ||
1208 expr_type.
id()==ID_unsignedbv) &&
1217 <<
"' not permitted" <<
eom;
1224 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1240 if(expr_type.
id()==ID_pointer)
1241 expr.
set(ID_C_lvalue,
true);
1258 const typet &array_type = array_expr.
type();
1262 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1263 array_type.
id() != ID_vector &&
1266 std::swap(array_expr, index_expr);
1274 const typet final_array_type = array_expr.
type();
1276 if(final_array_type.
id()==ID_array ||
1277 final_array_type.
id()==ID_vector)
1281 if(array_expr.
get_bool(ID_C_lvalue))
1282 expr.
set(ID_C_lvalue,
true);
1284 if(final_array_type.
get_bool(ID_C_constant))
1285 expr.
type().
set(ID_C_constant,
true);
1287 else if(final_array_type.
id()==ID_pointer)
1293 std::swap(summands, expr.
operands());
1295 expr.
id(ID_dereference);
1296 expr.
set(ID_C_lvalue,
true);
1302 error() <<
"operator [] must take array/vector or pointer but got '"
1311 if(expr.
op0().
type().
id() == ID_floatbv)
1313 if(expr.
id()==ID_equal)
1314 expr.
id(ID_ieee_float_equal);
1315 else if(expr.
id()==ID_notequal)
1316 expr.
id(ID_ieee_float_notequal);
1329 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1337 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1341 if(o_type0.
id() != ID_array)
1362 if(type0.
id()==ID_pointer)
1364 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1367 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1368 expr.
id()==ID_ge || expr.
id()==ID_gt)
1372 if(type0.
id()==ID_string_constant)
1374 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1381 if(type0.
id()==ID_pointer &&
1388 if(type1.
id()==ID_pointer &&
1408 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1416 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1427 if(o_type0.
id() != ID_vector || o_type0 != o_type1)
1430 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1444 if(expr.
id() == ID_notequal)
1445 expr.
id(ID_vector_notequal);
1453 const typet &op0_type = op.type();
1455 if(op0_type.
id() == ID_array)
1460 index_expr.
set(ID_C_lvalue,
true);
1461 op.swap(index_expr);
1463 else if(op0_type.
id() == ID_pointer)
1469 op.swap(deref_expr);
1474 error() <<
"ptrmember operator requires pointer or array type "
1475 "on left hand side, but got '"
1491 if(type.
id()!=ID_struct &&
1492 type.
id()!=ID_union)
1495 error() <<
"member operator requires structure type "
1496 "on left hand side but got '"
1507 error() <<
"member operator got incomplete " << type.
id()
1508 <<
" type on left hand side" <<
eom;
1513 expr.
get(ID_component_name);
1529 error() <<
"member '" << component_name <<
"' not found in '"
1542 expr.
set(ID_C_lvalue,
true);
1545 expr.
type().
set(ID_C_constant,
true);
1550 if(!identifier.
empty())
1551 expr.
set(ID_C_identifier, identifier);
1555 if(access==ID_private)
1558 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1567 assert(operands.size()==3);
1570 const typet o_type0=operands[0].type();
1571 const typet o_type1=operands[1].type();
1572 const typet o_type2=operands[2].type();
1577 if(operands[1].type().
id()==ID_pointer &&
1578 operands[2].type().
id()!=ID_pointer)
1580 else if(operands[2].type().
id()==ID_pointer &&
1581 operands[1].type().
id()!=ID_pointer)
1584 if(operands[1].type().
id()==ID_pointer &&
1585 operands[2].type().
id()==ID_pointer &&
1586 operands[1].type()!=operands[2].type())
1593 if(operands[1].type().subtype().
id()==ID_empty &&
1597 else if(operands[2].type().subtype().
id()==ID_empty &&
1601 else if(operands[1].type().subtype().
id()!=ID_code ||
1602 operands[2].type().subtype().
id()!=ID_code)
1626 if(operands[1].type().
id()==ID_empty ||
1627 operands[2].type().
id()==ID_empty)
1633 if(operands[1].type() == operands[2].type())
1635 expr.
type()=operands[1].type();
1641 if(operands[1].get_bool(ID_C_lvalue) &&
1642 operands[2].get_bool(ID_C_lvalue))
1643 expr.
set(ID_C_lvalue,
true);
1649 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1662 if(operands.size()!=2)
1665 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1671 if_exprt if_expr(operands[0], operands[0], operands[1]);
1686 if(op.
type().
id()==ID_c_bit_field)
1689 error() <<
"cannot take address of a bit field" <<
eom;
1693 if(op.
type().
id() == ID_bool)
1696 error() <<
"cannot take address of a single bit" <<
eom;
1701 if(op.
id()==ID_label)
1714 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1720 tmp.
set(ID_C_implicit,
false);
1725 if(op.
id()==ID_struct ||
1726 op.
id()==ID_union ||
1727 op.
id()==ID_array ||
1728 op.
id()==ID_string_constant)
1736 else if(op.
type().
id()==ID_code)
1743 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1757 if(op_type.
id()==ID_array)
1765 else if(op_type.
id()==ID_pointer)
1773 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1778 expr.
set(ID_C_lvalue,
true);
1789 if(expr.
type().
id()==ID_code)
1792 tmp.
set(ID_C_implicit,
true);
1802 if(statement==ID_preincrement ||
1803 statement==ID_predecrement ||
1804 statement==ID_postincrement ||
1805 statement==ID_postdecrement)
1814 <<
"' not an lvalue" <<
eom;
1825 if(type0.
id() == ID_c_enum_tag)
1831 error() <<
"operator '" << statement <<
"' given incomplete type '"
1840 else if(type0.
id() == ID_c_bit_field)
1845 expr.
type()=underlying_type;
1847 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1856 else if(type0.
id() == ID_pointer)
1864 error() <<
"operator '" << statement <<
"' not defined for type '"
1871 else if(statement==ID_function_call)
1874 else if(statement==ID_statement_expression)
1876 else if(statement==ID_gcc_conditional_expression)
1881 error() <<
"unknown side effect: " << statement <<
eom;
1892 error() <<
"function_call side effect expects two operands" <<
eom;
1901 if(f_op.
id()==ID_symbol)
1905 asm_label_mapt::const_iterator entry=
1908 identifier=entry->second;
1919 identifier ==
"__noop" &&
1933 identifier ==
"__builtin_shuffle" &&
1942 identifier ==
"__builtin_shufflevector" &&
1954 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1957 !parameters.empty(),
1958 "GCC polymorphic built-ins should have at least one parameter");
1963 if(parameters.front().type().id() == ID_pointer)
1965 identifier_with_type =
id2string(identifier) +
"_" +
1967 parameters.front().type().subtype(), *
this);
1971 identifier_with_type =
1975 gcc_polymorphic->set_identifier(identifier_with_type);
1979 for(std::size_t i = 0; i < parameters.size(); ++i)
1986 id2string(identifier_with_type) +
"::" + base_name;
1989 new_symbol.
type = parameters[i].type();
1992 new_symbol.
mode = ID_C;
1994 parameters[i].set_identifier(new_symbol.
name);
1995 parameters[i].set_base_name(new_symbol.
base_name);
2002 new_symbol.
name = identifier_with_type;
2003 new_symbol.
base_name = identifier_with_type;
2005 new_symbol.
type = gcc_polymorphic->type();
2006 new_symbol.
mode = ID_C;
2013 new_symbol.
value = implementation;
2018 f_op = std::move(*gcc_polymorphic);
2030 if(identifier==
"malloc" ||
2031 identifier==
"realloc" ||
2032 identifier==
"reallocf" ||
2033 identifier==
"valloc")
2040 new_symbol.
name=identifier;
2044 new_symbol.
type.
set(ID_C_incomplete,
true);
2052 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2062 if(f_op_type.
id() == ID_mathematical_function)
2064 const auto &mathematical_function_type =
2068 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2071 error() <<
"expected " << mathematical_function_type.domain().size()
2072 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2080 if(p.first.type() != p.second)
2093 expr.
swap(function_application);
2097 if(f_op_type.
id()!=ID_pointer)
2100 error() <<
"expected function/function pointer as argument but got '"
2106 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2113 tmp.
set(ID_C_implicit,
true);
2118 if(f_op.
type().
id()!=ID_code)
2121 error() <<
"expected code as argument" <<
eom;
2144 if(f_op.
id()!=ID_symbol)
2154 error() <<
"same_object expects two operands" <<
eom;
2160 exprt same_object_expr=
2164 return same_object_expr;
2171 error() <<
"get_must expects two operands" <<
eom;
2181 return std::move(get_must_expr);
2188 error() <<
"get_may expects two operands" <<
eom;
2198 return std::move(get_may_expr);
2205 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2214 return same_object_expr;
2221 error() <<
"buffer_size expects one operand" <<
eom;
2231 return buffer_size_expr;
2238 error() <<
"is_zero_string expects one operand" <<
eom;
2246 is_zero_string_expr.
set(ID_C_lvalue,
true);
2249 return std::move(is_zero_string_expr);
2256 error() <<
"zero_string_length expects one operand" <<
eom;
2262 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2264 zero_string_length_expr.
set(ID_C_lvalue,
true);
2267 return zero_string_length_expr;
2274 error() <<
"dynamic_object expects one argument" <<
eom;
2283 return is_dynamic_object_expr;
2290 error() <<
"pointer_offset expects one argument" <<
eom;
2306 error() <<
"object_size expects one operand" <<
eom;
2316 return std::move(object_size_expr);
2323 error() <<
"pointer_object expects one argument" <<
eom;
2334 else if(identifier==
"__builtin_bswap16" ||
2335 identifier==
"__builtin_bswap32" ||
2336 identifier==
"__builtin_bswap64")
2341 error() << identifier <<
" expects one operand" <<
eom;
2351 return std::move(bswap_expr);
2354 identifier ==
"__builtin_rotateleft8" ||
2355 identifier ==
"__builtin_rotateleft16" ||
2356 identifier ==
"__builtin_rotateleft32" ||
2357 identifier ==
"__builtin_rotateleft64" ||
2358 identifier ==
"__builtin_rotateright8" ||
2359 identifier ==
"__builtin_rotateright16" ||
2360 identifier ==
"__builtin_rotateright32" ||
2361 identifier ==
"__builtin_rotateright64")
2367 error() << identifier <<
" expects two operands" <<
eom;
2373 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2374 identifier ==
"__builtin_rotateleft16" ||
2375 identifier ==
"__builtin_rotateleft32" ||
2376 identifier ==
"__builtin_rotateleft64")
2383 return std::move(rotate_expr);
2385 else if(identifier==
"__builtin_nontemporal_load")
2390 error() << identifier <<
" expects one operand" <<
eom;
2399 if(ptr_arg.
type().
id()!=ID_pointer)
2402 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2411 identifier ==
"__builtin_fpclassify" ||
2417 error() << identifier <<
" expects six arguments" <<
eom;
2430 if(fp_value.
type().
id() != ID_floatbv)
2433 error() <<
"non-floating-point argument for " << identifier <<
eom;
2441 const auto &arguments = expr.
arguments();
2460 identifier==
"__builtin_isnan")
2465 error() <<
"isnan expects one operand" <<
eom;
2483 error() <<
"isfinite expects one operand" <<
eom;
2495 identifier==
"__builtin_inf")
2502 return std::move(inf_expr);
2511 return std::move(inff_expr);
2520 return std::move(infl_expr);
2532 error() <<
"abs-functions expect one operand" <<
eom;
2541 return std::move(abs_expr);
2548 error() <<
"allocate expects two operands" <<
eom;
2557 return std::move(malloc_expr);
2565 error() << identifier <<
" expects two operands" <<
eom;
2576 return std::move(ok_expr);
2581 identifier==
"__builtin_isinf")
2586 error() << identifier <<
" expects one operand" <<
eom;
2594 if(fp_value.
type().
id() != ID_floatbv)
2597 error() <<
"non-floating-point argument for " << identifier <<
eom;
2606 else if(identifier ==
"__builtin_isinf_sign")
2611 error() << identifier <<
" expects one operand" <<
eom;
2621 if(fp_value.
type().
id() != ID_floatbv)
2624 error() <<
"non-floating-point argument for " << identifier <<
eom;
2642 identifier ==
"__builtin_isnormal")
2647 error() << identifier <<
" expects one operand" <<
eom;
2655 if(fp_value.
type().
id() != ID_floatbv)
2658 error() <<
"non-floating-point argument for " << identifier <<
eom;
2670 identifier==
"__builtin_signbit" ||
2671 identifier==
"__builtin_signbitf" ||
2672 identifier==
"__builtin_signbitl")
2677 error() << identifier <<
" expects one operand" <<
eom;
2688 else if(identifier==
"__builtin_popcount" ||
2689 identifier==
"__builtin_popcountl" ||
2690 identifier==
"__builtin_popcountll" ||
2691 identifier==
"__popcnt16" ||
2692 identifier==
"__popcnt" ||
2693 identifier==
"__popcnt64")
2698 error() << identifier <<
" expects one operand" <<
eom;
2707 return std::move(popcount_expr);
2710 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2711 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2712 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2717 error() << identifier <<
" expects one operand" <<
eom;
2728 return std::move(clz);
2735 error() <<
"equal expects two operands" <<
eom;
2748 error() <<
"equal expects two operands of same type" <<
eom;
2752 return std::move(equality_expr);
2754 else if(identifier==
"__builtin_expect")
2765 error() <<
"__builtin_expect expects two arguments" <<
eom;
2773 else if(identifier==
"__builtin_object_size")
2782 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2799 error() <<
"__builtin_object_size expects constant as second argument, "
2807 if(arg1==0 || arg1==1)
2820 else if(identifier==
"__builtin_choose_expr")
2826 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2841 else if(identifier==
"__builtin_constant_p")
2848 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2864 tmp1.
id() == ID_typecast &&
2870 .
id() == ID_string_constant)
2882 else if(identifier==
"__builtin_classify_type")
2889 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2902 if(type.
id() == ID_c_bit_field)
2905 unsigned type_number;
2907 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2918 type.
id() == ID_empty
2920 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
2922 : (type.
id() == ID_pointer || type.
id() == ID_array)
2924 : type.
id() == ID_floatbv
2926 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
2928 : type.
id() == ID_struct
2930 : type.
id() == ID_union
2951 overflow.
id(ID_minus);
2956 overflow.id(ID_mult);
2961 overflow.id(ID_plus);
2966 overflow.id(ID_shl);
2971 overflow.
operands()[0], overflow.id(), overflow.operands()[1]};
2972 of.add_source_location() = overflow.source_location();
2973 return std::move(of);
2983 overflow.add_source_location() = tmp.source_location();
2984 return std::move(overflow);
2991 std::ostringstream error_message;
2993 <<
" takes exactly 1 argument, but "
2994 << expr.
arguments().size() <<
" were provided";
3002 std::ostringstream error_message;
3004 <<
" expects enum, but (" <<
expr2c(arg1, *
this)
3005 <<
") has type `" <<
type2c(arg1.type(), *
this) <<
'`';
3014 identifier ==
"__builtin_add_overflow" ||
3015 identifier ==
"__builtin_sub_overflow" ||
3016 identifier ==
"__builtin_mul_overflow" ||
3017 identifier ==
"__builtin_add_overflow_p" ||
3018 identifier ==
"__builtin_sub_overflow_p" ||
3019 identifier ==
"__builtin_mul_overflow_p")
3024 std::ostringstream error_message;
3026 <<
" takes exactly 3 arguments, but "
3027 << expr.
arguments().size() <<
" were provided";
3040 auto const raise_wrong_argument_error =
3042 const exprt &wrong_argument, std::size_t argument_number,
bool _p) {
3043 std::ostringstream error_message;
3045 << identifier <<
" has signature " << identifier
3046 <<
"(integral, integral, integral" << (_p ?
"" :
"*")
3048 <<
"but argument " << argument_number <<
" ("
3049 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3050 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3053 for(
int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3055 auto const &argument = expr.
arguments()[arg_index];
3059 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3064 (
result.type().id() != ID_pointer ||
3067 raise_wrong_argument_error(
result, 3, is__p_variant);
3100 if(code_type.
get_bool(ID_C_incomplete))
3104 else if(code_type.
is_KnR())
3109 while(parameter_types.size()>arguments.size())
3114 if(parameter_types.size()>arguments.size())
3117 error() <<
"not enough function arguments" <<
eom;
3121 else if(parameter_types.size()!=arguments.size())
3124 error() <<
"wrong number of function arguments: "
3125 <<
"expected " << parameter_types.size()
3126 <<
", but got " << arguments.size() <<
eom;
3130 for(std::size_t i=0; i<arguments.size(); i++)
3132 exprt &op=arguments[i];
3138 else if(i<parameter_types.size())
3143 const typet &op_type=parameter_type.
type();
3145 if(op_type.
id()==ID_bool &&
3146 op.
id()==ID_side_effect &&
3147 op.
get(ID_statement)==ID_assign &&
3151 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3160 if(op.
type().
id() == ID_array)
3163 dest_type.
subtype().
set(ID_C_constant,
true);
3181 if(o_type.
id()==ID_vector)
3200 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3224 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3225 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3234 if((type0.
subtype().
id()==ID_signedbv ||
3254 if(o_type0.
id()==ID_vector &&
3255 o_type1.
id()==ID_vector)
3269 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3274 expr.
type() = o_type0;
3278 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3283 expr.
type() = o_type1;
3294 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3295 expr.
id()==ID_mult || expr.
id()==ID_div)
3297 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3302 else if(type0==type1)
3311 else if(expr.
id()==ID_mod)
3315 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3323 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3324 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3333 else if(type0.
id()==ID_bool)
3335 if(expr.
id()==ID_bitand)
3337 else if(expr.
id() == ID_bitnand)
3339 else if(expr.
id()==ID_bitor)
3341 else if(expr.
id()==ID_bitxor)
3352 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3360 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3368 if(o_type0.
id()==ID_vector &&
3369 o_type1.
id()==ID_vector)
3400 if(expr.
id()==ID_shr)
3404 if(op0_type.
id()==ID_unsignedbv)
3409 else if(op0_type.
id()==ID_signedbv)
3420 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3429 assert(type.
id()==ID_pointer);
3434 subtype.
id() == ID_struct_tag &&
3438 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3442 subtype.
id() == ID_union_tag &&
3446 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3460 if(expr.
id()==ID_minus ||
3461 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3463 if(type0.
id()==ID_pointer &&
3464 type1.
id()==ID_pointer)
3474 if(type0.
id()==ID_pointer &&
3475 (type1.
id()==ID_bool ||
3476 type1.
id()==ID_c_bool ||
3477 type1.
id()==ID_unsignedbv ||
3478 type1.
id()==ID_signedbv ||
3479 type1.
id()==ID_c_bit_field ||
3480 type1.
id()==ID_c_enum_tag))
3488 else if(expr.
id()==ID_plus ||
3489 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3491 exprt *p_op, *int_op;
3493 if(type0.
id()==ID_pointer)
3498 else if(type1.
id()==ID_pointer)
3505 p_op=int_op=
nullptr;
3509 const typet &int_op_type = int_op->
type();
3511 if(int_op_type.
id()==ID_bool ||
3512 int_op_type.
id()==ID_c_bool ||
3513 int_op_type.
id()==ID_unsignedbv ||
3514 int_op_type.
id()==ID_signedbv ||
3515 int_op_type.
id()==ID_c_bit_field ||
3516 int_op_type.
id()==ID_c_enum_tag)
3527 if(expr.
id()==ID_side_effect)
3533 error() <<
"operator '" << op_name <<
"' not defined for types '"
3564 if(type0.
id()==ID_empty)
3567 error() <<
"cannot assign void" <<
eom;
3574 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3587 if(type0.
id() == ID_array)
3590 error() <<
"direct assignments to arrays not permitted" <<
eom;
3597 if(op0.
type().
id()==ID_c_bit_field)
3603 expr.
type()=o_type0;
3605 if(statement==ID_assign)
3610 else if(statement==ID_assign_shl ||
3611 statement==ID_assign_shr)
3613 if(o_type0.
id() == ID_vector)
3633 if(statement==ID_assign_shl)
3643 if(underlying_type.
id()==ID_unsignedbv ||
3644 underlying_type.
id()==ID_c_bool)
3646 expr.
set(ID_statement, ID_assign_lshr);
3649 else if(underlying_type.
id()==ID_signedbv)
3651 expr.
set(ID_statement, ID_assign_ashr);
3657 else if(statement==ID_assign_bitxor ||
3658 statement==ID_assign_bitand ||
3659 statement==ID_assign_bitor)
3662 if(o_type0.
id()==ID_bool ||
3663 o_type0.
id()==ID_c_bool)
3666 if(op1.
type().
id()==ID_bool ||
3667 op1.
type().
id()==ID_c_bool ||
3668 op1.
type().
id()==ID_c_enum_tag ||
3669 op1.
type().
id()==ID_unsignedbv ||
3670 op1.
type().
id()==ID_signedbv)
3673 else if(o_type0.
id()==ID_c_enum_tag ||
3674 o_type0.
id()==ID_unsignedbv ||
3675 o_type0.
id()==ID_signedbv ||
3676 o_type0.
id()==ID_c_bit_field)
3681 else if(o_type0.
id()==ID_vector &&
3682 o_type1.
id()==ID_vector)
3693 o_type0.
id() == ID_vector &&
3694 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
3695 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
3696 o_type1.
id() == ID_signedbv))
3705 if(o_type0.
id()==ID_pointer &&
3706 (statement==ID_assign_minus || statement==ID_assign_plus))
3711 else if(o_type0.
id()==ID_vector &&
3712 o_type1.
id()==ID_vector)
3722 else if(o_type0.
id() == ID_vector)
3728 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
3734 else if(o_type0.
id()==ID_bool ||
3735 o_type0.
id()==ID_c_bool)
3738 if(op1.
type().
id()==ID_bool ||
3739 op1.
type().
id()==ID_c_bool ||
3740 op1.
type().
id()==ID_c_enum_tag ||
3741 op1.
type().
id()==ID_unsignedbv ||
3742 op1.
type().
id()==ID_signedbv)
3750 op1.
type().
id()==ID_bool ||
3751 op1.
type().
id()==ID_c_bool ||
3752 op1.
type().
id()==ID_c_enum_tag)
3758 error() <<
"assignment '" << statement <<
"' not defined for types '"
3770 const auto rounding_mode =
3777 expr.
id()!=ID_infinity)
3780 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3793 expr.
id()!=ID_infinity)
3796 error() <<
"conversion to integer constant failed" <<
eom;
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
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)
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.
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
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)
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.
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.
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.