cprover
|
Renaming levels. More...
#include "renaming_level.h"
#include <util/namespace.h>
#include <util/ssa_expr.h>
#include <util/symbol.h>
#include "goto_symex_state.h"
Go to the source code of this file.
Functions | |
void | get_variables (const symex_renaming_levelt ¤t_names, std::unordered_set< ssa_exprt, irep_hash > &vars) |
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 typet &type) |
Check that type 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 exprt &expr) |
Check that expr is correctly renamed to level 2 and return true in case an error is detected. More... | |
Renaming levels.
Definition in file renaming_level.cpp.
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 250 of file renaming_level.cpp.
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 209 of file renaming_level.cpp.
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 225 of file renaming_level.cpp.
Undo all levels of renaming.
Definition at line 169 of file renaming_level.cpp.
Undo all levels of renaming.
Definition at line 183 of file renaming_level.cpp.
void get_variables | ( | const symex_renaming_levelt & | current_names, |
std::unordered_set< ssa_exprt, irep_hash > & | vars | ||
) |
Definition at line 20 of file renaming_level.cpp.
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 34 of file renaming_level.cpp.