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