29 if(expr.
id()==ID_side_effect &&
30 expr.
get(ID_statement)==ID_function_call)
43 if(statement==ID_assign)
50 else if(statement==ID_assign_plus ||
51 statement==ID_assign_minus ||
52 statement==ID_assign_mult ||
53 statement==ID_assign_div ||
54 statement==ID_assign_mod ||
55 statement==ID_assign_shl ||
56 statement==ID_assign_ashr ||
57 statement==ID_assign_lshr ||
58 statement==ID_assign_bitand ||
59 statement==ID_assign_bitxor ||
60 statement==ID_assign_bitor)
65 error() << statement <<
" takes two arguments" <<
eom;
71 if(statement==ID_assign_plus)
73 else if(statement==ID_assign_minus)
75 else if(statement==ID_assign_mult)
77 else if(statement==ID_assign_div)
79 else if(statement==ID_assign_mod)
81 else if(statement==ID_assign_shl)
83 else if(statement==ID_assign_ashr)
85 else if(statement==ID_assign_lshr)
87 else if(statement==ID_assign_bitand)
89 else if(statement==ID_assign_bitxor)
91 else if(statement==ID_assign_bitor)
96 error() <<
"assignment `" << statement <<
"' not yet supported" 106 if(op0_type.
id()==ID_c_bool)
147 error() <<
"preincrement/predecrement must have one operand" <<
eom;
153 assert(statement==ID_preincrement ||
154 statement==ID_predecrement);
159 if(statement==ID_preincrement)
166 if(op_type.
id()==ID_bool)
173 else if(op_type.
id()==ID_c_bool)
181 else if(op_type.
id()==ID_c_enum ||
182 op_type.
id()==ID_c_enum_tag)
193 if(op_type.
id()==ID_pointer)
195 else if(
is_number(op_type) || op_type.
id()==ID_c_bool)
196 constant_type=op_type;
238 error() <<
"postincrement/postdecrement must have one operand" 245 assert(statement==ID_postincrement ||
246 statement==ID_postdecrement);
251 if(statement==ID_postincrement)
258 if(op_type.
id()==ID_bool)
265 else if(op_type.
id()==ID_c_bool)
273 else if(op_type.
id()==ID_c_enum ||
274 op_type.
id()==ID_c_enum_tag)
285 if(op_type.
id()==ID_pointer)
287 else if(
is_number(op_type) || op_type.
id()==ID_c_bool)
288 constant_type=op_type;
298 if(constant_type.
id()==ID_complex)
358 if(expr.
id()!=ID_side_effect ||
359 expr.
get(ID_statement)!=ID_function_call)
362 error() <<
"expected function call" <<
eom;
369 error() <<
"function_call expects at least one operand" <<
eom;
373 if(expr.
op0().
id()==ID_symbol)
416 if(dest.
id()==
"new_object")
464 tmp.copy_to_operands(expr.
op0());
465 tmp.
set(ID_destructor, expr.
find(ID_destructor));
502 call=
codet(ID_expression);
518 error() <<
"temporary_object takes 0 or 1 operands" <<
eom;
525 new_symbol.
mode=expr.
get(ID_mode);
529 codet assignment(ID_assign);
540 exprt initializer=
static_cast<const exprt &
>(expr.
find(ID_initializer));
562 error() <<
"statement_expression takes 1 operand" <<
eom;
566 if(expr.
op0().
id()!=ID_code)
569 error() <<
"statement_expression takes code as operand" <<
eom;
585 error() <<
"statement_expression takes block as operand" <<
eom;
592 error() <<
"statement_expression takes non-empty block as operand" 606 tmp_symbol_expr.add_source_location()=source_location;
608 if(last.
get(ID_statement)==ID_expression)
615 else if(last.
get(ID_statement)==ID_assign)
620 code.
operands().push_back(assignment);
624 error() <<
"statement_expression expects expression as " 625 <<
"last statement, but got `" 626 << last.
get(ID_statement) <<
"'" <<
eom;
636 static_cast<exprt &
>(expr)=tmp_symbol_expr;
657 if(statement==ID_function_call)
659 else if(statement==ID_assign ||
660 statement==ID_assign_plus ||
661 statement==ID_assign_minus ||
662 statement==ID_assign_mult ||
663 statement==ID_assign_div ||
664 statement==ID_assign_bitor ||
665 statement==ID_assign_bitxor ||
666 statement==ID_assign_bitand ||
667 statement==ID_assign_lshr ||
668 statement==ID_assign_ashr ||
669 statement==ID_assign_shl ||
670 statement==ID_assign_mod)
672 else if(statement==ID_postincrement ||
673 statement==ID_postdecrement)
675 else if(statement==ID_preincrement ||
676 statement==ID_predecrement)
678 else if(statement==ID_cpp_new ||
679 statement==ID_cpp_new_array)
681 else if(statement==ID_cpp_delete ||
682 statement==ID_cpp_delete_array)
684 else if(statement==ID_malloc)
686 else if(statement==ID_temporary_object)
688 else if(statement==ID_statement_expression)
690 else if(statement==ID_nondet)
694 else if(statement==ID_skip)
698 else if(statement==ID_throw)
703 t->code.op0().operands().swap(expr.
operands());
710 else if(statement==ID_push_catch)
715 error() <<
"cannot remove side effect (" << statement <<
")" <<
eom;
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
const typet & follow(const typet &src) const
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
void convert(const codet &code, goto_programt &dest)
converts 'code' and appends the result to 'dest'
void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void remove_assignment(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void remove_push_catch(side_effect_exprt &expr, goto_programt &dest)
irep_idt mode
Language mode.
Deprecated expression utility functions.
void copy_to_operands(const exprt &expr)
void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
void move_to_operands(exprt &expr)
void convert_assign(const code_assignt &code, goto_programt &dest)
void remove_malloc(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
code_expressiont & to_code_expression(codet &code)
A side effect that throws an exception.
void remove_statement_expression(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
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
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 generic base class for binary expressions.
A declaration of a local variable.
const source_locationt & find_source_location() const
source_locationt source_location
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
void remove_cpp_new(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
#define forall_operands(it, expr)
bitvector_typet index_type()
void remove_pre(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
codet & find_last_statement()
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_function_call(const code_function_callt &code, goto_programt &dest)
void remove_post(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void convert_java_try_catch(const codet &code, goto_programt &dest)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void remove_side_effect(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
bool is_number(const typet &type)
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
void set_statement(const irep_idt &statement)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
const symbolt & lookup(const irep_idt &identifier)
irep_idt base_name
Base (non-scoped) name.
const source_locationt & source_location() const
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
const exprt & expression() const
unsigned temporary_counter
void remove_function_call(side_effect_exprt &expr, goto_programt &dest, bool result_is_used)
#define Forall_operands(it, expr)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
A statement in a programming language.
signedbv_typet signed_int_type()
const typet & subtype() const
An expression containing a side effect.
void make_typecast(const typet &_type)
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
complex constructor from a pair of numbers
void set(const irep_namet &name, const irep_idt &value)
void reserve_operands(operandst::size_type n)
const irep_idt & get_statement() const
instructionst::iterator targett