#include <abstract_object.h>

Inheritance diagram for abstract_objectt:

Collaboration diagram for abstract_objectt:

Classes
struct	abstract_object_visitort
	Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstract_object_pointert. More...

struct	combine_result
	Clones the first parameter and merges it with the second. More...

Public Types
typedef goto_programt::const_targett	locationt

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

Public Member Functions
	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 void	get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const

virtual abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
	Interface for transforms. 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 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
	A helper function to evaluate writing to a component of an abstract object. 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...

Static Public Member Functions
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
template<class T >
using	internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt >	internal_abstract_object_pointert

Protected Member Functions
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 ()

Private Member Functions
virtual void	set_top_internal ()

virtual void	set_not_top_internal ()

virtual abstract_object_pointert	abstract_object_merge_internal (const abstract_object_pointert &other) const
	Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed it's actions but immediately prior to it returning. More...

virtual abstract_object_pointert	abstract_object_meet_internal (const abstract_object_pointert &other) const
	Helper function for base meet, in case additional work was needed. More...

Private Attributes
typet	t
	To enforce copy-on-write these are private and have read-only accessors. More...

bool	bottom

bool	top

Detailed Description

Definition at line 72 of file abstract_object.h.

Member Typedef Documentation

◆ internal_abstract_object_pointert

typedef internal_sharing_ptrt<class abstract_objectt> abstract_objectt::internal_abstract_object_pointert

protected

Definition at line 409 of file abstract_object.h.

◆ internal_sharing_ptrt

template<class T >

using abstract_objectt::internal_sharing_ptrt = std::shared_ptr<T>

protected

Definition at line 406 of file abstract_object.h.

◆ locationt

typedef goto_programt::const_targett abstract_objectt::locationt

Definition at line 204 of file abstract_object.h.

◆ shared_mapt

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

Definition at line 206 of file abstract_object.h.

Constructor & Destructor Documentation

◆ abstract_objectt() [1/2]

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.

Parameters

type	the type the abstract_object is representing
top	is the abstract_object starting as top
bottom	is the abstract_object starting as bottom

Definition at line 19 of file abstract_object.cpp.

◆ abstract_objectt() [2/2]

abstract_objectt::abstract_objectt	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

Construct an abstract object from the expression.

Parameters

expr	The expression to use as the starting pointer for an abstract object
environment	The environment this abstract object is being created in
ns	The namespace

Definition at line 25 of file abstract_object.cpp.

◆ ~abstract_objectt()

virtual abstract_objectt::~abstract_objectt ( )

inlinevirtual

Definition at line 95 of file abstract_object.h.

Member Function Documentation

◆ abstract_object_meet()

abstract_object_pointert abstract_objectt::abstract_object_meet ( const abstract_object_pointert & other ) const

protected

Helper function for base meet.

Two cases: return itself (if trivially contained in other); return BOTTOM otherwise.

Parameters

other pointer to the other object

Returns: the resulting object

Definition at line 70 of file abstract_object.cpp.

◆ abstract_object_meet_internal()

abstract_object_pointert abstract_objectt::abstract_object_meet_internal ( const abstract_object_pointert & other ) const

privatevirtual

Helper function for base meet, in case additional work was needed.

Base implementation simply return pointer to itself.

Parameters

other pointer to the other object

Returns: the resulting object

Definition at line 85 of file abstract_object.cpp.

◆ abstract_object_merge()

abstract_object_pointert abstract_objectt::abstract_object_merge ( const abstract_object_pointert & other ) const

protected

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

Parameters

other The object to merge with this

Returns: Returns the result of the abstract object.

Definition at line 45 of file abstract_object.cpp.

◆ abstract_object_merge_internal()

abstract_object_pointert abstract_objectt::abstract_object_merge_internal ( const abstract_object_pointert & other ) const

privatevirtual

Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed it's actions but immediately prior to it returning.

As such, this function gives the ability to perform additional work for a merge.

This default implementation just returns itself.

Parameters

other the object to merge with this

Returns: the result of the merge

Reimplemented in write_location_contextt, liveness_contextt, and data_dependency_contextt.

