Go to the documentation of this file.
41 if(expr.
id()==ID_already_typechecked)
59 if(expr.
id()==ID_div ||
64 if(expr.
type().
id()==ID_floatbv &&
73 expr.
id(ID_floatbv_div);
74 else if(expr.
id()==ID_mult)
75 expr.
id(ID_floatbv_mult);
76 else if(expr.
id()==ID_plus)
77 expr.
id(ID_floatbv_plus);
78 else if(expr.
id()==ID_minus)
79 expr.
id(ID_floatbv_minus);
100 if(type1.
id()==ID_c_enum_tag)
102 else if(type2.
id()==ID_c_enum_tag)
105 if(type1.
id()==ID_c_enum)
107 if(type2.
id()==ID_c_enum)
109 else if(type2==type1.
subtype())
112 else if(type2.
id()==ID_c_enum)
117 else if(type1.
id()==ID_pointer &&
118 type2.
id()==ID_pointer)
122 else if(type1.
id()==ID_array &&
123 type2.
id()==ID_array)
128 else if(type1.
id()==ID_code &&
142 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
158 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
168 if(expr.
id()==ID_side_effect)
170 else if(expr.
id()==ID_constant)
172 else if(expr.
id()==ID_infinity)
176 else if(expr.
id()==ID_symbol)
178 else if(expr.
id()==ID_unary_plus ||
179 expr.
id()==ID_unary_minus ||
180 expr.
id()==ID_bitnot)
182 else if(expr.
id()==ID_not)
185 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
188 else if(expr.
id()==ID_address_of)
190 else if(expr.
id()==ID_dereference)
192 else if(expr.
id()==ID_member)
194 else if(expr.
id()==ID_ptrmember)
196 else if(expr.
id()==ID_equal ||
197 expr.
id()==ID_notequal ||
203 else if(expr.
id()==ID_index)
205 else if(expr.
id()==ID_typecast)
207 else if(expr.
id()==ID_sizeof)
209 else if(expr.
id()==ID_alignof)
212 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
213 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
214 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
218 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
220 else if(expr.
id()==ID_comma)
222 else if(expr.
id()==ID_if)
224 else if(expr.
id()==ID_code)
227 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
230 else if(expr.
id()==ID_gcc_builtin_va_arg)
232 else if(expr.
id()==ID_cw_va_arg_typeof)
234 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
239 assert(subtypes.size()==2);
245 subtypes[0].
remove(ID_C_constant);
246 subtypes[0].remove(ID_C_volatile);
247 subtypes[0].remove(ID_C_restricted);
248 subtypes[1].remove(ID_C_constant);
249 subtypes[1].remove(ID_C_volatile);
250 subtypes[1].remove(ID_C_restricted);
255 else if(expr.
id()==ID_clang_builtin_convertvector)
264 else if(expr.
id()==ID_builtin_offsetof)
266 else if(expr.
id()==ID_string_constant)
269 expr.
set(ID_C_lvalue,
true);
271 else if(expr.
id()==ID_arguments)
275 else if(expr.
id()==ID_designated_initializer)
277 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
281 if(it->id()==ID_index)
285 else if(expr.
id()==ID_initializer_list)
290 else if(expr.
id()==ID_forall ||
291 expr.
id()==ID_exists)
297 auto &bindings = binary_expr.op0().operands();
298 auto &where = binary_expr.op1();
300 for(
const auto &binding : bindings)
302 if(binding.get(ID_statement) != ID_decl)
305 error() <<
"expected declaration as operand of quantifier" <<
eom;
313 error() <<
"quantifier must not contain side effects" <<
eom;
320 for(
auto &binding : bindings)
325 else if(expr.
id()==ID_label)
329 else if(expr.
id()==ID_array)
333 else if(expr.
id()==ID_complex)
338 else if(expr.
id() == ID_complex_real)
342 if(op.
type().
id() != ID_complex)
347 error() <<
"real part retrieval expects numerical operand, "
355 expr.
swap(complex_real_expr);
363 complex_real_expr.
set(ID_C_lvalue,
true);
366 complex_real_expr.
type().
set(ID_C_constant,
true);
368 expr.
swap(complex_real_expr);
371 else if(expr.
id() == ID_complex_imag)
375 if(op.
type().
id() != ID_complex)
380 error() <<
"real part retrieval expects numerical operand, "
388 expr.
swap(complex_imag_expr);
396 complex_imag_expr.
set(ID_C_lvalue,
true);
399 complex_imag_expr.
type().
set(ID_C_constant,
true);
401 expr.
swap(complex_imag_expr);
404 else if(expr.
id()==ID_generic_selection)
414 if(op.type().id() == ID_bool)
422 if(it->get(ID_type_arg)!=ID_default)
424 typet &type=
static_cast<typet &
>(it->add(ID_type_arg));
436 if(it->get(ID_type_arg)==ID_default)
437 default_match=
static_cast<const exprt &
>(it->find(ID_value));
439 follow(
static_cast<const typet &
>(it->find(ID_type_arg))))
440 assoc_match=
static_cast<const exprt &
>(it->find(ID_value));
446 expr.
swap(default_match);
450 error() <<
"unmatched generic selection: " <<
to_string(op.type())
456 expr.
swap(assoc_match);
461 else if(expr.
id()==ID_gcc_asm_input ||
462 expr.
id()==ID_gcc_asm_output ||
463 expr.
id()==ID_gcc_asm_clobbered_register)
466 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
467 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
485 expr.
set(ID_C_lvalue,
true);
522 symbol.
name=ID_gcc_builtin_va_arg;
523 symbol.
type=symbol_type;
553 error() <<
"builtin_offsetof expects no operands" <<
eom;
568 if(m_it->id()==ID_member)
570 if(type.
id()!=ID_union && type.
id()!=ID_struct)
573 error() <<
"offsetof of member expects struct/union type, "
579 irep_idt component_name=m_it->get(ID_component_name);
583 assert(type.
id()==ID_union || type.
id()==ID_struct);
593 if(type.
id()==ID_struct)
598 if(!o_opt.has_value())
601 error() <<
"offsetof failed to determine offset of '"
602 << component_name <<
"'" <<
eom;
618 for(
const auto &c : struct_union_type.
components())
622 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
626 if(type.
id()==ID_struct)
631 if(!o_opt.has_value())
634 error() <<
"offsetof failed to determine offset of '"
635 << component_name <<
"'" <<
eom;
647 assert(type.
id()==ID_union || type.
id()==ID_struct);
657 error() <<
"offset-of of member failed to find component '"
658 << component_name <<
"' in '" <<
to_string(type) <<
"'"
665 else if(m_it->id()==ID_index)
667 if(type.
id()!=ID_array)
670 error() <<
"offsetof of index expects array type" <<
eom;
681 if(!sub_size_opt.has_value())
684 error() <<
"offsetof failed to determine array element size" <<
eom;
707 if(expr.
id()==ID_side_effect &&
708 expr.
get(ID_statement)==ID_function_call)
713 else if(expr.
id()==ID_side_effect &&
714 expr.
get(ID_statement)==ID_statement_expression)
718 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
724 auto &bindings = binary_expr.op0().operands();
726 for(
auto &binding : bindings)
735 error() <<
"forall/exists expects one declarator exactly" <<
eom;
742 symbol_tablet::symbolst::const_iterator s_it =
748 error() <<
"failed to find bound symbol `" << identifier
749 <<
"' in symbol table" <<
eom;
753 const symbolt &symbol = s_it->second;
760 error() <<
"unexpected quantified symbol" <<
eom;
784 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
788 expr.
type()=p_it->second;
789 expr.
set(ID_C_lvalue,
true);
794 asm_label_mapt::const_iterator entry=
798 identifier=entry->second;
804 if(
lookup(identifier, symbol_ptr))
807 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
811 const symbolt &symbol=*symbol_ptr;
816 error() <<
"did not expect a type symbol here, but got '"
834 if(expr.
id()==ID_constant &&
836 expr.
set(ID_C_cformat, base_name);
851 else if(identifier==
"__func__" ||
852 identifier==
"__FUNCTION__" ||
853 identifier==
"__PRETTY_FUNCTION__")
859 s.
set(ID_C_lvalue,
true);
870 expr.
set(ID_C_lvalue,
true);
872 if(expr.
type().
id()==ID_code)
875 tmp.
set(ID_C_implicit,
true);
894 if(last_statement==ID_expression)
900 if(op.
type().
id()==ID_array)
934 if(type.
id()==ID_c_bit_field)
937 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
940 else if(type.
id() == ID_bool)
943 error() <<
"sizeof cannot be applied to single bits" <<
eom;
946 else if(type.
id() == ID_empty)
955 (type.
id() == ID_struct_tag &&
957 (type.
id() == ID_union_tag &&
959 (type.
id() == ID_c_enum_tag &&
964 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
971 if(!size_of_opt.has_value())
978 new_expr = size_of_opt.value();
983 expr.
add(ID_C_c_sizeof_type)=type;
991 decl_block.set_statement(ID_decl_block);
1001 exprt comma_expr(ID_comma, expr.
type());
1003 expr.
swap(comma_expr);
1009 typet argument_type;
1017 argument_type=op_type;
1041 decl_block.set_statement(ID_decl_block);
1053 op.
swap(comma_expr);
1059 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1060 op.
id() != ID_initializer_list)
1068 if(op.
type().
id() == ID_bool)
1073 for(
const auto &c : union_type.components())
1075 if(c.type() == op.
type())
1081 expr.
set(ID_C_lvalue,
true);
1089 <<
"' not found in union" <<
eom;
1096 if(op.
id()==ID_initializer_list)
1105 exprt tmp(ID_compound_literal, expr.
type());
1109 if(op.
id()==ID_array &&
1110 expr.
type().
id()==ID_array &&
1115 expr.
set(ID_C_lvalue,
true);
1120 if(expr_type.
id()==ID_empty)
1126 if(expr_type == op_type)
1131 if(expr_type.
id()==ID_vector)
1134 if(op_type.
id()==ID_vector)
1136 else if(op_type.
id()==ID_signedbv ||
1137 op_type.
id()==ID_unsignedbv)
1144 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1152 else if(op_type.
id()==ID_array)
1157 else if(op_type.
id()==ID_empty)
1159 if(expr_type.
id()!=ID_empty)
1162 error() <<
"type cast from void only permitted to void, but got '"
1167 else if(op_type.
id()==ID_vector)
1174 if((expr_type.
id()==ID_signedbv ||
1175 expr_type.
id()==ID_unsignedbv) &&
1184 <<
"' not permitted" <<
eom;
1191 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1207 if(expr_type.
id()==ID_pointer)
1208 expr.
set(ID_C_lvalue,
true);
1225 const typet &array_type = array_expr.
type();
1229 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1230 array_type.
id() != ID_vector &&
1233 std::swap(array_expr, index_expr);
1241 const typet final_array_type = array_expr.
type();
1243 if(final_array_type.
id()==ID_array ||
1244 final_array_type.
id()==ID_vector)
1248 if(array_expr.
get_bool(ID_C_lvalue))
1249 expr.
set(ID_C_lvalue,
true);
1251 if(final_array_type.
get_bool(ID_C_constant))
1252 expr.
type().
set(ID_C_constant,
true);
1254 else if(final_array_type.
id()==ID_pointer)
1260 std::swap(summands, expr.
operands());
1262 expr.
id(ID_dereference);
1263 expr.
set(ID_C_lvalue,
true);
1269 error() <<
"operator [] must take array/vector or pointer but got '"
1278 if(expr.
op0().
type().
id() == ID_floatbv)
1280 if(expr.
id()==ID_equal)
1281 expr.
id(ID_ieee_float_equal);
1282 else if(expr.
id()==ID_notequal)
1283 expr.
id(ID_ieee_float_notequal);
1296 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1304 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1308 if(o_type0.
id() != ID_array)
1329 if(type0.
id()==ID_pointer)
1331 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1334 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1335 expr.
id()==ID_ge || expr.
id()==ID_gt)
1339 if(type0.
id()==ID_string_constant)
1341 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1348 if(type0.
id()==ID_pointer &&
1355 if(type1.
id()==ID_pointer &&
1375 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1383 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1399 o_type0.
id() != ID_vector || o_type1.
id() != ID_vector ||
1403 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1417 const typet &op0_type = op.type();
1419 if(op0_type.
id() == ID_array)
1424 index_expr.
set(ID_C_lvalue,
true);
1425 op.swap(index_expr);
1427 else if(op0_type.
id() == ID_pointer)
1433 op.swap(deref_expr);
1438 error() <<
"ptrmember operator requires pointer or array type "
1439 "on left hand side, but got '"
1455 if(type.
id()!=ID_struct &&
1456 type.
id()!=ID_union)
1459 error() <<
"member operator requires structure type "
1460 "on left hand side but got '"
1471 error() <<
"member operator got incomplete " << type.
id()
1472 <<
" type on left hand side" <<
eom;
1477 expr.
get(ID_component_name);
1493 error() <<
"member '" << component_name <<
"' not found in '"
1506 expr.
set(ID_C_lvalue,
true);
1509 expr.
type().
set(ID_C_constant,
true);
1514 if(!identifier.
empty())
1515 expr.
set(ID_C_identifier, identifier);
1519 if(access==ID_private)
1522 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1531 assert(operands.size()==3);
1534 const typet o_type0=operands[0].type();
1535 const typet o_type1=operands[1].type();
1536 const typet o_type2=operands[2].type();
1541 if(operands[1].type().
id()==ID_pointer &&
1542 operands[2].type().
id()!=ID_pointer)
1544 else if(operands[2].type().
id()==ID_pointer &&
1545 operands[1].type().
id()!=ID_pointer)
1548 if(operands[1].type().
id()==ID_pointer &&
1549 operands[2].type().
id()==ID_pointer &&
1550 operands[1].type()!=operands[2].type())
1557 if(operands[1].type().subtype().
id()==ID_empty &&
1561 else if(operands[2].type().subtype().
id()==ID_empty &&
1565 else if(operands[1].type().subtype().
id()!=ID_code ||
1566 operands[2].type().subtype().
id()!=ID_code)
1590 if(operands[1].type().
id()==ID_empty ||
1591 operands[2].type().
id()==ID_empty)
1597 if(operands[1].type() == operands[2].type())
1599 expr.
type()=operands[1].type();
1605 if(operands[1].get_bool(ID_C_lvalue) &&
1606 operands[2].get_bool(ID_C_lvalue))
1607 expr.
set(ID_C_lvalue,
true);
1613 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1626 if(operands.size()!=2)
1629 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1635 if_exprt if_expr(operands[0], operands[0], operands[1]);
1650 if(op.
type().
id()==ID_c_bit_field)
1653 error() <<
"cannot take address of a bit field" <<
eom;
1657 if(op.
type().
id() == ID_bool)
1660 error() <<
"cannot take address of a single bit" <<
eom;
1665 if(op.
id()==ID_label)
1678 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1684 tmp.
set(ID_C_implicit,
false);
1689 if(op.
id()==ID_struct ||
1690 op.
id()==ID_union ||
1691 op.
id()==ID_array ||
1692 op.
id()==ID_string_constant)
1700 else if(op.
type().
id()==ID_code)
1707 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1721 if(op_type.
id()==ID_array)
1729 else if(op_type.
id()==ID_pointer)
1737 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1742 expr.
set(ID_C_lvalue,
true);
1753 if(expr.
type().
id()==ID_code)
1756 tmp.
set(ID_C_implicit,
true);
1766 if(statement==ID_preincrement ||
1767 statement==ID_predecrement ||
1768 statement==ID_postincrement ||
1769 statement==ID_postdecrement)
1778 <<
"' not an lvalue" <<
eom;
1789 if(type0.
id() == ID_c_enum_tag)
1795 error() <<
"operator '" << statement <<
"' given incomplete type '"
1804 else if(type0.
id() == ID_c_bit_field)
1809 expr.
type()=underlying_type;
1811 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1820 else if(type0.
id() == ID_pointer)
1828 error() <<
"operator '" << statement <<
"' not defined for type '"
1835 else if(statement==ID_function_call)
1838 else if(statement==ID_statement_expression)
1840 else if(statement==ID_gcc_conditional_expression)
1845 error() <<
"unknown side effect: " << statement <<
eom;
1856 error() <<
"function_call side effect expects two operands" <<
eom;
1865 if(f_op.
id()==ID_symbol)
1869 asm_label_mapt::const_iterator entry=
1872 identifier=entry->second;
1886 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1889 !parameters.empty(),
1890 "GCC polymorphic built-ins should have at least one parameter");
1891 if(parameters.front().type().id() == ID_pointer)
1893 identifier_with_type =
1895 type2name(parameters.front().type().subtype(), *
this);
1899 identifier_with_type =
id2string(identifier) +
"_" +
1900 type2name(parameters.front().type(), *
this);
1902 gcc_polymorphic->set_identifier(identifier_with_type);
1906 for(std::size_t i = 0; i < parameters.size(); ++i)
1913 id2string(identifier_with_type) +
"::" + base_name;
1916 new_symbol.
type = parameters[i].type();
1919 new_symbol.
mode = ID_C;
1921 parameters[i].set_identifier(new_symbol.
name);
1922 parameters[i].set_base_name(new_symbol.
base_name);
1929 new_symbol.
name = identifier_with_type;
1930 new_symbol.
base_name = identifier_with_type;
1932 new_symbol.
type = gcc_polymorphic->type();
1933 new_symbol.
mode = ID_C;
1940 new_symbol.
value = implementation;
1945 f_op = std::move(*gcc_polymorphic);
1957 if(identifier==
"malloc" ||
1958 identifier==
"realloc" ||
1959 identifier==
"reallocf" ||
1960 identifier==
"valloc")
1967 new_symbol.
name=identifier;
1971 new_symbol.
type.
set(ID_C_incomplete,
true);
1979 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
1989 if(f_op_type.
id()!=ID_pointer)
1992 error() <<
"expected function/function pointer as argument but got '"
1998 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2005 tmp.
set(ID_C_implicit,
true);
2010 if(f_op.
type().
id()!=ID_code)
2013 error() <<
"expected code as argument" <<
eom;
2036 if(f_op.
id()!=ID_symbol)
2046 error() <<
"same_object expects two operands" <<
eom;
2052 exprt same_object_expr=
2056 return same_object_expr;
2063 error() <<
"get_must expects two operands" <<
eom;
2073 return std::move(get_must_expr);
2080 error() <<
"get_may expects two operands" <<
eom;
2090 return std::move(get_may_expr);
2097 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2106 return same_object_expr;
2113 error() <<
"buffer_size expects one operand" <<
eom;
2123 return buffer_size_expr;
2130 error() <<
"is_zero_string expects one operand" <<
eom;
2138 is_zero_string_expr.
set(ID_C_lvalue,
true);
2141 return std::move(is_zero_string_expr);
2148 error() <<
"zero_string_length expects one operand" <<
eom;
2154 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2156 zero_string_length_expr.
set(ID_C_lvalue,
true);
2159 return zero_string_length_expr;
2166 error() <<
"dynamic_object expects one argument" <<
eom;
2175 return is_dynamic_object_expr;
2182 error() <<
"pointer_offset expects one argument" <<
eom;
2198 error() <<
"object_size expects one operand" <<
eom;
2208 return std::move(object_size_expr);
2215 error() <<
"pointer_object expects one argument" <<
eom;
2226 else if(identifier==
"__builtin_bswap16" ||
2227 identifier==
"__builtin_bswap32" ||
2228 identifier==
"__builtin_bswap64")
2233 error() << identifier <<
" expects one operand" <<
eom;
2243 return std::move(bswap_expr);
2245 else if(identifier==
"__builtin_nontemporal_load")
2250 error() << identifier <<
" expects one operand" <<
eom;
2259 if(ptr_arg.
type().
id()!=ID_pointer)
2262 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2271 identifier ==
"__builtin_fpclassify" ||
2277 error() << identifier <<
" expects six arguments" <<
eom;
2290 if(fp_value.
type().
id() != ID_floatbv)
2293 error() <<
"non-floating-point argument for " << identifier <<
eom;
2301 const auto &arguments = expr.
arguments();
2320 identifier==
"__builtin_isnan")
2325 error() <<
"isnan expects one operand" <<
eom;
2343 error() <<
"isfinite expects one operand" <<
eom;
2355 identifier==
"__builtin_inf")
2362 return std::move(inf_expr);
2371 return std::move(inff_expr);
2380 return std::move(infl_expr);
2392 error() <<
"abs-functions expect one operand" <<
eom;
2401 return std::move(abs_expr);
2408 error() <<
"allocate expects two operands" <<
eom;
2417 return std::move(malloc_expr);
2425 error() << identifier <<
" expects two operands" <<
eom;
2437 return std::move(ok_expr);
2442 identifier==
"__builtin_isinf")
2447 error() << identifier <<
" expects one operand" <<
eom;
2458 else if(identifier ==
"__builtin_isinf_sign")
2463 error() << identifier <<
" expects one operand" <<
eom;
2487 identifier ==
"__builtin_isnormal")
2492 error() << identifier <<
" expects one operand" <<
eom;
2500 if(fp_value.
type().
id() != ID_floatbv)
2503 error() <<
"non-floating-point argument for " << identifier <<
eom;
2515 identifier==
"__builtin_signbit" ||
2516 identifier==
"__builtin_signbitf" ||
2517 identifier==
"__builtin_signbitl")
2522 error() << identifier <<
" expects one operand" <<
eom;
2533 else if(identifier==
"__builtin_popcount" ||
2534 identifier==
"__builtin_popcountl" ||
2535 identifier==
"__builtin_popcountll" ||
2536 identifier==
"__popcnt16" ||
2537 identifier==
"__popcnt" ||
2538 identifier==
"__popcnt64")
2543 error() << identifier <<
" expects one operand" <<
eom;
2552 return std::move(popcount_expr);
2559 error() <<
"equal expects two operands" <<
eom;
2572 error() <<
"equal expects two operands of same type" <<
eom;
2576 return std::move(equality_expr);
2578 else if(identifier==
"__builtin_expect")
2589 error() <<
"__builtin_expect expects two arguments" <<
eom;
2597 else if(identifier==
"__builtin_object_size")
2606 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2623 error() <<
"__builtin_object_size expects constant as second argument, "
2631 if(arg1==0 || arg1==1)
2644 else if(identifier==
"__builtin_choose_expr")
2650 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2665 else if(identifier==
"__builtin_constant_p")
2672 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2688 tmp1.
id() == ID_typecast &&
2694 .
id() == ID_string_constant)
2706 else if(identifier==
"__builtin_classify_type")
2713 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2726 if(type.
id() == ID_c_bit_field)
2729 unsigned type_number;
2731 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2742 type.
id() == ID_empty
2744 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
2746 : (type.
id() == ID_pointer || type.
id() == ID_array)
2748 : type.
id() == ID_floatbv
2750 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
2752 : type.
id() == ID_struct
2754 : type.
id() == ID_union
2776 overflow.
id(ID_minus);
2781 overflow.id(ID_mult);
2786 overflow.id(ID_plus);
2791 overflow.id(ID_shl);
2796 overflow.id(ID_unary_minus);
2800 overflow.id(
"overflow-" + overflow.id_string());
2821 if(code_type.
get_bool(ID_C_incomplete))
2825 else if(code_type.
is_KnR())
2830 while(parameter_types.size()>arguments.size())
2835 if(parameter_types.size()>arguments.size())
2838 error() <<
"not enough function arguments" <<
eom;
2842 else if(parameter_types.size()!=arguments.size())
2845 error() <<
"wrong number of function arguments: "
2846 <<
"expected " << parameter_types.size()
2847 <<
", but got " << arguments.size() <<
eom;
2851 for(std::size_t i=0; i<arguments.size(); i++)
2853 exprt &op=arguments[i];
2859 else if(i<parameter_types.size())
2864 const typet &op_type=parameter_type.
type();
2866 if(op_type.
id()==ID_bool &&
2867 op.
id()==ID_side_effect &&
2868 op.
get(ID_statement)==ID_assign &&
2872 warning() <<
"assignment where Boolean argument is expected" <<
eom;
2881 if(op.
type().
id() == ID_array)
2884 dest_type.
subtype().
set(ID_C_constant,
true);
2902 if(o_type.
id()==ID_vector)
2921 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
2945 const auto s0 = numeric_cast<mp_integer>(type0.
size());
2946 const auto s1 = numeric_cast<mp_integer>(type1.
size());
2955 if((type0.
subtype().
id()==ID_signedbv ||
2975 if(o_type0.
id()==ID_vector &&
2976 o_type1.
id()==ID_vector)
2990 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
2995 expr.
type() = o_type0;
2999 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3004 expr.
type() = o_type1;
3015 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3016 expr.
id()==ID_mult || expr.
id()==ID_div)
3018 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3023 else if(type0==type1)
3032 else if(expr.
id()==ID_mod)
3036 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3044 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3045 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3054 else if(type0.
id()==ID_bool)
3056 if(expr.
id()==ID_bitand)
3058 else if(expr.
id() == ID_bitnand)
3060 else if(expr.
id()==ID_bitor)
3062 else if(expr.
id()==ID_bitxor)
3073 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3081 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3089 if(o_type0.
id()==ID_vector &&
3090 o_type1.
id()==ID_vector)
3120 if(expr.
id()==ID_shr)
3124 if(op0_type.
id()==ID_unsignedbv)
3129 else if(op0_type.
id()==ID_signedbv)
3140 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3149 assert(type.
id()==ID_pointer);
3154 subtype.
id() == ID_struct_tag &&
3158 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3162 subtype.
id() == ID_union_tag &&
3166 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3180 if(expr.
id()==ID_minus ||
3181 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3183 if(type0.
id()==ID_pointer &&
3184 type1.
id()==ID_pointer)
3194 if(type0.
id()==ID_pointer &&
3195 (type1.
id()==ID_bool ||
3196 type1.
id()==ID_c_bool ||
3197 type1.
id()==ID_unsignedbv ||
3198 type1.
id()==ID_signedbv ||
3199 type1.
id()==ID_c_bit_field ||
3200 type1.
id()==ID_c_enum_tag))
3208 else if(expr.
id()==ID_plus ||
3209 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3211 exprt *p_op, *int_op;
3213 if(type0.
id()==ID_pointer)
3218 else if(type1.
id()==ID_pointer)
3225 p_op=int_op=
nullptr;
3229 const typet &int_op_type = int_op->
type();
3231 if(int_op_type.
id()==ID_bool ||
3232 int_op_type.
id()==ID_c_bool ||
3233 int_op_type.
id()==ID_unsignedbv ||
3234 int_op_type.
id()==ID_signedbv ||
3235 int_op_type.
id()==ID_c_bit_field ||
3236 int_op_type.
id()==ID_c_enum_tag)
3247 if(expr.
id()==ID_side_effect)
3253 error() <<
"operator '" << op_name <<
"' not defined for types '"
3284 if(type0.
id()==ID_empty)
3287 error() <<
"cannot assign void" <<
eom;
3294 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3307 if(type0.
id() == ID_array)
3310 error() <<
"direct assignments to arrays not permitted" <<
eom;
3317 if(op0.
type().
id()==ID_c_bit_field)
3323 expr.
type()=o_type0;
3325 if(statement==ID_assign)
3330 else if(statement==ID_assign_shl ||
3331 statement==ID_assign_shr)
3338 if(statement==ID_assign_shl)
3348 if(underlying_type.
id()==ID_unsignedbv ||
3349 underlying_type.
id()==ID_c_bool)
3351 expr.
set(ID_statement, ID_assign_lshr);
3354 else if(underlying_type.
id()==ID_signedbv)
3356 expr.
set(ID_statement, ID_assign_ashr);
3362 else if(statement==ID_assign_bitxor ||
3363 statement==ID_assign_bitand ||
3364 statement==ID_assign_bitor)
3367 if(o_type0.
id()==ID_bool ||
3368 o_type0.
id()==ID_c_bool)
3371 if(op1.
type().
id()==ID_bool ||
3372 op1.
type().
id()==ID_c_bool ||
3373 op1.
type().
id()==ID_c_enum_tag ||
3374 op1.
type().
id()==ID_unsignedbv ||
3375 op1.
type().
id()==ID_signedbv)
3378 else if(o_type0.
id()==ID_c_enum_tag ||
3379 o_type0.
id()==ID_unsignedbv ||
3380 o_type0.
id()==ID_signedbv ||
3381 o_type0.
id()==ID_c_bit_field)
3386 else if(o_type0.
id()==ID_vector &&
3387 o_type1.
id()==ID_vector)
3400 if(o_type0.
id()==ID_pointer &&
3401 (statement==ID_assign_minus || statement==ID_assign_plus))
3406 else if(o_type0.
id()==ID_vector &&
3407 o_type1.
id()==ID_vector)
3417 else if(o_type0.
id()==ID_bool ||
3418 o_type0.
id()==ID_c_bool)
3421 if(op1.
type().
id()==ID_bool ||
3422 op1.
type().
id()==ID_c_bool ||
3423 op1.
type().
id()==ID_c_enum_tag ||
3424 op1.
type().
id()==ID_unsignedbv ||
3425 op1.
type().
id()==ID_signedbv)
3433 op1.
type().
id()==ID_bool ||
3434 op1.
type().
id()==ID_c_bool ||
3435 op1.
type().
id()==ID_c_enum_tag)
3441 error() <<
"assignment '" << statement <<
"' not defined for types '"
3453 const auto rounding_mode =
3460 expr.
id()!=ID_infinity)
3463 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3476 expr.
id()!=ID_infinity)
3479 error() <<
"conversion to integer constant failed" <<
eom;
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
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.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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
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
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_declaration(ansi_c_declarationt &)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
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.
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)
Base class for all expressions.
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
Generic base class for unary expressions.
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
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)
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
Expression to hold a symbol (variable)
bitvector_typet index_type()
#define Forall_irep(it, irep)
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 shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
virtual void typecheck_expr_member(exprt &expr)
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
static ieee_float_spect double_precision()
signedbv_typet signed_int_type()
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
preprocessort preprocessor
source_locationt source_location
A base class for expressions that are predicates, i.e., Boolean-typed.
virtual void typecheck_expr_function_identifier(exprt &expr)
#define forall_operands(it, expr)
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
virtual void typecheck_expr_dereference(exprt &expr)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#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)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool simplify(exprt &expr, const namespacet &ns)
Binary multiplication Associativity is not specified.
exprt simplify_expr(exprt src, const namespacet &ns)
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()
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
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)
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)
std::vector< exprt > operandst
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() const
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)
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
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Deprecated expression utility functions.
A base class for shift operators.
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
#define forall_irep(it, irep)
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)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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
codet & find_last_statement()
Symbol table entry of function parameter.
Operator to return the address of an object.
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.
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)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
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.