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)
59 throw "printf: unexpected assignment";
62 else if(statement==ID_gcc_builtin_va_arg_next)
65 throw "symex_assign: unexpected side effect: "+
id2string(statement);
72 if(lhs.
id()==ID_symbol &&
74 "#return_value!")!=std::string::npos)
82 if(state.
source.
pc->source_location.get_hide())
94 assert(lhs.
id()!=ID_symbol);
97 if(tmp_what.id()!=ID_symbol)
99 assert(tmp_what.operands().size()>=1);
109 assert(p->
id()!=ID_symbol);
123 const exprt &full_lhs,
128 if(lhs.
id()==ID_symbol &&
131 state,
to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
132 else if(lhs.
id()==ID_index)
134 state,
to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
135 else if(lhs.
id()==ID_member)
138 if(type.
id()==ID_struct)
140 state,
to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
141 else if(type.
id()==ID_union)
144 throw "symex_assign_rec: unexpected assignment to union member";
148 "symex_assign_rec: unexpected assignment to member of `"+
151 else if(lhs.
id()==ID_if)
153 state,
to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
154 else if(lhs.
id()==ID_typecast)
157 else if(lhs.
id() == ID_string_constant ||
158 lhs.
id() == ID_null_object ||
159 lhs.
id() ==
"zero_string" ||
160 lhs.
id() ==
"is_zero_string" ||
161 lhs.
id() ==
"zero_string_length")
165 else if(lhs.
id()==ID_byte_extract_little_endian ||
166 lhs.
id()==ID_byte_extract_big_endian)
171 else if(lhs.
id()==ID_complex_real ||
172 lhs.
id()==ID_complex_imag)
180 if(lhs.
id()==ID_complex_real)
192 state, lhs.
op0(), full_lhs, new_rhs, guard, assignment_type);
195 throw "assignment to `"+lhs.
id_string()+
"' not handled";
201 const exprt &full_lhs,
227 tmp_ssa_rhs.
swap(ssa_rhs);
242 exprt ssa_full_lhs=full_lhs;
243 ssa_full_lhs=
add_to_lhs(ssa_full_lhs, ssa_lhs);
279 const exprt &full_lhs,
288 exprt rhs_typecasted=rhs;
294 state, lhs.
op0(), new_full_lhs, rhs_typecasted, guard, assignment_type);
300 const exprt &full_lhs,
310 throw "index must have two operands";
316 if(lhs_type.
id()!=ID_array)
317 throw "index must take array type operand, but got `"+
328 new_rhs.
old()=lhs_array;
335 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
343 with_exprt new_rhs(lhs_array, lhs_index, rhs);
344 new_rhs.
type() = lhs_type;
349 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
356 const exprt &full_lhs,
369 if(lhs_struct.
id()==ID_typecast)
371 assert(lhs_struct.
operands().size()==1);
373 if(lhs_struct.
op0().
id() == ID_null_object)
384 if(op0_type.
id()==ID_struct)
401 new_rhs.
old()=lhs_struct;
403 new_rhs.new_value()=rhs;
408 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
417 new_rhs.
op1().
set(ID_component_name, component_name);
422 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
429 const exprt &full_lhs,
444 guard.
add(renamed_guard);
446 state, lhs.
true_case(), full_lhs, rhs, guard, assignment_type);
447 guard.swap(old_guard);
454 state, lhs.
false_case(), full_lhs, rhs, guard, assignment_type);
455 guard.swap(old_guard);
462 const exprt &full_lhs,
472 if(lhs.
id()==ID_byte_extract_little_endian)
473 new_rhs.
id(ID_byte_update_little_endian);
474 else if(lhs.
id()==ID_byte_extract_big_endian)
475 new_rhs.
id(ID_byte_update_big_endian);
485 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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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
virtual void symex_printf(statet &, const exprt &rhs)
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
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)