Definition at line 57 of file abstract_object.cpp.

◆ clear_top()

abstract_object_pointert abstract_objectt::clear_top ( ) const

inline

Definition at line 313 of file abstract_object.h.

◆ dump_map()

void abstract_objectt::dump_map	(	std::ostream	out,
		const shared_mapt &	m
	)

static

Definition at line 256 of file abstract_object.cpp.

◆ dump_map_diff()

void abstract_objectt::dump_map_diff	(	std::ostream	out,
		const shared_mapt &	m1,
		const shared_mapt &	m2
	)

static

Dump all elements in m1 that are different or missing in m2.

Parameters

out	the stream to write output to
m1	the 'target' sharing_map
m2	the reference sharing map

Definition at line 273 of file abstract_object.cpp.

◆ expression_transform()

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

virtual

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 in context_abstract_objectt, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >, and abstract_value_objectt.

Definition at line 98 of file abstract_object.cpp.

◆ get_statistics()

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

virtual

Reimplemented in interval_abstract_valuet, context_abstract_objectt, constant_pointer_abstract_objectt, constant_abstract_valuet, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, and abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 296 of file abstract_object.cpp.

◆ has_been_modified()

virtual bool abstract_objectt::has_been_modified ( const abstract_object_pointert & before ) const

inlinevirtual

Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

Parameters

before The abstract_object_pointert to use as a reference to compare against

Returns: true if 'this' is considered to have been modified in comparison to 'before', false otherwise.

Default implementation, with no other information to go on falls back to relying on copy-on-write and pointer inequality to indicate if an abstract_objectt has been modified

Reimplemented in write_location_contextt, data_dependency_contextt, and context_abstract_objectt.

Definition at line 227 of file abstract_object.h.

◆ internal_equality()

virtual bool abstract_objectt::internal_equality ( const abstract_object_pointert & other ) const

inlinevirtual

Reimplemented in interval_abstract_valuet, and constant_abstract_valuet.

Definition at line 357 of file abstract_object.h.

◆ internal_hash()

virtual size_t abstract_objectt::internal_hash ( ) const

inlinevirtual

Reimplemented in interval_abstract_valuet, and constant_abstract_valuet.

Definition at line 352 of file abstract_object.h.

◆ is_bottom()

bool abstract_objectt::is_bottom ( ) const

virtual

Find out if the abstract object is bottom.

Returns: Returns true if the abstract object is representing the bottom.

Reimplemented in context_abstract_objectt.

Definition at line 146 of file abstract_object.cpp.

◆ is_top()

bool abstract_objectt::is_top ( ) const

virtual

Find out if the abstract object is top.

Returns: Returns true if the abstract object is representing the top (i.e. we don't know anything about the value).

Reimplemented in context_abstract_objectt.

Definition at line 141 of file abstract_object.cpp.

◆ make_top()

abstract_object_pointert abstract_objectt::make_top ( ) const

inline

Definition at line 303 of file abstract_object.h.

◆ meet() [1/2]

abstract_objectt::combine_result abstract_objectt::meet	(	const abstract_object_pointert &	op1,
		const abstract_object_pointert &	op2
	)

static

Interface method for the meet operation.

Decides whether to use the base implementation or if a more precise abstraction is attainable.

Parameters

op1	lhs object for meet
op2	rhs object for meet

Returns: A pair containing the merged abstract object with the same sensitivity as op1, and a modified flag which will be true if the returned object is different from op1

Definition at line 227 of file abstract_object.cpp.

◆ meet() [2/2]

abstract_object_pointert abstract_objectt::meet ( const abstract_object_pointert & other ) const

virtual

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}.

Parameters

other pointer to the abstract object to meet

Returns: the resulting abstract object pointer

Reimplemented in write_location_contextt, data_dependency_contextt, and abstract_value_objectt.

Definition at line 65 of file abstract_object.cpp.

◆ merge() [1/3]

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

static

Definition at line 195 of file abstract_object.cpp.

◆ merge() [2/3]

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

static

Definition at line 208 of file abstract_object.cpp.

◆ merge() [3/3]

