Renaming levels. More...
Include dependency graph for renaming_level.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| struct | symex_level1t |
| Functor to set the level 1 renaming of SSA expressions. More... | |
| struct | symex_level2t |
| Functor to set the level 2 renaming of SSA expressions. More... | |
Typedefs | |
| using | symex_renaming_levelt = sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > > |
Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter. More... | |
Functions | |
| renamedt< ssa_exprt, L0 > | symex_level0 (ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr) |
| Set the level 0 renaming of SSA expressions. More... | |
| exprt | get_original_name (exprt expr) |
| Undo all levels of renaming. More... | |
| typet | get_original_name (typet type) |
| Undo all levels of renaming. More... | |
| bool | check_renaming (const exprt &expr) |
Check that expr is correctly renamed to level 2 and return true in case an error is detected. More... | |
| bool | check_renaming_l1 (const exprt &expr) |
Check that expr is correctly renamed to level 1 and return true in case an error is detected. More... | |
| bool | check_renaming (const typet &type) |
Check that type is correctly renamed to level 2 and return true in case an error is detected. More... | |
Detailed Description
Renaming levels.
Definition in file renaming_level.h.
Typedef Documentation
◆ symex_renaming_levelt
| using symex_renaming_levelt = sharing_mapt<irep_idt, std::pair<ssa_exprt, std::size_t> > |
Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.
This is extended by the different symex_level structures which are used during symex to ensure static single assignment (SSA) form.
Definition at line 24 of file renaming_level.h.
Function Documentation
◆ check_renaming() [1/2]
| bool check_renaming | ( | const exprt & | expr | ) |
Check that expr is correctly renamed to level 2 and return true in case an error is detected.
Definition at line 242 of file renaming_level.cpp.
◆ check_renaming() [2/2]
| bool check_renaming | ( | const typet & | type | ) |
Check that type is correctly renamed to level 2 and return true in case an error is detected.
Definition at line 199 of file renaming_level.cpp.
◆ check_renaming_l1()
| bool check_renaming_l1 | ( | const exprt & | expr | ) |
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
Definition at line 215 of file renaming_level.cpp.
◆ get_original_name() [1/2]
Undo all levels of renaming.
Definition at line 158 of file renaming_level.cpp.
◆ get_original_name() [2/2]
Undo all levels of renaming.
Definition at line 172 of file renaming_level.cpp.
◆ symex_level0()
| renamedt<ssa_exprt, L0> symex_level0 | ( | ssa_exprt | ssa_expr, |
| const namespacet & | ns, | ||
| std::size_t | thread_nr | ||
| ) |
Set the level 0 renaming of SSA expressions.
Level 0 corresponds to threads. The renaming is built for one particular interleaving. Rename ssa_expr using thread_nr as L0 tag, unless ssa_expr is a guard, a shared variable or a function. ns is queried to decide whether we are in one of these cases.
Definition at line 60 of file renaming_level.cpp.
