37 if(expr.
id()==ID_already_typechecked)
58 if(expr.
id()==ID_div ||
63 if(expr.
type().
id()==ID_floatbv &&
72 expr.
id(ID_floatbv_div);
73 else if(expr.
id()==ID_mult)
74 expr.
id(ID_floatbv_mult);
75 else if(expr.
id()==ID_plus)
76 expr.
id(ID_floatbv_plus);
77 else if(expr.
id()==ID_minus)
78 expr.
id(ID_floatbv_minus);
94 if(type1.
id()==ID_symbol)
96 else if(type2.
id()==ID_symbol)
103 if(type1.
id()==ID_c_enum_tag)
105 else if(type2.
id()==ID_c_enum_tag)
108 if(type1.
id()==ID_c_enum)
110 if(type2.
id()==ID_c_enum)
112 else if(type2==type1.
subtype())
115 else if(type2.
id()==ID_c_enum)
120 else if(type1.
id()==ID_pointer &&
121 type2.
id()==ID_pointer)
125 else if(type1.
id()==ID_array &&
126 type2.
id()==ID_array)
131 else if(type1.
id()==ID_code &&
145 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
161 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
171 if(expr.
id()==ID_side_effect)
173 else if(expr.
id()==ID_constant)
175 else if(expr.
id()==ID_infinity)
179 else if(expr.
id()==ID_symbol)
181 else if(expr.
id()==ID_unary_plus ||
182 expr.
id()==ID_unary_minus ||
183 expr.
id()==ID_bitnot)
185 else if(expr.
id()==ID_not)
187 else if(expr.
id()==ID_and || expr.
id()==ID_or || expr.
id()==ID_implies)
189 else if(expr.
id()==ID_address_of)
191 else if(expr.
id()==ID_dereference)
193 else if(expr.
id()==ID_member)
195 else if(expr.
id()==ID_ptrmember)
197 else if(expr.
id()==ID_equal ||
198 expr.
id()==ID_notequal ||
204 else if(expr.
id()==ID_index)
206 else if(expr.
id()==ID_typecast)
208 else if(expr.
id()==ID_sizeof)
210 else if(expr.
id()==ID_alignof)
212 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
213 expr.
id()==ID_mult || expr.
id()==ID_div ||
215 expr.
id()==ID_bitand || expr.
id()==ID_bitxor || expr.
id()==ID_bitor)
217 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
219 else if(expr.
id()==ID_comma)
221 else if(expr.
id()==ID_if)
223 else if(expr.
id()==ID_code)
226 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
229 else if(expr.
id()==ID_gcc_builtin_va_arg)
231 else if(expr.
id()==ID_cw_va_arg_typeof)
233 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
237 assert(subtypes.size()==2);
243 subtypes[0].
remove(ID_C_constant);
244 subtypes[0].remove(ID_C_volatile);
245 subtypes[0].remove(ID_C_restricted);
246 subtypes[1].remove(ID_C_constant);
247 subtypes[1].remove(ID_C_volatile);
248 subtypes[1].remove(ID_C_restricted);
253 else if(expr.
id()==ID_clang_builtin_convertvector)
257 else if(expr.
id()==ID_builtin_offsetof)
259 else if(expr.
id()==ID_string_constant)
262 expr.
set(ID_C_lvalue,
true);
264 else if(expr.
id()==ID_arguments)
268 else if(expr.
id()==ID_designated_initializer)
270 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
274 if(it->id()==ID_index)
276 assert(it->operands().size()==1);
281 else if(expr.
id()==ID_initializer_list)
286 else if(expr.
id()==ID_forall ||
287 expr.
id()==ID_exists)
294 if(expr.
op0().
get(ID_statement)!=ID_decl)
297 error() <<
"expected declaration as operand of quantifier" <<
eom;
305 else if(expr.
id()==ID_label)
309 else if(expr.
id()==ID_array)
313 else if(expr.
id()==ID_complex)
318 else if(expr.
id()==ID_complex_real ||
319 expr.
id()==ID_complex_imag)
324 if(op_type.id()!=ID_complex)
329 error() <<
"real/imag expect numerical operand, " 344 expr.
set(ID_C_lvalue,
true);
347 expr.
set(ID_C_constant,
true);
350 else if(expr.
id()==ID_generic_selection)
359 error() <<
"_Generic expects one operand" <<
eom;
374 if(it->get(ID_type_arg)!=ID_default)
376 typet &type=
static_cast<typet &
>(it->add(ID_type_arg));
388 if(it->get(ID_type_arg)==ID_default)
389 default_match=static_cast<const exprt &>(it->find(ID_value));
391 follow(static_cast<const typet &>(it->find(ID_type_arg))))
392 assoc_match=static_cast<const exprt &>(it->find(ID_value));
398 expr.
swap(default_match);
402 error() <<
"unmatched generic selection: " 408 expr.
swap(assoc_match);
413 else if(expr.
id()==ID_gcc_asm_input ||
414 expr.
id()==ID_gcc_asm_output ||
415 expr.
id()==ID_gcc_asm_clobbered_register)
418 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
419 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
436 error() <<
"comma operator expects two operands" <<
eom;
444 expr.
set(ID_C_lvalue,
true);
469 result.function().type()=new_type;
470 result.arguments().push_back(arg);
471 result.type()=new_type.return_type();
484 symbol.
name=ID_gcc_builtin_va_arg;
485 symbol.
type=symbol_type;
514 error() <<
"builtin_offsetof expects no operands" <<
eom;
527 if(type.
id()==ID_symbol)
530 if(m_it->id()==ID_member)
532 if(type.
id()!=ID_union && type.
id()!=ID_struct)
535 error() <<
"offsetof of member expects struct/union type, " 541 irep_idt component_name=m_it->get(ID_component_name);
545 assert(type.
id()==ID_union || type.
id()==ID_struct);
551 if(struct_union_type.has_component(component_name))
555 if(type.
id()==ID_struct)
564 error() <<
"offsetof failed to determine offset of `" 565 << component_name <<
"'" <<
eom;
575 type=struct_union_type.get_component(component_name).type();
582 struct_union_type.components();
586 for(struct_union_typet::componentst::const_iterator
587 c_it=components.begin();
588 c_it!=components.end();
591 if(c_it->get_anonymous() &&
592 (
follow(c_it->type()).
id()==ID_struct ||
593 follow(c_it->type()).
id()==ID_union))
597 if(type.
id()==ID_struct)
606 error() <<
"offsetof failed to determine offset of `" 607 << component_name <<
"'" <<
eom;
619 assert(type.id()==ID_union || type.id()==ID_struct);
629 error() <<
"offset-of of member failed to find component `" 630 << component_name <<
"' in `" 637 else if(m_it->id()==ID_index)
639 assert(m_it->operands().size()==1);
641 if(type.
id()!=ID_array)
644 error() <<
"offsetof of index expects array type" <<
eom;
673 if(expr.
id()==ID_side_effect &&
674 expr.
get(ID_statement)==ID_function_call)
681 else if(expr.
id()==ID_side_effect &&
682 expr.
get(ID_statement)==ID_statement_expression)
686 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
695 if(declaration.declarators().size()!=1)
698 error() <<
"expected one declarator exactly" <<
eom;
703 declaration.declarators().front().get_name();
706 symbol_tablet::symbolst::const_iterator s_it=
712 error() <<
"failed to find decl symbol `" << identifier
713 <<
"' in symbol table" <<
eom;
717 const symbolt &symbol=s_it->second;
723 error() <<
"unexpected quantified symbol" <<
eom;
747 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
751 expr.
type()=p_it->second;
752 expr.
set(ID_C_lvalue,
true);
757 asm_label_mapt::const_iterator entry=
761 identifier=entry->second;
767 if(
lookup(identifier, symbol_ptr))
770 error() <<
"failed to find symbol `" 771 << identifier <<
"'" <<
eom;
775 const symbolt &symbol=*symbol_ptr;
780 error() <<
"did not expect a type symbol here, but got `" 798 if(expr.
id()==ID_constant &&
800 expr.
set(ID_C_cformat, base_name);
815 else if(identifier==
"__func__" ||
816 identifier==
"__FUNCTION__" ||
817 identifier==
"__PRETTY_FUNCTION__")
823 s.
set(ID_C_lvalue,
true);
834 expr.
set(ID_C_lvalue,
true);
836 if(expr.
type().
id()==ID_code)
839 tmp.
set(
"#implicit",
true);
852 error() <<
"statement expression expects one operand" <<
eom;
863 irep_idt last_statement=last.get_statement();
865 if(last_statement==ID_expression)
867 assert(last.operands().size()==1);
871 if(op.type().id()==ID_array)
874 expr.
type()=op.type();
876 else if(last_statement==ID_function_call)
900 last.
swap(code_expr);
906 assign.move_to_operands(fc.
lhs(), sideeffect);
911 last.
swap(code_expr);
924 type.
swap(static_cast<typet &>(expr.
add(ID_type_arg)));
934 error() <<
"sizeof operator expects zero or one operand, " 941 if(type.
id()==ID_c_bit_field)
944 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
947 else if(type.
id() == ID_empty)
967 expr.
add(ID_C_c_sizeof_type)=type;
986 expr.
swap(comma_expr);
995 argument_type=expr.
op0().
type();
1000 argument_type=op_type;
1017 error() <<
"typecast operator expects one operand" <<
eom;
1042 op.
swap(comma_expr);
1047 if(expr_type.
id()==ID_union &&
1049 op.
id()!=ID_initializer_list)
1064 for(union_typet::componentst::const_iterator
1065 it=components.begin();
1066 it!=components.end();
1075 union_expr.set_component_name(it->get_name());
1077 expr.
set(ID_C_lvalue,
true);
1084 error() <<
"type cast to union: type `" 1092 if(op.
id()==ID_initializer_list)
1101 exprt tmp(ID_compound_literal, expr.
type());
1105 if(op.
id()==ID_array &&
1106 expr.
type().
id()==ID_array &&
1108 tmp.type()=op.
type();
1111 expr.
set(ID_C_lvalue,
true);
1116 if(expr_type.
id()==ID_empty)
1127 if(expr_type.
id()==ID_vector)
1130 if(op_type.
id()==ID_vector)
1132 else if(op_type.
id()==ID_signedbv ||
1133 op_type.
id()==ID_unsignedbv)
1140 error() <<
"type cast to `" 1141 <<
to_string(expr_type) <<
"' is not permitted" <<
eom;
1148 else if(op_type.
id()==ID_array)
1156 else if(op_type.
id()==ID_empty)
1158 if(expr_type.
id()!=ID_empty)
1161 error() <<
"type cast from void only permitted to void, but got `" 1166 else if(op_type.
id()==ID_vector)
1173 if((expr_type.
id()==ID_signedbv ||
1174 expr_type.
id()==ID_unsignedbv) &&
1182 error() <<
"type cast from vector to `" 1190 error() <<
"type cast from `" 1206 if(expr_type.
id()==ID_pointer)
1207 expr.
set(ID_C_lvalue,
true);
1221 error() <<
"operator `" << expr.
id()
1222 <<
"' expects two operands" <<
eom;
1235 if(array_full_type.
id()!=ID_array &&
1236 array_full_type.
id()!=ID_pointer &&
1237 array_full_type.
id()!=ID_vector &&
1238 (index_full_type.id()==ID_array ||
1239 index_full_type.id()==ID_pointer ||
1240 index_full_type.id()==ID_vector))
1241 std::swap(array_expr, index_expr);
1251 if(final_array_type.
id()==ID_array ||
1252 final_array_type.
id()==ID_vector)
1254 if(array_expr.
get_bool(ID_C_lvalue))
1255 expr.
set(ID_C_lvalue,
true);
1257 else if(final_array_type.
id()==ID_pointer)
1262 exprt addition(ID_plus, array_expr.
type());
1265 expr.
id(ID_dereference);
1266 expr.
set(ID_C_lvalue,
true);
1271 error() <<
"operator [] must take array/vector or pointer but got `" 1286 if(expr.
id()==ID_equal)
1287 expr.
id(ID_ieee_float_equal);
1288 else if(expr.
id()==ID_notequal)
1289 expr.
id(ID_ieee_float_notequal);
1302 if(
follow(o_type0).
id()==ID_vector ||
1303 follow(o_type1).
id()==ID_vector)
1311 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1316 if(final_type.
id()!=ID_array &&
1317 final_type.
id()!=ID_incomplete_struct)
1338 if(type0.
id()==ID_pointer)
1340 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1343 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1344 expr.
id()==ID_ge || expr.
id()==ID_gt)
1348 if(type0.
id()==ID_string_constant)
1350 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1357 if(type0.
id()==ID_pointer &&
1364 if(type1.
id()==ID_pointer &&
1384 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1392 error() <<
"operator `" << expr.
id()
1393 <<
"' not defined for types `" 1408 if(o_type0.
id()!=ID_vector ||
1409 o_type1.id()!=ID_vector ||
1413 error() <<
"vector operator `" << expr.
id()
1414 <<
"' not defined for types `" 1430 error() <<
"ptrmember operator expects one operand" <<
eom;
1436 if(final_op0_type.
id()==ID_array)
1441 index_expr.
set(ID_C_lvalue,
true);
1444 else if(final_op0_type.
id()==ID_pointer)
1455 error() <<
"ptrmember operator requires pointer or array type " 1456 "on left hand side, but got `" 1470 error() <<
"member operator expects one operand" <<
eom;
1479 if(type.
id()==ID_incomplete_struct)
1482 error() <<
"member operator got incomplete struct type " 1483 "on left hand side" <<
eom;
1487 if(type.
id()==ID_incomplete_union)
1490 error() <<
"member operator got incomplete union type " 1491 "on left hand side" <<
eom;
1495 if(type.
id()!=ID_struct &&
1496 type.
id()!=ID_union)
1499 error() <<
"member operator requires structure type " 1500 "on left hand side but got `" 1509 expr.
get(ID_component_name);
1525 error() <<
"member `" << component_name
1526 <<
"' not found in `" 1539 expr.
set(ID_C_lvalue,
true);
1542 expr.
set(ID_C_constant,
true);
1545 const irep_idt &identifier=component.
get(ID_C_identifier);
1547 if(!identifier.
empty())
1548 expr.
set(ID_C_identifier, identifier);
1552 if(access==ID_private)
1555 error() <<
"member `" << component_name
1556 <<
"' is " << access <<
eom;
1565 assert(operands.size()==3);
1568 const typet o_type0=operands[0].type();
1569 const typet o_type1=operands[1].type();
1570 const typet o_type2=operands[2].type();
1575 if(operands[1].type().
id()==ID_pointer &&
1576 operands[2].type().
id()!=ID_pointer)
1578 else if(operands[2].type().
id()==ID_pointer &&
1579 operands[1].type().
id()!=ID_pointer)
1582 if(operands[1].type().
id()==ID_pointer &&
1583 operands[2].type().
id()==ID_pointer &&
1584 operands[1].type()!=operands[2].type())
1591 if(operands[1].type().subtype().
id()==ID_empty &&
1595 else if(operands[2].type().subtype().id()==ID_empty &&
1599 else if(operands[1].type().subtype().id()!=ID_code ||
1600 operands[2].type().subtype().id()!=ID_code)
1624 if(operands[1].type().id()==ID_empty ||
1625 operands[2].type().id()==ID_empty)
1631 if(
follow(operands[1].type())==
follow(operands[2].type()))
1633 expr.
type()=operands[1].type();
1639 if(operands[1].get_bool(ID_C_lvalue) &&
1640 operands[2].get_bool(ID_C_lvalue))
1641 expr.
set(ID_C_lvalue,
true);
1647 error() <<
"operator ?: not defined for types `" 1661 if(operands.size()!=2)
1664 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1671 if_expr.
cond()=operands[0];
1679 expr.
op0()=if_expr.
op1();
1680 expr.
op1()=if_expr.
op2();
1689 error() <<
"unary operator & expects one operand" <<
eom;
1695 if(op.
type().
id()==ID_c_bit_field)
1698 error() <<
"cannot take address of a bit field" <<
eom;
1703 if(op.
id()==ID_label)
1715 if(op.
id()==ID_address_of &&
1723 tmp.
set(ID_C_implicit,
false);
1728 if(op.
id()==ID_struct ||
1729 op.
id()==ID_union ||
1730 op.
id()==ID_array ||
1731 op.
id()==ID_string_constant)
1739 else if(op.
type().
id()==ID_code)
1747 <<
"' not an lvalue" <<
eom;
1759 error() <<
"unary operator * expects one operand" <<
eom;
1767 if(op_type.
id()==ID_array)
1775 else if(op_type.
id()==ID_pointer)
1783 <<
"' is not a pointer, but got `" 1788 expr.
set(ID_C_lvalue,
true);
1799 if(expr.
type().
id()==ID_code)
1802 tmp.
set(ID_C_implicit,
true);
1812 if(statement==ID_preincrement ||
1813 statement==ID_predecrement ||
1814 statement==ID_postincrement ||
1815 statement==ID_postdecrement)
1820 error() << statement <<
"operator expects one operand" <<
eom;
1831 <<
"' not an lvalue" <<
eom;
1839 <<
"' is constant" <<
eom;
1843 if(final_type0.
id()==ID_c_enum_tag)
1846 ID_incomplete_c_enum)
1849 error() <<
"operator `" << statement
1850 <<
"' given incomplete type `" 1857 else if(final_type0.
id()==ID_c_bit_field)
1862 expr.
type()=underlying_type;
1868 else if(final_type0.
id()==ID_pointer)
1876 error() <<
"operator `" << statement
1877 <<
"' not defined for type `" 1884 else if(statement==ID_function_call)
1887 else if(statement==ID_statement_expression)
1889 else if(statement==ID_gcc_conditional_expression)
1894 error() <<
"unknown side effect: " << statement <<
eom;
1905 error() <<
"function_call side effect expects two operands" <<
eom;
1914 if(f_op.
id()==ID_symbol)
1918 asm_label_mapt::const_iterator entry=
1921 identifier=entry->second;
1923 symbol_tablet::symbolst::const_iterator sym_entry =
1944 if(identifier==
"malloc" ||
1945 identifier==
"realloc" ||
1946 identifier==
"reallocf" ||
1947 identifier==
"valloc")
1952 new_symbol.
name=identifier;
1956 new_symbol.
type.
set(ID_C_incomplete,
true);
1965 warning() <<
"function `" << identifier <<
"' is not declared" <<
eom;
1969 sym_entry->second.type.get_bool(ID_C_inlined) &&
1970 sym_entry->second.is_macro && sym_entry->second.value.is_not_nil())
1973 const symbolt &func_sym = sym_entry->second;
1979 auto p_it = parameters.begin();
1982 if(p_it == parameters.end())
1986 error() <<
"function call has additional arguments, " 1987 <<
"cannot apply always_inline" <<
eom;
1991 irep_idt p_id = p_it->get_identifier();
1997 replace.
insert(p_id, arg);
2002 if(p_it != parameters.end())
2005 error() <<
"function call has missing arguments, " 2006 <<
"cannot apply always_inline" <<
eom;
2014 ID_statement_expression, func_type.
return_type());
2037 error() <<
"function has multiple return statements, " 2038 <<
"cannot apply always_inline" <<
eom;
2042 side_effect_expr.copy_to_operands(body);
2045 expr.
swap(side_effect_expr);
2056 if(f_op_type.
id()!=ID_pointer)
2059 error() <<
"expected function/function pointer as argument but got `" 2065 if(f_op.
id()==ID_address_of &&
2076 tmp.
set(ID_C_implicit,
true);
2081 if(f_op.
type().
id()!=ID_code)
2084 error() <<
"expected code as argument" <<
eom;
2107 if(f_op.
id()!=ID_symbol)
2117 error() <<
"same_object expects two operands" <<
eom;
2121 exprt same_object_expr=
2125 return same_object_expr;
2132 error() <<
"get_must expects two operands" <<
eom;
2142 return get_must_expr;
2149 error() <<
"get_may expects two operands" <<
eom;
2159 return get_may_expr;
2166 error() <<
"invalid_pointer expects one operand" <<
eom;
2173 return same_object_expr;
2180 error() <<
"buffer_size expects one operand" <<
eom;
2188 return buffer_size_expr;
2195 error() <<
"is_zero_string expects one operand" <<
eom;
2201 is_zero_string_expr.
set(ID_C_lvalue,
true);
2204 return is_zero_string_expr;
2211 error() <<
"zero_string_length expects one operand" <<
eom;
2215 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2217 zero_string_length_expr.
set(ID_C_lvalue,
true);
2220 return zero_string_length_expr;
2227 error() <<
"dynamic_object expects one argument" <<
eom;
2235 return dynamic_object_expr;
2242 error() <<
"pointer_offset expects one argument" <<
eom;
2256 error() <<
"pointer_object expects one argument" <<
eom;
2265 else if(identifier==
"__builtin_bswap16" ||
2266 identifier==
"__builtin_bswap32" ||
2267 identifier==
"__builtin_bswap64")
2274 error() << identifier <<
" expects one operand" <<
eom;
2285 identifier ==
"__builtin_fpclassify" ||
2291 error() << identifier <<
" expects six arguments" <<
eom;
2302 if(fp_value.
type().
id() != ID_floatbv)
2305 error() <<
"non-floating-point argument for " << identifier <<
eom;
2313 const auto &arguments = expr.
arguments();
2332 identifier==
"__builtin_isnan")
2337 error() <<
"isnan expects one operand" <<
eom;
2353 error() <<
"isfinite expects one operand" <<
eom;
2363 identifier==
"__builtin_inf")
2400 error() <<
"abs-functions expect one operand" <<
eom;
2414 error() <<
"allocate expects two operands" <<
eom;
2420 malloc_expr.operands()=expr.
arguments();
2427 identifier==
"__builtin_isinf")
2432 error() << identifier <<
" expects one operand" <<
eom;
2441 else if(identifier ==
"__builtin_isinf_sign")
2446 error() << identifier <<
" expects one operand" <<
eom;
2468 identifier ==
"__builtin_isnormal")
2473 error() << identifier <<
" expects one operand" <<
eom;
2479 if(fp_value.
type().
id() != ID_floatbv)
2482 error() <<
"non-floating-point argument for " << identifier <<
eom;
2494 identifier==
"__builtin_signbit" ||
2495 identifier==
"__builtin_signbitf" ||
2496 identifier==
"__builtin_signbitl")
2501 error() << identifier <<
" expects one operand" <<
eom;
2510 else if(identifier==
"__builtin_popcount" ||
2511 identifier==
"__builtin_popcountl" ||
2512 identifier==
"__builtin_popcountll" ||
2513 identifier==
"__popcnt16" ||
2514 identifier==
"__popcnt" ||
2515 identifier==
"__popcnt64")
2520 error() << identifier <<
" expects one operand" <<
eom;
2527 return popcount_expr;
2534 error() <<
"equal expects two operands" <<
eom;
2543 equality_expr.
rhs().
type(), *
this))
2546 error() <<
"equal expects two operands of same type" <<
eom;
2550 return equality_expr;
2552 else if(identifier==
"__builtin_expect")
2563 error() <<
"__builtin_expect expects two arguments" <<
eom;
2569 else if(identifier==
"__builtin_object_size")
2578 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2593 error() <<
"__builtin_object_size expects constant as second argument, " 2601 if(arg1==0 || arg1==1)
2614 else if(identifier==
"__builtin_choose_expr")
2620 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2632 else if(identifier==
"__builtin_constant_p")
2639 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2647 bool is_constant=
false;
2651 if(tmp1.
id()==ID_typecast &&
2653 tmp1.
op0().
id()==ID_address_of &&
2669 else if(identifier==
"__builtin_classify_type")
2676 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2687 if(type.
id() == ID_c_bit_field)
2690 unsigned type_number;
2692 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2703 type.
id() == ID_empty ? 0
2704 : (type.
id() == ID_bool || type.
id() == ID_c_bool) ? 4
2705 : (type.
id() == ID_pointer || type.
id() == ID_array) ? 5
2706 : type.
id() == ID_floatbv ? 8
2707 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv) ? 9
2708 : type.
id() == ID_struct ? 12
2709 : type.
id() == ID_union ? 13
2724 error() <<
"float_debug expects two operands" <<
eom;
2730 "float_debug1":
"float_debug2";
2732 exprt float_debug_expr(
id, expr.
type());
2734 float_debug_expr.add_source_location()=source_location;
2736 return float_debug_expr;
2738 else if(identifier==
"__sync_fetch_and_add" ||
2739 identifier==
"__sync_fetch_and_sub" ||
2740 identifier==
"__sync_fetch_and_or" ||
2741 identifier==
"__sync_fetch_and_and" ||
2742 identifier==
"__sync_fetch_and_xor" ||
2743 identifier==
"__sync_fetch_and_nand" ||
2744 identifier==
"__sync_add_and_fetch" ||
2745 identifier==
"__sync_sub_and_fetch" ||
2746 identifier==
"__sync_or_and_fetch" ||
2747 identifier==
"__sync_and_and_fetch" ||
2748 identifier==
"__sync_xor_and_fetch" ||
2749 identifier==
"__sync_nand_and_fetch" ||
2750 identifier==
"__sync_val_compare_and_swap" ||
2751 identifier==
"__sync_lock_test_and_set" ||
2752 identifier==
"__sync_lock_release")
2761 error() <<
"__sync_* primitives take as least one argument" <<
eom;
2767 if(ptr_arg.
type().
id()!=ID_pointer)
2770 error() <<
"__sync_* primitives take pointer as first argument" <<
eom;
2795 if(code_type.
get_bool(ID_C_incomplete))
2799 else if(code_type.
is_KnR())
2804 while(parameter_types.size()>arguments.size())
2809 if(parameter_types.size()>arguments.size())
2812 error() <<
"not enough function arguments" <<
eom;
2816 else if(parameter_types.size()!=arguments.size())
2819 error() <<
"wrong number of function arguments: " 2820 <<
"expected " << parameter_types.size()
2821 <<
", but got " << arguments.size() <<
eom;
2825 for(std::size_t i=0; i<arguments.size(); i++)
2827 exprt &op=arguments[i];
2833 else if(i<parameter_types.size())
2838 const typet &op_type=parameter_type.
type();
2840 if(op_type.
id()==ID_bool &&
2841 op.
id()==ID_side_effect &&
2842 op.
get(ID_statement)==ID_assign &&
2846 warning() <<
"assignment where Boolean argument is expected" <<
eom;
2856 if(type.
id()==ID_array)
2859 dest_type.
subtype().
set(ID_C_constant, ID_1);
2876 error() <<
"operator `" << expr.
id()
2877 <<
"' expects one operand" <<
eom;
2885 if(o_type.
id()==ID_vector)
2904 error() <<
"operator `" << expr.
id()
2905 <<
"' not defined for type `" 2915 error() <<
"operator `" << expr.
id()
2916 <<
"' expects one operand" <<
eom;
2948 if((type0.
subtype().
id()==ID_signedbv ||
2964 error() <<
"operator `" << expr.
id()
2965 <<
"' expects two operands" <<
eom;
2975 if(o_type0.
id()==ID_vector &&
2976 o_type1.id()==ID_vector)
2983 if(o_type0!=o_type1)
2997 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
2998 expr.
id()==ID_mult || expr.
id()==ID_div)
3000 if(type0.
id()==ID_pointer || type1.id()==ID_pointer)
3005 else if(type0==type1)
3014 else if(expr.
id()==ID_mod)
3018 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3025 else if(expr.
id()==ID_bitand ||
3026 expr.
id()==ID_bitxor ||
3027 expr.
id()==ID_bitor)
3036 else if(type0.
id()==ID_bool)
3038 if(expr.
id()==ID_bitand)
3040 else if(expr.
id()==ID_bitor)
3042 else if(expr.
id()==ID_bitxor)
3053 error() <<
"operator `" << expr.
id()
3054 <<
"' not defined for types `" 3062 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3070 if(o_type0.
id()==ID_vector &&
3071 o_type1.id()==ID_vector)
3079 expr.
type()=op0.type();
3084 if(o_type0.
id()==ID_vector &&
3089 expr.
type()=op0.type();
3100 expr.
type()=op0.type();
3102 if(expr.
id()==ID_shr)
3106 if(op0_type.
id()==ID_unsignedbv)
3111 else if(op0_type.
id()==ID_signedbv)
3122 error() <<
"operator `" << expr.
id()
3123 <<
"' not defined for types `" 3132 assert(type.
id()==ID_pointer);
3136 if(subtype.id()==ID_symbol)
3139 if(subtype.id()==ID_incomplete_struct)
3142 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3157 if(expr.
id()==ID_minus ||
3158 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3160 if(type0.
id()==ID_pointer &&
3161 type1.id()==ID_pointer)
3171 if(type0.
id()==ID_pointer &&
3172 (type1.id()==ID_bool ||
3173 type1.id()==ID_c_bool ||
3174 type1.id()==ID_unsignedbv ||
3175 type1.id()==ID_signedbv ||
3176 type1.id()==ID_c_bit_field ||
3177 type1.id()==ID_c_enum_tag))
3185 else if(expr.
id()==ID_plus ||
3186 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3188 exprt *p_op, *int_op;
3190 if(type0.
id()==ID_pointer)
3195 else if(type1.id()==ID_pointer)
3202 p_op=int_op=
nullptr;
3208 if(int_op_type.
id()==ID_bool ||
3209 int_op_type.
id()==ID_c_bool ||
3210 int_op_type.
id()==ID_unsignedbv ||
3211 int_op_type.
id()==ID_signedbv ||
3212 int_op_type.
id()==ID_c_bit_field ||
3213 int_op_type.
id()==ID_c_enum_tag)
3224 if(expr.
id()==ID_side_effect)
3230 error() <<
"operator `" << op_name
3231 <<
"' not defined for types `" 3242 error() <<
"operator `" << expr.
id()
3243 <<
"' expects two operands" <<
eom;
3265 <<
"' expects two operands" <<
eom;
3277 if(type0.
id()==ID_empty)
3280 error() <<
"cannot assign void" <<
eom;
3288 <<
"' not an lvalue" <<
eom;
3296 <<
"' is constant" <<
eom;
3301 if(type0.
id()==ID_array ||
3302 type0.
id()==ID_incomplete_array)
3305 error() <<
"direct assignments to arrays not permitted" <<
eom;
3312 if(op0.
type().
id()==ID_c_bit_field)
3318 expr.
type()=o_type0;
3320 if(statement==ID_assign)
3325 else if(statement==ID_assign_shl ||
3326 statement==ID_assign_shr)
3332 if(statement==ID_assign_shl)
3342 if(underlying_type.
id()==ID_c_enum_tag)
3344 const typet &c_enum_type=
3346 underlying_type=c_enum_type.
subtype();
3349 if(underlying_type.
id()==ID_unsignedbv ||
3350 underlying_type.
id()==ID_c_bool)
3352 expr.
set(ID_statement, ID_assign_lshr);
3355 else if(underlying_type.
id()==ID_signedbv)
3357 expr.
set(ID_statement, ID_assign_ashr);
3363 else if(statement==ID_assign_bitxor ||
3364 statement==ID_assign_bitand ||
3365 statement==ID_assign_bitor)
3368 if(o_type0.
id()==ID_bool ||
3369 o_type0.
id()==ID_c_bool)
3372 if(op1.
type().
id()==ID_bool ||
3373 op1.
type().
id()==ID_c_bool ||
3374 op1.
type().
id()==ID_c_enum_tag ||
3375 op1.
type().
id()==ID_unsignedbv ||
3376 op1.
type().
id()==ID_signedbv)
3379 else if(o_type0.
id()==ID_c_enum_tag ||
3380 o_type0.
id()==ID_unsignedbv ||
3381 o_type0.
id()==ID_signedbv ||
3382 o_type0.
id()==ID_c_bit_field)
3387 else if(o_type0.
id()==ID_vector &&
3388 o_type1.
id()==ID_vector)
3394 if(o_type0!=o_type1)
3402 if(o_type0.
id()==ID_pointer &&
3403 (statement==ID_assign_minus || statement==ID_assign_plus))
3408 else if(o_type0.
id()==ID_vector &&
3409 o_type1.
id()==ID_vector)
3415 if(o_type0!=o_type1)
3420 else if(o_type0.
id()==ID_bool ||
3421 o_type0.
id()==ID_c_bool)
3424 if(op1.
type().
id()==ID_bool ||
3425 op1.
type().
id()==ID_c_bool ||
3426 op1.
type().
id()==ID_c_enum_tag ||
3427 op1.
type().
id()==ID_unsignedbv ||
3428 op1.
type().
id()==ID_signedbv)
3436 op1.
type().
id()==ID_bool ||
3437 op1.
type().
id()==ID_c_bool ||
3438 op1.
type().
id()==ID_c_enum_tag)
3444 error() <<
"assignment `" << statement
3445 <<
"' not defined for types `" 3458 expr.
id()!=ID_infinity)
3461 error() <<
"expected constant expression, but got `" 3474 expr.
id()!=ID_infinity)
3477 error() <<
"conversion to integer constant failed" <<
eom;
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
virtual void typecheck_expr_binary_boolean(exprt &expr)
const irep_idt & get_statement() const
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression.
irep_idt name
The unique identifier.
exprt size_of_expr(const typet &type, const namespacet &ns)
std::map< irep_idt, source_locationt > labels_used
struct configt::ansi_ct ansi_c
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
void typecheck_declaration(ansi_c_declarationt &)
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
asm_label_mapt asm_label_map
virtual void typecheck_expr_index(exprt &expr)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
constant_exprt to_expr() const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Fixed-width bit-vector with IEEE floating-point interpretation.
std::vector< irept > subt
virtual void make_constant(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Evaluates to true if the operand is infinite.
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
bool has_ellipsis() const
Deprecated expression utility functions.
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
unsignedbv_typet unsigned_int_type()
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_function() const
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
const componentst & components() const
id_type_mapt parameter_map
The trinary if-then-else operator.
Evaluates to true if the operand is a normal number.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
void make_bool(bool value)
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
signedbv_typet pointer_diff_type()
virtual std::string to_string(const exprt &expr)
const typet & follow_tag(const union_tag_typet &) const
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
side_effect_exprt & to_side_effect_expr(exprt &expr)
static ieee_float_spect double_precision()
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
symbol_tablet & symbol_table
mstreamt & warning() const
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
preprocessort preprocessor
void follow_macros(exprt &) const
virtual void typecheck_expr_symbol(exprt &expr)
static bool is_numeric_type(const typet &src)
const irep_idt & id() const
Evaluates to true if the operand is NaN.
An expression denoting infinity.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
class code_blockt & make_block()
virtual void typecheck_expr_operands(exprt &expr)
ANSI-C Language Type Checking.
ANSI-C Language Type Checking.
A declaration of a local variable.
virtual void typecheck_expr_member(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
const source_locationt & find_source_location() const
source_locationt source_location
Operator to dereference a pointer.
A constant-size array type.
exprt pointer_object(const exprt &p)
virtual void make_index_type(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
union constructor from single element
mp_integer alignment(const typet &type, const namespacet &ns)
const irep_idt & get(const irep_namet &name) const
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
static ieee_float_spect single_precision()
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
const exprt & size() const
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
bool has_prefix(const std::string &s, const std::string &prefix)
virtual void typecheck_expr(exprt &expr)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void err_location(const source_locationt &loc)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
const typet & follow(const typet &) const
bitvector_typet index_type()
#define Forall_irep(it, irep)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::list< codet > clean_code
codet & find_last_statement()
Operator to return the address of an object.
std::vector< typet > subtypest
Various predicates over pointers in programs.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
virtual void typecheck_expr_function_identifier(exprt &expr)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
static exprt conditional_cast(const exprt &expr, const typet &type)
std::vector< exprt > operandst
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
bitvector_typet long_double_type()
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
const irep_idt & display_name() const
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
A function call side effect.
Complex numbers made of pair of given subtype.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
virtual void typecheck_expr_sizeof(exprt &expr)
message_handlert & get_message_handler()
const irep_idt & get_access() const
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Base type of C structs and unions, and C++ classes.
mstreamt & result() const
bool is_number(const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
The popcount (counting the number of bits set to 1) expression.
Evaluates to true if the operand is finite.
void set_statement(const irep_idt &statement)
exprt invalid_pointer(const exprt &pointer)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
exprt pointer_offset(const exprt &pointer)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
const source_locationt & source_location() const
virtual void typecheck_expr_dereference(exprt &expr)
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
exprt::operandst & arguments()
void set_identifier(const irep_idt &identifier)
#define Forall_operands(it, expr)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
source_locationt & add_source_location()
void insert(const irep_idt &identifier, const exprt &expr)
const codet & to_code(const exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
static void add_rounding_mode(exprt &)
Expression to hold a symbol (variable)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const code_blockt & to_code_block(const codet &code)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A statement in a programming language.
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
signedbv_typet signed_int_type()
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
void remove(const irep_namet &name)
const typet & subtype() const
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_constant(exprt &expr)
virtual void make_constant_rec(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
An expression containing a side effect.
virtual void typecheck_expr_main(exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
exprt same_object(const exprt &p1, const exprt &p2)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
A base class for shift operators.
bitvector_typet char_type()
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
The byte swap expression.
void set(const irep_namet &name, const irep_idt &value)
virtual void typecheck_expr_shifts(shift_exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
const irep_idt & get_statement() const
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
virtual void typecheck_code(codet &code)
const code_function_callt & to_code_function_call(const codet &code)
bool simplify(exprt &expr, const namespacet &ns)
A generic base class for expressions that are predicates, i.e., boolean-typed.
static ieee_floatt zero(const floatbv_typet &type)
IEEE-floating-point equality.
#define forall_irep(it, irep)
C Language Type Checking.
virtual void adjust_float_rel(exprt &expr)