45 if(rhs.
id()==ID_side_effect)
50 if(statement==ID_function_call)
52 assert(!side_effect_expr.
operands().empty());
54 if(side_effect_expr.
op0().
id()!=ID_symbol)
55 throw "symex_assign: expected symbol as function";
60 throw "symex_assign: unexpected function call: "+
id2string(identifier);
62 else if(statement==ID_cpp_new ||
63 statement==ID_cpp_new_array)
65 else if(statement==ID_malloc)
67 else if(statement==ID_printf)
69 else if(statement==ID_gcc_builtin_va_arg_next)
72 throw "symex_assign: unexpected side effect: "+
id2string(statement);
79 if(lhs.
id()==ID_symbol &&
81 "#return_value!")!=std::string::npos)
89 if(state.
source.
pc->source_location.get_hide())
101 assert(lhs.
id()!=ID_symbol);
104 if(tmp_what.id()!=ID_symbol)
106 assert(tmp_what.operands().size()>=1);
116 assert(p->
id()!=ID_symbol);
130 const exprt &full_lhs,
135 if(lhs.
id()==ID_symbol &&
138 state,
to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
139 else if(lhs.
id()==ID_index)
141 state,
to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
142 else if(lhs.
id()==ID_member)
145 if(type.
id()==ID_struct)
147 state,
to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
148 else if(type.
id()==ID_union)
151 throw "symex_assign_rec: unexpected assignment to union member";
155 "symex_assign_rec: unexpected assignment to member of `"+
158 else if(lhs.
id()==ID_if)
160 state,
to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
161 else if(lhs.
id()==ID_typecast)
164 else if(lhs.
id()==ID_string_constant ||
165 lhs.
id()==
"NULL-object" ||
166 lhs.
id()==
"zero_string" ||
167 lhs.
id()==
"is_zero_string" ||
168 lhs.
id()==
"zero_string_length")
172 else if(lhs.
id()==ID_byte_extract_little_endian ||
173 lhs.
id()==ID_byte_extract_big_endian)
178 else if(lhs.
id()==ID_complex_real ||
179 lhs.
id()==ID_complex_imag)
187 if(lhs.
id()==ID_complex_real)
199 state, lhs.
op0(), full_lhs, new_rhs, guard, assignment_type);
202 throw "assignment to `"+lhs.
id_string()+
"' not handled";
208 const exprt &full_lhs,
234 tmp_ssa_rhs.
swap(ssa_rhs);
248 exprt ssa_full_lhs=full_lhs;
249 ssa_full_lhs=
add_to_lhs(ssa_full_lhs, ssa_lhs);
275 const exprt &full_lhs,
284 exprt rhs_typecasted=rhs;
290 state, lhs.
op0(), new_full_lhs, rhs_typecasted, guard, assignment_type);
296 const exprt &full_lhs,
306 throw "index must have two operands";
312 if(lhs_type.
id()!=ID_array)
313 throw "index must take array type operand, but got `"+
324 new_rhs.
old()=lhs_array;
331 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
339 exprt new_rhs(ID_with, lhs_type);
345 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
352 const exprt &full_lhs,
365 if(lhs_struct.
id()==ID_typecast)
367 assert(lhs_struct.
operands().size()==1);
369 if(lhs_struct.
op0().
id()==
"NULL-object")
380 if(op0_type.
id()==ID_struct)
397 new_rhs.
old()=lhs_struct;
399 new_rhs.new_value()=rhs;
404 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
412 exprt new_rhs(ID_with, lhs_struct.
type());
414 new_rhs.op1().set(ID_component_name, component_name);
419 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
426 const exprt &full_lhs,
441 guard.
add(renamed_guard);
443 state, lhs.
true_case(), full_lhs, rhs, guard, assignment_type);
444 guard.swap(old_guard);
451 state, lhs.
false_case(), full_lhs, rhs, guard, assignment_type);
452 guard.swap(old_guard);
459 const exprt &full_lhs,
469 if(lhs.
id()==ID_byte_extract_little_endian)
470 new_rhs.
id(ID_byte_update_little_endian);
471 else if(lhs.
id()==ID_byte_extract_big_endian)
472 new_rhs.
id(ID_byte_update_big_endian);
482 state, lhs.
op(), new_full_lhs, new_rhs, guard, assignment_type);
virtual void do_simplify(exprt &expr)
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
void append(const guardt &guard)
Operator to update elements in structs and arrays.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
void symex_assign_byte_extract(statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const irep_idt & get_identifier() const
exprt::operandst & designator()
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
void symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
bool constant_propagation
The trinary if-then-else operator.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
void replace_nondet(exprt &expr)
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
const irep_idt get_level_1() const
goto_symex_statet::level2t level2
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
const irep_idt & id() const
Expression classes for byte-level operators.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
bool get_bool_option(const std::string &option) const
Generic base class for unary expressions.
void clean_expr(exprt &expr, statet &state, bool write)
void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
void symex_assign_rec(statet &state, const code_assignt &code)
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
irep_idt get_object_name() const
const exprt & get_original_expr() const
irep_idt get_component_name() const
const std::string & id_string() const
An expression containing a side effect.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
void make_typecast(const typet &_type)
Expression providing an SSA-renamed symbol of expressions.
void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
void add(const exprt &expr)
void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
const irep_idt & get_statement() const
symex_targett::sourcet source