#include <global_may_alias.h>

Inheritance diagram for global_may_alias_domaint:

Collaboration diagram for global_may_alias_domaint:

Public Types
typedef union_find< irep_idt >	aliasest

Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Public Member Functions
	global_may_alias_domaint ()

void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
	Abstract Interpretation domain transform function. More...

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
	Abstract Interpretation domain output function. More...

bool	merge (const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
	Abstract Interpretation domain merge function. More...

void	make_bottom () final override
	Clear list of aliases, and mark domain as bottom. More...

void	make_top () final override
	Clear list of aliases, and mark domain as top. More...

void	make_entry () final override
	Make this domain a reasonable entry-point state. More...

bool	is_bottom () const final override
	Returns true if domain is bottom. More...

bool	is_top () const final override
	Returns false if domain is top. More...

Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()

virtual jsont	output_json (const ai_baset &ai, const namespacet &ns) const

virtual xmlt	output_xml (const ai_baset &ai, const namespacet &ns) const

virtual bool	ai_simplify (exprt &condition, const namespacet &) const
	also add More...

virtual bool	ai_simplify_lhs (exprt &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value. More...

virtual exprt	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain. More...

Public Attributes
aliasest	aliases

Private Member Functions
void	assign_lhs_aliases (const exprt &, const std::set< irep_idt > &)
	Populate list of aliases for a given identifier in a context in which an object is being written to. More...

void	get_rhs_aliases (const exprt &, std::set< irep_idt > &)
	Populate list of aliases for a given identifier in a context in which is an object is being read. More...

void	get_rhs_aliases_address_of (const exprt &, std::set< irep_idt > &)
	Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions. More...

Private Attributes
tvt	has_values

Additional Inherited Members
Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...

	ai_domain_baset (const ai_domain_baset &old)
	A copy constructor is part of the domain interface. More...

Detailed Description

Definition at line 22 of file global_may_alias.h.

Member Typedef Documentation

◆ aliasest

typedef union_find<irep_idt> global_may_alias_domaint::aliasest

Definition at line 86 of file global_may_alias.h.

Constructor & Destructor Documentation

◆ global_may_alias_domaint()

global_may_alias_domaint::global_may_alias_domaint ( )

inline

Definition at line 25 of file global_may_alias.h.

Member Function Documentation

◆ assign_lhs_aliases()

void global_may_alias_domaint::assign_lhs_aliases	(	const exprt &	lhs,
		const std::set< irep_idt > &	alias_set
	)

private

Populate list of aliases for a given identifier in a context in which an object is being written to.

Parameters

lhs	A left hand side expression, containing an identifier.
alias_set	An external set of aliases to populate internal aliases set.

Definition at line 21 of file global_may_alias.cpp.

◆ get_rhs_aliases()

void global_may_alias_domaint::get_rhs_aliases	(	const exprt &	rhs,
		std::set< irep_idt > &	alias_set
	)

private

Populate list of aliases for a given identifier in a context in which is an object is being read.

Parameters

rhs	A right hand side expression.
alias_set	A external set of aliases to populate internal aliases set.

Definition at line 43 of file global_may_alias.cpp.

◆ get_rhs_aliases_address_of()

void global_may_alias_domaint::get_rhs_aliases_address_of	(	const exprt &	rhs,
		std::set< irep_idt > &	alias_set
	)

private

Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.

Parameters

rhs	A right hand side expression.
alias_set	A external set of aliases to populate internal aliases set.

Definition at line 76 of file global_may_alias.cpp.

◆ is_bottom()

bool global_may_alias_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Returns true if domain is bottom.

Implements ai_domain_baset.

Definition at line 71 of file global_may_alias.h.

◆ is_top()

bool global_may_alias_domaint::is_top ( ) const

inlinefinaloverridevirtual

Returns false if domain is top.

Implements ai_domain_baset.

Definition at line 79 of file global_may_alias.h.

◆ make_bottom()

void global_may_alias_domaint::make_bottom ( )

inlinefinaloverridevirtual

Clear list of aliases, and mark domain as bottom.

Implements ai_domain_baset.

Definition at line 52 of file global_may_alias.h.

◆ make_entry()

void global_may_alias_domaint::make_entry ( )

inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 65 of file global_may_alias.h.

◆ make_top()

void global_may_alias_domaint::make_top ( )

inlinefinaloverridevirtual

Clear list of aliases, and mark domain as top.

Implements ai_domain_baset.

Definition at line 59 of file global_may_alias.h.

◆ merge()

bool global_may_alias_domaint::merge	(	const global_may_alias_domaint &	b,
		trace_ptrt	from,
		trace_ptrt	to
	)

Abstract Interpretation domain merge function.

Definition at line 196 of file global_may_alias.cpp.

◆ output()

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

finaloverridevirtual

Abstract Interpretation domain output function.

Parameters

out	A stream to dump domain state on.
ai	A reference to the currently active abstract interpreter.
ns	A namespace to resolve symbols during output.

Reimplemented from ai_domain_baset.

Definition at line 158 of file global_may_alias.cpp.

◆ transform()

void global_may_alias_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	trace_from,
		const irep_idt &	function_to,
		trace_ptrt	trace_to,
		ai_baset &	ai,
		const namespacet &	ns
	)

finaloverridevirtual

Abstract Interpretation domain transform function.

Implements ai_domain_baset.

Definition at line 95 of file global_may_alias.cpp.

Member Data Documentation

◆ aliases

aliasest global_may_alias_domaint::aliases

Definition at line 87 of file global_may_alias.h.

◆ has_values

tvt global_may_alias_domaint::has_values

private

Definition at line 90 of file global_may_alias.h.

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

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

Public Types

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ aliasest

Constructor & Destructor Documentation

◆ global_may_alias_domaint()

Member Function Documentation

◆ assign_lhs_aliases()

◆ get_rhs_aliases()

◆ get_rhs_aliases_address_of()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ merge()

◆ output()

◆ transform()

Member Data Documentation

◆ aliases

◆ has_values