Go to the documentation of this file.
43 if(expr.
id()==ID_already_typechecked)
61 if(expr.
id()==ID_div ||
66 if(expr.
type().
id()==ID_floatbv &&
75 expr.
id(ID_floatbv_div);
76 else if(expr.
id()==ID_mult)
77 expr.
id(ID_floatbv_mult);
78 else if(expr.
id()==ID_plus)
79 expr.
id(ID_floatbv_plus);
80 else if(expr.
id()==ID_minus)
81 expr.
id(ID_floatbv_minus);
102 if(type1.
id()==ID_c_enum_tag)
104 else if(type2.
id()==ID_c_enum_tag)
107 if(type1.
id()==ID_c_enum)
109 if(type2.
id()==ID_c_enum)
111 else if(type2==type1.
subtype())
114 else if(type2.
id()==ID_c_enum)
119 else if(type1.
id()==ID_pointer &&
120 type2.
id()==ID_pointer)
124 else if(type1.
id()==ID_array &&
125 type2.
id()==ID_array)
130 else if(type1.
id()==ID_code &&
144 for(std::size_t i=0; i<c_type1.
parameters().size(); i++)
160 if(type1.
get(ID_C_c_type)==type2.
get(ID_C_c_type))
170 if(expr.
id()==ID_side_effect)
172 else if(expr.
id()==ID_constant)
174 else if(expr.
id()==ID_infinity)
178 else if(expr.
id()==ID_symbol)
180 else if(expr.
id()==ID_unary_plus ||
181 expr.
id()==ID_unary_minus ||
182 expr.
id()==ID_bitnot)
184 else if(expr.
id()==ID_not)
187 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies ||
190 else if(expr.
id()==ID_address_of)
192 else if(expr.
id()==ID_dereference)
194 else if(expr.
id()==ID_member)
196 else if(expr.
id()==ID_ptrmember)
198 else if(expr.
id()==ID_equal ||
199 expr.
id()==ID_notequal ||
205 else if(expr.
id()==ID_index)
207 else if(expr.
id()==ID_typecast)
209 else if(expr.
id()==ID_sizeof)
211 else if(expr.
id()==ID_alignof)
214 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
215 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitand ||
216 expr.
id() == ID_bitxor || expr.
id() == ID_bitor || expr.
id() == ID_bitnand)
220 else if(expr.
id()==ID_shl || expr.
id()==ID_shr)
222 else if(expr.
id()==ID_comma)
224 else if(expr.
id()==ID_if)
226 else if(expr.
id()==ID_code)
229 error() <<
"typecheck_expr_main got code: " << expr.
pretty() <<
eom;
232 else if(expr.
id()==ID_gcc_builtin_va_arg)
234 else if(expr.
id()==ID_cw_va_arg_typeof)
236 else if(expr.
id()==ID_gcc_builtin_types_compatible_p)
241 assert(subtypes.size()==2);
247 subtypes[0].
remove(ID_C_constant);
248 subtypes[0].remove(ID_C_volatile);
249 subtypes[0].remove(ID_C_restricted);
250 subtypes[1].remove(ID_C_constant);
251 subtypes[1].remove(ID_C_volatile);
252 subtypes[1].remove(ID_C_restricted);
257 else if(expr.
id()==ID_clang_builtin_convertvector)
266 else if(expr.
id()==ID_builtin_offsetof)
268 else if(expr.
id()==ID_string_constant)
271 expr.
set(ID_C_lvalue,
true);
273 else if(expr.
id()==ID_arguments)
277 else if(expr.
id()==ID_designated_initializer)
279 exprt &designator=
static_cast<exprt &
>(expr.
add(ID_designator));
283 if(it->id()==ID_index)
287 else if(expr.
id()==ID_initializer_list)
292 else if(expr.
id()==ID_forall ||
293 expr.
id()==ID_exists)
299 auto &bindings = binary_expr.op0().operands();
300 auto &where = binary_expr.op1();
302 for(
const auto &binding : bindings)
304 if(binding.get(ID_statement) != ID_decl)
307 error() <<
"expected declaration as operand of quantifier" <<
eom;
315 error() <<
"quantifier must not contain side effects" <<
eom;
322 for(
auto &binding : bindings)
327 else if(expr.
id()==ID_label)
331 else if(expr.
id()==ID_array)
335 else if(expr.
id()==ID_complex)
340 else if(expr.
id() == ID_complex_real)
344 if(op.
type().
id() != ID_complex)
349 error() <<
"real part retrieval expects numerical operand, "
357 expr.
swap(complex_real_expr);
365 complex_real_expr.
set(ID_C_lvalue,
true);
368 complex_real_expr.
type().
set(ID_C_constant,
true);
370 expr.
swap(complex_real_expr);
373 else if(expr.
id() == ID_complex_imag)
377 if(op.
type().
id() != ID_complex)
382 error() <<
"real part retrieval expects numerical operand, "
390 expr.
swap(complex_imag_expr);
398 complex_imag_expr.
set(ID_C_lvalue,
true);
401 complex_imag_expr.
type().
set(ID_C_constant,
true);
403 expr.
swap(complex_imag_expr);
406 else if(expr.
id()==ID_generic_selection)
416 if(op.type().id() == ID_bool)
424 if(it->get(ID_type_arg)!=ID_default)
426 typet &type=
static_cast<typet &
>(it->add(ID_type_arg));
438 if(it->get(ID_type_arg)==ID_default)
439 default_match=
static_cast<const exprt &
>(it->find(ID_value));
441 follow(
static_cast<const typet &
>(it->find(ID_type_arg))))
442 assoc_match=
static_cast<const exprt &
>(it->find(ID_value));
448 expr.
swap(default_match);
452 error() <<
"unmatched generic selection: " <<
to_string(op.type())
458 expr.
swap(assoc_match);
463 else if(expr.
id()==ID_gcc_asm_input ||
464 expr.
id()==ID_gcc_asm_output ||
465 expr.
id()==ID_gcc_asm_clobbered_register)
468 else if(expr.
id()==ID_lshr || expr.
id()==ID_ashr ||
469 expr.
id()==ID_assign_lshr || expr.
id()==ID_assign_ashr)
473 else if(expr.
id() == ID_C_spec_assigns || expr.
id() == ID_target_list)
491 expr.
set(ID_C_lvalue,
true);
528 symbol.
name=ID_gcc_builtin_va_arg;
529 symbol.
type=symbol_type;
559 error() <<
"builtin_offsetof expects no operands" <<
eom;
574 if(m_it->id()==ID_member)
576 if(type.
id()!=ID_union && type.
id()!=ID_struct)
579 error() <<
"offsetof of member expects struct/union type, "
585 irep_idt component_name=m_it->get(ID_component_name);
589 assert(type.
id()==ID_union || type.
id()==ID_struct);
599 if(type.
id()==ID_struct)
604 if(!o_opt.has_value())
607 error() <<
"offsetof failed to determine offset of '"
608 << component_name <<
"'" <<
eom;
624 for(
const auto &c : struct_union_type.
components())
628 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
632 if(type.
id()==ID_struct)
637 if(!o_opt.has_value())
640 error() <<
"offsetof failed to determine offset of '"
641 << component_name <<
"'" <<
eom;
653 assert(type.
id()==ID_union || type.
id()==ID_struct);
663 error() <<
"offset-of of member failed to find component '"
664 << component_name <<
"' in '" <<
to_string(type) <<
"'"
671 else if(m_it->id()==ID_index)
673 if(type.
id()!=ID_array)
676 error() <<
"offsetof of index expects array type" <<
eom;
687 if(!sub_size_opt.has_value())
690 error() <<
"offsetof failed to determine array element size" <<
eom;
713 if(expr.
id()==ID_side_effect &&
714 expr.
get(ID_statement)==ID_function_call)
719 else if(expr.
id()==ID_side_effect &&
720 expr.
get(ID_statement)==ID_statement_expression)
724 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
730 auto &bindings = binary_expr.op0().operands();
732 for(
auto &binding : bindings)
741 error() <<
"forall/exists expects one declarator exactly" <<
eom;
748 symbol_tablet::symbolst::const_iterator s_it =
754 error() <<
"failed to find bound symbol `" << identifier
755 <<
"' in symbol table" <<
eom;
759 const symbolt &symbol = s_it->second;
766 error() <<
"unexpected quantified symbol" <<
eom;
790 id_type_mapt::const_iterator p_it=
parameter_map.find(identifier);
794 expr.
type()=p_it->second;
795 expr.
set(ID_C_lvalue,
true);
800 asm_label_mapt::const_iterator entry=
804 identifier=entry->second;
810 if(
lookup(identifier, symbol_ptr))
813 error() <<
"failed to find symbol '" << identifier <<
"'" <<
eom;
817 const symbolt &symbol=*symbol_ptr;
822 error() <<
"did not expect a type symbol here, but got '"
840 if(expr.
id()==ID_constant &&
842 expr.
set(ID_C_cformat, base_name);
857 else if(identifier==
"__func__" ||
858 identifier==
"__FUNCTION__" ||
859 identifier==
"__PRETTY_FUNCTION__")
865 s.
set(ID_C_lvalue,
true);
876 expr.
set(ID_C_lvalue,
true);
878 if(expr.
type().
id()==ID_code)
881 tmp.
set(ID_C_implicit,
true);
900 if(last_statement==ID_expression)
906 if(op.
type().
id()==ID_array)
940 if(type.
id()==ID_c_bit_field)
943 error() <<
"sizeof cannot be applied to bit fields" <<
eom;
946 else if(type.
id() == ID_bool)
949 error() <<
"sizeof cannot be applied to single bits" <<
eom;
952 else if(type.
id() == ID_empty)
961 (type.
id() == ID_struct_tag &&
963 (type.
id() == ID_union_tag &&
965 (type.
id() == ID_c_enum_tag &&
970 error() <<
"invalid application of \'sizeof\' to an incomplete type\n\t\'"
977 if(!size_of_opt.has_value())
984 new_expr = size_of_opt.value();
989 expr.
add(ID_C_c_sizeof_type)=type;
997 decl_block.set_statement(ID_decl_block);
1007 exprt comma_expr(ID_comma, expr.
type());
1009 expr.
swap(comma_expr);
1015 typet argument_type;
1023 argument_type=op_type;
1047 decl_block.set_statement(ID_decl_block);
1059 op.
swap(comma_expr);
1065 expr_type.
id() == ID_union_tag && expr_type != op.
type() &&
1066 op.
id() != ID_initializer_list)
1074 if(op.
type().
id() == ID_bool)
1079 for(
const auto &c : union_type.components())
1081 if(c.type() == op.
type())
1087 expr.
set(ID_C_lvalue,
true);
1095 <<
"' not found in union" <<
eom;
1102 if(op.
id()==ID_initializer_list)
1111 exprt tmp(ID_compound_literal, expr.
type());
1115 if(op.
id()==ID_array &&
1116 expr.
type().
id()==ID_array &&
1121 expr.
set(ID_C_lvalue,
true);
1126 if(expr_type.
id()==ID_empty)
1132 if(expr_type == op_type)
1137 if(expr_type.
id()==ID_vector)
1140 if(op_type.
id()==ID_vector)
1142 else if(op_type.
id()==ID_signedbv ||
1143 op_type.
id()==ID_unsignedbv)
1150 error() <<
"type cast to '" <<
to_string(expr_type) <<
"' is not permitted"
1158 else if(op_type.
id()==ID_array)
1163 else if(op_type.
id()==ID_empty)
1165 if(expr_type.
id()!=ID_empty)
1168 error() <<
"type cast from void only permitted to void, but got '"
1173 else if(op_type.
id()==ID_vector)
1180 if((expr_type.
id()==ID_signedbv ||
1181 expr_type.
id()==ID_unsignedbv) &&
1190 <<
"' not permitted" <<
eom;
1197 error() <<
"type cast from '" <<
to_string(op_type) <<
"' not permitted"
1213 if(expr_type.
id()==ID_pointer)
1214 expr.
set(ID_C_lvalue,
true);
1231 const typet &array_type = array_expr.
type();
1235 array_type.
id() != ID_array && array_type.
id() != ID_pointer &&
1236 array_type.
id() != ID_vector &&
1239 std::swap(array_expr, index_expr);
1247 const typet final_array_type = array_expr.
type();
1249 if(final_array_type.
id()==ID_array ||
1250 final_array_type.
id()==ID_vector)
1254 if(array_expr.
get_bool(ID_C_lvalue))
1255 expr.
set(ID_C_lvalue,
true);
1257 if(final_array_type.
get_bool(ID_C_constant))
1258 expr.
type().
set(ID_C_constant,
true);
1260 else if(final_array_type.
id()==ID_pointer)
1266 std::swap(summands, expr.
operands());
1268 expr.
id(ID_dereference);
1269 expr.
set(ID_C_lvalue,
true);
1275 error() <<
"operator [] must take array/vector or pointer but got '"
1284 if(expr.
op0().
type().
id() == ID_floatbv)
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(o_type0.
id() == ID_vector || o_type1.
id() == ID_vector)
1310 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1314 if(o_type0.
id() != ID_array)
1335 if(type0.
id()==ID_pointer)
1337 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1340 if(expr.
id()==ID_le || expr.
id()==ID_lt ||
1341 expr.
id()==ID_ge || expr.
id()==ID_gt)
1345 if(type0.
id()==ID_string_constant)
1347 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1354 if(type0.
id()==ID_pointer &&
1361 if(type1.
id()==ID_pointer &&
1381 if(type0.
id()==ID_pointer && type1.
id()==ID_pointer)
1389 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
1405 o_type0.
id() != ID_vector || o_type1.
id() != ID_vector ||
1409 error() <<
"vector operator '" << expr.
id() <<
"' not defined for types '"
1423 const typet &op0_type = op.type();
1425 if(op0_type.
id() == ID_array)
1430 index_expr.
set(ID_C_lvalue,
true);
1431 op.swap(index_expr);
1433 else if(op0_type.
id() == ID_pointer)
1439 op.swap(deref_expr);
1444 error() <<
"ptrmember operator requires pointer or array type "
1445 "on left hand side, but got '"
1461 if(type.
id()!=ID_struct &&
1462 type.
id()!=ID_union)
1465 error() <<
"member operator requires structure type "
1466 "on left hand side but got '"
1477 error() <<
"member operator got incomplete " << type.
id()
1478 <<
" type on left hand side" <<
eom;
1483 expr.
get(ID_component_name);
1499 error() <<
"member '" << component_name <<
"' not found in '"
1512 expr.
set(ID_C_lvalue,
true);
1515 expr.
type().
set(ID_C_constant,
true);
1520 if(!identifier.
empty())
1521 expr.
set(ID_C_identifier, identifier);
1525 if(access==ID_private)
1528 error() <<
"member '" << component_name <<
"' is " << access <<
eom;
1537 assert(operands.size()==3);
1540 const typet o_type0=operands[0].type();
1541 const typet o_type1=operands[1].type();
1542 const typet o_type2=operands[2].type();
1547 if(operands[1].type().
id()==ID_pointer &&
1548 operands[2].type().
id()!=ID_pointer)
1550 else if(operands[2].type().
id()==ID_pointer &&
1551 operands[1].type().
id()!=ID_pointer)
1554 if(operands[1].type().
id()==ID_pointer &&
1555 operands[2].type().
id()==ID_pointer &&
1556 operands[1].type()!=operands[2].type())
1563 if(operands[1].type().subtype().
id()==ID_empty &&
1567 else if(operands[2].type().subtype().
id()==ID_empty &&
1571 else if(operands[1].type().subtype().
id()!=ID_code ||
1572 operands[2].type().subtype().
id()!=ID_code)
1596 if(operands[1].type().
id()==ID_empty ||
1597 operands[2].type().
id()==ID_empty)
1603 if(operands[1].type() == operands[2].type())
1605 expr.
type()=operands[1].type();
1611 if(operands[1].get_bool(ID_C_lvalue) &&
1612 operands[2].get_bool(ID_C_lvalue))
1613 expr.
set(ID_C_lvalue,
true);
1619 error() <<
"operator ?: not defined for types '" <<
to_string(o_type1)
1632 if(operands.size()!=2)
1635 error() <<
"gcc conditional_expr expects two operands" <<
eom;
1641 if_exprt if_expr(operands[0], operands[0], operands[1]);
1656 if(op.
type().
id()==ID_c_bit_field)
1659 error() <<
"cannot take address of a bit field" <<
eom;
1663 if(op.
type().
id() == ID_bool)
1666 error() <<
"cannot take address of a single bit" <<
eom;
1671 if(op.
id()==ID_label)
1684 op.
id() == ID_address_of && op.
get_bool(ID_C_implicit) &&
1690 tmp.
set(ID_C_implicit,
false);
1695 if(op.
id()==ID_struct ||
1696 op.
id()==ID_union ||
1697 op.
id()==ID_array ||
1698 op.
id()==ID_string_constant)
1706 else if(op.
type().
id()==ID_code)
1713 error() <<
"address_of error: '" <<
to_string(op) <<
"' not an lvalue"
1727 if(op_type.
id()==ID_array)
1735 else if(op_type.
id()==ID_pointer)
1743 <<
"' is not a pointer, but got '" <<
to_string(op_type) <<
"'"
1748 expr.
set(ID_C_lvalue,
true);
1759 if(expr.
type().
id()==ID_code)
1762 tmp.
set(ID_C_implicit,
true);
1772 if(statement==ID_preincrement ||
1773 statement==ID_predecrement ||
1774 statement==ID_postincrement ||
1775 statement==ID_postdecrement)
1784 <<
"' not an lvalue" <<
eom;
1795 if(type0.
id() == ID_c_enum_tag)
1801 error() <<
"operator '" << statement <<
"' given incomplete type '"
1810 else if(type0.
id() == ID_c_bit_field)
1815 expr.
type()=underlying_type;
1817 else if(type0.
id() == ID_bool || type0.
id() == ID_c_bool)
1826 else if(type0.
id() == ID_pointer)
1834 error() <<
"operator '" << statement <<
"' not defined for type '"
1841 else if(statement==ID_function_call)
1844 else if(statement==ID_statement_expression)
1846 else if(statement==ID_gcc_conditional_expression)
1851 error() <<
"unknown side effect: " << statement <<
eom;
1862 error() <<
"function_call side effect expects two operands" <<
eom;
1871 if(f_op.
id()==ID_symbol)
1875 asm_label_mapt::const_iterator entry=
1878 identifier=entry->second;
1892 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1895 !parameters.empty(),
1896 "GCC polymorphic built-ins should have at least one parameter");
1898 if(parameters.front().type().id() == ID_pointer)
1900 identifier_with_type =
id2string(identifier) +
"_" +
1902 parameters.front().type().subtype(), *
this);
1906 identifier_with_type =
1910 gcc_polymorphic->set_identifier(identifier_with_type);
1914 for(std::size_t i = 0; i < parameters.size(); ++i)
1921 id2string(identifier_with_type) +
"::" + base_name;
1924 new_symbol.
type = parameters[i].type();
1927 new_symbol.
mode = ID_C;
1929 parameters[i].set_identifier(new_symbol.
name);
1930 parameters[i].set_base_name(new_symbol.
base_name);
1937 new_symbol.
name = identifier_with_type;
1938 new_symbol.
base_name = identifier_with_type;
1940 new_symbol.
type = gcc_polymorphic->type();
1941 new_symbol.
mode = ID_C;
1948 new_symbol.
value = implementation;
1953 f_op = std::move(*gcc_polymorphic);
1965 if(identifier==
"malloc" ||
1966 identifier==
"realloc" ||
1967 identifier==
"reallocf" ||
1968 identifier==
"valloc")
1975 new_symbol.
name=identifier;
1979 new_symbol.
type.
set(ID_C_incomplete,
true);
1987 warning() <<
"function '" << identifier <<
"' is not declared" <<
eom;
1997 if(f_op_type.
id()!=ID_pointer)
2000 error() <<
"expected function/function pointer as argument but got '"
2006 if(f_op.
id() == ID_address_of && f_op.
get_bool(ID_C_implicit))
2013 tmp.
set(ID_C_implicit,
true);
2018 if(f_op.
type().
id()!=ID_code)
2021 error() <<
"expected code as argument" <<
eom;
2044 if(f_op.
id()!=ID_symbol)
2054 error() <<
"same_object expects two operands" <<
eom;
2060 exprt same_object_expr=
2064 return same_object_expr;
2071 error() <<
"get_must expects two operands" <<
eom;
2081 return std::move(get_must_expr);
2088 error() <<
"get_may expects two operands" <<
eom;
2098 return std::move(get_may_expr);
2105 error() <<
"is_invalid_pointer expects one operand" <<
eom;
2114 return same_object_expr;
2121 error() <<
"buffer_size expects one operand" <<
eom;
2131 return buffer_size_expr;
2138 error() <<
"is_zero_string expects one operand" <<
eom;
2146 is_zero_string_expr.
set(ID_C_lvalue,
true);
2149 return std::move(is_zero_string_expr);
2156 error() <<
"zero_string_length expects one operand" <<
eom;
2162 exprt zero_string_length_expr(
"zero_string_length",
size_type());
2164 zero_string_length_expr.
set(ID_C_lvalue,
true);
2167 return zero_string_length_expr;
2174 error() <<
"dynamic_object expects one argument" <<
eom;
2183 return is_dynamic_object_expr;
2190 error() <<
"pointer_offset expects one argument" <<
eom;
2206 error() <<
"object_size expects one operand" <<
eom;
2216 return std::move(object_size_expr);
2223 error() <<
"pointer_object expects one argument" <<
eom;
2234 else if(identifier==
"__builtin_bswap16" ||
2235 identifier==
"__builtin_bswap32" ||
2236 identifier==
"__builtin_bswap64")
2241 error() << identifier <<
" expects one operand" <<
eom;
2251 return std::move(bswap_expr);
2253 else if(identifier==
"__builtin_nontemporal_load")
2258 error() << identifier <<
" expects one operand" <<
eom;
2267 if(ptr_arg.
type().
id()!=ID_pointer)
2270 error() <<
"__builtin_nontemporal_load takes pointer as argument" <<
eom;
2279 identifier ==
"__builtin_fpclassify" ||
2285 error() << identifier <<
" expects six arguments" <<
eom;
2298 if(fp_value.
type().
id() != ID_floatbv)
2301 error() <<
"non-floating-point argument for " << identifier <<
eom;
2309 const auto &arguments = expr.
arguments();
2328 identifier==
"__builtin_isnan")
2333 error() <<
"isnan expects one operand" <<
eom;
2351 error() <<
"isfinite expects one operand" <<
eom;
2363 identifier==
"__builtin_inf")
2370 return std::move(inf_expr);
2379 return std::move(inff_expr);
2388 return std::move(infl_expr);
2400 error() <<
"abs-functions expect one operand" <<
eom;
2409 return std::move(abs_expr);
2416 error() <<
"allocate expects two operands" <<
eom;
2425 return std::move(malloc_expr);
2433 error() << identifier <<
" expects two operands" <<
eom;
2445 return std::move(ok_expr);
2450 identifier==
"__builtin_isinf")
2455 error() << identifier <<
" expects one operand" <<
eom;
2466 else if(identifier ==
"__builtin_isinf_sign")
2471 error() << identifier <<
" expects one operand" <<
eom;
2495 identifier ==
"__builtin_isnormal")
2500 error() << identifier <<
" expects one operand" <<
eom;
2508 if(fp_value.
type().
id() != ID_floatbv)
2511 error() <<
"non-floating-point argument for " << identifier <<
eom;
2523 identifier==
"__builtin_signbit" ||
2524 identifier==
"__builtin_signbitf" ||
2525 identifier==
"__builtin_signbitl")
2530 error() << identifier <<
" expects one operand" <<
eom;
2541 else if(identifier==
"__builtin_popcount" ||
2542 identifier==
"__builtin_popcountl" ||
2543 identifier==
"__builtin_popcountll" ||
2544 identifier==
"__popcnt16" ||
2545 identifier==
"__popcnt" ||
2546 identifier==
"__popcnt64")
2551 error() << identifier <<
" expects one operand" <<
eom;
2560 return std::move(popcount_expr);
2567 error() <<
"equal expects two operands" <<
eom;
2580 error() <<
"equal expects two operands of same type" <<
eom;
2584 return std::move(equality_expr);
2586 else if(identifier==
"__builtin_expect")
2597 error() <<
"__builtin_expect expects two arguments" <<
eom;
2605 else if(identifier==
"__builtin_object_size")
2614 error() <<
"__builtin_object_size expects two arguments" <<
eom;
2631 error() <<
"__builtin_object_size expects constant as second argument, "
2639 if(arg1==0 || arg1==1)
2652 else if(identifier==
"__builtin_choose_expr")
2658 error() <<
"__builtin_choose_expr expects three arguments" <<
eom;
2673 else if(identifier==
"__builtin_constant_p")
2680 error() <<
"__builtin_constant_p expects one argument" <<
eom;
2696 tmp1.
id() == ID_typecast &&
2702 .
id() == ID_string_constant)
2714 else if(identifier==
"__builtin_classify_type")
2721 error() <<
"__builtin_classify_type expects one argument" <<
eom;
2734 if(type.
id() == ID_c_bit_field)
2737 unsigned type_number;
2739 if(type.
id() == ID_bool || type.
id() == ID_c_bool)
2750 type.
id() == ID_empty
2752 : (type.
id() == ID_bool || type.
id() == ID_c_bool)
2754 : (type.
id() == ID_pointer || type.
id() == ID_array)
2756 : type.
id() == ID_floatbv
2758 : (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv)
2760 : type.
id() == ID_struct
2762 : type.
id() == ID_union
2784 overflow.
id(ID_minus);
2789 overflow.id(ID_mult);
2794 overflow.id(ID_plus);
2799 overflow.id(ID_shl);
2804 overflow.id(ID_unary_minus);
2808 overflow.id(
"overflow-" + overflow.id_string());
2813 identifier ==
"__builtin_add_overflow" ||
2814 identifier ==
"__builtin_sub_overflow" ||
2815 identifier ==
"__builtin_mul_overflow")
2820 std::ostringstream error_message;
2822 <<
" takes exactly 3 arguments, but "
2823 << expr.
arguments().size() <<
" were provided";
2836 auto const raise_wrong_argument_error =
2838 identifier](
const exprt &wrong_argument, std::size_t argument_number) {
2839 std::ostringstream error_message;
2841 << identifier <<
" has signature " << identifier
2842 <<
"(integral, integral, integral*), "
2843 <<
"but argument " << argument_number <<
" ("
2844 <<
expr2c(wrong_argument, *
this) <<
") has type `"
2845 <<
type2c(wrong_argument.
type(), *
this) <<
'`';
2848 for(
auto const arg_index : {0, 1})
2850 auto const &argument = expr.
arguments()[arg_index];
2854 raise_wrong_argument_error(argument, arg_index + 1);
2858 result_ptr.type().id() != ID_pointer ||
2861 raise_wrong_argument_error(result_ptr, 3);
2866 auto const make_operation = [&identifier](
exprt lhs,
exprt rhs) ->
exprt {
2867 if(identifier ==
"__builtin_add_overflow")
2871 else if(identifier ==
"__builtin_sub_overflow")
2878 identifier ==
"__builtin_mul_overflow",
2879 "the three overflow operations are add, sub and mul");
2890 auto operation = make_operation(
2894 auto operation_result =
2901 return exprt{ID_comma,
2925 if(code_type.
get_bool(ID_C_incomplete))
2929 else if(code_type.
is_KnR())
2934 while(parameter_types.size()>arguments.size())
2939 if(parameter_types.size()>arguments.size())
2942 error() <<
"not enough function arguments" <<
eom;
2946 else if(parameter_types.size()!=arguments.size())
2949 error() <<
"wrong number of function arguments: "
2950 <<
"expected " << parameter_types.size()
2951 <<
", but got " << arguments.size() <<
eom;
2955 for(std::size_t i=0; i<arguments.size(); i++)
2957 exprt &op=arguments[i];
2963 else if(i<parameter_types.size())
2968 const typet &op_type=parameter_type.
type();
2970 if(op_type.
id()==ID_bool &&
2971 op.
id()==ID_side_effect &&
2972 op.
get(ID_statement)==ID_assign &&
2976 warning() <<
"assignment where Boolean argument is expected" <<
eom;
2985 if(op.
type().
id() == ID_array)
2988 dest_type.
subtype().
set(ID_C_constant,
true);
3006 if(o_type.
id()==ID_vector)
3025 error() <<
"operator '" << expr.
id() <<
"' not defined for type '"
3049 const auto s0 = numeric_cast<mp_integer>(type0.
size());
3050 const auto s1 = numeric_cast<mp_integer>(type1.
size());
3059 if((type0.
subtype().
id()==ID_signedbv ||
3079 if(o_type0.
id()==ID_vector &&
3080 o_type1.
id()==ID_vector)
3094 o_type0.
id() == ID_vector && o_type1.
id() != ID_vector &&
3099 expr.
type() = o_type0;
3103 o_type0.
id() != ID_vector && o_type1.
id() == ID_vector &&
3108 expr.
type() = o_type1;
3119 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
3120 expr.
id()==ID_mult || expr.
id()==ID_div)
3122 if(type0.
id()==ID_pointer || type1.
id()==ID_pointer)
3127 else if(type0==type1)
3136 else if(expr.
id()==ID_mod)
3140 if(type0.
id()==ID_signedbv || type0.
id()==ID_unsignedbv)
3148 expr.
id() == ID_bitand || expr.
id() == ID_bitnand ||
3149 expr.
id() == ID_bitxor || expr.
id() == ID_bitor)
3158 else if(type0.
id()==ID_bool)
3160 if(expr.
id()==ID_bitand)
3162 else if(expr.
id() == ID_bitnand)
3164 else if(expr.
id()==ID_bitor)
3166 else if(expr.
id()==ID_bitxor)
3177 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3185 assert(expr.
id()==ID_shl || expr.
id()==ID_shr);
3193 if(o_type0.
id()==ID_vector &&
3194 o_type1.
id()==ID_vector)
3224 if(expr.
id()==ID_shr)
3228 if(op0_type.
id()==ID_unsignedbv)
3233 else if(op0_type.
id()==ID_signedbv)
3244 error() <<
"operator '" << expr.
id() <<
"' not defined for types '"
3253 assert(type.
id()==ID_pointer);
3258 subtype.
id() == ID_struct_tag &&
3262 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3266 subtype.
id() == ID_union_tag &&
3270 error() <<
"pointer arithmetic with unknown object size" <<
eom;
3284 if(expr.
id()==ID_minus ||
3285 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_minus))
3287 if(type0.
id()==ID_pointer &&
3288 type1.
id()==ID_pointer)
3298 if(type0.
id()==ID_pointer &&
3299 (type1.
id()==ID_bool ||
3300 type1.
id()==ID_c_bool ||
3301 type1.
id()==ID_unsignedbv ||
3302 type1.
id()==ID_signedbv ||
3303 type1.
id()==ID_c_bit_field ||
3304 type1.
id()==ID_c_enum_tag))
3312 else if(expr.
id()==ID_plus ||
3313 (expr.
id()==ID_side_effect && expr.
get(ID_statement)==ID_assign_plus))
3315 exprt *p_op, *int_op;
3317 if(type0.
id()==ID_pointer)
3322 else if(type1.
id()==ID_pointer)
3329 p_op=int_op=
nullptr;
3333 const typet &int_op_type = int_op->
type();
3335 if(int_op_type.
id()==ID_bool ||
3336 int_op_type.
id()==ID_c_bool ||
3337 int_op_type.
id()==ID_unsignedbv ||
3338 int_op_type.
id()==ID_signedbv ||
3339 int_op_type.
id()==ID_c_bit_field ||
3340 int_op_type.
id()==ID_c_enum_tag)
3351 if(expr.
id()==ID_side_effect)
3357 error() <<
"operator '" << op_name <<
"' not defined for types '"
3388 if(type0.
id()==ID_empty)
3391 error() <<
"cannot assign void" <<
eom;
3398 error() <<
"assignment error: '" <<
to_string(op0) <<
"' not an lvalue"
3411 if(type0.
id() == ID_array)
3414 error() <<
"direct assignments to arrays not permitted" <<
eom;
3421 if(op0.
type().
id()==ID_c_bit_field)
3427 expr.
type()=o_type0;
3429 if(statement==ID_assign)
3434 else if(statement==ID_assign_shl ||
3435 statement==ID_assign_shr)
3442 if(statement==ID_assign_shl)
3452 if(underlying_type.
id()==ID_unsignedbv ||
3453 underlying_type.
id()==ID_c_bool)
3455 expr.
set(ID_statement, ID_assign_lshr);
3458 else if(underlying_type.
id()==ID_signedbv)
3460 expr.
set(ID_statement, ID_assign_ashr);
3466 else if(statement==ID_assign_bitxor ||
3467 statement==ID_assign_bitand ||
3468 statement==ID_assign_bitor)
3471 if(o_type0.
id()==ID_bool ||
3472 o_type0.
id()==ID_c_bool)
3475 if(op1.
type().
id()==ID_bool ||
3476 op1.
type().
id()==ID_c_bool ||
3477 op1.
type().
id()==ID_c_enum_tag ||
3478 op1.
type().
id()==ID_unsignedbv ||
3479 op1.
type().
id()==ID_signedbv)
3482 else if(o_type0.
id()==ID_c_enum_tag ||
3483 o_type0.
id()==ID_unsignedbv ||
3484 o_type0.
id()==ID_signedbv ||
3485 o_type0.
id()==ID_c_bit_field)
3490 else if(o_type0.
id()==ID_vector &&
3491 o_type1.
id()==ID_vector)
3504 if(o_type0.
id()==ID_pointer &&
3505 (statement==ID_assign_minus || statement==ID_assign_plus))
3510 else if(o_type0.
id()==ID_vector &&
3511 o_type1.
id()==ID_vector)
3521 else if(o_type0.
id()==ID_bool ||
3522 o_type0.
id()==ID_c_bool)
3525 if(op1.
type().
id()==ID_bool ||
3526 op1.
type().
id()==ID_c_bool ||
3527 op1.
type().
id()==ID_c_enum_tag ||
3528 op1.
type().
id()==ID_unsignedbv ||
3529 op1.
type().
id()==ID_signedbv)
3537 op1.
type().
id()==ID_bool ||
3538 op1.
type().
id()==ID_c_bool ||
3539 op1.
type().
id()==ID_c_enum_tag)
3545 error() <<
"assignment '" << statement <<
"' not defined for types '"
3557 const auto rounding_mode =
3564 expr.
id()!=ID_infinity)
3567 error() <<
"expected constant expression, but got '" <<
to_string(expr)
3580 expr.
id()!=ID_infinity)
3583 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.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
std::vector< parametert > parameterst
ANSI-C Language Type Checking.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void typecheck_declaration(ansi_c_declarationt &)
const 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)
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()
#define Forall_irep(it, irep)
virtual void typecheck_expr_binary_boolean(exprt &expr)
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
An expression denoting infinity.
Evaluates to true if the operand is finite.
std::list< codet > clean_code
virtual void make_constant(exprt &expr)
const codet & to_code(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
virtual void typecheck_expr_operands(exprt &expr)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
virtual void typecheck_expr_member(exprt &expr)
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
typet & type()
Return the type of the expression.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
bool get_bool(const irep_namet &name) const
asm_label_mapt asm_label_map
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
irep_idt mode
Language mode.
mstreamt & result() const
static ieee_float_spect double_precision()
signedbv_typet signed_int_type()
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual void implicit_typecast_bool(exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
preprocessort preprocessor
source_locationt source_location
A base class for expressions that are predicates, i.e., Boolean-typed.
virtual void typecheck_expr_function_identifier(exprt &expr)
#define forall_operands(it, expr)
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.
bool simplify(exprt &expr, const namespacet &ns)
Binary multiplication Associativity is not specified.
A side_effect_exprt that performs an assignment.
exprt simplify_expr(exprt src, const namespacet &ns)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
symbol_tablet & symbol_table
virtual bool gcc_types_compatible_p(const typet &, const typet &)
mp_integer alignment(const typet &type, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_int_type()
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
virtual void typecheck_code(codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
bool has_component(const irep_idt &component_name) const
virtual void make_constant_index(exprt &expr)
const irep_idt & id() const
virtual void typecheck_expr_trinary(if_exprt &expr)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void remove(const irep_namet &name)
std::vector< exprt > operandst
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
const parameterst & parameters() const
const constant_exprt & size() const
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
id_type_mapt parameter_map
exprt pointer_offset(const exprt &pointer)
std::map< irep_idt, source_locationt > labels_used
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
const irep_idt & get_statement() const
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr(exprt &expr)
std::size_t get_width() const
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Deprecated expression utility functions.
A base class for shift operators.
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
#define forall_irep(it, irep)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_main(exprt &expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
Evaluates to true if the operand is infinite.
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
exprt::operandst & arguments()
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Imaginary part of the expression describing a complex number.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
exprt same_object(const exprt &p1, const exprt &p2)
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
virtual void typecheck_expr_constant(exprt &expr)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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()
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.
Operator to return the address of an object.
source_locationt & add_source_location()
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
signedbv_typet pointer_diff_type()
unsignedbv_typet size_type()
const irep_idt & get_statement() const
A constant literal expression.
IEEE-floating-point equality.
mstreamt & warning() const
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
virtual void typecheck_expr_sizeof(exprt &expr)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
static ieee_float_spect single_precision()
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
Evaluates to true if the operand is a normal number.
void set_identifier(const irep_idt &identifier)
irep_idt name
The unique identifier.
An expression containing a side effect.
virtual void typecheck_expr_index(exprt &expr)
virtual void make_index_type(exprt &expr)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
Evaluates to true if the operand is NaN.
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.