ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
renaming::renaming_levelt Struct Referenceabstract

#include <renaming.h>

Inheritance diagram for renaming::renaming_levelt:
[legend]

Public Member Functions

virtual void get_original_name (expr2tc &expr) const =0
virtual void rename (expr2tc &expr)=0
virtual void remove (const expr2tc &symbol)=0
virtual void get_ident_name (expr2tc &symbol) const =0
virtual ~renaming_levelt ()=default

Static Public Member Functions

static void get_original_name (expr2tc &expr, symbol2t::renaming_level lev)

Friends

void build_goto_symex_classes ()

Constructor & Destructor Documentation

◆ ~renaming_levelt()

virtual renaming::renaming_levelt::~renaming_levelt ( )
virtualdefault

Member Function Documentation

◆ get_ident_name()

virtual void renaming::renaming_levelt::get_ident_name ( expr2tc & symbol) const
pure virtual

Implemented in renaming::level1t, and renaming::level2t.

◆ get_original_name() [1/2]

virtual void renaming::renaming_levelt::get_original_name ( expr2tc & expr) const
pure virtual

Implemented in renaming::level1t, and renaming::level2t.

◆ get_original_name() [2/2]

void renaming::renaming_levelt::get_original_name ( expr2tc & expr,
symbol2t::renaming_level lev )
static

◆ remove()

virtual void renaming::renaming_levelt::remove ( const expr2tc & symbol)
pure virtual

Implemented in renaming::level1t, and renaming::level2t.

◆ rename()

virtual void renaming::renaming_levelt::rename ( expr2tc & expr)
pure virtual

Implemented in execution_statet::ex_state_level2t, renaming::level1t, and renaming::level2t.

◆ build_goto_symex_classes

void build_goto_symex_classes ( )
friend
The documentation for this struct was generated from the following files: