Go to the documentation of this file.
38 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);
99 if(type1.
id()==ID_c_enum_tag)
101 else if(type2.
id()==ID_c_enum_tag)
104 if(type1.
id()==ID_c_enum)
106 if(type2.
id()==ID_c_enum)
108 else if(type2==type1.
subtype())
111 else if(type2.
id()==ID_c_enum)
116 else if(type1.
id()==ID_pointer &&
117 type2.
id()==ID_pointer)
121 else if(type1.
id()==ID_array &&
122 type2.
id()==ID_array)
127 else if(type1.
id()==ID_code &&
141 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
157 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
167 if(expr.
id()==ID_side_effect)
169 else if(expr.
id()==ID_constant)
171 else if(expr.
id()==ID_infinity)
175 else if(expr.
id()==ID_symbol)
177 else if(expr.
id()==ID_unary_plus ||
178 expr.
id()==ID_unary_minus ||
179 expr.
id()==ID_bitnot)
181 else if(expr.
id()==ID_not)
184 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
187 else if(expr.
id()==ID_address_of)
189 else if(expr.
id()==ID_dereference)
191 else if(expr.
id()==ID_member)
193 else if(expr.
id()==ID_ptrmember)
195 else if(expr.
id()==ID_equal ||
196 expr.
id()==ID_notequal ||
202 else if(expr.
id()==ID_index)
204 else if(expr.
id()==ID_typecast)
206 else if(expr.
id()==ID_sizeof)
208 else if(expr.
id()==ID_alignof)
210 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
211 expr.
id()==ID_mult || expr.
id()==ID_div ||
213 expr.
id()==ID_bitand || expr.
id()==ID_bitxor || expr.
id()==ID_bitor)
215 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
217 else if(expr.
id()==ID_comma)
219 else if(expr.
id()==ID_if)
221 else if(expr.
id()==ID_code)
224 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
227 else if(expr.
id()==ID_gcc_builtin_va_arg)
229 else if(expr.
id()==ID_cw_va_arg_typeof)
231 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
236 assert(subtypes.size()==2);
242 subtypes[0].
remove(ID_C_constant);
243 subtypes[0].remove(ID_C_volatile);
244 subtypes[0].remove(ID_C_restricted);
245 subtypes[1].remove(ID_C_constant);
246 subtypes[1].remove(ID_C_volatile);
247 subtypes[1].remove(ID_C_restricted);
252 else if(expr.
id()==ID_clang_builtin_convertvector)
261 else if(expr.
id()==ID_builtin_offsetof)
263 else if(expr.
id()==ID_string_constant)
266 expr.
set(ID_C_lvalue,
true);
268 else if(expr.
id()==ID_arguments)
272 else if(expr.
id()==ID_designated_initializer)
274 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
278 if(it->id()==ID_index)
280 assert(it->operands().size()==1);
285 else if(expr.
id()==ID_initializer_list)
290 else if(expr.
id()==ID_forall ||
291 expr.
id()==ID_exists)
298 if(expr.
op0().
get(ID_statement)!=ID_decl)
301 error() <<
"expected declaration as operand of quantifier" <<
eom;
308 error() <<
"quantifier must not contain side effects" <<
eom;
318 else if(expr.
id()==ID_label)
322 else if(expr.
id()==ID_array)
326 else if(expr.
id()==ID_complex)
331 else if(expr.
id() == ID_complex_real)
335 "real part retrieval operation should have one operand");
340 if(op.
type().
id() != ID_complex)
345 error() <<
"real part retrieval expects numerical operand, "
353 expr.
swap(complex_real_expr);
361 complex_real_expr.
set(ID_C_lvalue,
true);
364 complex_real_expr.
type().
set(ID_C_constant,
true);
366 expr.
swap(complex_real_expr);
369 else if(expr.
id() == ID_complex_imag)
373 "imaginary part retrieval operation should have one operand");
378 if(op.
type().
id() != ID_complex)
383 error() <<
"real part retrieval expects numerical operand, "
391 expr.
swap(complex_imag_expr);
399 complex_imag_expr.
set(ID_C_lvalue,
true);
402 complex_imag_expr.
type().
set(ID_C_constant,
true);
404 expr.
swap(complex_imag_expr);
407 else if(expr.
id()==ID_generic_selection)
416 error() <<
"_Generic expects one operand" <<
eom;
431 if(it->get(ID_type_arg)!=ID_default)
433 typet &type=
static_cast<typet &
>(it->add(ID_type_arg));
445 if(it->get(ID_type_arg)==ID_default)
446 default_match=
static_cast<const exprt &
>(it->find(ID_value));
448 follow(
static_cast<const typet &
>(it->find(ID_type_arg))))
449 assoc_match=
static_cast<const exprt &
>(it->find(ID_value));
455 expr.
swap(default_match);
459 error() <<
"unmatched generic selection: "
465 expr.
swap(assoc_match);
470 else if(expr.
id()==ID_gcc_asm_input ||
471 expr.
id()==ID_gcc_asm_output ||
472 expr.
id()==ID_gcc_asm_clobbered_register)
475 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
476 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
493 error() <<
"comma operator expects two operands" <<
eom;
501 expr.
set(ID_C_lvalue,
true);
539 symbol.
name=ID_gcc_builtin_va_arg;
540 symbol.
type=symbol_type;
569 error() <<
"builtin_offsetof expects no operands" <<
eom;
584 if(m_it->id()==ID_member)
586 if(type.
id()!=ID_union && type.
id()!=ID_struct)
589 error() <<
"offsetof of member expects struct/union type, "
595 irep_idt component_name=m_it->get(ID_component_name);
599 assert(type.
id()==ID_union || type.
id()==ID_struct);
609 if(type.
id()==ID_struct)
618 error() <<
"offsetof failed to determine offset of `"
619 << component_name <<
"'" <<
eom;
636 for(
const auto &c : struct_union_type.
components())
639 c.get_anonymous() && (
follow(c.type()).
id() == ID_struct ||
644 if(type.
id()==ID_struct)
652 error() <<
"offsetof failed to determine offset of `"
653 << component_name <<
"'" <<
eom;
665 assert(type.
id()==ID_union || type.
id()==ID_struct);
675 error() <<
"offset-of of member failed to find component `"
676 << component_name <<
"' in `"
683 else if(m_it->id()==ID_index)
685 assert(m_it->operands().size()==1);
687 if(type.
id()!=ID_array)
690 error() <<
"offsetof of index expects array type" <<
eom;
719 if(expr.
id()==ID_side_effect &&
720 expr.
get(ID_statement)==ID_function_call)
727 else if(expr.
id()==ID_side_effect &&
728 expr.
get(ID_statement)==ID_statement_expression)
732 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
744 error() <<
"expected one declarator exactly" <<
eom;
752 symbol_tablet::symbolst::const_iterator s_it=
758 error() <<
"failed to find decl symbol `" << identifier
759 <<
"' in symbol table" <<
eom;
763 const symbolt &symbol=s_it->second;
769 error() <<
"unexpected quantified symbol" <<
eom;
792 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
796 expr.
type()=p_it->second;
797 expr.
set(ID_C_lvalue,
true);
802 asm_label_mapt::const_iterator entry=
806 identifier=entry->second;
812 if(
lookup(identifier, symbol_ptr))
815 error() <<
"failed to find symbol `"
816 << identifier <<
"'" <<
eom;
820 const symbolt &symbol=*symbol_ptr;
825 error() <<
"did not expect a type symbol here, but got `"
843 if(expr.
id()==ID_constant &&
845 expr.
set(ID_C_cformat, base_name);
860 else if(identifier==
"__func__" ||
861 identifier==
"__FUNCTION__" ||
862 identifier==
"__PRETTY_FUNCTION__")
868 s.
set(ID_C_lvalue,
true);
879 expr.
set(ID_C_lvalue,
true);
881 if(expr.
type().
id()==ID_code)
884 tmp.
set(ID_C_implicit,
true);
897 error() <<
"statement expression expects one operand" <<
eom;
910 if(last_statement==ID_expression)
916 if(op.
type().
id()==ID_array)
921 else if(last_statement==ID_function_call)
942 last.
swap(code_expr);
953 last.
swap(code_expr);
976 error() <<
"sizeof operator expects zero or one operand, "
983 if(type.
id()==ID_c_bit_field)
986 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
989 else if(type.
id() == ID_bool)
992 error() <<
"sizeof cannot be applied to single bits" <<
eom;
995 else if(type.
id() == ID_empty)
1013 new_expr.
swap(expr);
1015 expr.
add(ID_C_c_sizeof_type)=type;
1023 decl_block.set_statement(ID_decl_block);
1033 exprt comma_expr(ID_comma, expr.
type());
1035 expr.
swap(comma_expr);
1041 typet argument_type;
1044 argument_type=expr.
op0().
type();
1049 argument_type=op_type;
1066 error() <<
"typecast operator expects one operand" <<
eom;
1080 decl_block.set_statement(ID_decl_block);
1092 op.
swap(comma_expr);
1097 if(expr_type.
id()==ID_union &&
1099 op.
id()!=ID_initializer_list)
1121 expr.
set(ID_C_lvalue,
true);
1128 error() <<
"type cast to union: type `"
1136 if(op.
id()==ID_initializer_list)
1145 exprt tmp(ID_compound_literal, expr.
type());
1149 if(op.
id()==ID_array &&
1150 expr.
type().
id()==ID_array &&
1155 expr.
set(ID_C_lvalue,
true);
1160 if(expr_type.
id()==ID_empty)
1171 if(expr_type.
id()==ID_vector)
1174 if(op_type.
id()==ID_vector)
1176 else if(op_type.
id()==ID_signedbv ||
1177 op_type.
id()==ID_unsignedbv)
1184 error() <<
"type cast to `"
1185 <<
to_string(expr_type) <<
"' is not permitted" <<
eom;
1192 else if(op_type.
id()==ID_array)
1200 else if(op_type.
id()==ID_empty)
1202 if(expr_type.
id()!=ID_empty)
1205 error() <<
"type cast from void only permitted to void, but got `"
1210 else if(op_type.
id()==ID_vector)
1217 if((expr_type.
id()==ID_signedbv ||
1218 expr_type.
id()==ID_unsignedbv) &&
1226 error() <<
"type cast from vector to `"
1234 error() <<
"type cast from `"
1250 if(expr_type.
id()==ID_pointer)
1251 expr.
set(ID_C_lvalue,
true);
1265 error() <<
"operator `" << expr.
id()
1266 <<
"' expects two operands" <<
eom;
1279 if(array_full_type.
id()!=ID_array &&
1280 array_full_type.
id()!=ID_pointer &&
1281 array_full_type.
id()!=ID_vector &&
1282 (index_full_type.
id()==ID_array ||
1283 index_full_type.
id()==ID_pointer ||
1284 index_full_type.
id()==ID_vector))
1285 std::swap(array_expr, index_expr);
1295 if(final_array_type.
id()==ID_array ||
1296 final_array_type.
id()==ID_vector)
1300 if(array_expr.
get_bool(ID_C_lvalue))
1301 expr.
set(ID_C_lvalue,
true);
1303 if(final_array_type.
get_bool(ID_C_constant))
1304 expr.
type().
set(ID_C_constant,
true);
1306 else if(final_array_type.
id()==ID_pointer)
1311 exprt addition(ID_plus, array_expr.
type());
1314 expr.
id(ID_dereference);
1315 expr.
set(ID_C_lvalue,
true);
1321 error() <<
"operator [] must take array/vector or pointer but got `"
1334 if(expr.
id()==ID_equal)
1335 expr.
id(ID_ieee_float_equal);
1336 else if(expr.
id()==ID_notequal)
1337 expr.
id(ID_ieee_float_notequal);
1350 if(
follow(o_type0).
id()==ID_vector ||
1351 follow(o_type1).
id()==ID_vector)
1359 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1364 if(final_type.
id()!=ID_array &&
1365 final_type.
id()!=ID_incomplete_struct)
1386 if(type0.
id()==ID_pointer)
1388 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1391 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1392 expr.
id()==ID_ge || expr.
id()==ID_gt)
1396 if(type0.
id()==ID_string_constant)
1398 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1405 if(type0.
id()==ID_pointer &&
1412 if(type1.
id()==ID_pointer &&
1432 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1440 error() <<
"operator `" << expr.
id()
1441 <<
"' not defined for types `"
1456 if(o_type0.
id()!=ID_vector ||
1457 o_type1.
id()!=ID_vector ||
1461 error() <<
"vector operator `" << expr.
id()
1462 <<
"' not defined for types `"
1478 error() <<
"ptrmember operator expects one operand" <<
eom;
1484 if(final_op0_type.
id()==ID_array)
1489 index_expr.
set(ID_C_lvalue,
true);
1492 else if(final_op0_type.
id()==ID_pointer)
1503 error() <<
"ptrmember operator requires pointer or array type "
1504 "on left hand side, but got `"
1518 error() <<
"member operator expects one operand" <<
eom;
1527 if(type.
id()==ID_incomplete_struct)
1530 error() <<
"member operator got incomplete struct type "
1531 "on left hand side" <<
eom;
1535 if(type.
id()==ID_incomplete_union)
1538 error() <<
"member operator got incomplete union type "
1539 "on left hand side" <<
eom;
1543 if(type.
id()!=ID_struct &&
1544 type.
id()!=ID_union)
1547 error() <<
"member operator requires structure type "
1548 "on left hand side but got `"
1557 expr.
get(ID_component_name);
1573 error() <<
"member `" << component_name
1574 <<
"' not found in `"
1587 expr.
set(ID_C_lvalue,
true);
1590 expr.
type().
set(ID_C_constant,
true);
1595 if(!identifier.
empty())
1596 expr.
set(ID_C_identifier, identifier);
1600 if(access==ID_private)
1603 error() <<
"member `" << component_name
1604 <<
"' is " << access <<
eom;
1613 assert(operands.size()==3);
1616 const typet o_type0=operands[0].type();
1617 const typet o_type1=operands[1].type();
1618 const typet o_type2=operands[2].type();
1623 if(operands[1].type().
id()==ID_pointer &&
1624 operands[2].type().
id()!=ID_pointer)
1626 else if(operands[2].type().
id()==ID_pointer &&
1627 operands[1].type().
id()!=ID_pointer)
1630 if(operands[1].type().
id()==ID_pointer &&
1631 operands[2].type().
id()==ID_pointer &&
1632 operands[1].type()!=operands[2].type())
1639 if(operands[1].type().subtype().
id()==ID_empty &&
1643 else if(operands[2].type().subtype().
id()==ID_empty &&
1647 else if(operands[1].type().subtype().
id()!=ID_code ||
1648 operands[2].type().subtype().
id()!=ID_code)
1672 if(operands[1].type().
id()==ID_empty ||
1673 operands[2].type().
id()==ID_empty)
1679 if(
follow(operands[1].type())==
follow(operands[2].type()))
1681 expr.
type()=operands[1].type();
1687 if(operands[1].get_bool(ID_C_lvalue) &&
1688 operands[2].get_bool(ID_C_lvalue))
1689 expr.
set(ID_C_lvalue,
true);
1695 error() <<
"operator ?: not defined for types `"
1709 if(operands.size()!=2)
1712 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1719 if_expr.
cond()=operands[0];
1727 expr.
op0()=if_expr.
op1();
1728 expr.
op1()=if_expr.
op2();
1737 error() <<
"unary operator & expects one operand" <<
eom;
1743 if(op.
type().
id()==ID_c_bit_field)
1746 error() <<
"cannot take address of a bit field" <<
eom;
1750 if(op.
type().
id() == ID_bool)
1753 error() <<
"cannot take address of a single bit" <<
eom;
1758 if(op.
id()==ID_label)
1770 if(op.
id()==ID_address_of &&
1778 tmp.
set(ID_C_implicit,
false);
1783 if(op.
id()==ID_struct ||
1784 op.
id()==ID_union ||
1785 op.
id()==ID_array ||
1786 op.
id()==ID_string_constant)
1794 else if(op.
type().
id()==ID_code)
1802 <<
"' not an lvalue" <<
eom;
1814 error() <<
"unary operator * expects one operand" <<
eom;
1822 if(op_type.
id()==ID_array)
1830 else if(op_type.
id()==ID_pointer)
1838 <<
"' is not a pointer, but got `"
1843 expr.
set(ID_C_lvalue,
true);
1854 if(expr.
type().
id()==ID_code)
1857 tmp.
set(ID_C_implicit,
true);
1867 if(statement==ID_preincrement ||
1868 statement==ID_predecrement ||
1869 statement==ID_postincrement ||
1870 statement==ID_postdecrement)
1875 error() << statement <<
"operator expects one operand" <<
eom;
1886 <<
"' not an lvalue" <<
eom;
1894 <<
"' is constant" <<
eom;
1898 if(final_type0.
id()==ID_c_enum_tag)
1901 ID_incomplete_c_enum)
1904 error() <<
"operator `" << statement
1905 <<
"' given incomplete type `"
1912 else if(final_type0.
id()==ID_c_bit_field)
1917 expr.
type()=underlying_type;
1923 else if(final_type0.
id()==ID_pointer)
1931 error() <<
"operator `" << statement
1932 <<
"' not defined for type `"
1939 else if(statement==ID_function_call)
1942 else if(statement==ID_statement_expression)
1944 else if(statement==ID_gcc_conditional_expression)
1949 error() <<
"unknown side effect: " << statement <<
eom;
1960 error() <<
"function_call side effect expects two operands" <<
eom;
1969 if(f_op.
id()==ID_symbol)
1973 asm_label_mapt::const_iterator entry=
1976 identifier=entry->second;
1996 if(identifier==
"malloc" ||
1997 identifier==
"realloc" ||
1998 identifier==
"reallocf" ||
1999 identifier==
"valloc")
2006 new_symbol.
name=identifier;
2010 new_symbol.
type.
set(ID_C_incomplete,
true);
2018 warning() <<
"function `" << identifier <<
"' is not declared" <<
eom;
2028 if(f_op_type.
id()!=ID_pointer)
2031 error() <<
"expected function/function pointer as argument but got `"
2037 if(f_op.
id()==ID_address_of &&
2048 tmp.
set(ID_C_implicit,
true);
2053 if(f_op.
type().
id()!=ID_code)
2056 error() <<
"expected code as argument" <<
eom;
2079 if(f_op.
id()!=ID_symbol)
2089 error() <<
"same_object expects two operands" <<
eom;
2093 exprt same_object_expr=
2097 return same_object_expr;
2104 error() <<
"get_must expects two operands" <<
eom;
2114 return std::move(get_must_expr);
2121 error() <<
"get_may expects two operands" <<
eom;
2131 return std::move(get_may_expr);
2138 error() <<
"invalid_pointer expects one operand" <<
eom;
2145 return same_object_expr;
2152 error() <<
"buffer_size expects one operand" <<
eom;
2160 return buffer_size_expr;
2167 error() <<
"is_zero_string expects one operand" <<
eom;
2173 is_zero_string_expr.
set(ID_C_lvalue,
true);
2176 return std::move(is_zero_string_expr);
2183 error() <<
"zero_string_length expects one operand" <<
eom;
2187 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2189 zero_string_length_expr.
set(ID_C_lvalue,
true);
2192 return zero_string_length_expr;
2199 error() <<
"dynamic_object expects one argument" <<
eom;
2207 return dynamic_object_expr;
2214 error() <<
"pointer_offset expects one argument" <<
eom;
2228 error() <<
"object_size expects one operand" <<
eom;
2236 return std::move(object_size_expr);
2243 error() <<
"pointer_object expects one argument" <<
eom;
2252 else if(identifier==
"__builtin_bswap16" ||
2253 identifier==
"__builtin_bswap32" ||
2254 identifier==
"__builtin_bswap64")
2261 error() << identifier <<
" expects one operand" <<
eom;
2269 return std::move(bswap_expr);
2271 else if(identifier==
"__builtin_nontemporal_load")
2278 error() << identifier <<
" expects one operand" <<
eom;
2285 if(ptr_arg.
type().
id()!=ID_pointer)
2288 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2297 identifier ==
"__builtin_fpclassify" ||
2303 error() << identifier <<
" expects six arguments" <<
eom;
2314 if(fp_value.
type().
id() != ID_floatbv)
2317 error() <<
"non-floating-point argument for " << identifier <<
eom;
2325 const auto &arguments = expr.
arguments();
2344 identifier==
"__builtin_isnan")
2349 error() <<
"isnan expects one operand" <<
eom;
2365 error() <<
"isfinite expects one operand" <<
eom;
2375 identifier==
"__builtin_inf")
2382 return std::move(inf_expr);
2391 return std::move(inff_expr);
2400 return std::move(infl_expr);
2412 error() <<
"abs-functions expect one operand" <<
eom;
2419 return std::move(abs_expr);
2426 error() <<
"allocate expects two operands" <<
eom;
2433 return std::move(malloc_expr);
2441 error() << identifier <<
" expects two operands" <<
eom;
2450 return std::move(ok_expr);
2455 identifier==
"__builtin_isinf")
2460 error() << identifier <<
" expects one operand" <<
eom;
2469 else if(identifier ==
"__builtin_isinf_sign")
2474 error() << identifier <<
" expects one operand" <<
eom;
2496 identifier ==
"__builtin_isnormal")
2501 error() << identifier <<
" expects one operand" <<
eom;
2507 if(fp_value.
type().
id() != ID_floatbv)
2510 error() <<
"non-floating-point argument for " << identifier <<
eom;
2522 identifier==
"__builtin_signbit" ||
2523 identifier==
"__builtin_signbitf" ||
2524 identifier==
"__builtin_signbitl")
2529 error() << identifier <<
" expects one operand" <<
eom;
2538 else if(identifier==
"__builtin_popcount" ||
2539 identifier==
"__builtin_popcountl" ||
2540 identifier==
"__builtin_popcountll" ||
2541 identifier==
"__popcnt16" ||
2542 identifier==
"__popcnt" ||
2543 identifier==
"__popcnt64")
2548 error() << identifier <<
" expects one operand" <<
eom;
2555 return std::move(popcount_expr);
2562 error() <<
"equal expects two operands" <<
eom;
2571 equality_expr.
rhs().
type(), *
this))
2574 error() <<
"equal expects two operands of same type" <<
eom;
2578 return std::move(equality_expr);
2580 else if(identifier==
"__builtin_expect")
2591 error() <<
"__builtin_expect expects two arguments" <<
eom;
2597 else if(identifier==
"__builtin_object_size")
2606 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2621 error() <<
"__builtin_object_size expects constant as second argument, "
2629 if(arg1==0 || arg1==1)
2642 else if(identifier==
"__builtin_choose_expr")
2648 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2660 else if(identifier==
"__builtin_constant_p")
2667 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2675 bool is_constant=
false;
2679 if(tmp1.
id()==ID_typecast &&
2681 tmp1.
op0().
id()==ID_address_of &&
2697 else if(identifier==
"__builtin_classify_type")
2704 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2715 if(type.
id() == ID_c_bit_field)
2718 unsigned type_number;
2720 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2731 type.
id() == ID_empty
2733 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
2735 : (type.
id() == ID_pointer || type.
id() == ID_array)
2737 : type.
id() == ID_floatbv
2739 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
2741 : type.
id() == ID_struct
2743 : type.
id() == ID_union
2753 else if(identifier==
"__sync_fetch_and_add" ||
2754 identifier==
"__sync_fetch_and_sub" ||
2755 identifier==
"__sync_fetch_and_or" ||
2756 identifier==
"__sync_fetch_and_and" ||
2757 identifier==
"__sync_fetch_and_xor" ||
2758 identifier==
"__sync_fetch_and_nand" ||
2759 identifier==
"__sync_add_and_fetch" ||
2760 identifier==
"__sync_sub_and_fetch" ||
2761 identifier==
"__sync_or_and_fetch" ||
2762 identifier==
"__sync_and_and_fetch" ||
2763 identifier==
"__sync_xor_and_fetch" ||
2764 identifier==
"__sync_nand_and_fetch" ||
2765 identifier==
"__sync_val_compare_and_swap" ||
2766 identifier==
"__sync_lock_test_and_set" ||
2767 identifier==
"__sync_lock_release")
2776 error() <<
"__sync_* primitives take as least one argument" <<
eom;
2782 if(ptr_arg.
type().
id()!=ID_pointer)
2785 error() <<
"__sync_* primitives take pointer as first argument" <<
eom;
2810 if(code_type.
get_bool(ID_C_incomplete))
2814 else if(code_type.
is_KnR())
2819 while(parameter_types.size()>arguments.size())
2824 if(parameter_types.size()>arguments.size())
2827 error() <<
"not enough function arguments" <<
eom;
2831 else if(parameter_types.size()!=arguments.size())
2834 error() <<
"wrong number of function arguments: "
2835 <<
"expected " << parameter_types.size()
2836 <<
", but got " << arguments.size() <<
eom;
2840 for(std::size_t i=0; i<arguments.size(); i++)
2842 exprt &op=arguments[i];
2848 else if(i<parameter_types.size())
2853 const typet &op_type=parameter_type.
type();
2855 if(op_type.
id()==ID_bool &&
2856 op.
id()==ID_side_effect &&
2857 op.
get(ID_statement)==ID_assign &&
2861 warning() <<
"assignment where Boolean argument is expected" <<
eom;
2871 if(type.
id()==ID_array)
2874 dest_type.
subtype().
set(ID_C_constant,
true);
2891 error() <<
"operator `" << expr.
id()
2892 <<
"' expects one operand" <<
eom;
2900 if(o_type.
id()==ID_vector)
2919 error() <<
"operator `" << expr.
id()
2920 <<
"' not defined for type `"
2930 error() <<
"operator `" << expr.
id()
2931 <<
"' expects one operand" <<
eom;
2963 if((type0.
subtype().
id()==ID_signedbv ||
2979 error() <<
"operator `" << expr.
id()
2980 <<
"' expects two operands" <<
eom;
2990 if(o_type0.
id()==ID_vector &&
2991 o_type1.
id()==ID_vector)
2998 if(o_type0!=o_type1)
3005 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3010 expr.
type() = o_type0;
3014 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3019 expr.
type() = o_type1;
3030 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3031 expr.
id()==ID_mult || expr.
id()==ID_div)
3033 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3038 else if(type0==type1)
3047 else if(expr.
id()==ID_mod)
3051 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3058 else if(expr.
id()==ID_bitand ||
3059 expr.
id()==ID_bitxor ||
3060 expr.
id()==ID_bitor)
3069 else if(type0.
id()==ID_bool)
3071 if(expr.
id()==ID_bitand)
3073 else if(expr.
id()==ID_bitor)
3075 else if(expr.
id()==ID_bitxor)
3086 error() <<
"operator `" << expr.
id()
3087 <<
"' not defined for types `"
3095 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3103 if(o_type0.
id()==ID_vector &&
3104 o_type1.
id()==ID_vector)
3117 if(o_type0.
id()==ID_vector &&
3135 if(expr.
id()==ID_shr)
3139 if(op0_type.
id()==ID_unsignedbv)
3144 else if(op0_type.
id()==ID_signedbv)
3155 error() <<
"operator `" << expr.
id()
3156 <<
"' not defined for types `"
3165 assert(type.
id()==ID_pointer);
3169 if(subtype.
id()==ID_incomplete_struct)
3172 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3187 if(expr.
id()==ID_minus ||
3188 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3190 if(type0.
id()==ID_pointer &&
3191 type1.
id()==ID_pointer)
3201 if(type0.
id()==ID_pointer &&
3202 (type1.
id()==ID_bool ||
3203 type1.
id()==ID_c_bool ||
3204 type1.
id()==ID_unsignedbv ||
3205 type1.
id()==ID_signedbv ||
3206 type1.
id()==ID_c_bit_field ||
3207 type1.
id()==ID_c_enum_tag))
3215 else if(expr.
id()==ID_plus ||
3216 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3218 exprt *p_op, *int_op;
3220 if(type0.
id()==ID_pointer)
3225 else if(type1.
id()==ID_pointer)
3232 p_op=int_op=
nullptr;
3238 if(int_op_type.
id()==ID_bool ||
3239 int_op_type.
id()==ID_c_bool ||
3240 int_op_type.
id()==ID_unsignedbv ||
3241 int_op_type.
id()==ID_signedbv ||
3242 int_op_type.
id()==ID_c_bit_field ||
3243 int_op_type.
id()==ID_c_enum_tag)
3254 if(expr.
id()==ID_side_effect)
3260 error() <<
"operator `" << op_name
3261 <<
"' not defined for types `"
3272 error() <<
"operator `" << expr.
id()
3273 <<
"' expects two operands" <<
eom;
3295 <<
"' expects two operands" <<
eom;
3307 if(type0.
id()==ID_empty)
3310 error() <<
"cannot assign void" <<
eom;
3318 <<
"' not an lvalue" <<
eom;
3326 <<
"' is constant" <<
eom;
3331 if(type0.
id()==ID_array ||
3332 type0.
id()==ID_incomplete_array)
3335 error() <<
"direct assignments to arrays not permitted" <<
eom;
3342 if(op0.
type().
id()==ID_c_bit_field)
3348 expr.
type()=o_type0;
3350 if(statement==ID_assign)
3355 else if(statement==ID_assign_shl ||
3356 statement==ID_assign_shr)
3362 if(statement==ID_assign_shl)
3372 if(underlying_type.
id()==ID_c_enum_tag)
3374 const typet &c_enum_type=
3376 underlying_type=c_enum_type.
subtype();
3379 if(underlying_type.
id()==ID_unsignedbv ||
3380 underlying_type.
id()==ID_c_bool)
3382 expr.
set(ID_statement, ID_assign_lshr);
3385 else if(underlying_type.
id()==ID_signedbv)
3387 expr.
set(ID_statement, ID_assign_ashr);
3393 else if(statement==ID_assign_bitxor ||
3394 statement==ID_assign_bitand ||
3395 statement==ID_assign_bitor)
3398 if(o_type0.
id()==ID_bool ||
3399 o_type0.
id()==ID_c_bool)
3402 if(op1.
type().
id()==ID_bool ||
3403 op1.
type().
id()==ID_c_bool ||
3404 op1.
type().
id()==ID_c_enum_tag ||
3405 op1.
type().
id()==ID_unsignedbv ||
3406 op1.
type().
id()==ID_signedbv)
3409 else if(o_type0.
id()==ID_c_enum_tag ||
3410 o_type0.
id()==ID_unsignedbv ||
3411 o_type0.
id()==ID_signedbv ||
3412 o_type0.
id()==ID_c_bit_field)
3417 else if(o_type0.
id()==ID_vector &&
3418 o_type1.
id()==ID_vector)
3424 if(o_type0!=o_type1)
3432 if(o_type0.
id()==ID_pointer &&
3433 (statement==ID_assign_minus || statement==ID_assign_plus))
3438 else if(o_type0.
id()==ID_vector &&
3439 o_type1.
id()==ID_vector)
3445 if(o_type0!=o_type1)
3450 else if(o_type0.
id()==ID_bool ||
3451 o_type0.
id()==ID_c_bool)
3454 if(op1.
type().
id()==ID_bool ||
3455 op1.
type().
id()==ID_c_bool ||
3456 op1.
type().
id()==ID_c_enum_tag ||
3457 op1.
type().
id()==ID_unsignedbv ||
3458 op1.
type().
id()==ID_signedbv)
3466 op1.
type().
id()==ID_bool ||
3467 op1.
type().
id()==ID_c_bool ||
3468 op1.
type().
id()==ID_c_enum_tag)
3474 error() <<
"assignment `" << statement
3475 <<
"' not defined for types `"
3487 const auto rounding_mode =
3494 expr.
id()!=ID_infinity)
3497 error() <<
"expected constant expression, but got `"
3510 expr.
id()!=ID_infinity)
3513 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.
const componentst & components() const
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
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
static exprt conditional_cast(const exprt &expr, const typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
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
const exprt & size() const
#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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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.
std::vector< parametert > parameterst
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
virtual void adjust_float_rel(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
virtual std::string to_string(const exprt &expr)
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)
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...
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
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.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Union constructor from single element.
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.
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)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
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)
exprt simplify_expr(const exprt &src, const namespacet &ns)
bitvector_typet index_type()
#define Forall_irep(it, irep)
virtual void typecheck_expr_binary_boolean(exprt &expr)
#define UNREACHABLE
This should be used to mark dead code.
An expression denoting infinity.
Evaluates to true if the operand is finite.
void set_component_name(const irep_idt &component_name)
std::list< codet > clean_code
virtual void make_constant(exprt &expr)
const codet & to_code(const exprt &expr)
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 lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
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)
mstreamt & result() const
static ieee_float_spect double_precision()
signedbv_typet signed_int_type()
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
exprt size_of_expr(const typet &type, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
preprocessort preprocessor
source_locationt source_location
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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)
virtual void typecheck_expr_dereference(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
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.
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
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)
const irep_idt & id() const
virtual void typecheck_expr_trinary(if_exprt &expr)
void remove(const irep_namet &name)
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() 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)
bitvector_typet char_type()
std::size_t get_width() const
Deprecated expression utility functions.
A base class for shift operators.
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)
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates.
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)
exprt invalid_pointer(const exprt &pointer)
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
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)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
constant_exprt to_expr() const
codet & find_last_statement()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
source_locationt & add_source_location()
The popcount (counting the number of bits set to 1) expression.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
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
virtual void typecheck_expr_sizeof(exprt &expr)
std::vector< irept > subt
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
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)
codet representation of an expression statement.
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.