12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H 16 #include <unordered_set> 61 current_namest::const_iterator it=
62 current_names.find(identifier);
63 return it==current_names.end()?0:it->second.second;
68 assert(current_names.find(identifier)!=current_names.end());
69 ++current_names[identifier].second;
72 void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars)
const 74 for(current_namest::const_iterator it=current_names.begin();
75 it!=current_names.end();
77 vars.insert(it->second.first);
104 for(current_namest::const_iterator
115 assert(it->first==ito->first);
116 it->second=ito->second;
140 void operator()(
exprt &expr);
144 values.erase(identifier);
162 bool rhs_is_simplified,
180 typedef std::unordered_map<irep_idt, typet, irep_id_hash>
l1_typest;
202 value_set(s.value_set),
205 propagation(s.propagation),
206 atomic_section_id(s.atomic_section_id)
212 std::unordered_set<ssa_exprt, irep_hash> &vars)
const 214 for(level2t::current_namest::const_iterator
215 it=level2_current_names.begin();
216 it!=level2_current_names.end();
218 vars.insert(it->second.first);
223 level2t::current_namest::const_iterator it=
224 level2_current_names.find(identifier);
225 return it==level2_current_names.end()?0:it->second.second;
231 typedef std::map<goto_programt::const_targett, goto_state_listt>
255 hidden_function(false)
260 typedef std::map<irep_idt, goto_programt::targett>
catch_mapt;
275 typedef std::unordered_map<irep_idt, loop_infot, irep_id_hash>
313 typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash>
316 typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
347 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
The type of an expression.
std::map< irep_idt, irep_idt > original_identifierst
goto_statet(const goto_symex_statet &s)
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
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Goto Programs with Functions.
Generate Equation using Symbolic Execution.
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
symex_targett * symex_target
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".
goto_symex_statet::level2t level2
void initialize(const goto_functionst &goto_functions)
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
instructionst::const_iterator const_targett
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_sectiont
local_objectst local_objects
std::set< irep_idt > local_objectst
const framet & top() const
API to expression classes.
std::map< irep_idt, goto_programt::targett > catch_mapt
std::map< irep_idt, unsigned > function_frame
goto_symex_statet::level1t level1
unsigned atomic_section_id
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
goto_state_mapt goto_state_map
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
std::list< guardt > a_s_w_entryt
std::vector< framet > call_stackt
irep_idt function_identifier
void get_l1_name(exprt &expr) const
unsigned current_count(const irep_idt &identifier) const
Base class for all expressions.
std::unordered_map< irep_idt, typet, irep_id_hash > l1_typest
call_stackt & call_stack()
virtual ~renaming_levelt()
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
std::map< goto_programt::const_targett, goto_state_listt > goto_state_mapt
const call_stackt & call_stack() const
symex_targett::sourcet calling_location
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
std::unordered_map< irep_idt, loop_infot, irep_id_hash > loop_iterationst
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