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.

References add(), is_constant(), and is_constant_address().

Member Function Documentation

§ add()

§ 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, output(), and to_string().

§ 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(), get(), and inv_object_storet().

§ 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().

Referenced by get_expr(), and invariant_sett::invariant_sett().

§ 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 invariant_sett::add_bounds(), get_expr(), output(), and invariant_sett::output().

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


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