Loading...

Searching...

No Matches

renaming_level.cpp File Reference

Renaming levels. More...

#include "renaming_level.h"
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/ssa_expr.h>
#include <util/symbol.h>
#include "goto_symex_state.h"

+ Include dependency graph for renaming_level.cpp:

[フレーム]

Go to the source code of this file.

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.

exprt get_original_name (exprt expr)

Undo all levels of renaming.

typet get_original_name (typet type)

Undo all levels of renaming.

bool check_renaming (const typet &type)

Check that type is correctly renamed to level 2 and return true in case an error is detected.

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.

bool check_renaming (const exprt &expr)

Check that expr is correctly renamed to level 2 and return true in case an error is detected.

Detailed Description

Renaming levels.

Definition in file renaming_level.cpp.

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]

exprt get_original_name ( exprt expr )

Undo all levels of renaming.

Definition at line 158 of file renaming_level.cpp.

◆ get_original_name() [2/2]

typet get_original_name ( typet type )

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 22 of file renaming_level.cpp.