39 const exprt &
function,
43 const irep_idt &identifier=
function.get(ID_identifier);
46 if(arguments.size()!=2)
49 error() <<
"`" << identifier
50 <<
"' expected to have two arguments" <<
eom;
57 error() <<
"`" << identifier <<
"' expected to have LHS" <<
eom;
64 if(lhs.
type().
id()!=ID_unsignedbv &&
65 lhs.
type().
id()!=ID_signedbv)
68 error() <<
"`" << identifier <<
"' expected other type" <<
eom;
72 if(arguments[0].type().
id()!=lhs.
type().
id() ||
73 arguments[1].type().id()!=lhs.
type().
id())
76 error() <<
"`" << identifier
77 <<
"' expected operands to be of same type as LHS" <<
eom;
81 if(!arguments[0].is_constant() ||
82 !arguments[1].is_constant())
85 error() <<
"`" << identifier
86 <<
"' expected operands to be constant literals" <<
eom;
96 error() <<
"error converting operands" <<
eom;
103 error() <<
"expected lower bound to be smaller or equal to the " 104 <<
"upper bound" <<
eom;
117 const exprt &
function,
121 const irep_idt &identifier=
function.get(ID_identifier);
124 if(arguments.size()!=2)
127 error() <<
"`" << identifier <<
"' expected to have two arguments" 135 error() <<
"`" << identifier <<
"' expected to have LHS" <<
eom;
145 error() <<
"`" << identifier <<
"' expected bool" <<
eom;
149 if(arguments[0].type().
id()!=ID_unsignedbv ||
150 arguments[0].
id()!=ID_constant)
153 error() <<
"`" << identifier <<
"' expected first operand to be " 154 <<
"a constant literal of type unsigned long" <<
eom;
164 error() <<
"error converting operands" <<
eom;
171 error() <<
"probability has to be smaller than 1" <<
eom;
178 error() <<
"denominator may not be zero" <<
eom;
182 rationalt numerator(num), denominator(den);
183 rationalt prob = numerator / denominator;
194 const exprt &
function,
198 const irep_idt &f_id=
function.get(ID_identifier);
204 static_cast<const typet &
>(
function.type().find(ID_return_type));
218 printf_code.
id(ID_code);
229 const exprt &
function,
233 const irep_idt &f_id=
function.get(ID_identifier);
237 if(arguments.empty())
240 error() <<
"scanf takes at least one argument" <<
eom;
252 std::size_t argument_number=1;
254 for(
const auto &t : token_list)
260 if(argument_number<arguments.size())
266 if(type.
id()==ID_array)
275 type,
"scanf_string", dest,
function.source_location());
284 codet array_copy_statement;
286 array_copy_statement.
operands().resize(2);
287 array_copy_statement.
op0()=ptr;
288 \ array_copy_statement.
op1()=rhs;
290 function.source_location();
299 assign.add_source_location()=
function.source_location();
320 function_call.
lhs()=lhs;
334 const exprt &
function,
343 if(arguments.size()<2)
346 error() <<
"input takes at least two arguments" <<
eom;
355 const exprt &
function,
364 if(arguments.size()<2)
367 error() <<
"output takes at least two arguments" <<
eom;
376 const exprt &
function,
383 error() <<
"atomic_begin does not expect an LHS" <<
eom;
387 if(!arguments.empty())
390 error() <<
"atomic_begin takes no arguments" <<
eom;
395 t->source_location=
function.source_location();
400 const exprt &
function,
407 error() <<
"atomic_end does not expect an LHS" <<
eom;
411 if(!arguments.empty())
414 error() <<
"atomic_end takes no arguments" <<
eom;
419 t->source_location=
function.source_location();
430 error() <<
"do_cpp_new without lhs is yet to be implemented" <<
eom;
436 static_cast<const exprt &
>(rhs.
find(ID_sizeof));
438 bool new_array=rhs.
get(ID_statement)==ID_cpp_new_array;
444 count=
static_cast<const exprt &
>(rhs.
find(ID_size));
453 exprt tmp_symbol_expr;
460 ns.
lookup(new_array?
"__new_array":
"__new").symbol_expr();
465 const typet &return_type=
474 tmp_symbol_expr=tmp_symbol.symbol_expr();
482 new_call.
lhs()=tmp_symbol_expr;
492 new_array?
"__placement_new_array":
"__placement_new").symbol_expr();
505 tmp_symbol_expr=tmp_symbol.symbol_expr();
514 new_call.
lhs()=tmp_symbol_expr;
517 for(
unsigned i=0; i<code_type.
parameters().size(); i++)
526 error() <<
"cpp_new expected to have 0 or 1 operands" <<
eom;
551 if(components.empty())
555 if(components.front().get_name()==
"@class_identifier")
557 assert(expr.
op0().
id()==ID_constant);
562 assert(expr.
op0().
id()==ID_struct);
575 error() <<
"do_java_new without lhs is yet to be implemented" <<
eom;
583 if(rhs.
type().
id()!=ID_pointer)
586 error() <<
"do_java_new returns pointer" <<
eom;
598 error() <<
"do_java_new got nil object_size" <<
eom;
609 t_n->source_location=location;
619 t_i->source_location=location;
630 error() <<
"do_java_new_array without lhs is yet to be implemented" 639 if(rhs.
type().
id()!=ID_pointer)
642 error() <<
"do_java_new_array returns pointer" <<
eom;
654 error() <<
"do_java_new_array got nil object_size" <<
eom;
665 t_n->source_location=location;
669 assert(
ns.
follow(object_type).
id()==ID_struct);
671 assert(struct_type.components().size()==3);
677 struct_type.components()[1].get_name(),
678 struct_type.components()[1].type());
686 struct_type.components()[2].get_name(),
687 struct_type.components()[2].type());
695 const irept size_bound=rhs.
find(ID_length_upper_bound);
696 if(size_bound.is_nil())
697 data_cpp_new_expr.
set(ID_size, rhs.
op0());
699 data_cpp_new_expr.set(ID_size, size_bound);
702 t_p->source_location=location;
707 data.type().subtype(),
711 codet array_set(ID_array_set);
712 array_set.copy_to_operands(
data, zero_element);
715 t_d->source_location=location;
726 new_tmp_symbol(length.type(),
"index", tmp, location).symbol_expr();
733 assert(rhs.
type().
id()==ID_pointer);
736 assert(sub_type.id()==ID_pointer);
737 sub_java_new.
type()=sub_type;
755 for_body.move_to_operands(init_subarray);
756 for_body.move_to_operands(assign_subarray);
761 for_loop.
body()=for_body;
775 static_cast<const exprt &
>(rhs.
find(ID_initializer));
799 if(src.
id()==ID_typecast)
805 if(src.
id()!=ID_address_of)
808 error() <<
"expected array-pointer as argument" <<
eom;
814 if(src.
op0().
id()!=ID_index)
817 error() <<
"expected array-element as argument" <<
eom;
826 error() <<
"expected array as argument" <<
eom;
836 const exprt &
function,
840 if(arguments.size()!=2)
843 error() <<
id <<
" expects two arguments" <<
eom;
847 codet array_op_statement;
849 array_op_statement.
operands()=arguments;
857 const exprt &
function,
861 if(arguments.size()!=2)
864 error() <<
"array_equal expects two arguments" <<
eom;
871 if(arg0_type.
id()!=ID_pointer ||
872 arg1_type.
id()!=ID_pointer)
875 error() <<
"array_equal expects pointer arguments" <<
eom;
885 lhs_array.
op0()=arguments[0];
886 rhs_array.
op0()=arguments[1];
890 assignment.
lhs()=lhs;
892 lhs_array, ID_array_equal, rhs_array, lhs.
type());
901 if(expr.
id()==ID_index)
903 else if(expr.
id()==ID_member)
905 else if(expr.
id()==ID_dereference)
907 else if(expr.
id()==ID_symbol)
916 if(expr.
id()==ID_typecast)
920 if(expr.
id()==ID_address_of &&
935 if(
function.get_bool(
"#invalid_object"))
939 const irep_idt &identifier=
function.get_identifier();
945 error() <<
"error: function `" << identifier <<
"' not found" 950 if(symbol->
type.
id()!=ID_code)
953 error() <<
"error: function `" << identifier
954 <<
"' type mismatch: expected code" <<
eom;
959 identifier==
"__VERIFIER_assume")
961 if(arguments.size()!=1)
964 error() <<
"`" << identifier <<
"' expected to have one argument" 970 t->guard=arguments.front();
971 t->source_location=
function.source_location();
972 t->source_location.set(
"user-provided",
true);
975 if(t->guard.type().id()!=ID_bool)
981 error() << identifier <<
" expected not to have LHS" <<
eom;
985 else if(identifier==
"__VERIFIER_error")
987 if(!arguments.empty())
990 error() <<
"`" << identifier <<
"' expected to have no arguments" 997 t->source_location=
function.source_location();
998 t->source_location.set(
"user-provided",
true);
999 t->source_location.set_property_class(ID_assertion);
1004 error() << identifier <<
" expected not to have LHS" <<
eom;
1012 a->source_location=
function.source_location();
1013 a->source_location.set(
"user-provided",
true);
1016 id2string(identifier),
"java::java.lang.AssertionError.<init>:"))
1020 function_call.
lhs()=lhs;
1027 if(arguments.size()!=1 && arguments.size()!=2)
1030 error() <<
"`" << identifier
1031 <<
"' expected to have one or two arguments" <<
eom;
1037 t->source_location=
function.source_location();
1038 t->source_location.set(
"user-provided",
true);
1039 t->source_location.set_property_class(ID_assertion);
1040 t->source_location.set_comment(
1041 "assertion at "+
function.source_location().
as_string());
1043 else if(identifier==
"assert" &&
1044 !
ns.
lookup(identifier).location.get_function().empty())
1046 if(arguments.size()!=1)
1049 error() <<
"`" << identifier <<
"' expected to have one argument" 1055 t->guard=arguments.front();
1056 t->source_location=
function.source_location();
1057 t->source_location.set(
"user-provided",
true);
1058 t->source_location.set_property_class(ID_assertion);
1059 t->source_location.set_comment(
1063 if(t->guard.type().id()!=ID_bool)
1069 error() << identifier <<
" expected not to have LHS" <<
eom;
1075 if(arguments.size()!=2)
1078 error() <<
"`" << identifier <<
"' expected to have two arguments" 1087 t->guard=arguments[0];
1088 t->source_location=
function.source_location();
1089 t->source_location.set(
1091 !
function.source_location().is_built_in());
1092 t->source_location.set_property_class(ID_assertion);
1093 t->source_location.set_comment(description);
1096 if(t->guard.type().id()!=ID_bool)
1102 error() << identifier <<
" expected not to have LHS" <<
eom;
1108 do_printf(lhs,
function, arguments, dest);
1112 do_scanf(lhs,
function, arguments, dest);
1115 identifier==
"__CPROVER::input")
1117 do_input(lhs,
function, arguments, dest);
1120 identifier==
"__CPROVER::output")
1122 do_output(lhs,
function, arguments, dest);
1125 identifier==
"__CPROVER::atomic_begin" ||
1126 identifier==
"__VERIFIER_atomic_begin")
1131 identifier==
"__CPROVER::atomic_end" ||
1132 identifier==
"__VERIFIER_atomic_end")
1155 if(lhs.
type().
id()==ID_c_bool)
1159 rhs.
set(ID_C_identifier, identifier);
1166 rhs.
set(ID_C_identifier, identifier);
1195 do_array_op(ID_array_set, lhs,
function, arguments, dest);
1199 do_array_op(ID_array_copy, lhs,
function, arguments, dest);
1203 do_array_op(ID_array_replace, lhs,
function, arguments, dest);
1205 else if(identifier==
"printf")
1212 do_printf(lhs,
function, arguments, dest);
1214 else if(identifier==
"__assert_fail" ||
1215 identifier==
"_assert" ||
1216 identifier==
"__assert_c99" ||
1217 identifier==
"_wassert")
1238 if(arguments.size()!=4 &&
1239 arguments.size()!=3)
1242 error() <<
"`" << identifier <<
"' expected to have four arguments" 1252 t->source_location=
function.source_location();
1253 t->source_location.set(
"user-provided",
true);
1254 t->source_location.set_property_class(ID_assertion);
1255 t->source_location.set_comment(description);
1258 else if(identifier==
"__assert_rtn" ||
1259 identifier==
"__assert")
1270 if(arguments.size()==4)
1275 else if(arguments.size()==3)
1283 error() <<
"`" << identifier <<
"' expected to have four arguments" 1290 t->source_location=
function.source_location();
1291 t->source_location.set(
"user-provided",
true);
1292 t->source_location.set_property_class(ID_assertion);
1293 t->source_location.set_comment(description);
1296 else if(identifier==
"__assert_func")
1301 if(arguments.size()!=4)
1304 error() <<
"`" << identifier <<
"' expected to have four arguments" 1319 description=
"assertion";
1324 t->source_location=
function.source_location();
1325 t->source_location.set(
"user-provided",
true);
1326 t->source_location.set_property_class(ID_assertion);
1327 t->source_location.set_comment(description);
1332 if(arguments.empty())
1335 error() <<
"`" << identifier
1336 <<
"' expected to have at least one argument" <<
eom;
1341 t->source_location=
function.source_location();
1342 t->code.set(ID_statement, ID_fence);
1347 t->code.set(kind,
true);
1350 else if(identifier==
"__builtin_prefetch")
1354 else if(identifier==
"__builtin_unreachable")
1358 else if(identifier==ID_gcc_builtin_va_arg)
1366 if(arguments.size()!=1)
1369 error() <<
"`" << identifier <<
"' expected to have one argument" 1379 rhs.set(ID_C_va_arg_type,
to_code_type(
function.type()).return_type());
1381 t1->source_location=
function.source_location();
1390 rhs.add_source_location()=
function.source_location();
1392 t2->source_location=
function.source_location();
1396 else if(identifier==
"__builtin_va_copy")
1398 if(arguments.size()!=2)
1401 error() <<
"`" << identifier <<
"' expected to have two arguments" 1412 error() <<
"va_copy argument expected to be lvalue" <<
eom;
1417 t->source_location=
function.source_location();
1420 else if(identifier==
"__builtin_va_start")
1424 if(arguments.size()!=2)
1427 error() <<
"`" << identifier <<
"' expected to have two arguments" 1439 error() <<
"va_start argument expected to be lvalue" <<
eom;
1444 t->source_location=
function.source_location();
1447 else if(identifier==
"__builtin_va_end")
1450 if(arguments.size()!=1)
1453 error() <<
"`" << identifier <<
"' expected to have one argument" 1463 error() <<
"va_end argument expected to be lvalue" <<
eom;
1471 t->source_location=
function.source_location();
1481 else if(identifier==
"__sync_fetch_and_add" ||
1482 identifier==
"__sync_fetch_and_sub" ||
1483 identifier==
"__sync_fetch_and_or" ||
1484 identifier==
"__sync_fetch_and_and" ||
1485 identifier==
"__sync_fetch_and_xor" ||
1486 identifier==
"__sync_fetch_and_nand")
1491 if(arguments.size()<2)
1494 error() <<
"`" << identifier
1495 <<
"' expected to have at least two arguments" <<
eom;
1499 if(arguments[0].type().
id()!=ID_pointer)
1502 error() <<
"`" << identifier <<
"' expected to have pointer argument" 1511 t1->source_location=
function.source_location();
1517 t2->source_location=
function.source_location();
1519 if(t2->code.op0().type()!=t2->code.op1().type())
1520 t2->code.op1().make_typecast(t2->code.op0().type());
1524 identifier==
"__sync_fetch_and_add"?ID_plus:
1525 identifier==
"__sync_fetch_and_sub"?ID_minus:
1526 identifier==
"__sync_fetch_and_or"?ID_bitor:
1527 identifier==
"__sync_fetch_and_and"?ID_bitand:
1528 identifier==
"__sync_fetch_and_xor"?ID_bitxor:
1529 identifier==
"__sync_fetch_and_nand"?ID_bitnand:
1534 if(op_expr.op1().type()!=op_expr.type())
1538 t3->source_location=
function.source_location();
1543 t4->source_location=
function.source_location();
1544 t4->code=
codet(ID_fence);
1545 t4->code.set(ID_WRfence,
true);
1548 t5->source_location=
function.source_location();
1550 else if(identifier==
"__sync_add_and_fetch" ||
1551 identifier==
"__sync_sub_and_fetch" ||
1552 identifier==
"__sync_or_and_fetch" ||
1553 identifier==
"__sync_and_and_fetch" ||
1554 identifier==
"__sync_xor_and_fetch" ||
1555 identifier==
"__sync_nand_and_fetch")
1560 if(arguments.size()<2)
1563 error() <<
"`" << identifier
1564 <<
"' expected to have at least two arguments" <<
eom;
1568 if(arguments[0].type().
id()!=ID_pointer)
1571 error() <<
"`" << identifier
1572 <<
"' expected to have pointer argument" <<
eom;
1580 t1->source_location=
function.source_location();
1583 identifier==
"__sync_add_and_fetch"?ID_plus:
1584 identifier==
"__sync_sub_and_fetch"?ID_minus:
1585 identifier==
"__sync_or_and_fetch"?ID_bitor:
1586 identifier==
"__sync_and_and_fetch"?ID_bitand:
1587 identifier==
"__sync_xor_and_fetch"?ID_bitxor:
1588 identifier==
"__sync_nand_and_fetch"?ID_bitnand:
1593 if(op_expr.op1().type()!=op_expr.type())
1597 t3->source_location=
function.source_location();
1604 t2->source_location=
function.source_location();
1606 if(t2->code.op0().type()!=t2->code.op1().type())
1607 t2->code.op1().make_typecast(t2->code.op0().type());
1612 t4->source_location=
function.source_location();
1613 t4->code=
codet(ID_fence);
1614 t4->code.set(ID_WRfence,
true);
1617 t5->source_location=
function.source_location();
1619 else if(identifier==
"__sync_bool_compare_and_swap")
1633 if(arguments.size()<3)
1636 error() <<
"`" << identifier
1637 <<
"' expected to have at least three arguments" <<
eom;
1641 if(arguments[0].type().
id()!=ID_pointer)
1644 error() <<
"`" << identifier
1645 <<
"' expected to have pointer argument" <<
eom;
1653 t1->source_location=
function.source_location();
1664 t2->source_location=
function.source_location();
1666 if(t2->code.op0().type()!=t2->code.op1().type())
1667 t2->code.op1().make_typecast(t2->code.op0().type());
1671 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1672 if(if_expr.op1().type()!=if_expr.type())
1676 t3->source_location=
function.source_location();
1681 t4->source_location=
function.source_location();
1682 t4->code=
codet(ID_fence);
1683 t4->code.set(ID_WRfence,
true);
1686 t5->source_location=
function.source_location();
1688 else if(identifier==
"__sync_val_compare_and_swap")
1692 if(arguments.size()<3)
1695 error() <<
"`" << identifier
1696 <<
"' expected to have at least three arguments" <<
eom;
1700 if(arguments[0].type().
id()!=ID_pointer)
1703 error() <<
"`" << identifier
1704 <<
"' expected to have pointer argument" <<
eom;
1712 t1->source_location=
function.source_location();
1718 t2->source_location=
function.source_location();
1720 if(t2->code.op0().type()!=t2->code.op1().type())
1721 t2->code.op1().make_typecast(t2->code.op0().type());
1730 if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.
type());
1731 if(if_expr.op1().type()!=if_expr.type())
1735 t3->source_location=
function.source_location();
1740 t4->source_location=
function.source_location();
1741 t4->code=
codet(ID_fence);
1742 t4->code.set(ID_WRfence,
true);
1745 t5->source_location=
function.source_location();
1747 else if(identifier==
"__sync_lock_test_and_set")
1760 else if(identifier==
"__sync_lock_release")
1770 else if(identifier==
"__builtin_isgreater" ||
1771 identifier==
"__builtin_isgreater" ||
1772 identifier==
"__builtin_isgreaterequal" ||
1773 identifier==
"__builtin_isless" ||
1774 identifier==
"__builtin_islessequal" ||
1775 identifier==
"__builtin_islessgreater" ||
1776 identifier==
"__builtin_isunordered")
1780 if(arguments.size()!=2 ||
1787 error() <<
"`" << identifier
1788 <<
"' expected to have two float/double arguments" 1795 bool use_double=arguments[0].type()==
double_type();
1796 if(arguments[0].type()!=arguments[1].type())
1799 new_arguments[1].make_typecast(arguments[0].type());
1802 new_arguments[0].make_typecast(arguments[1].type());
1809 const typet &a_t=new_arguments[0].type();
1816 name+=use_double?
'd':
'f';
1820 new_function.
type()=f_type;
1823 function_call.
lhs()=lhs;
1824 function_call.
function()=new_function;
1825 function_call.
arguments()=new_arguments;
1833 new_symbol.
name=name;
1834 new_symbol.
type=f_type;
1835 new_symbol.
location=
function.source_location();
1847 function_call.
lhs()=lhs;
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Linking: Zero Initialization.
targett add_instruction()
Adds an instruction at the end.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
void convert(const codet &code, goto_programt &dest)
converts 'code' and appends the result to 'dest'
pointer_typet pointer_type(const typet &subtype)
const exprt & init() const
symbol_tablet & symbol_table
application of (mathematical) function
void do_input(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const codet & body() const
bool is_lvalue(const exprt &expr)
void copy_to_operands(const exprt &expr)
#define forall_expr(it, expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
std::vector< parametert > parameterst
const componentst & components() const
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
void do_atomic_begin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_array_equal(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
The trinary if-then-else operator.
bitvector_typet double_type()
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.
static mstreamt & eom(mstreamt &m)
Extract member of struct or union.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const char * as_string(coverage_criteriont c)
exprt make_va_list(const exprt &expr)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
irep_idt get_string_constant(const exprt &expr)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
A reference into the symbol table.
A generic base class for binary expressions.
bitvector_typet float_type()
const source_locationt & find_source_location() const
const exprt & cond() const
source_locationt source_location
Operator to dereference a pointer.
API to expression classes.
void do_prob_coin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const irep_idt & get(const irep_namet &name) const
void do_prob_uniform(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
A side effect that returns a non-deterministically chosen value.
const exprt & size() const
Base class for tree-like data structures with sharing.
bitvector_typet index_type()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
Operator to return the address of an object.
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
Various predicates over pointers in programs.
exprt get_array_argument(const exprt &src)
The boolean constant false.
void do_array_op(const irep_idt &id, const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void do_printf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const source_locationt & source_location() const
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
message_handlert & get_message_handler()
void do_scanf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_output(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
void set_statement(const irep_idt &statement)
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const source_locationt & source_location() const
const exprt & iter() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_identifier(const irep_idt &identifier)
bool has_symbol(const irep_idt &name) const
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A statement in a programming language.
const typet & subtype() const
An expression containing a side effect.
struct constructor from list of elements
void make_typecast(const typet &_type)
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
void do_atomic_end(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const typet & return_type() const
const irep_idt & get_identifier() const
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const
instructionst::iterator targett