Container for data that varies per program point, e.g. More...
#include <goto_state.h>
Inheritance diagram for goto_statet: Collaboration diagram for goto_statet:Public Member Functions | |
| const symex_level2t & | get_level2 () const |
| void | output_propagation_map (std::ostream &) |
| Print the constant propagation map in a human-friendly format. More... | |
| goto_statet ()=delete | |
| Constructors. More... | |
| goto_statet & | operator= (const goto_statet &other)=delete |
| goto_statet & | operator= (goto_statet &&other)=default |
| goto_statet (const goto_statet &other)=default | |
| goto_statet (goto_statet &&other)=default | |
| goto_statet (guard_managert &guard_manager) | |
| void | apply_condition (const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns) |
| Given a condition that must hold on this path, propagate as much knowledge as possible. More... | |
Public Attributes | |
| unsigned | depth = 0 |
| Distance from entry. More... | |
| sharing_mapt< exprt, symbol_exprt, false, irep_hash > | dereference_cache |
| This is used for eliminating repeated complicated dereferences. More... | |
| value_sett | value_set |
| Uses level 1 names, and is used to do dereferencing. More... | |
| guardt | guard |
| bool | reachable |
| Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual. More... | |
| sharing_mapt< irep_idt, exprt > | propagation |
| unsigned | atomic_section_id = 0 |
| Threads. More... | |
Protected Attributes | |
| symex_level2t | level2 |
Detailed Description
Container for data that varies per program point, e.g.
the constant propagator state, when state needs to branch. This is copied out of goto_symex_statet at a control-flow fork and then back into it at a control-flow merge.
Definition at line 31 of file goto_state.h.
Constructor & Destructor Documentation
◆ goto_statet() [1/4]
|
delete |
Constructors.
◆ goto_statet() [2/4]
|
default |
◆ goto_statet() [3/4]
|
default |
◆ goto_statet() [4/4]
|
inlineexplicit |
Definition at line 85 of file goto_state.h.
Member Function Documentation
◆ apply_condition()
| void goto_statet::apply_condition | ( | const exprt & | condition, |
| const goto_symex_statet & | previous_state, | ||
| const namespacet & | ns | ||
| ) |
Given a condition that must hold on this path, propagate as much knowledge as possible.
For example, if the condition is (x == 5), whether that's an assumption or a GOTO condition that we just passed through, we can propagate the constant '5' for future 'x' references. If the condition is (y == &o1) then we can use that to populate the value set.
- Parameters
-
condition condition that must hold on this path. Expected to already be L2-renamed. previous_state currently active state, not necessarily the same as *this. For a GOTO instruction this is the state immediately preceding the branch while *this is the state that will be used on the taken- or not-taken path. For an ASSUME instruction previous_stateand *this are equal.ns global namespace
Definition at line 43 of file goto_state.cpp.
◆ get_level2()
|
inline |
Definition at line 45 of file goto_state.h.
◆ operator=() [1/2]
|
delete |
◆ operator=() [2/2]
|
default |
◆ output_propagation_map()
| void goto_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 19 of file goto_state.cpp.
Member Data Documentation
◆ atomic_section_id
| unsigned goto_statet::atomic_section_id = 0 |
Threads.
Definition at line 76 of file goto_state.h.
◆ depth
| unsigned goto_statet::depth = 0 |
Distance from entry.
Definition at line 35 of file goto_state.h.
◆ dereference_cache
| sharing_mapt<exprt, symbol_exprt, false, irep_hash> goto_statet::dereference_cache |
This is used for eliminating repeated complicated dereferences.
- See also
- goto_symext::dereference_rec
Definition at line 43 of file goto_state.h.
◆ guard
| guardt goto_statet::guard |
Definition at line 58 of file goto_state.h.
◆ level2
|
protected |
Definition at line 38 of file goto_state.h.
◆ propagation
| sharing_mapt<irep_idt, exprt> goto_statet::propagation |
Definition at line 71 of file goto_state.h.
◆ reachable
| bool goto_statet::reachable |
Is this code reachable? If not we can take shortcuts such as not entering function calls, but we still conduct guard arithmetic as usual.
Definition at line 62 of file goto_state.h.
◆ value_set
| value_sett goto_statet::value_set |
Uses level 1 names, and is used to do dereferencing.
Definition at line 51 of file goto_state.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-symex/goto_state.h
- /home/runner/work/cbmc/cbmc/src/goto-symex/goto_state.cpp
