33 if(rhs.
id()==ID_side_effect)
38 if(statement==ID_function_call)
40 assert(!side_effect_expr.
operands().empty());
42 if(side_effect_expr.
op0().
id()!=ID_symbol)
43 throw "symex_assign: expected symbol as function";
48 throw "symex_assign: unexpected function call: "+
id2string(identifier);
51 statement == ID_cpp_new || statement == ID_cpp_new_array ||
52 statement == ID_java_new_array_data)
54 else if(statement==ID_allocate)
56 else if(statement==ID_printf)
58 else if(statement==ID_gcc_builtin_va_arg_next)
61 throw "symex_assign: unexpected side effect: "+
id2string(statement);
68 if(lhs.
id()==ID_symbol &&
70 "#return_value!")!=std::string::npos)
78 if(state.
source.
pc->source_location.get_hide())
90 assert(lhs.
id()!=ID_symbol);
93 if(tmp_what.id()!=ID_symbol)
95 assert(tmp_what.operands().size()>=1);
105 assert(p->
id()!=ID_symbol);
119 const exprt &full_lhs,
124 if(lhs.
id()==ID_symbol &&
127 state,
to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
128 else if(lhs.
id()==ID_index)
130 state,
to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
131 else if(lhs.
id()==ID_member)
134 if(type.
id()==ID_struct)
136 state,
to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
137 else if(type.
id()==ID_union)
140 throw "symex_assign_rec: unexpected assignment to union member";
144 "symex_assign_rec: unexpected assignment to member of `"+
147 else if(lhs.
id()==ID_if)
149 state,
to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
150 else if(lhs.
id()==ID_typecast)
153 else if(lhs.
id() == ID_string_constant ||
154 lhs.
id() == ID_null_object ||
155 lhs.
id() ==
"zero_string" ||
156 lhs.
id() ==
"is_zero_string" ||
157 lhs.
id() ==
"zero_string_length")
161 else if(lhs.
id()==ID_byte_extract_little_endian ||
162 lhs.
id()==ID_byte_extract_big_endian)
167 else if(lhs.
id()==ID_complex_real ||
168 lhs.
id()==ID_complex_imag)
176 if(lhs.
id()==ID_complex_real)
188 state, lhs.
op0(), full_lhs, new_rhs, guard, assignment_type);
191 throw "assignment to `"+lhs.
id_string()+
"' not handled";
197 const exprt &full_lhs,
223 tmp_ssa_rhs.
swap(ssa_rhs);
238 exprt ssa_full_lhs=full_lhs;
239 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 with_exprt new_rhs(lhs_array, lhs_index, rhs);
340 new_rhs.
type() = 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() == 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);
413 new_rhs.
op1().
set(ID_component_name, component_name);
418 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
425 const exprt &full_lhs,
440 guard.
add(renamed_guard);
442 state, lhs.
true_case(), full_lhs, rhs, guard, assignment_type);
443 guard.swap(old_guard);
450 state, lhs.
false_case(), full_lhs, rhs, guard, assignment_type);
451 guard.swap(old_guard);
458 const exprt &full_lhs,
468 if(lhs.
id()==ID_byte_extract_little_endian)
469 new_rhs.
id(ID_byte_update_little_endian);
470 else if(lhs.
id()==ID_byte_extract_big_endian)
471 new_rhs.
id(ID_byte_update_big_endian);
481 state, lhs.
op(), new_full_lhs, new_rhs, guard, assignment_type);
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
const bool allow_pointer_unsoundness
const std::string & id2string(const irep_idt &d)
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)
const irep_idt & get_identifier() const
exprt::operandst & designator()
bool constant_propagation
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
The trinary if-then-else operator.
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void do_simplify(exprt &)
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
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
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Expression classes for byte-level operators.
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes...
bool get_bool_option(const std::string &option) const
symex_target_equationt & target
Generic base class for unary expressions.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
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)
write to a variable
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void symex_assign(statet &, const code_assignt &)
void clean_expr(exprt &, statet &, bool write)
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Operator to update elements in structs and arrays.
irep_idt get_object_name() const
const exprt & get_original_expr() const
irep_idt get_component_name() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to mstream using output_generator if the configured verbosity is at least as high as ...
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const std::string & id_string() const
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void add(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const
symex_targett::sourcet source
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)