Go to the documentation of this file.
45 if(expr.
id()==ID_already_typechecked)
63 if(expr.
id()==ID_div ||
68 if(expr.
type().
id()==ID_floatbv &&
77 expr.
id(ID_floatbv_div);
78 else if(expr.
id()==ID_mult)
79 expr.
id(ID_floatbv_mult);
80 else if(expr.
id()==ID_plus)
81 expr.
id(ID_floatbv_plus);
82 else if(expr.
id()==ID_minus)
83 expr.
id(ID_floatbv_minus);
104 if(type1.
id()==ID_c_enum_tag)
106 else if(type2.
id()==ID_c_enum_tag)
109 if(type1.
id()==ID_c_enum)
111 if(type2.
id()==ID_c_enum)
113 else if(type2==type1.
subtype())
116 else if(type2.
id()==ID_c_enum)
121 else if(type1.
id()==ID_pointer &&
122 type2.
id()==ID_pointer)
126 else if(type1.
id()==ID_array &&
127 type2.
id()==ID_array)
132 else if(type1.
id()==ID_code &&
146 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
162 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
172 if(expr.
id()==ID_side_effect)
174 else if(expr.
id()==ID_constant)
176 else if(expr.
id()==ID_infinity)
180 else if(expr.
id()==ID_symbol)
182 else if(expr.
id()==ID_unary_plus ||
183 expr.
id()==ID_unary_minus ||
184 expr.
id()==ID_bitnot)
186 else if(expr.
id()==ID_not)
189 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
192 else if(expr.
id()==ID_address_of)
194 else if(expr.
id()==ID_dereference)
196 else if(expr.
id()==ID_member)
198 else if(expr.
id()==ID_ptrmember)
200 else if(expr.
id()==ID_equal ||
201 expr.
id()==ID_notequal ||
207 else if(expr.
id()==ID_index)
209 else if(expr.
id()==ID_typecast)
211 else if(expr.
id()==ID_sizeof)
213 else if(expr.
id()==ID_alignof)
216 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
217 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
218 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
222 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
224 else if(expr.
id()==ID_comma)
226 else if(expr.
id()==ID_if)
228 else if(expr.
id()==ID_code)
231 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
234 else if(expr.
id()==ID_gcc_builtin_va_arg)
236 else if(expr.
id()==ID_cw_va_arg_typeof)
238 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
243 assert(subtypes.size()==2);
249 subtypes[0].
remove(ID_C_constant);
250 subtypes[0].remove(ID_C_volatile);
251 subtypes[0].remove(ID_C_restricted);
252 subtypes[1].remove(ID_C_constant);
253 subtypes[1].remove(ID_C_volatile);
254 subtypes[1].remove(ID_C_restricted);
259 else if(expr.
id()==ID_clang_builtin_convertvector)
268 else if(expr.
id()==ID_builtin_offsetof)
270 else if(expr.
id()==ID_string_constant)
273 expr.
set(ID_C_lvalue,
true);
275 else if(expr.
id()==ID_arguments)
279 else if(expr.
id()==ID_designated_initializer)
281 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
285 if(it->id()==ID_index)
289 else if(expr.
id()==ID_initializer_list)
295 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
301 auto &bindings = binary_expr.op0().operands();
302 auto &where = binary_expr.op1();
304 for(
const auto &binding : bindings)
306 if(binding.get(ID_statement) != ID_decl)
309 error() <<
"expected declaration as operand of quantifier" <<
eom;
317 error() <<
"quantifier must not contain side effects" <<
eom;
322 for(
auto &binding : bindings)
325 if(expr.
id() == ID_lambda)
329 for(
auto &binding : bindings)
330 domain.push_back(binding.type());
340 else if(expr.
id()==ID_label)
344 else if(expr.
id()==ID_array)
348 else if(expr.
id()==ID_complex)
353 else if(expr.
id() == ID_complex_real)
357 if(op.
type().
id() != ID_complex)
362 error() <<
"real part retrieval expects numerical operand, "
370 expr.
swap(complex_real_expr);
378 complex_real_expr.
set(ID_C_lvalue,
true);
381 complex_real_expr.
type().
set(ID_C_constant,
true);
383 expr.
swap(complex_real_expr);
386 else if(expr.
id() == ID_complex_imag)
390 if(op.
type().
id() != ID_complex)
395 error() <<
"real part retrieval expects numerical operand, "
403 expr.
swap(complex_imag_expr);
411 complex_imag_expr.
set(ID_C_lvalue,
true);
414 complex_imag_expr.
type().
set(ID_C_constant,
true);
416 expr.
swap(complex_imag_expr);
419 else if(expr.
id()==ID_generic_selection)
429 if(op.type().id() == ID_bool)
436 for(
auto &irep : generic_associations)
438 if(irep.get(ID_type_arg) != ID_default)
440 typet &type =
static_cast<typet &
>(irep.add(ID_type_arg));
451 for(
const auto &irep : generic_associations)
453 if(irep.get(ID_type_arg) == ID_default)
454 default_match =
static_cast<const exprt &
>(irep.find(ID_value));
456 op_type ==
follow(
static_cast<const typet &
>(irep.find(ID_type_arg))))
458 assoc_match =
static_cast<const exprt &
>(irep.find(ID_value));
465 expr.
swap(default_match);
469 error() <<
"unmatched generic selection: " <<
to_string(op.type())
475 expr.
swap(assoc_match);
480 else if(expr.
id()==ID_gcc_asm_input ||
481 expr.
id()==ID_gcc_asm_output ||
482 expr.
id()==ID_gcc_asm_clobbered_register)
485 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
486 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
490 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
508 expr.
set(ID_C_lvalue,
true);
545 symbol.
name=ID_gcc_builtin_va_arg;
546 symbol.
type=symbol_type;
576 error() <<
"builtin_offsetof expects no operands" <<
eom;
591 if(m_it->id()==ID_member)
593 if(type.
id()!=ID_union && type.
id()!=ID_struct)
596 error() <<
"offsetof of member expects struct/union type, "
602 irep_idt component_name=m_it->get(ID_component_name);
606 assert(type.
id()==ID_union || type.
id()==ID_struct);
616 if(type.
id()==ID_struct)
621 if(!o_opt.has_value())
624 error() <<
"offsetof failed to determine offset of '"
625 << component_name <<
"'" <<
eom;
641 for(
const auto &c : struct_union_type.
components())
645 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
649 if(type.
id()==ID_struct)
654 if(!o_opt.has_value())
657 error() <<
"offsetof failed to determine offset of '"
658 << component_name <<
"'" <<
eom;
670 assert(type.
id()==ID_union || type.
id()==ID_struct);
680 error() <<
"offset-of of member failed to find component '"
681 << component_name <<
"' in '" <<
to_string(type) <<
"'"
688 else if(m_it->id()==ID_index)
690 if(type.
id()!=ID_array)
693 error() <<
"offsetof of index expects array type" <<
eom;
704 if(!sub_size_opt.has_value())
707 error() <<
"offsetof failed to determine array element size" <<
eom;
730 if(expr.
id()==ID_side_effect &&
731 expr.
get(ID_statement)==ID_function_call)
736 else if(expr.
id()==ID_side_effect &&
737 expr.
get(ID_statement)==ID_statement_expression)
742 expr.
id() == ID_forall || expr.
id() == ID_exists || expr.
id() == ID_lambda)
748 auto &bindings = binary_expr.op0().operands();
750 for(
auto &binding : bindings)
759 error() <<
"forall/exists expects one declarator exactly" <<
eom;
766 symbol_tablet::symbolst::const_iterator s_it =
772 error() <<
"failed to find bound symbol `" << identifier
773 <<
"' in symbol table" <<
eom;
777 const symbolt &symbol = s_it->second;
784 error() <<
"unexpected quantified symbol" <<
eom;
808 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
812 expr.
type()=p_it->second;
813 expr.
set(ID_C_lvalue,
true);
818 asm_label_mapt::const_iterator entry=
822 identifier=entry->second;
828 if(
lookup(identifier, symbol_ptr))
831 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
835 const symbolt &symbol=*symbol_ptr;
840 error() <<
"did not expect a type symbol here, but got '"
858 if(expr.
id()==ID_constant &&
860 expr.
set(ID_C_cformat, base_name);
875 else if(identifier==
"__func__" ||
876 identifier==
"__FUNCTION__" ||
877 identifier==
"__PRETTY_FUNCTION__")
883 s.
set(ID_C_lvalue,
true);
894 expr.
set(ID_C_lvalue,
true);
896 if(expr.
type().
id()==ID_code)
899 tmp.
set(ID_C_implicit,
true);
918 if(last_statement==ID_expression)
924 if(op.
type().
id()==ID_array)
958 if(type.
id()==ID_c_bit_field)
961 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
964 else if(type.
id() == ID_bool)
967 error() <<
"sizeof cannot be applied to single bits" <<
eom;
970 else if(type.
id() == ID_empty)
979 (type.
id() == ID_struct_tag &&
981 (type.
id() == ID_union_tag &&
983 (type.
id() == ID_c_enum_tag &&
988 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
995 if(!size_of_opt.has_value())
1002 new_expr = size_of_opt.value();
1005 new_expr.
swap(expr);
1007 expr.
add(ID_C_c_sizeof_type)=type;
1015 decl_block.set_statement(ID_decl_block);
1025 exprt comma_expr(ID_comma, expr.
type());
1027 expr.
swap(comma_expr);
1033 typet argument_type;
1041 argument_type=op_type;
1065 decl_block.set_statement(ID_decl_block);
1077 op.
swap(comma_expr);
1083 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1084 op.
id() != ID_initializer_list)
1092 if(op.
type().
id() == ID_bool)
1097 for(
const auto &c : union_type.components())
1099 if(c.type() == op.
type())
1105 expr.
set(ID_C_lvalue,
true);
1113 <<
"' not found in union" <<
eom;
1120 if(op.
id()==ID_initializer_list)
1129 exprt tmp(ID_compound_literal, expr.
type());
1133 if(op.
id()==ID_array &&
1134 expr.
type().
id()==ID_array &&
1139 expr.
set(ID_C_lvalue,
true);
1144 if(expr_type.
id()==ID_empty)
1150 if(expr_type == op_type)
1155 if(expr_type.
id()==ID_vector)
1158 if(op_type.
id()==ID_vector)
1160 else if(op_type.
id()==ID_signedbv ||
1161 op_type.
id()==ID_unsignedbv)
1168 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1176 else if(op_type.
id()==ID_array)
1181 else if(op_type.
id()==ID_empty)
1183 if(expr_type.
id()!=ID_empty)
1186 error() <<
"type cast from void only permitted to void, but got '"
1191 else if(op_type.
id()==ID_vector)
1198 if((expr_type.
id()==ID_signedbv ||
1199 expr_type.
id()==ID_unsignedbv) &&
1208 <<
"' not permitted" <<
eom;
1215 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1231 if(expr_type.
id()==ID_pointer)
1232 expr.
set(ID_C_lvalue,
true);
1249 const typet &array_type = array_expr.
type();
1253 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1254 array_type.
id() != ID_vector &&
1257 std::swap(array_expr, index_expr);
1265 const typet final_array_type = array_expr.
type();
1267 if(final_array_type.
id()==ID_array ||
1268 final_array_type.
id()==ID_vector)
1272 if(array_expr.
get_bool(ID_C_lvalue))
1273 expr.
set(ID_C_lvalue,
true);
1275 if(final_array_type.
get_bool(ID_C_constant))
1276 expr.
type().
set(ID_C_constant,
true);
1278 else if(final_array_type.
id()==ID_pointer)
1284 std::swap(summands, expr.
operands());
1286 expr.
id(ID_dereference);
1287 expr.
set(ID_C_lvalue,
true);
1293 error() <<
"operator [] must take array/vector or pointer but got '"
1302 if(expr.
op0().
type().
id() == ID_floatbv)
1304 if(expr.
id()==ID_equal)
1305 expr.
id(ID_ieee_float_equal);
1306 else if(expr.
id()==ID_notequal)
1307 expr.
id(ID_ieee_float_notequal);
1320 if(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1328 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1332 if(o_type0.
id() != ID_array)
1353 if(type0.
id()==ID_pointer)
1355 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1358 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1359 expr.
id()==ID_ge || expr.
id()==ID_gt)
1363 if(type0.
id()==ID_string_constant)
1365 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1372 if(type0.
id()==ID_pointer &&
1379 if(type1.
id()==ID_pointer &&
1399 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1407 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1423 o_type0.
id() != ID_vector || o_type1.
id() != ID_vector ||
1427 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1441 const typet &op0_type = op.type();
1443 if(op0_type.
id() == ID_array)
1448 index_expr.
set(ID_C_lvalue,
true);
1449 op.swap(index_expr);
1451 else if(op0_type.
id() == ID_pointer)
1457 op.swap(deref_expr);
1462 error() <<
"ptrmember operator requires pointer or array type "
1463 "on left hand side, but got '"
1479 if(type.
id()!=ID_struct &&
1480 type.
id()!=ID_union)
1483 error() <<
"member operator requires structure type "
1484 "on left hand side but got '"
1495 error() <<
"member operator got incomplete " << type.
id()
1496 <<
" type on left hand side" <<
eom;
1501 expr.
get(ID_component_name);
1517 error() <<
"member '" << component_name <<
"' not found in '"
1530 expr.
set(ID_C_lvalue,
true);
1533 expr.
type().
set(ID_C_constant,
true);
1538 if(!identifier.
empty())
1539 expr.
set(ID_C_identifier, identifier);
1543 if(access==ID_private)
1546 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1555 assert(operands.size()==3);
1558 const typet o_type0=operands[0].type();
1559 const typet o_type1=operands[1].type();
1560 const typet o_type2=operands[2].type();
1565 if(operands[1].type().
id()==ID_pointer &&
1566 operands[2].type().
id()!=ID_pointer)
1568 else if(operands[2].type().
id()==ID_pointer &&
1569 operands[1].type().
id()!=ID_pointer)
1572 if(operands[1].type().
id()==ID_pointer &&
1573 operands[2].type().
id()==ID_pointer &&
1574 operands[1].type()!=operands[2].type())
1581 if(operands[1].type().subtype().
id()==ID_empty &&
1585 else if(operands[2].type().subtype().
id()==ID_empty &&
1589 else if(operands[1].type().subtype().
id()!=ID_code ||
1590 operands[2].type().subtype().
id()!=ID_code)
1614 if(operands[1].type().
id()==ID_empty ||
1615 operands[2].type().
id()==ID_empty)
1621 if(operands[1].type() == operands[2].type())
1623 expr.
type()=operands[1].type();
1629 if(operands[1].get_bool(ID_C_lvalue) &&
1630 operands[2].get_bool(ID_C_lvalue))
1631 expr.
set(ID_C_lvalue,
true);
1637 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1650 if(operands.size()!=2)
1653 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1659 if_exprt if_expr(operands[0], operands[0], operands[1]);
1674 if(op.
type().
id()==ID_c_bit_field)
1677 error() <<
"cannot take address of a bit field" <<
eom;
1681 if(op.
type().
id() == ID_bool)
1684 error() <<
"cannot take address of a single bit" <<
eom;
1689 if(op.
id()==ID_label)
1702 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1708 tmp.
set(ID_C_implicit,
false);
1713 if(op.
id()==ID_struct ||
1714 op.
id()==ID_union ||
1715 op.
id()==ID_array ||
1716 op.
id()==ID_string_constant)
1724 else if(op.
type().
id()==ID_code)
1731 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1745 if(op_type.
id()==ID_array)
1753 else if(op_type.
id()==ID_pointer)
1761 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1766 expr.
set(ID_C_lvalue,
true);
1777 if(expr.
type().
id()==ID_code)
1780 tmp.
set(ID_C_implicit,
true);
1790 if(statement==ID_preincrement ||
1791 statement==ID_predecrement ||
1792 statement==ID_postincrement ||
1793 statement==ID_postdecrement)
1802 <<
"' not an lvalue" <<
eom;
1813 if(type0.
id() == ID_c_enum_tag)
1819 error() <<
"operator '" << statement <<
"' given incomplete type '"
1828 else if(type0.
id() == ID_c_bit_field)
1833 expr.
type()=underlying_type;
1835 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1844 else if(type0.
id() == ID_pointer)
1852 error() <<
"operator '" << statement <<
"' not defined for type '"
1859 else if(statement==ID_function_call)
1862 else if(statement==ID_statement_expression)
1864 else if(statement==ID_gcc_conditional_expression)
1869 error() <<
"unknown side effect: " << statement <<
eom;
1880 error() <<
"function_call side effect expects two operands" <<
eom;
1889 if(f_op.
id()==ID_symbol)
1893 asm_label_mapt::const_iterator entry=
1896 identifier=entry->second;
1907 identifier ==
"__noop" &&
1924 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1927 !parameters.empty(),
1928 "GCC polymorphic built-ins should have at least one parameter");
1933 if(parameters.front().type().id() == ID_pointer)
1935 identifier_with_type =
id2string(identifier) +
"_" +
1937 parameters.front().type().subtype(), *
this);
1941 identifier_with_type =
1945 gcc_polymorphic->set_identifier(identifier_with_type);
1949 for(std::size_t i = 0; i < parameters.size(); ++i)
1956 id2string(identifier_with_type) +
"::" + base_name;
1959 new_symbol.
type = parameters[i].type();
1962 new_symbol.
mode = ID_C;
1964 parameters[i].set_identifier(new_symbol.
name);
1965 parameters[i].set_base_name(new_symbol.
base_name);
1972 new_symbol.
name = identifier_with_type;
1973 new_symbol.
base_name = identifier_with_type;
1975 new_symbol.
type = gcc_polymorphic->type();
1976 new_symbol.
mode = ID_C;
1983 new_symbol.
value = implementation;
1988 f_op = std::move(*gcc_polymorphic);
2000 if(identifier==
"malloc" ||
2001 identifier==
"realloc" ||
2002 identifier==
"reallocf" ||
2003 identifier==
"valloc")
2010 new_symbol.
name=identifier;
2014 new_symbol.
type.
set(ID_C_incomplete,
true);
2022 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
2032 if(f_op_type.
id() == ID_mathematical_function)
2034 const auto &mathematical_function_type =
2038 if(expr.
arguments().size() != mathematical_function_type.domain().size())
2041 error() <<
"expected " << mathematical_function_type.domain().size()
2042 <<
" arguments but got " << expr.
arguments().size() <<
eom;
2050 if(p.first.type() != p.second)
2063 expr.
swap(function_application);
2067 if(f_op_type.
id()!=ID_pointer)
2070 error() <<
"expected function/function pointer as argument but got '"
2076 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2083 tmp.
set(ID_C_implicit,
true);
2088 if(f_op.
type().
id()!=ID_code)
2091 error() <<
"expected code as argument" <<
eom;
2114 if(f_op.
id()!=ID_symbol)
2124 error() <<
"same_object expects two operands" <<
eom;
2130 exprt same_object_expr=
2134 return same_object_expr;
2141 error() <<
"get_must expects two operands" <<
eom;
2151 return std::move(get_must_expr);
2158 error() <<
"get_may expects two operands" <<
eom;
2168 return std::move(get_may_expr);
2175 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2184 return same_object_expr;
2191 error() <<
"buffer_size expects one operand" <<
eom;
2201 return buffer_size_expr;
2208 error() <<
"is_zero_string expects one operand" <<
eom;
2216 is_zero_string_expr.
set(ID_C_lvalue,
true);
2219 return std::move(is_zero_string_expr);
2226 error() <<
"zero_string_length expects one operand" <<
eom;
2232 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2234 zero_string_length_expr.
set(ID_C_lvalue,
true);
2237 return zero_string_length_expr;
2244 error() <<
"dynamic_object expects one argument" <<
eom;
2253 return is_dynamic_object_expr;
2260 error() <<
"pointer_offset expects one argument" <<
eom;
2276 error() <<
"object_size expects one operand" <<
eom;
2286 return std::move(object_size_expr);
2293 error() <<
"pointer_object expects one argument" <<
eom;
2304 else if(identifier==
"__builtin_bswap16" ||
2305 identifier==
"__builtin_bswap32" ||
2306 identifier==
"__builtin_bswap64")
2311 error() << identifier <<
" expects one operand" <<
eom;
2321 return std::move(bswap_expr);
2324 identifier ==
"__builtin_rotateleft8" ||
2325 identifier ==
"__builtin_rotateleft16" ||
2326 identifier ==
"__builtin_rotateleft32" ||
2327 identifier ==
"__builtin_rotateleft64" ||
2328 identifier ==
"__builtin_rotateright8" ||
2329 identifier ==
"__builtin_rotateright16" ||
2330 identifier ==
"__builtin_rotateright32" ||
2331 identifier ==
"__builtin_rotateright64")
2337 error() << identifier <<
" expects two operands" <<
eom;
2343 irep_idt id = (identifier ==
"__builtin_rotateleft8" ||
2344 identifier ==
"__builtin_rotateleft16" ||
2345 identifier ==
"__builtin_rotateleft32" ||
2346 identifier ==
"__builtin_rotateleft64")
2353 return std::move(rotate_expr);
2355 else if(identifier==
"__builtin_nontemporal_load")
2360 error() << identifier <<
" expects one operand" <<
eom;
2369 if(ptr_arg.
type().
id()!=ID_pointer)
2372 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2381 identifier ==
"__builtin_fpclassify" ||
2387 error() << identifier <<
" expects six arguments" <<
eom;
2400 if(fp_value.
type().
id() != ID_floatbv)
2403 error() <<
"non-floating-point argument for " << identifier <<
eom;
2411 const auto &arguments = expr.
arguments();
2430 identifier==
"__builtin_isnan")
2435 error() <<
"isnan expects one operand" <<
eom;
2453 error() <<
"isfinite expects one operand" <<
eom;
2465 identifier==
"__builtin_inf")
2472 return std::move(inf_expr);
2481 return std::move(inff_expr);
2490 return std::move(infl_expr);
2502 error() <<
"abs-functions expect one operand" <<
eom;
2511 return std::move(abs_expr);
2518 error() <<
"allocate expects two operands" <<
eom;
2527 return std::move(malloc_expr);
2535 error() << identifier <<
" expects two operands" <<
eom;
2547 return std::move(ok_expr);
2552 identifier==
"__builtin_isinf")
2557 error() << identifier <<
" expects one operand" <<
eom;
2565 if(fp_value.
type().
id() != ID_floatbv)
2568 error() <<
"non-floating-point argument for " << identifier <<
eom;
2577 else if(identifier ==
"__builtin_isinf_sign")
2582 error() << identifier <<
" expects one operand" <<
eom;
2592 if(fp_value.
type().
id() != ID_floatbv)
2595 error() <<
"non-floating-point argument for " << identifier <<
eom;
2613 identifier ==
"__builtin_isnormal")
2618 error() << identifier <<
" expects one operand" <<
eom;
2626 if(fp_value.
type().
id() != ID_floatbv)
2629 error() <<
"non-floating-point argument for " << identifier <<
eom;
2641 identifier==
"__builtin_signbit" ||
2642 identifier==
"__builtin_signbitf" ||
2643 identifier==
"__builtin_signbitl")
2648 error() << identifier <<
" expects one operand" <<
eom;
2659 else if(identifier==
"__builtin_popcount" ||
2660 identifier==
"__builtin_popcountl" ||
2661 identifier==
"__builtin_popcountll" ||
2662 identifier==
"__popcnt16" ||
2663 identifier==
"__popcnt" ||
2664 identifier==
"__popcnt64")
2669 error() << identifier <<
" expects one operand" <<
eom;
2678 return std::move(popcount_expr);
2681 identifier ==
"__builtin_clz" || identifier ==
"__builtin_clzl" ||
2682 identifier ==
"__builtin_clzll" || identifier ==
"__lzcnt16" ||
2683 identifier ==
"__lzcnt" || identifier ==
"__lzcnt64")
2688 error() << identifier <<
" expects one operand" <<
eom;
2694 exprt argument = try_constant.arguments().front();
2696 const auto int_constant = numeric_cast<mp_integer>(argument);
2699 !int_constant.has_value() || *int_constant == 0 ||
2700 argument.
type().
id() != ID_unsignedbv)
2707 std::size_t n_leading_zeros = binary_value.find(
'1');
2719 error() <<
"equal expects two operands" <<
eom;
2732 error() <<
"equal expects two operands of same type" <<
eom;
2736 return std::move(equality_expr);
2738 else if(identifier==
"__builtin_expect")
2749 error() <<
"__builtin_expect expects two arguments" <<
eom;
2757 else if(identifier==
"__builtin_object_size")
2766 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2783 error() <<
"__builtin_object_size expects constant as second argument, "
2791 if(arg1==0 || arg1==1)
2804 else if(identifier==
"__builtin_choose_expr")
2810 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2825 else if(identifier==
"__builtin_constant_p")
2832 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2848 tmp1.
id() == ID_typecast &&
2854 .
id() == ID_string_constant)
2866 else if(identifier==
"__builtin_classify_type")
2873 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2886 if(type.
id() == ID_c_bit_field)
2889 unsigned type_number;
2891 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2902 type.
id() == ID_empty
2904 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
2906 : (type.
id() == ID_pointer || type.
id() == ID_array)
2908 : type.
id() == ID_floatbv
2910 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
2912 : type.
id() == ID_struct
2914 : type.
id() == ID_union
2936 overflow.
id(ID_minus);
2941 overflow.id(ID_mult);
2946 overflow.id(ID_plus);
2951 overflow.id(ID_shl);
2956 overflow.id(ID_unary_minus);
2960 overflow.id(
"overflow-" + overflow.id_string());
2969 std::ostringstream error_message;
2971 <<
" takes exactly 1 argument, but "
2972 << expr.
arguments().size() <<
" were provided";
2980 std::ostringstream error_message;
2982 <<
" expects enum, but (" <<
expr2c(arg1, *
this)
2983 <<
") has type `" <<
type2c(arg1.type(), *
this) <<
'`';
2992 identifier ==
"__builtin_add_overflow" ||
2993 identifier ==
"__builtin_sub_overflow" ||
2994 identifier ==
"__builtin_mul_overflow")
2999 std::ostringstream error_message;
3001 <<
" takes exactly 3 arguments, but "
3002 << expr.
arguments().size() <<
" were provided";
3015 auto const raise_wrong_argument_error =
3017 identifier](
const exprt &wrong_argument, std::size_t argument_number) {
3018 std::ostringstream error_message;
3020 << identifier <<
" has signature " << identifier
3021 <<
"(integral, integral, integral*), "
3022 <<
"but argument " << argument_number <<
" ("
3023 <<
expr2c(wrong_argument, *
this) <<
") has type `"
3024 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
3027 for(
auto const arg_index : {0, 1})
3029 auto const &argument = expr.
arguments()[arg_index];
3033 raise_wrong_argument_error(argument, arg_index + 1);
3037 result_ptr.type().id() != ID_pointer ||
3040 raise_wrong_argument_error(result_ptr, 3);
3045 auto const make_operation = [&identifier](
exprt lhs,
exprt rhs) ->
exprt {
3046 if(identifier ==
"__builtin_add_overflow")
3050 else if(identifier ==
"__builtin_sub_overflow")
3057 identifier ==
"__builtin_mul_overflow",
3058 "the three overflow operations are add, sub and mul");
3069 auto operation = make_operation(
3073 auto operation_result =
3080 return exprt{ID_comma,
3104 if(code_type.
get_bool(ID_C_incomplete))
3108 else if(code_type.
is_KnR())
3113 while(parameter_types.size()>arguments.size())
3118 if(parameter_types.size()>arguments.size())
3121 error() <<
"not enough function arguments" <<
eom;
3125 else if(parameter_types.size()!=arguments.size())
3128 error() <<
"wrong number of function arguments: "
3129 <<
"expected " << parameter_types.size()
3130 <<
", but got " << arguments.size() <<
eom;
3134 for(std::size_t i=0; i<arguments.size(); i++)
3136 exprt &op=arguments[i];
3142 else if(i<parameter_types.size())
3147 const typet &op_type=parameter_type.
type();
3149 if(op_type.
id()==ID_bool &&
3150 op.
id()==ID_side_effect &&
3151 op.
get(ID_statement)==ID_assign &&
3155 warning() <<
"assignment where Boolean argument is expected" <<
eom;
3164 if(op.
type().
id() == ID_array)
3167 dest_type.
subtype().
set(ID_C_constant,
true);
3185 if(o_type.
id()==ID_vector)
3204 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3228 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3229 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3238 if((type0.
subtype().
id()==ID_signedbv ||
3258 if(o_type0.
id()==ID_vector &&
3259 o_type1.
id()==ID_vector)
3273 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3278 expr.
type() = o_type0;
3282 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3287 expr.
type() = o_type1;
3298 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3299 expr.
id()==ID_mult || expr.
id()==ID_div)
3301 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3306 else if(type0==type1)
3315 else if(expr.
id()==ID_mod)
3319 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3327 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3328 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3337 else if(type0.
id()==ID_bool)
3339 if(expr.
id()==ID_bitand)
3341 else if(expr.
id() == ID_bitnand)
3343 else if(expr.
id()==ID_bitor)
3345 else if(expr.
id()==ID_bitxor)
3356 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3364 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3372 if(o_type0.
id()==ID_vector &&
3373 o_type1.
id()==ID_vector)
3404 if(expr.
id()==ID_shr)
3408 if(op0_type.
id()==ID_unsignedbv)
3413 else if(op0_type.
id()==ID_signedbv)
3424 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3433 assert(type.
id()==ID_pointer);
3438 subtype.
id() == ID_struct_tag &&
3442 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3446 subtype.
id() == ID_union_tag &&
3450 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3464 if(expr.
id()==ID_minus ||
3465 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3467 if(type0.
id()==ID_pointer &&
3468 type1.
id()==ID_pointer)
3478 if(type0.
id()==ID_pointer &&
3479 (type1.
id()==ID_bool ||
3480 type1.
id()==ID_c_bool ||
3481 type1.
id()==ID_unsignedbv ||
3482 type1.
id()==ID_signedbv ||
3483 type1.
id()==ID_c_bit_field ||
3484 type1.
id()==ID_c_enum_tag))
3492 else if(expr.
id()==ID_plus ||
3493 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3495 exprt *p_op, *int_op;
3497 if(type0.
id()==ID_pointer)
3502 else if(type1.
id()==ID_pointer)
3509 p_op=int_op=
nullptr;
3513 const typet &int_op_type = int_op->
type();
3515 if(int_op_type.
id()==ID_bool ||
3516 int_op_type.
id()==ID_c_bool ||
3517 int_op_type.
id()==ID_unsignedbv ||
3518 int_op_type.
id()==ID_signedbv ||
3519 int_op_type.
id()==ID_c_bit_field ||
3520 int_op_type.
id()==ID_c_enum_tag)
3531 if(expr.
id()==ID_side_effect)
3537 error() <<
"operator '" << op_name <<
"' not defined for types '"
3568 if(type0.
id()==ID_empty)
3571 error() <<
"cannot assign void" <<
eom;
3578 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3591 if(type0.
id() == ID_array)
3594 error() <<
"direct assignments to arrays not permitted" <<
eom;
3601 if(op0.
type().
id()==ID_c_bit_field)
3607 expr.
type()=o_type0;
3609 if(statement==ID_assign)
3614 else if(statement==ID_assign_shl ||
3615 statement==ID_assign_shr)
3617 if(o_type0.
id() == ID_vector)
3637 if(statement==ID_assign_shl)
3647 if(underlying_type.
id()==ID_unsignedbv ||
3648 underlying_type.
id()==ID_c_bool)
3650 expr.
set(ID_statement, ID_assign_lshr);
3653 else if(underlying_type.
id()==ID_signedbv)
3655 expr.
set(ID_statement, ID_assign_ashr);
3661 else if(statement==ID_assign_bitxor ||
3662 statement==ID_assign_bitand ||
3663 statement==ID_assign_bitor)
3666 if(o_type0.
id()==ID_bool ||
3667 o_type0.
id()==ID_c_bool)
3670 if(op1.
type().
id()==ID_bool ||
3671 op1.
type().
id()==ID_c_bool ||
3672 op1.
type().
id()==ID_c_enum_tag ||
3673 op1.
type().
id()==ID_unsignedbv ||
3674 op1.
type().
id()==ID_signedbv)
3677 else if(o_type0.
id()==ID_c_enum_tag ||
3678 o_type0.
id()==ID_unsignedbv ||
3679 o_type0.
id()==ID_signedbv ||
3680 o_type0.
id()==ID_c_bit_field)
3685 else if(o_type0.
id()==ID_vector &&
3686 o_type1.
id()==ID_vector)
3697 o_type0.
id() == ID_vector &&
3698 (o_type1.
id() == ID_bool || o_type1.
id() == ID_c_bool ||
3699 o_type1.
id() == ID_c_enum_tag || o_type1.
id() == ID_unsignedbv ||
3700 o_type1.
id() == ID_signedbv))
3709 if(o_type0.
id()==ID_pointer &&
3710 (statement==ID_assign_minus || statement==ID_assign_plus))
3715 else if(o_type0.
id()==ID_vector &&
3716 o_type1.
id()==ID_vector)
3726 else if(o_type0.
id() == ID_vector)
3732 op1.
type().
id() == ID_c_bool || op1.
type().
id() == ID_c_enum_tag)
3738 else if(o_type0.
id()==ID_bool ||
3739 o_type0.
id()==ID_c_bool)
3742 if(op1.
type().
id()==ID_bool ||
3743 op1.
type().
id()==ID_c_bool ||
3744 op1.
type().
id()==ID_c_enum_tag ||
3745 op1.
type().
id()==ID_unsignedbv ||
3746 op1.
type().
id()==ID_signedbv)
3754 op1.
type().
id()==ID_bool ||
3755 op1.
type().
id()==ID_c_bool ||
3756 op1.
type().
id()==ID_c_enum_tag)
3762 error() <<
"assignment '" << statement <<
"' not defined for types '"
3774 const auto rounding_mode =
3781 expr.
id()!=ID_infinity)
3784 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3797 expr.
id()!=ID_infinity)
3800 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
std::string as_string() const
bool is_incomplete() const
enum types may be incomplete
#define Forall_operands(it, expr)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
virtual void typecheck_expr_shifts(shift_exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_declt & to_code_decl(const codet &code)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
#define CHECK_RETURN(CONDITION)
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
std::vector< parametert > parameterst
ANSI-C Language Type Checking.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_declaration(ansi_c_declarationt &)
const 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.
Various predicates over pointers in programs.
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
Real part of the expression describing a complex number.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
A codet representing the declaration of a local variable.
Union constructor from single element.
Unbounded, signed integers (mathematical integers, not bitvectors)
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
The plus expression Associativity is not specified.
virtual void typecheck_expr_symbol(exprt &expr)
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
Base class for all expressions.
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
Generic base class for unary expressions.
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)
Thrown when we can't handle something in an input source file.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_type(typet &type)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
bool is_true() const
Return whether the expression is a constant representing true.
side_effect_exprt & to_side_effect_expr(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
struct configt::ansi_ct ansi_c
Expression to hold a symbol (variable)
bitvector_typet index_type()
virtual void typecheck_expr_binary_boolean(exprt &expr)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
An expression denoting infinity.
Evaluates to true if the operand is finite.
std::list< codet > clean_code
virtual void make_constant(exprt &expr)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
virtual void typecheck_expr_operands(exprt &expr)
const exprt & size() const
virtual void typecheck_expr_member(exprt &expr)
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()
bool has_prefix(const std::string &s, const std::string &prefix)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual void implicit_typecast_bool(exprt &expr)
const std::string & id2string(const irep_idt &d)
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)
virtual void typecheck_expr_dereference(exprt &expr)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
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.
API to expression classes for Pointers.
bool simplify(exprt &expr, const namespacet &ns)
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
A side_effect_exprt that performs an assignment.
std::vector< typet > domaint
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()
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)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
API to expression classes for floating-point arithmetic.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() const
const constant_exprt & size() const
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
id_type_mapt parameter_map
exprt pointer_offset(const exprt &pointer)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
std::map< irep_idt, source_locationt > labels_used
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const irep_idt & get_statement() const
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr(exprt &expr)
std::size_t get_width() const
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Deprecated expression utility functions.
A base class for shift and rotate operators.
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_main(exprt &expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is infinite.
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
exprt::operandst & arguments()
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Imaginary part of the expression describing a complex number.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
exprt same_object(const exprt &p1, const exprt &p2)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
virtual void typecheck_expr_constant(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
static ieee_floatt zero(const floatbv_typet &type)
const typet & return_type() const
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const code_blockt & to_code_block(const codet &code)
The byte swap expression.
C Language Type Checking.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
constant_exprt to_expr() const
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
codet & find_last_statement()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
const std::string integer2binary(const mp_integer &n, std::size_t width)
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
signedbv_typet pointer_diff_type()
unsignedbv_typet size_type()
const irep_idt & get_statement() const
A constant literal expression.
IEEE-floating-point equality.
mstreamt & warning() const
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
virtual void typecheck_expr_sizeof(exprt &expr)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
static ieee_float_spect single_precision()
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
ranget< iteratort > make_range(iteratort begin, iteratort end)
A type for mathematical functions (do not confuse with functions/methods in code)
Evaluates to true if the operand is a normal number.
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
An expression containing a side effect.
virtual void typecheck_expr_index(exprt &expr)
virtual void make_index_type(exprt &expr)
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.
API to expression classes for 'mathematical' expressions.
ANSI-C Language Type Checking.
Data structure for representing an arbitrary statement in a program.
virtual void typecheck_expr_comma(exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.