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

Member Typedef Documentation

mapt

typedef hash_numbering<irep_idt, irep_id_hash> inv_object_storet::mapt

protected

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

)

Definition at line 58 of file invariant_set.cpp.

References build_string(), entries, is_constant(), map, and hash_numbering< T, hash_fkt >::number().

Referenced by invariant_propagationt::get_objects().

build_string()

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

protected

Definition at line 88 of file invariant_set.cpp.

References from_expr(), irept::get(), irept::get_string(), irept::id(), integer2string(), exprt::is_constant(), is_constant_address(), ns, exprt::op0(), exprt::operands(), to_bitvector_type(), to_integer(), and exprt::type().

Referenced by add(), and get().

get()

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

Definition at line 34 of file invariant_set.cpp.

References build_string(), entries, hash_numbering< T, hash_fkt >::get_number(), is_constant(), map, and hash_numbering< T, hash_fkt >::number().

Referenced by invariant_sett::get_object().

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

Definition at line 152 of file invariant_set.cpp.

References irept::id(), is_constant_address_rec(), exprt::op0(), and exprt::operands().

Referenced by build_string(), invariant_sett::get_constant(), and is_constant().

is_constant_address_rec()

bool inv_object_storet::is_constant_address_rec ( const exprt &  expr )

staticprotected

Definition at line 161 of file invariant_set.cpp.

References irept::id(), exprt::is_constant(), exprt::op0(), exprt::op1(), and exprt::operands().

Referenced by is_constant_address().

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:

• analyses/invariant_set.h
• analyses/invariant_set.cpp