#include <value_set_fi.h>

Collaboration diagram for value_set_fit:

Classes
struct	entryt

class	object_map_dt

Public Types
typedef irep_idt	idt

typedef std::optional< mp_integer >	offsett
	Represents the offset into an object: either a unique integer offset, or an unknown value, represented by `!offset`.

typedef reference_counting< object_map_dt >	object_mapt

typedef std::unordered_set< exprt, irep_hash >	expr_sett

typedef std::unordered_set< unsigned int >	dynamic_object_id_sett

typedef std::map< idt, entryt >	valuest

typedef std::set< idt >	flatten_seent

typedef std::unordered_set< idt >	gvs_recursion_sett

typedef std::unordered_set< idt >	recfind_recursion_sett

typedef std::unordered_set< idt >	assign_recursion_sett

Public Member Functions
	value_set_fit ()

void	set_from (const irep_idt &function, unsigned inx)

void	set_to (const irep_idt &function, unsigned inx)

bool	offset_is_zero (const offsett &offset) const

exprt	to_expr (const object_map_dt::value_type &it) const

void	set (object_mapt &dest, const object_map_dt::value_type &it) const

bool	insert (object_mapt &dest, const object_map_dt::value_type &it) const

bool	insert (object_mapt &dest, const exprt &src) const

bool	insert (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const

bool	insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const

bool	insert (object_mapt &dest, const exprt &expr, const offsett &offset) const

std::vector< exprt >	get_value_set (const exprt &expr, const namespacet &ns) const

expr_sett &	get (const idt &identifier, const std::string &suffix)

void	clear ()

void	add_var (const idt &id)

void	add_var (const entryt &e)

entryt &	get_entry (const idt &id, const std::string &suffix)

entryt &	get_entry (const entryt &e)

void	add_vars (const std::list< entryt > &vars)

void	output (const namespacet &ns, std::ostream &out) const

bool	make_union (object_mapt &dest, const object_mapt &src) const

bool	make_union (const valuest &new_values)

bool	make_union (const value_set_fit &new_values)

void	apply_code (const codet &code, const namespacet &ns)

void	assign (const exprt &lhs, const exprt &rhs, const namespacet &ns)

void	do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)

void	do_end_function (const exprt &lhs, const namespacet &ns)

