symex_level2t Struct Reference
Functor to set the level 2 renaming of SSA expressions. More...
#include <renaming_level.h>
Collaboration diagram for symex_level2t:Public Member Functions | |
| renamedt< ssa_exprt, L2 > | operator() (renamedt< ssa_exprt, L1 > l1_expr) const |
Set L2 tag to correspond to the current count of the identifier of l1_expr's. More... | |
| unsigned | latest_index (const irep_idt &identifier) const |
| Counter corresponding to an identifier. More... | |
| std::size_t | increase_generation (const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider) |
| Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this path. More... | |
Public Attributes | |
| symex_renaming_levelt | current_names |
Detailed Description
Functor to set the level 2 renaming of SSA expressions.
Level 2 corresponds to SSA. This is to ensure each variable is only assigned once.
Definition at line 68 of file renaming_level.h.
Member Function Documentation
◆ increase_generation()
| std::size_t symex_level2t::increase_generation | ( | const irep_idt & | l1_identifier, |
| const ssa_exprt & | lhs, | ||
| std::function< std::size_t(const irep_idt &)> | fresh_l2_name_provider | ||
| ) |
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this path.
Definition at line 137 of file renaming_level.cpp.
◆ latest_index()
| unsigned symex_level2t::latest_index | ( | const irep_idt & | identifier | ) | const |
Counter corresponding to an identifier.
Definition at line 131 of file renaming_level.cpp.
◆ operator()()
Set L2 tag to correspond to the current count of the identifier of l1_expr's.
Definition at line 101 of file renaming_level.cpp.
Member Data Documentation
◆ current_names
| symex_renaming_levelt symex_level2t::current_names |
Definition at line 70 of file renaming_level.h.
The documentation for this struct was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-symex/renaming_level.h
- /home/runner/work/cbmc/cbmc/src/goto-symex/renaming_level.cpp
