12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 16 #include <unordered_set> 76 current_namest::const_iterator it=
87 void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars)
const 92 vars.insert(it->second.first);
119 for(current_namest::const_iterator
131 it->second=ito->second;
177 bool rhs_is_simplified,
179 bool allow_pointer_unsoundness=
false);
228 std::unordered_set<ssa_exprt, irep_hash> &vars)
const 230 for(level2t::current_namest::const_iterator
234 vars.insert(it->second.first);
239 level2t::current_namest::const_iterator it=
258 typedef std::map<goto_programt::const_targett, goto_state_listt>
287 typedef std::map<irep_idt, goto_programt::targett>
catch_mapt;
339 typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash>
342 typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
399 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression.
std::map< irep_idt, irep_idt > original_identifierst
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)
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
class goto_symex_statet::propagationt propagation
level2t::current_namest level2_current_names
read_in_atomic_sectiont read_in_atomic_section
Variables whose address is taken.
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void operator()(exprt &expr)
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
symex_target_equationt * symex_target
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
written_in_atomic_sectiont written_in_atomic_section
loop_iterationst loop_iterations
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
void switch_to_thread(unsigned t)
void restore_from(const current_namest &other)
void get_original_name(exprt &expr) const
std::set< irep_idt > l1_historyt
unsigned level2_current_count(const irep_idt &identifier) const
bool constant_propagation(const exprt &expr) const
This function determines what expressions are to be propagated as "constants".
unsigned depth
distance from entry
goto_symex_statet::level2t level2
std::map< irep_idt, exprt > valuest
unsigned atomic_section_id
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_sectiont
local_objectst local_objects
void populate_dirty_for_function(const irep_idt &id, const goto_functiont &)
std::set< irep_idt > local_objectst
const framet & top() const
API to expression classes.
instructionst::const_iterator const_targett
std::map< irep_idt, goto_programt::targett > catch_mapt
std::map< irep_idt, unsigned > function_frame
#define PRECONDITION(CONDITION)
goto_symex_statet::level1t level1
unsigned atomic_section_id
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
State type in value_set_domaint, used in value-set analysis and goto-symex.
goto_state_mapt goto_state_map
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
current_namest current_names
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, loop_infot > loop_iterationst
std::unordered_map< irep_idt, typet > l1_typest
bool saved_target_is_backwards
std::vector< framet > call_stackt
irep_idt function_identifier
void get_l1_name(exprt &expr) const
void operator()(ssa_exprt &ssa_expr)
unsigned current_count(const irep_idt &identifier) const
goto_programt::const_targett saved_target
Base class for all expressions.
call_stackt & call_stack()
virtual ~renaming_levelt()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
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.
const call_stackt & call_stack() const
symex_targett::sourcet calling_location
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_sectiont
goto_programt::const_targett pc
std::list< goto_statet > goto_state_listt
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source
std::vector< threadt > threadst
goto_programt::const_targett end_of_function
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source