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_idt &	operator[] (unsigned n) const
const exprt &	get_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_idt >	mapt

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 namespacet &	ns
mapt	map
std::vector< entryt >	entries

Detailed Description

Definition at line 29 of file invariant_set.h.

Member Typedef Documentation

mapt

typedef numberingt<irep_idt> inv_object_storet::mapt

protected

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 874 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:

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/invariant_set.h
• /home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/invariant_set.cpp