cprover
inv_object_storet Class Reference

#include <invariant_set.h>

Collaboration diagram for inv_object_storet:
[legend]

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 irep_idt &identifier) const
 

Static Public Member Functions

static bool is_constant_address (const exprt &expr)
 

Protected Types

typedef hash_numbering< irep_idt, irep_id_hashmapt
 

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 25 of file invariant_set.h.

Member Typedef Documentation

◆ mapt

Definition at line 61 of file invariant_set.h.

Constructor & Destructor Documentation

◆ inv_object_storet()

inv_object_storet::inv_object_storet ( const namespacet _ns)
inlineexplicit

Definition at line 28 of file invariant_set.h.

Member Function Documentation

◆ add()

unsigned inv_object_storet::add ( const exprt expr)

◆ build_string()

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

◆ get()

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

◆ get_expr()

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

Definition at line 46 of file invariant_set.h.

References entries.

Referenced by invariant_sett::get_bounds(), and invariant_sett::get_constant().

◆ is_constant() [1/2]

bool inv_object_storet::is_constant ( unsigned  n) const

Definition at line 76 of file invariant_set.cpp.

References entries.

Referenced by add(), invariant_sett::add_eq(), and get().

◆ is_constant() [2/2]

bool inv_object_storet::is_constant ( const exprt expr) const

Definition at line 82 of file invariant_set.cpp.

References exprt::is_constant(), and is_constant_address().

◆ is_constant_address()

bool inv_object_storet::is_constant_address ( const exprt expr)
static

◆ is_constant_address_rec()

bool inv_object_storet::is_constant_address_rec ( const exprt expr)
staticprotected

◆ operator[]()

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

Definition at line 41 of file invariant_set.h.

References map.

◆ output()

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

Definition at line 28 of file invariant_set.cpp.

References entries, and to_string().

◆ to_string()

std::string inv_object_storet::to_string ( unsigned  n,
const irep_idt identifier 
) const

Definition at line 892 of file invariant_set.cpp.

References id2string(), and map.

Referenced by output(), and invariant_sett::to_string().

Member Data Documentation

◆ entries

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

Definition at line 70 of file invariant_set.h.

Referenced by add(), get(), get_expr(), is_constant(), and output().

◆ map

mapt inv_object_storet::map
protected

Definition at line 62 of file invariant_set.h.

Referenced by add(), get(), operator[](), and to_string().

◆ ns

const namespacet& inv_object_storet::ns
protected

Definition at line 59 of file invariant_set.h.

Referenced by build_string().


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