12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 16 #include <unordered_set> 86 bool rhs_is_simplified,
88 bool allow_pointer_unsoundness=
false);
140 std::unordered_set<ssa_exprt, irep_hash> &vars)
const 143 vars.insert(pair.second.first);
169 typedef std::map<goto_programt::const_targett, goto_state_listt>
238 std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
286 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression, extends irept.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
goto_statet(const goto_symex_statet &s)
std::map< irep_idt, unsigned > function_frame
Generate Equation using Symbolic Execution.
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
void level2_get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
Variables whose address is taken.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool run_validation_checks
Should the additional validation checks be run?
unsigned atomic_section_id
std::map< irep_idt, exprt > propagation
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
symex_target_equationt * symex_target
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
goto_state_mapt goto_state_map
void set_l1_indices(ssa_exprt &expr, const namespacet &ns)
goto_programt::const_targett end_of_function
std::map< irep_idt, exprt > propagation
void get_original_name(exprt &expr) const
unsigned level2_current_count(const irep_idt &identifier) const
unsigned depth
distance from entry
goto_programt::const_targett pc
irep_idt function_identifier
unsigned atomic_section_id
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
std::set< irep_idt > l1_history
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
void set_l0_indices(ssa_exprt &expr, const namespacet &ns)
Identifies source in the context of symbolic execution.
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
symex_targett::sourcet calling_location
const framet & top() const
API to expression classes.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
std::vector< threadt > threads
Functor to set the level 2 renaming of SSA expressions.
current_namest current_names
std::unordered_map< irep_idt, loop_infot > loop_iterations
State type in value_set_domaint, used in value-set analysis and goto-symex.
std::set< irep_idt > local_objects
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void set_l2_indices(ssa_exprt &expr, const namespacet &ns)
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
const framet & previous_frame()
unsigned atomic_section_id
goto_symex_statet(const goto_symex_statet &other, symex_target_equationt *const target)
Fake "copy constructor" that initializes the symex_target member.
std::list< guardt > a_s_w_entryt
std::unordered_map< irep_idt, typet > l1_typest
std::vector< framet > call_stackt
std::map< irep_idt, goto_programt::targett > catch_map
symex_level2t::current_namest level2_current_names
goto_programt::const_targett saved_target
Base class for all expressions.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
call_stackt & call_stack()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
Local safe pointer analysis.
std::map< goto_programt::const_targett, goto_state_listt > goto_state_mapt
goto_symex_statet(const goto_statet &s)
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
const call_stackt & call_stack() const
symex_renaming_levelt::current_namest old_level1
Functor to set the level 0 renaming of SSA expressions.
std::list< goto_statet > goto_state_listt
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source
Functor to set the level 1 renaming of SSA expressions.
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source