Skip to content

Commit 58f0771

Browse files
Introduce renamedt type for result of rename
This is a wrapper that will be used to signal that an expression or type has been renamed to a given level. It makes it possible to define functions which only accept expression which have been through renaming.
1 parent 9f62e4f commit 58f0771

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/goto-symex/renaming_level.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,16 @@ struct symex_renaming_levelt
5454
}
5555
};
5656

57+
/// Wrapper for expressions or types that have been renamed at level0
58+
template <typename underlyingt, levelt level>
59+
struct renamedt
60+
{
61+
static_assert(
62+
std::is_base_of<exprt, underlyingt>::value || std::is_base_of<typet, underlyingt>::value,
63+
"underlyingt should inherit from exprt or typet");
64+
underlyingt expr;
65+
};
66+
5767
/// Functor to set the level 0 renaming of SSA expressions.
5868
/// Level 0 corresponds to threads.
5969
/// The renaming is built for one particular interleaving.

0 commit comments

Comments
 (0)