abstract_object_pointert abstract_objectt::merge	(	const abstract_object_pointert &	other,
		const widen_modet &	widen_mode
	)		const

protectedvirtual

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

Parameters

other	The object to merge with this
widen_mode	Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented in write_location_contextt, value_set_pointer_abstract_objectt, liveness_contextt, full_struct_abstract_objectt, full_array_abstract_objectt, data_dependency_contextt, abstract_value_objectt, and constant_pointer_abstract_objectt.

Definition at line 38 of file abstract_object.cpp.

◆ merge_location_context()

abstract_object_pointert abstract_objectt::merge_location_context ( const locationt & location ) const

virtual

Update the merge location context for an abstract object.

Parameters

location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented in liveness_contextt, full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 251 of file abstract_object.cpp.

◆ mutable_clone()

virtual internal_abstract_object_pointert abstract_objectt::mutable_clone ( ) const

inlineprotectedvirtual

Reimplemented in write_location_contextt, value_set_pointer_abstract_objectt, value_set_abstract_objectt, liveness_contextt, interval_abstract_valuet, full_struct_abstract_objectt, full_array_abstract_objectt, data_dependency_contextt, constant_pointer_abstract_objectt, and constant_abstract_valuet.

Definition at line 412 of file abstract_object.h.

◆ output()

void abstract_objectt::output	(	std::ostream &	out,
		const class ai_baset &	ai,
		const namespacet &	ns
	)		const

virtual

Print the value of the abstract object.

Parameters

out	the stream to write to
ai	the abstract interpreter that contains the abstract domain (that contains the object ... )
ns	the current namespace

Reimplemented in write_location_contextt, liveness_contextt, data_dependency_contextt, and context_abstract_objectt.

Definition at line 176 of file abstract_object.cpp.

◆ set_not_bottom()

void abstract_objectt::set_not_bottom ( )

inlineprotected

Definition at line 470 of file abstract_object.h.

◆ set_not_top()

void abstract_objectt::set_not_top ( )

inlineprotected

Definition at line 465 of file abstract_object.h.

◆ set_not_top_internal()

virtual void abstract_objectt::set_not_top_internal ( )

inlineprivatevirtual

Reimplemented in context_abstract_objectt.

Definition at line 378 of file abstract_object.h.

◆ set_top()

void abstract_objectt::set_top ( )

inlineprotected

Definition at line 460 of file abstract_object.h.

◆ set_top_internal()

virtual void abstract_objectt::set_top_internal ( )

inlineprivatevirtual

Reimplemented in value_set_abstract_objectt, interval_abstract_valuet, full_array_abstract_objectt, and context_abstract_objectt.

Definition at line 375 of file abstract_object.h.

◆ should_use_base_meet()

bool abstract_objectt::should_use_base_meet ( const abstract_object_pointert & other ) const

protected

Helper function to decide if base meet implementation should be used.

Parameters

other pointer to the other object to meet

Returns: true if base implementation would yield the most precise abstraction anyway

Definition at line 238 of file abstract_object.cpp.

◆ should_use_base_merge()

bool abstract_objectt::should_use_base_merge ( const abstract_object_pointert & other ) const

protected

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.

Parameters

other the object being merged with

Returns: Returns true if the base class is capable of doing a complete merge

Definition at line 221 of file abstract_object.cpp.

◆ to_constant()

exprt abstract_objectt::to_constant ( ) const

virtual

Converts to a constant expression if possible.

Returns: Returns an exprt representing the value if the value is known and constant. Otherwise returns the nil expression

If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.

Reimplemented in value_set_pointer_abstract_objectt, value_set_abstract_objectt, interval_abstract_valuet, context_abstract_objectt, constant_pointer_abstract_objectt, and constant_abstract_valuet.

Definition at line 156 of file abstract_object.cpp.

◆ to_predicate()

exprt abstract_objectt::to_predicate ( const exprt & name ) const

Converts to an invariant expression.

Parameters

name	- the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

The the abstract element represents a single value the expression will have the form name = value, if the value is an interval it will have the the form lower <= name <= upper, etc. If the value is bottom returns false, if top returns true.

