34 if(rhs.
id()==ID_side_effect)
39 if(statement==ID_function_call)
41 const auto &function_call =
45 !side_effect_expr.
operands().empty(),
46 "function call statement expects non-empty list of side effects");
49 function_call.function().id() == ID_symbol,
50 "expected symbol as function");
56 "symex_assign: unexpected function call: " +
id2string(identifier));
59 statement == ID_cpp_new || statement == ID_cpp_new_array ||
60 statement == ID_java_new_array_data)
62 else if(statement==ID_allocate)
64 else if(statement==ID_printf)
69 else if(statement==ID_gcc_builtin_va_arg_next)
79 if(lhs.
id()==ID_symbol &&
81 "#return_value!")!=std::string::npos)
89 if(state.
source.
pc->source_location.get_hide())
104 if(tmp_what.id()!=ID_symbol)
107 tmp_what.op0().make_nil();
117 p->
id() != ID_symbol,
118 "expected pointed-to expression not to be a symbol");
121 "expected pointed-to expression to have at least one operand");
134 const exprt &full_lhs,
139 if(lhs.
id()==ID_symbol &&
142 state,
to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
143 else if(lhs.
id()==ID_index)
145 state,
to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
146 else if(lhs.
id()==ID_member)
149 if(type.
id()==ID_struct)
151 state,
to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
152 else if(type.
id()==ID_union)
156 "symex_assign_rec: unexpected assignment to union member");
160 "symex_assign_rec: unexpected assignment to member of `" +
163 else if(lhs.
id()==ID_if)
165 state,
to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
166 else if(lhs.
id()==ID_typecast)
169 else if(lhs.
id() == ID_string_constant ||
170 lhs.
id() == ID_null_object ||
171 lhs.
id() ==
"zero_string" ||
172 lhs.
id() ==
"is_zero_string" ||
173 lhs.
id() ==
"zero_string_length")
177 else if(lhs.
id()==ID_byte_extract_little_endian ||
178 lhs.
id()==ID_byte_extract_big_endian)
183 else if(lhs.
id() == ID_complex_real)
194 state, complex_real_expr.
op(), full_lhs, new_rhs, guard, assignment_type);
196 else if(lhs.
id() == ID_complex_imag)
206 state, complex_imag_expr.
op(), full_lhs, new_rhs, guard, assignment_type);
210 "assignment to `" + lhs.
id_string() +
"' not handled");
216 const exprt &full_lhs,
242 tmp_ssa_rhs.
swap(ssa_rhs);
257 exprt ssa_full_lhs=full_lhs;
258 ssa_full_lhs=
add_to_lhs(ssa_full_lhs, ssa_lhs);
296 const exprt &full_lhs,
302 exprt rhs_typecasted=rhs;
308 state, lhs.
op(), new_full_lhs, rhs_typecasted, guard, assignment_type);
314 const exprt &full_lhs,
333 new_rhs.old()=lhs_array;
335 new_rhs.new_value()=rhs;
340 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
348 with_exprt new_rhs(lhs_array, lhs_index, rhs);
349 new_rhs.
type() = lhs_index_type;
354 state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
361 const exprt &full_lhs,
374 if(lhs_struct.
id()==ID_typecast)
387 if(op0_type.
id()==ID_struct)
404 new_rhs.
old()=lhs_struct;
406 new_rhs.new_value()=rhs;
411 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
420 new_rhs.
where().
set(ID_component_name, component_name);
425 state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
432 const exprt &full_lhs,
447 guard.
add(renamed_guard);
449 state, lhs.
true_case(), full_lhs, rhs, guard, assignment_type);
450 guard.swap(old_guard);
457 state, lhs.
false_case(), full_lhs, rhs, guard, assignment_type);
458 guard.swap(old_guard);
465 const exprt &full_lhs,
475 if(lhs.
id()==ID_byte_extract_little_endian)
476 new_rhs.
id(ID_byte_update_little_endian);
477 else if(lhs.
id()==ID_byte_extract_big_endian)
478 new_rhs.
id(ID_byte_update_big_endian);
488 state, lhs.
op(), new_full_lhs, new_rhs, guard, assignment_type);
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression, extends irept.
bool constant_propagation
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)
Semantic type conversion.
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)
Copy the given argument to the end of exprt's operands.
const irep_idt & get_identifier() const
bool is_false() const
Return whether the expression is a constant representing false.
Thrown when we encounter an instruction, parameters to an instruction etc.
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.
bool is_true() const
Return whether the expression is a constant representing true.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
typet & type()
Return the type of the expression.
virtual void do_simplify(exprt &)
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)
Imaginary part of the expression describing a complex number.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
const irep_idt get_level_1() const
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
Store the what expression by recursively descending into the operands of lhs until the first operand ...
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.
Real part of the expression describing a complex number.
symex_target_equationt & target
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an 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 local variable.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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)
const symex_configt symex_config
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
bool allow_pointer_unsoundness
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
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)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#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.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Expression providing an SSA-renamed symbol of expressions.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
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 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)