cprover
Loading...
Searching...
No Matches
inv_object_storet Class Reference

#include <invariant_set.h>

Collaboration diagram for inv_object_storet:

Classes

struct  entryt

Public Member Functions

 inv_object_storet (const namespacet &_ns)
bool get (const exprt &expr, unsigned &n)
unsigned add (const exprt &expr)
bool is_constant (unsigned n) const
bool is_constant (const exprt &expr) const
const irep_idtoperator[] (unsigned n) const
const exprtget_expr (unsigned n) const
void output (std::ostream &out) const
std::string to_string (unsigned n) const

Static Public Member Functions

static bool is_constant_address (const exprt &expr)

Protected Types

typedef numberingt< irep_idtmapt

Protected Member Functions

std::string build_string (const exprt &expr) const

Static Protected Member Functions

static bool is_constant_address_rec (const exprt &expr)

Protected Attributes

const namespacetns
mapt map
std::vector< entrytentries

Detailed Description

Definition at line 29 of file invariant_set.h.

Member Typedef Documentation

◆ mapt

Definition at line 63 of file invariant_set.h.

Constructor & Destructor Documentation

◆ inv_object_storet()

inv_object_storet::inv_object_storet ( const namespacet & _ns)
inlineexplicit

Definition at line 32 of file invariant_set.h.

Member Function Documentation

◆ add()

unsigned inv_object_storet::add ( const exprt & expr)

Definition at line 61 of file invariant_set.cpp.

◆ build_string()

std::string inv_object_storet::build_string ( const exprt & expr) const
protected

Definition at line 90 of file invariant_set.cpp.

◆ get()

bool inv_object_storet::get ( const exprt & expr,
unsigned & n )

Definition at line 32 of file invariant_set.cpp.

◆ get_expr()

const exprt & inv_object_storet::get_expr ( unsigned n) const
inline

Definition at line 50 of file invariant_set.h.

◆ is_constant() [1/2]

bool inv_object_storet::is_constant ( const exprt & expr) const

Definition at line 84 of file invariant_set.cpp.

◆ is_constant() [2/2]

bool inv_object_storet::is_constant ( unsigned n) const

Definition at line 78 of file invariant_set.cpp.

◆ is_constant_address()

bool inv_object_storet::is_constant_address ( const exprt & expr)
static

Definition at line 157 of file invariant_set.cpp.

◆ is_constant_address_rec()

bool inv_object_storet::is_constant_address_rec ( const exprt & expr)
staticprotected

Definition at line 165 of file invariant_set.cpp.

◆ operator[]()

const irep_idt & inv_object_storet::operator[] ( unsigned n) const
inline

Definition at line 45 of file invariant_set.h.

◆ output()

void inv_object_storet::output ( std::ostream & out) const

Definition at line 26 of file invariant_set.cpp.

◆ to_string()

std::string inv_object_storet::to_string ( unsigned n) const

Definition at line 880 of file invariant_set.cpp.

Member Data Documentation

◆ entries

std::vector<entryt> inv_object_storet::entries
protected

Definition at line 72 of file invariant_set.h.

◆ map

mapt inv_object_storet::map
protected

Definition at line 64 of file invariant_set.h.

◆ ns

const namespacet& inv_object_storet::ns
protected

Definition at line 61 of file invariant_set.h.


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