CBMC
designatort Class Reference

#include <designator.h>

+ Collaboration diagram for designatort:

Classes

struct  entryt
 

Public Member Functions

bool empty () const
 
size_t size () const
 
const entrytoperator[] (size_t i) const
 
entrytoperator[] (size_t i)
 
const entrytback () const
 
const entrytfront () const
 
 designatort ()
 
void push_entry (const entryt &entry)
 
void pop_entry ()
 
void print (std::ostream &out) const
 

Protected Types

typedef std::vector< entrytindex_listt
 

Protected Attributes

index_listt index_list
 

Detailed Description

Definition at line 20 of file designator.h.

Member Typedef Documentation

◆ index_listt

typedef std::vector<entryt> designatort::index_listt
protected

Definition at line 59 of file designator.h.

Constructor & Destructor Documentation

◆ designatort()

designatort::designatort ( )
inline

Definition at line 43 of file designator.h.

Member Function Documentation

◆ back()

const entryt& designatort::back ( ) const
inline

Definition at line 40 of file designator.h.

◆ empty()

bool designatort::empty ( ) const
inline

Definition at line 36 of file designator.h.

◆ front()

const entryt& designatort::front ( ) const
inline

Definition at line 41 of file designator.h.

◆ operator[]() [1/2]

entryt& designatort::operator[] ( size_t  i)
inline

Definition at line 39 of file designator.h.

◆ operator[]() [2/2]

const entryt& designatort::operator[] ( size_t  i) const
inline

Definition at line 38 of file designator.h.

◆ pop_entry()

void designatort::pop_entry ( )
inline

Definition at line 50 of file designator.h.

◆ print()

void designatort::print ( std::ostream &  out) const

Definition at line 16 of file designator.cpp.

◆ push_entry()

void designatort::push_entry ( const entryt entry)
inline

Definition at line 45 of file designator.h.

◆ size()

size_t designatort::size ( ) const
inline

Definition at line 37 of file designator.h.

Member Data Documentation

◆ index_list

index_listt designatort::index_list
protected

Definition at line 60 of file designator.h.


The documentation for this class was generated from the following files: