#include <abstract_aggregate_object.h>

Inheritance diagram for abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >:

Collaboration diagram for abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >:

Public Member Functions
	abstract_aggregate_objectt (const typet &type, bool tp, bool bttm)

	abstract_aggregate_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
	Interface for transforms. More...

abstract_object_pointert	write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
	A helper function to evaluate writing to a component of an abstract object. More...

void	get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override

Public Member Functions inherited from abstract_objectt
	abstract_objectt (const typet &type, bool top, bool bottom)
	Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...

	abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct an abstract object from the expression. More...

virtual	~abstract_objectt ()

virtual const typet &	type () const
	Get the real type of the variable this abstract object is representing. More...

virtual bool	is_top () const
	Find out if the abstract object is top. More...

virtual bool	is_bottom () const
	Find out if the abstract object is bottom. More...

virtual bool	verify () const
	Verify the internal structure of an abstract_object is correct. More...

virtual exprt	to_constant () const
	Converts to a constant expression if possible. More...

exprt	to_predicate (const exprt &name) const
	Converts to an invariant expression. More...

virtual void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
	Print the value of the abstract object. More...

virtual bool	has_been_modified (const abstract_object_pointert &before) const
	Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More...

virtual abstract_object_pointert	meet (const abstract_object_pointert &other) const
	Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}. More...

virtual abstract_object_pointert	write_location_context (const locationt &location) const
	Update the write location context for an abstract object. More...

virtual abstract_object_pointert	merge_location_context (const locationt &location) const
	Update the merge location context for an abstract object. More...

abstract_object_pointert	make_top () const

abstract_object_pointert	clear_top () const

virtual abstract_object_pointert	unwrap_context () const

virtual abstract_object_pointert	visit_sub_elements (const abstract_object_visitort &visitor) const
	Apply a visitor operation to all sub elements of this abstract_object. More...

virtual size_t	internal_hash () const

virtual bool	internal_equality (const abstract_object_pointert &other) const

virtual exprt	to_predicate_internal (const exprt &name) const
	to_predicate implementation - derived classes will override More...

Protected Member Functions
virtual abstract_object_pointert	read_component (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const

virtual abstract_object_pointert	write_component (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const

virtual void	statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const =0

Protected Member Functions inherited from abstract_objectt
virtual internal_abstract_object_pointert	mutable_clone () const

abstract_object_pointert	abstract_object_merge (const abstract_object_pointert &other) const
	Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...

bool	should_use_base_merge (const abstract_object_pointert &other) const
	To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific. More...

virtual abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const
	Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...

abstract_object_pointert	abstract_object_meet (const abstract_object_pointert &other) const
	Helper function for base meet. More...

bool	should_use_base_meet (const abstract_object_pointert &other) const
	Helper function to decide if base meet implementation should be used. More...

void	set_top ()

void	set_not_top ()

void	set_not_bottom ()

Static Protected Member Functions
template<class keyt , typename hash >
static bool	merge_shared_maps (const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map, const widen_modet &widen_mode)

Additional Inherited Members
Public Types inherited from abstract_objectt
typedef goto_programt::const_targett	locationt

typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >	shared_mapt

Static Public Member Functions inherited from abstract_objectt
static void	dump_map (std::ostream out, const shared_mapt &m)

static void	dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
	Dump all elements in m1 that are different or missing in m2. More...

static combine_result	merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)

static combine_result	merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode)

static combine_result	meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2)
	Interface method for the meet operation. More...

Protected Types inherited from abstract_objectt
template<class T >
using	internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt >	internal_abstract_object_pointert

Detailed Description

template<class aggregate_typet, class aggregate_traitst>
class abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >

Definition at line 29 of file abstract_aggregate_object.h.

Constructor & Destructor Documentation

◆ abstract_aggregate_objectt() [1/2]

template<class aggregate_typet , class aggregate_traitst >

abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::abstract_aggregate_objectt	(	const typet &	type,
		bool	tp,
		bool	bttm
	)

inline

Definition at line 33 of file abstract_aggregate_object.h.

◆ abstract_aggregate_objectt() [2/2]

template<class aggregate_typet , class aggregate_traitst >

abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::abstract_aggregate_objectt	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

inline

Definition at line 45 of file abstract_aggregate_object.h.

Member Function Documentation

◆ expression_transform()

template<class aggregate_typet , class aggregate_traitst >

abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::expression_transform	(	const exprt &	expr,
		const std::vector< abstract_object_pointert > &	operands,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)		const

inlineoverridevirtual

Interface for transforms.

Parameters

expr	the expression to evaluate and find the result of it. This will be the symbol referred to be op0()
operands	an abstract_object (pointer) that represent the possible values of each operand
environment	the abstract environment in which the expression is being evaluated
ns	the current variable namespace

Returns: Returns the abstract_object representing the result of this expression to the maximum precision available.

To try and resolve different expressions with the maximum level of precision available.

Reimplemented from abstract_objectt.

Definition at line 62 of file abstract_aggregate_object.h.

◆ get_statistics()

template<class aggregate_typet , class aggregate_traitst >

void abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::get_statistics	(	abstract_object_statisticst &	statistics,
		abstract_object_visitedt &	visited,
		const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

inlineoverridevirtual

Reimplemented from abstract_objectt.

Definition at line 87 of file abstract_aggregate_object.h.

◆ merge_shared_maps()

template<class aggregate_typet , class aggregate_traitst >

template<class keyt , typename hash >

static bool abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::merge_shared_maps	(	const sharing_mapt< keyt, abstract_object_pointert, false, hash > &	map1,
		const sharing_mapt< keyt, abstract_object_pointert, false, hash > &	map2,
		sharing_mapt< keyt, abstract_object_pointert, false, hash > &	out_map,
		const widen_modet &	widen_mode
	)

inlinestaticprotected

Definition at line 138 of file abstract_aggregate_object.h.

◆ read_component()

template<class aggregate_typet , class aggregate_traitst >

virtual abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::read_component	(	const abstract_environmentt &	environment,
		const exprt &	expr,
		const namespacet &	ns
	)		const

inlineprotectedvirtual

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 99 of file abstract_aggregate_object.h.

◆ statistics()

template<class aggregate_typet , class aggregate_traitst >

virtual void abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::statistics	(	abstract_object_statisticst &	statistics,
		abstract_object_visitedt &	visited,
		const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

protectedpure virtual

Implemented in two_value_union_abstract_objectt, two_value_struct_abstract_objectt, two_value_array_abstract_objectt, full_struct_abstract_objectt, and full_array_abstract_objectt.

◆ write()

template<class aggregate_typet , class aggregate_traitst >

abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::write	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const std::stack< exprt > &	stack,
		const exprt &	specifier,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

inlineoverridevirtual

A helper function to evaluate writing to a component of an abstract object.

More precise abstractions may override this to update what they are storing for a specific component.

Parameters

environment	the abstract environment
ns	the current namespace
stack	the remaining stack of expressions on the LHS to evaluate
specifier	the expression uses to access a specific component
value	the value we are trying to write to the component
merging_write	if true, this and all future writes will be merged with the current value

Returns: the abstract_objectt representing the result of writing to a specific component.

Reimplemented from abstract_objectt.

Definition at line 75 of file abstract_aggregate_object.h.

◆ write_component()

template<class aggregate_typet , class aggregate_traitst >

virtual abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::write_component	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const std::stack< exprt > &	stack,
		const exprt &	expr,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

inlineprotectedvirtual

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 113 of file abstract_aggregate_object.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_aggregate_object.h

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Additional Inherited Members

Detailed Description

template<class aggregate_typet, class aggregate_traitst> class abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >

Constructor & Destructor Documentation

◆ abstract_aggregate_objectt() [1/2]

◆ abstract_aggregate_objectt() [2/2]

Member Function Documentation

◆ expression_transform()

◆ get_statistics()

◆ merge_shared_maps()

◆ read_component()

◆ statistics()

◆ write()

◆ write_component()

template<class aggregate_typet, class aggregate_traitst>
class abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >