#include <goto_symex_state.h>
|
| goto_symex_statet () |
|
| ~goto_symex_statet () |
|
| goto_symex_statet (const goto_symex_statet &other, symex_target_equationt *const target) |
| Fake "copy constructor" that initializes the symex_target member. More...
|
|
void | output_propagation_map (std::ostream &) |
| Print the constant propagation map in a human-friendly format. More...
|
|
void | rename (exprt &expr, const namespacet &ns, levelt level=L2) |
|
void | rename (typet &type, const irep_idt &l1_identifier, const namespacet &ns, levelt level=L2) |
|
void | assignment (ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false) |
|
void | get_original_name (exprt &expr) const |
|
void | get_original_name (typet &type) const |
|
| goto_symex_statet (const goto_statet &s) |
|
call_stackt & | call_stack () |
|
const call_stackt & | call_stack () const |
|
framet & | top () |
|
const framet & | top () const |
|
framet & | new_frame () |
|
void | pop_frame () |
|
const framet & | previous_frame () |
|
void | print_backtrace (std::ostream &) const |
| Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread. More...
|
|
bool | l2_thread_read_encoding (ssa_exprt &expr, const namespacet &ns) |
| thread encoding More...
|
|
bool | l2_thread_write_encoding (const ssa_exprt &expr, const namespacet &ns) |
| thread encoding More...
|
|
Definition at line 34 of file goto_symex_state.h.
◆ a_s_r_entryt
◆ a_s_w_entryt
◆ call_stackt
◆ goto_state_listt
◆ goto_state_mapt
◆ l1_typest
◆ levelt
◆ goto_symex_statet() [1/4]
goto_symex_statet::goto_symex_statet |
( |
| ) |
|
◆ ~goto_symex_statet()
goto_symex_statet::~goto_symex_statet |
( |
| ) |
|
|
default |
◆ goto_symex_statet() [2/4]
Fake "copy constructor" that initializes the symex_target
member.
Definition at line 41 of file goto_symex_state.h.
◆ goto_symex_statet() [3/4]
goto_symex_statet::goto_symex_statet |
( |
const goto_statet & |
s | ) |
|
|
inlineexplicit |
◆ goto_symex_statet() [4/4]
Dangerous, do not use.
Copying a state S1 to S2 risks S2 pointing to a deallocated symex_target_equationt if S1 (and the symex_target_equationt that its symex_target
member points to) go out of scope. If your class has a goto_symex_statet member and needs a copy constructor, copy instances of this class using the public two-argument copy constructor constructor to ensure that the copy points to an allocated symex_target_equationt. The two-argument copy constructor uses this private copy constructor as a delegate.
◆ assignment()
void goto_symex_statet::assignment |
( |
ssa_exprt & |
lhs, |
|
|
const exprt & |
rhs, |
|
|
const namespacet & |
ns, |
|
|
bool |
rhs_is_simplified, |
|
|
bool |
record_value, |
|
|
bool |
allow_pointer_unsoundness = false |
|
) |
| |
◆ call_stack() [1/2]
◆ call_stack() [2/2]
const call_stackt& goto_symex_statet::call_stack |
( |
| ) |
const |
|
inline |
◆ get_original_name() [1/2]
void goto_symex_statet::get_original_name |
( |
exprt & |
expr | ) |
const |
◆ get_original_name() [2/2]
void goto_symex_statet::get_original_name |
( |
typet & |
type | ) |
const |
◆ l2_thread_read_encoding()
◆ l2_thread_write_encoding()
bool goto_symex_statet::l2_thread_write_encoding |
( |
const ssa_exprt & |
expr, |
|
|
const namespacet & |
ns |
|
) |
| |
◆ new_frame()
framet& goto_symex_statet::new_frame |
( |
| ) |
|
|
inline |
◆ output_propagation_map()
void goto_symex_statet::output_propagation_map |
( |
std::ostream & |
out | ) |
|
Print the constant propagation map in a human-friendly format.
This is primarily for use from the debugger; please don't delete me just because there aren't any current callers.
Definition at line 799 of file goto_symex_state.cpp.
◆ pop_frame()
void goto_symex_statet::pop_frame |
( |
| ) |
|
|
inline |
◆ previous_frame()
const framet& goto_symex_statet::previous_frame |
( |
| ) |
|
|
inline |
◆ print_backtrace()
void goto_symex_statet::print_backtrace |
( |
std::ostream & |
out | ) |
const |
Dumps the current state of symex, printing the function name and location number for each stack frame in the currently active thread.
This is for use from the debugger or in debug code; please don't delete it just because it isn't called at present.
- Parameters
-
Definition at line 772 of file goto_symex_state.cpp.
◆ rename() [1/2]
◆ rename() [2/2]
◆ rename_address()
◆ set_l0_indices()
◆ set_l1_indices()
◆ set_l2_indices()
◆ top() [1/2]
framet& goto_symex_statet::top |
( |
| ) |
|
|
inline |
◆ top() [2/2]
const framet& goto_symex_statet::top |
( |
| ) |
const |
|
inline |
◆ atomic_section_id
unsigned goto_symex_statet::atomic_section_id |
◆ depth
unsigned goto_symex_statet::depth |
◆ dirty
◆ guard
guardt goto_symex_statet::guard |
◆ has_saved_jump_target
bool goto_symex_statet::has_saved_jump_target |
This state is saved, with the PC pointing to the target of a GOTO.
Definition at line 263 of file goto_symex_state.h.
◆ has_saved_next_instruction
bool goto_symex_statet::has_saved_next_instruction |
This state is saved, with the PC pointing to the next instruction of a GOTO.
Definition at line 267 of file goto_symex_state.h.
◆ l1_history
std::set<irep_idt> goto_symex_statet::l1_history |
◆ l1_types
◆ level0
◆ level1
◆ level2
◆ propagation
◆ read_in_atomic_section
◆ record_events
bool goto_symex_statet::record_events |
◆ remaining_vccs
unsigned goto_symex_statet::remaining_vccs |
◆ run_validation_checks
bool goto_symex_statet::run_validation_checks |
◆ safe_pointers
◆ saved_target
◆ source
◆ symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
The names in this table are needed for error traces even after symbolic execution has finished.
Definition at line 52 of file goto_symex_state.h.
◆ symex_target
◆ threads
std::vector<threadt> goto_symex_statet::threads |
◆ total_vccs
unsigned goto_symex_statet::total_vccs |
◆ value_set
◆ written_in_atomic_section
The documentation for this class was generated from the following files: