49 if(index->array().id() == ID_string_constant && index->index().is_zero())
72 if(is_string_constant_init)
83 else if(lhs.
id() == ID_index)
85 else if(lhs.
id()==ID_member)
88 if(type.
id() == ID_struct || type.
id() == ID_struct_tag)
93 else if(type.
id() == ID_union || type.
id() == ID_union_tag)
97 "assign_rec: unexpected assignment to union member");
101 "assign_rec: unexpected assignment to member of '" + type.
id_string() +
104 else if(lhs.
id()==ID_if)
106 else if(lhs.
id()==ID_typecast)
112 else if(lhs.
id()==ID_byte_extract_little_endian ||
113 lhs.
id()==ID_byte_extract_big_endian)
117 else if(lhs.
id() == ID_complex_real)
129 else if(lhs.
id() == ID_complex_imag)
142 "assignment to '" + lhs.
id_string() +
"' not handled");
171 const auto &components =
172 lhs.
type().
id() == ID_struct_tag
179 const auto &comp = comp_rhs.first;
180 const exprt lhs_field =
state.field_sensitivity.apply(
183 lhs_field.
id() == ID_symbol,
184 "member of symbol should be susceptible to field-sensitivity");
202 :
static_cast<exprt>(
if_exprt{conjunction(guard), rhs, lhs}),
224 state.record_events.push(
false);
232 !
check_renaming(l2_full_lhs),
"l2_full_lhs should be renamed to L2");
234 state.record_events.pop();
236 auto current_assignment_type =
250 current_assignment_type);
253 if(
state.field_sensitivity.is_divisible(l1_lhs,
false))
256 state.field_sensitivity.field_assignments(
273 if(rhs.
id() == ID_struct)
292template <
bool use_update>
301 const typet &lhs_index_type = lhs_array.
type();
322 const with_exprt new_rhs{lhs_array, lhs_index, rhs};
329template <
bool use_update>
344 if(lhs_struct.
id()==ID_typecast)
356 if(tmp.
type().
id() == ID_struct || tmp.
type().
id() == ID_struct_tag)
385 new_rhs.
where().
set(ID_component_name, component_name);
419 if(lhs.
id()==ID_byte_extract_little_endian)
421 else if(lhs.
id()==ID_byte_extract_big_endian)
static irep_idt byte_update_id()
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static exprt guard(const exprt::operandst &guards, exprt cond)
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.
Expression in which some part is missing and can be substituted for another expression.
exprt apply(exprt expr) const
Replace the missing part by the given expression, to end-up with a complete 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.
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
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
virtual bool simplify(exprt &expr)
Expression providing an SSA-renamed symbol of expressions.
irep_idt get_object_name() const
Struct constructor from list of elements.
const componentst & components() 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 irep_idt & language_mode
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)
std::optional< shadow_memoryt > shadow_memory
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.
Operator to update elements in structs and arrays.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
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.
#define SHADOW_MEMORY_SYMBOL_PREFIX
#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(exprt a, exprt b)
Conjunction of two expressions.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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.
constexpr bool use_update()
static bool is_string_constant_initialization(const exprt &rhs)
Determine whether the RHS expression is a string constant initialization.
Symbolic Execution of assignments.