void	get_reference_set (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const

Public Attributes
unsigned	to_function

unsigned	from_function

unsigned	to_target_index

unsigned	from_target_index

valuest	values

bool	changed

Static Public Attributes
static object_numberingt	object_numbering

static numberingt< irep_idt >	function_numbering

Protected Member Functions
void	get_reference_set_sharing (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const

void	get_value_set_rec (const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const

void	get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void	get_reference_set_sharing (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void	get_reference_set_sharing_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void	dereference_rec (const exprt &src, exprt &dest) const

void	assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)

void	flatten (const entryt &e, object_mapt &dest) const

void	flatten_rec (const entryt &, object_mapt &, flatten_seent &) const

Detailed Description

Definition at line 29 of file value_set_fi.h.

Member Typedef Documentation

◆ assign_recursion_sett

typedef std::unordered_set<idt> value_set_fit::assign_recursion_sett

Definition at line 198 of file value_set_fi.h.

◆ dynamic_object_id_sett

typedef std::unordered_set<unsigned int> value_set_fit::dynamic_object_id_sett

Definition at line 192 of file value_set_fi.h.

◆ expr_sett

typedef std::unordered_set<exprt, irep_hash> value_set_fit::expr_sett

Definition at line 190 of file value_set_fi.h.

◆ flatten_seent

typedef std::set<idt> value_set_fit::flatten_seent

Definition at line 195 of file value_set_fi.h.

◆ gvs_recursion_sett

typedef std::unordered_set<idt> value_set_fit::gvs_recursion_sett

Definition at line 196 of file value_set_fi.h.

◆ idt

typedef irep_idt value_set_fit::idt

Definition at line 56 of file value_set_fi.h.

◆ object_mapt

typedef reference_counting<object_map_dt> value_set_fit::object_mapt

Definition at line 108 of file value_set_fi.h.

◆ offsett

typedef std::optional<mp_integer> value_set_fit::offsett

Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.

Definition at line 60 of file value_set_fi.h.

◆ recfind_recursion_sett

typedef std::unordered_set<idt> value_set_fit::recfind_recursion_sett

Definition at line 197 of file value_set_fi.h.

◆ valuest

typedef std::map<idt, entryt> value_set_fit::valuest

Definition at line 194 of file value_set_fi.h.

Constructor & Destructor Documentation

◆ value_set_fit()

value_set_fit::value_set_fit ( )

inline

Definition at line 32 of file value_set_fi.h.

Member Function Documentation

◆ add_var() [1/2]

void value_set_fit::add_var ( const entryt & e )

inline

Definition at line 217 of file value_set_fi.h.

◆ add_var() [2/2]

void value_set_fit::add_var ( const idt & id )

inline

Definition at line 212 of file value_set_fi.h.

◆ add_vars()

void value_set_fit::add_vars ( const std::list< entryt > & vars )

inline

Definition at line 237 of file value_set_fi.h.

◆ apply_code()

void value_set_fit::apply_code	(	const codet &	code,
		const namespacet &	ns
	)

Definition at line 1383 of file value_set_fi.cpp.

◆ assign()

void value_set_fit::assign	(	const exprt &	lhs,
		const exprt &	rhs,
		const namespacet &	ns
	)

Definition at line 997 of file value_set_fi.cpp.

◆ assign_rec()

void value_set_fit::assign_rec	(	const exprt &	lhs,
		const object_mapt &	values_rhs,
		const std::string &	suffix,
		const namespacet &	ns,
		assign_recursion_sett &	recursion_set
	)

protected

Definition at line 1163 of file value_set_fi.cpp.

◆ clear()

void value_set_fit::clear ( )

inline

Definition at line 207 of file value_set_fi.h.

◆ dereference_rec()

void value_set_fit::dereference_rec	(	const exprt &	src,
		exprt &	dest
	)		const

protected

Definition at line 716 of file value_set_fi.cpp.

◆ do_end_function()

void value_set_fit::do_end_function	(	const exprt &	lhs,
		const namespacet &	ns
	)

Definition at line 1370 of file value_set_fi.cpp.

◆ do_function_call()

void value_set_fit::do_function_call	(	const irep_idt &	function,
		const exprt::operandst &	arguments,
		const namespacet &	ns
	)

Definition at line 1321 of file value_set_fi.cpp.

◆ flatten()

void value_set_fit::flatten	(	const entryt &	e,
		object_mapt &	dest
	)		const

protected

Definition at line 133 of file value_set_fi.cpp.

◆ flatten_rec()

void value_set_fit::flatten_rec	(	const entryt &	e,
		object_mapt &	dest,
		flatten_seent &	seen
	)		const

protected

Definition at line 149 of file value_set_fi.cpp.

◆ get()

expr_sett & value_set_fit::get	(	const idt &	identifier,
		const std::string &	suffix
	)

◆ get_entry() [1/2]

entryt & value_set_fit::get_entry ( const entryt & e )

inline

Definition at line 227 of file value_set_fi.h.

◆ get_entry() [2/2]

entryt & value_set_fit::get_entry	(	const idt &	id,
		const std::string &	suffix
	)

inline

Definition at line 222 of file value_set_fi.h.

◆ get_reference_set()

void value_set_fit::get_reference_set	(	const exprt &	expr,
		expr_sett &	expr_set,
		const namespacet &	ns
	)		const

Definition at line 731 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [1/2]

void value_set_fit::get_reference_set_sharing	(	const exprt &	expr,
		expr_sett &	expr_set,
		const namespacet &	ns
	)		const

protected

Definition at line 779 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [2/2]

void value_set_fit::get_reference_set_sharing	(	const exprt &	expr,
		object_mapt &	dest,
		const namespacet &	ns
	)		const

inlineprotected

Definition at line 308 of file value_set_fi.h.

◆ get_reference_set_sharing_rec()

void value_set_fit::get_reference_set_sharing_rec	(	const exprt &	expr,
		object_mapt &	dest,
		const namespacet &	ns
	)		const

protected

Definition at line 791 of file value_set_fi.cpp.

◆ get_value_set() [1/2]

std::vector< exprt > value_set_fit::get_value_set	(	const exprt &	expr,
		const namespacet &	ns
	)		const

Definition at line 291 of file value_set_fi.cpp.

◆ get_value_set() [2/2]

void value_set_fit::get_value_set	(	const exprt &	expr,
		object_mapt &	dest,
		const namespacet &	ns
	)		const

protected

Definition at line 352 of file value_set_fi.cpp.

◆ get_value_set_rec()

void value_set_fit::get_value_set_rec	(	const exprt &	expr,
		object_mapt &	dest,
		bool &	includes_nondet_pointer,
		const std::string &	suffix,
		const typet &	original_type,
		const namespacet &	ns,
		gvs_recursion_sett &	recursion_set
	)		const

protected

Definition at line 366 of file value_set_fi.cpp.

◆ insert() [1/5]

bool value_set_fit::insert	(	object_mapt &	dest,
		const exprt &	expr,
		const offsett &	offset
	)		const

inline

Definition at line 168 of file value_set_fi.h.

◆ insert() [2/5]

bool value_set_fit::insert	(	object_mapt &	dest,
		const exprt &	src
	)		const

inline

Definition at line 120 of file value_set_fi.h.

◆ insert() [3/5]

bool value_set_fit::insert	(	object_mapt &	dest,
		const exprt &	src,
		const mp_integer &	offset_value
	)		const

inline

Definition at line 125 of file value_set_fi.h.

◆ insert() [4/5]

bool value_set_fit::insert	(	object_mapt &	dest,
		const object_map_dt::value_type &	it
	)		const

inline

Definition at line 115 of file value_set_fi.h.

◆ insert() [5/5]

bool value_set_fit::insert	(	object_mapt &	dest,
		object_numberingt::number_type	n,
		const offsett &	offset
	)		const

inline

Definition at line 133 of file value_set_fi.h.

◆ make_union() [1/3]

bool value_set_fit::make_union ( const value_set_fit & new_values )

inline

Definition at line 261 of file value_set_fi.h.

◆ make_union() [2/3]

bool value_set_fit::make_union ( const valuest & new_values )

Definition at line 239 of file value_set_fi.cpp.

◆ make_union() [3/3]

bool value_set_fit::make_union	(	object_mapt &	dest,
		const object_mapt &	src
	)		const

Definition at line 277 of file value_set_fi.cpp.

◆ offset_is_zero()

bool value_set_fit::offset_is_zero ( const offsett & offset ) const

inline

Definition at line 61 of file value_set_fi.h.

◆ output()

void value_set_fit::output	(	const namespacet &	ns,
		std::ostream &	out
	)		const

Definition at line 36 of file value_set_fi.cpp.

◆ set()

void value_set_fit::set	(	object_mapt &	dest,
		const object_map_dt::value_type &	it
	)		const

inline

Definition at line 110 of file value_set_fi.h.

◆ set_from()

void value_set_fit::set_from	(	const irep_idt &	function,
		unsigned	inx
	)

inline

Definition at line 44 of file value_set_fi.h.

◆ set_to()

void value_set_fit::set_to	(	const irep_idt &	function,
		unsigned	inx
	)

inline

Definition at line 50 of file value_set_fi.h.

◆ to_expr()

exprt value_set_fit::to_expr ( const object_map_dt::value_type & it ) const

Definition at line 219 of file value_set_fi.cpp.

Member Data Documentation

◆ changed

bool value_set_fit::changed

Definition at line 252 of file value_set_fi.h.

◆ from_function

unsigned value_set_fit::from_function

Definition at line 39 of file value_set_fi.h.

◆ from_target_index

unsigned value_set_fit::from_target_index

Definition at line 40 of file value_set_fi.h.

◆ function_numbering

numberingt< irep_idt > value_set_fit::function_numbering

static

Definition at line 42 of file value_set_fi.h.

◆ object_numbering

object_numberingt value_set_fit::object_numbering

static

Definition at line 41 of file value_set_fi.h.

◆ to_function

unsigned value_set_fit::to_function

Definition at line 39 of file value_set_fi.h.

◆ to_target_index

unsigned value_set_fit::to_target_index

Definition at line 40 of file value_set_fi.h.

◆ values

valuest value_set_fit::values

Definition at line 250 of file value_set_fi.h.

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

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_fi.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_fi.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Protected Member Functions

Detailed Description

Member Typedef Documentation

◆ assign_recursion_sett

◆ dynamic_object_id_sett

◆ expr_sett

◆ flatten_seent

◆ gvs_recursion_sett

◆ idt

◆ object_mapt

◆ offsett

◆ recfind_recursion_sett

◆ valuest

Constructor & Destructor Documentation

◆ value_set_fit()

Member Function Documentation

◆ add_var() [1/2]

◆ add_var() [2/2]

◆ add_vars()

◆ apply_code()

◆ assign()

◆ assign_rec()

◆ clear()

◆ dereference_rec()

◆ do_end_function()

◆ do_function_call()

◆ flatten()

◆ flatten_rec()

◆ get()

◆ get_entry() [1/2]

◆ get_entry() [2/2]

◆ get_reference_set()

◆ get_reference_set_sharing() [1/2]

◆ get_reference_set_sharing() [2/2]

◆ get_reference_set_sharing_rec()

◆ get_value_set() [1/2]

◆ get_value_set() [2/2]

◆ get_value_set_rec()

◆ insert() [1/5]

◆ insert() [2/5]

◆ insert() [3/5]

◆ insert() [4/5]

◆ insert() [5/5]

◆ make_union() [1/3]

◆ make_union() [2/3]

◆ make_union() [3/3]

◆ offset_is_zero()

◆ output()

◆ set()

◆ set_from()

◆ set_to()

◆ to_expr()

Member Data Documentation

◆ changed

◆ from_function

◆ from_target_index

◆ function_numbering

◆ object_numbering

◆ to_function

◆ to_target_index

◆ values