Definition at line 161 of file abstract_object.cpp.

◆ to_predicate_internal()

exprt abstract_objectt::to_predicate_internal ( const exprt & name ) const

virtual

to_predicate implementation - derived classes will override

Parameters

name	- the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

Reimplemented in value_set_pointer_abstract_objectt, value_set_abstract_objectt, interval_abstract_valuet, full_struct_abstract_objectt, full_array_abstract_objectt, context_abstract_objectt, constant_pointer_abstract_objectt, and constant_abstract_valuet.

Definition at line 170 of file abstract_object.cpp.

◆ type()

const typet & abstract_objectt::type ( ) const

virtual

Get the real type of the variable this abstract object is representing.

Returns: The program type this abstract object represents

Reimplemented in context_abstract_objectt.

Definition at line 33 of file abstract_object.cpp.

◆ unwrap_context()

abstract_object_pointert abstract_objectt::unwrap_context ( ) const

virtual

Reimplemented in context_abstract_objectt.

Definition at line 291 of file abstract_object.cpp.

◆ verify()

bool abstract_objectt::verify ( ) const

virtual

Verify the internal structure of an abstract_object is correct.

Returns: true if the abstract_object is correctly constructed, or false otherwise

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 151 of file abstract_object.cpp.

◆ visit_sub_elements()

virtual abstract_object_pointert abstract_objectt::visit_sub_elements ( const abstract_object_visitort & visitor ) const

inlinevirtual

Apply a visitor operation to all sub elements of this abstract_object.

A sub element might be a member of a struct, or an element of an array, for instance, but this is entirely determined by the particular derived instance of abstract_objectt.

Parameters

visitor an instance of a visitor class that will be applied to all sub elements

Returns: A new abstract_object if it's contents is modifed, or this if no modification is needed

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 347 of file abstract_object.h.

◆ write()

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

virtual

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 in write_location_contextt, liveness_contextt, data_dependency_contextt, context_abstract_objectt, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >, and abstract_value_objectt.

Definition at line 130 of file abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert abstract_objectt::write_location_context ( const locationt & location ) const

virtual

Update the write location context for an abstract object.

Parameters

location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented in full_struct_abstract_objectt, full_array_abstract_objectt, and context_abstract_objectt.

Definition at line 245 of file abstract_object.cpp.

Member Data Documentation

◆ bottom

bool abstract_objectt::bottom

private

Definition at line 370 of file abstract_object.h.

◆ t

typet abstract_objectt::t

private

To enforce copy-on-write these are private and have read-only accessors.

Definition at line 369 of file abstract_object.h.

◆ top

bool abstract_objectt::top

private

Definition at line 371 of file abstract_object.h.

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

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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ internal_abstract_object_pointert

◆ internal_sharing_ptrt

◆ locationt

◆ shared_mapt

Constructor & Destructor Documentation

◆ abstract_objectt() [1/2]

◆ abstract_objectt() [2/2]

◆ ~abstract_objectt()

Member Function Documentation

◆ abstract_object_meet()

◆ abstract_object_meet_internal()

◆ abstract_object_merge()

◆ abstract_object_merge_internal()

◆ clear_top()

◆ dump_map()

◆ dump_map_diff()

◆ expression_transform()

◆ get_statistics()

◆ has_been_modified()

◆ internal_equality()

◆ internal_hash()

◆ is_bottom()

◆ is_top()

◆ make_top()

◆ meet() [1/2]

◆ meet() [2/2]

◆ merge() [1/3]

◆ merge() [2/3]

◆ merge() [3/3]

◆ merge_location_context()

◆ mutable_clone()

◆ output()

◆ set_not_bottom()

◆ set_not_top()

◆ set_not_top_internal()

◆ set_top()

◆ set_top_internal()

◆ should_use_base_meet()

◆ should_use_base_merge()

◆ to_constant()

◆ to_predicate()

◆ to_predicate_internal()

◆ type()

◆ unwrap_context()

◆ verify()

◆ visit_sub_elements()

◆ write()

◆ write_location_context()

Member Data Documentation

◆ bottom

◆ t

◆ top