29 if(expr.
id()==ID_side_effect &&
30 expr.
get(ID_statement)==ID_function_call)
44 if(statement==ID_assign)
51 else if(statement==ID_assign_plus ||
52 statement==ID_assign_minus ||
53 statement==ID_assign_mult ||
54 statement==ID_assign_div ||
55 statement==ID_assign_mod ||
56 statement==ID_assign_shl ||
57 statement==ID_assign_ashr ||
58 statement==ID_assign_lshr ||
59 statement==ID_assign_bitand ||
60 statement==ID_assign_bitxor ||
61 statement==ID_assign_bitor)
65 id2string(statement) +
" expects two arguments",
70 if(statement==ID_assign_plus)
72 else if(statement==ID_assign_minus)
74 else if(statement==ID_assign_mult)
76 else if(statement==ID_assign_div)
78 else if(statement==ID_assign_mod)
80 else if(statement==ID_assign_shl)
82 else if(statement==ID_assign_ashr)
84 else if(statement==ID_assign_lshr)
86 else if(statement==ID_assign_bitand)
88 else if(statement==ID_assign_bitxor)
90 else if(statement==ID_assign_bitor)
101 if(op0_type.
id()==ID_c_bool)
108 else if(op0_type.
id() == ID_c_enum_tag)
130 convert(assignment, dest, mode);
154 "preincrement/predecrement must have one operand",
160 statement == ID_preincrement || statement == ID_predecrement,
161 "expects preincrement or predecrement");
166 if(statement==ID_preincrement)
173 if(op_type.
id()==ID_bool)
180 else if(op_type.
id()==ID_c_bool)
188 else if(op_type.
id()==ID_c_enum ||
189 op_type.
id()==ID_c_enum_tag)
200 if(op_type.
id()==ID_pointer)
202 else if(
is_number(op_type) || op_type.
id()==ID_c_bool)
203 constant_type=op_type;
219 convert(assignment, dest, mode);
243 "postincrement/postdecrement must have one operand",
249 statement == ID_postincrement || statement == ID_postdecrement,
250 "expects postincrement or postdecrement");
255 if(statement==ID_postincrement)
262 if(op_type.
id()==ID_bool)
269 else if(op_type.
id()==ID_c_bool)
277 else if(op_type.
id()==ID_c_enum ||
278 op_type.
id()==ID_c_enum_tag)
289 if(op_type.
id()==ID_pointer)
291 else if(
is_number(op_type) || op_type.
id()==ID_c_bool)
292 constant_type=op_type;
300 if(constant_type.
id()==ID_complex)
317 convert(assignment, tmp2, mode);
342 "function_call expects two operands",
357 expr.
id() == ID_side_effect && expr.
get(ID_statement) == ID_function_call,
358 "expects function call",
361 std::string new_base_name =
"return_value";
364 if(expr.
op0().
id()==ID_symbol)
371 new_symbol_mode = symbol.
mode;
396 static_cast<exprt &>(expr)=new_symbol.
symbol_expr();
403 if(dest.
id()==
"new_object")
430 static_cast<exprt &>(expr)=new_symbol.
symbol_expr();
445 tmp.copy_to_operands(expr.
op0());
446 tmp.
set(ID_destructor, expr.
find(ID_destructor));
478 static_cast<exprt &>(expr)=new_symbol.
symbol_expr();
482 call=
codet(ID_expression);
496 "temporary_object takes zero or one operands",
506 convert(assignment, dest, mode);
513 "temporary_object takes zero operands",
515 exprt initializer=static_cast<const exprt &>(expr.
find(ID_initializer));
521 static_cast<exprt &>(expr)=new_symbol.symbol_expr();
537 "statement_expression takes one operand",
541 expr.
op0().
id() == ID_code,
542 "statement_expression takes code as operand",
555 code.get_statement() == ID_block,
556 "statement_expression takes block as operand",
557 code.find_source_location());
560 !code.operands().empty(),
561 "statement_expression takes non-empty block as operand",
570 expr.
type(),
"statement_expression", dest, source_location, mode);
573 tmp_symbol_expr.add_source_location()=source_location;
575 if(last.get(ID_statement)==ID_expression)
580 last.add_source_location()=source_location;
582 else if(last.get(ID_statement)==ID_assign)
587 code.operands().push_back(assignment);
600 static_cast<exprt &>(expr)=tmp_symbol_expr;
611 if(statement==ID_function_call)
613 else if(statement==ID_assign ||
614 statement==ID_assign_plus ||
615 statement==ID_assign_minus ||
616 statement==ID_assign_mult ||
617 statement==ID_assign_div ||
618 statement==ID_assign_bitor ||
619 statement==ID_assign_bitxor ||
620 statement==ID_assign_bitand ||
621 statement==ID_assign_lshr ||
622 statement==ID_assign_ashr ||
623 statement==ID_assign_shl ||
624 statement==ID_assign_mod)
626 else if(statement==ID_postincrement ||
627 statement==ID_postdecrement)
629 else if(statement==ID_preincrement ||
630 statement==ID_predecrement)
632 else if(statement==ID_cpp_new ||
633 statement==ID_cpp_new_array)
635 else if(statement==ID_cpp_delete ||
636 statement==ID_cpp_delete_array)
638 else if(statement==ID_allocate)
640 else if(statement==ID_temporary_object)
642 else if(statement==ID_statement_expression)
644 else if(statement==ID_nondet)
648 else if(statement==ID_skip)
652 else if(statement==ID_throw)
658 t->code.op0().operands().swap(expr.
operands());
The type of an expression, extends irept.
irep_idt name
The unique identifier.
Semantic type conversion.
const std::string & id2string(const irep_idt &d)
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
codet & find_last_statement()
irep_idt mode
Language mode.
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
Deprecated expression utility functions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Fresh auxiliary symbol creation.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
typet & type()
Return the type of the expression.
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest)
codet representation of an expression statement.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
code_expressiont & to_code_expression(codet &code)
A side_effect_exprt representation of a side effect that throws an exception.
static bool has_function_call(const exprt &expr)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
std::string tmp_symbol_prefix
A base class for binary expressions.
instructionst::iterator targett
A codet representing the declaration of a local variable.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
codet representation of a function call statement.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void convert_cpp_delete(const codet &code, goto_programt &dest)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
A generic container class for the GOTO intermediate representation of one function.
void remove_post(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const exprt & expression() const
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
symbol_table_baset & symbol_table
#define Forall_operands(it, expr)
source_locationt & add_source_location()
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const code_blockt & to_code_block(const codet &code)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Data structure for representing an arbitrary statement in a program.
signedbv_typet signed_int_type()
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
An expression containing a side effect.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Complex constructor from a pair of numbers.
A codet representing an assignment in the program.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const