46 else if(lhs.
id() == ID_index)
47 assign_array<use_update()>(
to_index_expr(lhs), full_lhs, rhs, guard);
48 else if(lhs.
id()==ID_member)
51 if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
53 assign_struct_member<use_update()>(
56 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
60 "assign_rec: unexpected assignment to union member");
64 "assign_rec: unexpected assignment to member of '" + type.
id_string() +
67 else if(lhs.
id()==ID_if)
69 else if(lhs.
id()==ID_typecast)
75 else if(lhs.
id()==ID_byte_extract_little_endian ||
76 lhs.
id()==ID_byte_extract_big_endian)
80 else if(lhs.
id() == ID_complex_real)
90 assign_rec(complex_real_expr.
op(), full_lhs, new_rhs, guard);
92 else if(lhs.
id() == ID_complex_imag)
101 assign_rec(complex_imag_expr.
op(), full_lhs, new_rhs, guard);
105 "assignment to '" + lhs.
id_string() +
"' not handled");
139 const auto &comp = comp_rhs.first;
143 lhs_field.
id() == ID_symbol,
144 "member of symbol should be susceptible to field-sensitivity");
162 :
static_cast<exprt>(
if_exprt{conjunction(guard), rhs, lhs}),
185 const exprt l2_full_lhs = assignment.original_lhs_skeleton.apply(l2_lhs);
189 !
check_renaming(l2_full_lhs),
"l2_full_lhs should be renamed to L2");
193 auto current_assignment_type =
205 current_assignment_type);
207 const ssa_exprt &l1_lhs = assignment.lhs;
228 if(rhs.
id() == ID_struct)
244 assign_rec(lhs.
op(), new_skeleton, rhs_typecasted, guard);
247template <
bool use_update>
256 const typet &lhs_index_type = lhs_array.
type();
269 assign_rec(lhs, new_skeleton, new_rhs, guard);
277 const with_exprt new_rhs{lhs_array, lhs_index, rhs};
280 assign_rec(lhs_array, new_skeleton, new_rhs, guard);
284template <
bool use_update>
299 if(lhs_struct.
id()==ID_typecast)
311 if(tmp.
type().
id() == ID_struct || tmp.
type().
id() == ID_struct_tag)
330 assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
340 new_rhs.
where().
set(ID_component_name, component_name);
343 assign_rec(lhs_struct, new_skeleton, new_rhs, guard);
355 guard.push_back(lhs.
cond());
374 if(lhs.
id()==ID_byte_extract_little_endian)
376 else if(lhs.
id()==ID_byte_extract_big_endian)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Expression in which some part is missing and can be substituted for another expression.
expr_skeletont compose(expr_skeletont other) const
Replace the missing part of the current skeleton by another skeleton, ending in a bigger skeleton cor...
static expr_skeletont remove_op0(exprt e)
Create a skeleton by removing the first operand of e.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
void field_assignments(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &lhs, symex_targett &target, bool allow_pointer_unsoundness)
Assign to the individual fields of a non-expanded symbol lhs.
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
sharing_mapt< irep_idt, exprt > propagation
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
std::stack< bool > record_events
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
The trinary if-then-else operator.
void set(const irep_idt &name, const irep_idt &value)
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression providing an SSA-renamed symbol of expressions.
irep_idt get_object_name() const
Struct constructor from list of elements.
const componentst & components() const
const irep_idt & get_identifier() const
void assign_byte_extract(const byte_extract_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_if(const if_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
const symex_configt & symex_config
void assign_non_struct_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
goto_symex_statet & state
void assign_array(const index_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_rec(const exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
void assign_struct_member(const member_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
symex_targett::assignment_typet assignment_type
void assign_from_struct(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const struct_exprt &rhs, const exprt::operandst &guard)
Assign a struct expression to a symbol.
void assign_typecast(const typecast_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, exprt::operandst &guard)
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
Write to a local variable.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Thrown when we encounter an instruction, parameters to an instruction etc.
Operator to update elements in structs and arrays.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
Operator to update elements in structs and arrays.
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Deprecated expression utility functions.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt get_original_name(exprt expr)
Undo all levels of renaming.
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Assignment from the rhs value to the lhs variable.
expr_skeletont original_lhs_skeleton
Skeleton to reconstruct the original lhs in the assignment.
bool allow_pointer_unsoundness
bool constant_propagation
bool run_validation_checks
Should the additional validation checks be run? If this flag is set the checks for renaming (both lev...
constexpr bool use_update()
Symbolic Execution of assignments.
static irep_idt byte_update_id()