35 return path_storage.get_unique_l1_index(l0_name, 1);
45 state.
source.
pc->source_location().get_hide();
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
unsigned atomic_section_id
Threads.
ssa_exprt declare(ssa_exprt ssa, const namespacet &ns)
Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of sy...
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
call_stackt & call_stack()
field_sensitivityt field_sensitivity
symex_targett::sourcet source
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
symex_target_equationt & target
The equation that this execution is building up.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Expression providing an SSA-renamed symbol of expressions.
irep_idt get_object_name() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
Storage of symbolic execution paths to resume.
API to expression classes.
goto_programt::const_targett pc