#include <variable_sensitivity_domain.h>

Inheritance diagram for variable_sensitivity_domaint:

Collaboration diagram for variable_sensitivity_domaint:

Public Member Functions
	variable_sensitivity_domaint (variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)

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) override
	Compute the abstract transformer for a single instruction. More...

void	make_bottom () override
	Sets the domain to bottom (no states / unreachable). More...

void	make_top () override
	Sets the domain to top (all states). More...

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
	Basic text output of the abstract domain. More...

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

exprt	to_predicate (const exprt &expr, const namespacet &ns) const

exprt	to_predicate (const exprt::operandst &exprs, const namespacet &ns) const

virtual bool	merge (const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
	Computes the join between "this" and "b". More...

virtual void	merge_three_way_function_return (const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
	Merges just the things that have changes between "function_start" and "function_end" into "this". More...

bool	ai_simplify (exprt &condition, const namespacet &ns) const override
	Use the information in the domain to simplify the expression with respect to the current location. More...

bool	is_bottom () const override
	Find out if the domain is currently unreachable. More...

bool	is_top () const override
	Is the domain completely top at this state. More...

virtual abstract_object_pointert	eval (const exprt &expr, const namespacet &ns) const

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 void	make_entry ()
	Make this domain a reasonable entry-point state For most domains top is sufficient. More...

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

Private Member Functions
void	transform_function_call (locationt from, locationt to, ai_baset &ai, const namespacet &ns)
	Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms. More...

bool	ignore_function_call_transform (const irep_idt &function_id) const
	Used to specify which CPROVER internal functions should be skipped over when doing function call transforms. More...

void	assume (exprt expr, namespacet ns)

Private Attributes
abstract_environmentt	abstract_state

flow_sensitivityt	flow_sensitivity

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

typedef ai_history_baset::trace_ptrt	trace_ptrt

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 115 of file variable_sensitivity_domain.h.

Constructor & Destructor Documentation

◆ variable_sensitivity_domaint()

variable_sensitivity_domaint::variable_sensitivity_domaint	(	variable_sensitivity_object_factory_ptrt	_object_factory,
		const vsd_configt &	_configuration
	)

inlineexplicit

Definition at line 118 of file variable_sensitivity_domain.h.

Member Function Documentation

◆ ai_simplify()

bool variable_sensitivity_domaint::ai_simplify	(	exprt &	condition,
		const namespacet &	ns
	)		const

overridevirtual

Use the information in the domain to simplify the expression with respect to the current location.

This may be able to reduce some values to constants.

Parameters

condition	the expression to simplify
ns	the namespace

Returns: True if no simplification was made

Reimplemented from ai_domain_baset.

Definition at line 241 of file variable_sensitivity_domain.cpp.

◆ assume()

void variable_sensitivity_domaint::assume	(	exprt	expr,
		namespacet	ns
	)

private

Definition at line 452 of file variable_sensitivity_domain.cpp.

◆ eval()

virtual abstract_object_pointert variable_sensitivity_domaint::eval	(	const exprt &	expr,
		const namespacet &	ns
	)		const

inlinevirtual

Definition at line 211 of file variable_sensitivity_domain.h.

◆ ignore_function_call_transform()

bool variable_sensitivity_domaint::ignore_function_call_transform ( const irep_idt & function_id ) const

private

Used to specify which CPROVER internal functions should be skipped over when doing function call transforms.

Parameters

function_id the name of the function being called

Returns: Returns true if the function should be ignored

Definition at line 403 of file variable_sensitivity_domain.cpp.

◆ is_bottom()

bool variable_sensitivity_domaint::is_bottom ( ) const

overridevirtual

Find out if the domain is currently unreachable.

Returns: True if the domain is bottom (i.e. unreachable).

Implements ai_domain_baset.

Definition at line 268 of file variable_sensitivity_domain.cpp.

◆ is_top()

bool variable_sensitivity_domaint::is_top ( ) const

overridevirtual

Is the domain completely top at this state.

Returns: True if the domain is top

Implements ai_domain_baset.

Definition at line 273 of file variable_sensitivity_domain.cpp.

◆ make_bottom()

void variable_sensitivity_domaint::make_bottom ( )

overridevirtual

Sets the domain to bottom (no states / unreachable).

Implements ai_domain_baset.

Definition at line 210 of file variable_sensitivity_domain.cpp.

◆ make_top()

void variable_sensitivity_domaint::make_top ( )

overridevirtual

Sets the domain to top (all states).

Implements ai_domain_baset.

Definition at line 216 of file variable_sensitivity_domain.cpp.

◆ merge()

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

virtual

Computes the join between "this" and "b".

Parameters

b	the other domain
from	it's preceding location
to	it's current location

Returns: true if something has changed.

Reimplemented in variable_sensitivity_dependence_domaint.

Definition at line 221 of file variable_sensitivity_domain.cpp.

◆ merge_three_way_function_return()

void variable_sensitivity_domaint::merge_three_way_function_return	(	const ai_domain_baset &	function_start,
		const ai_domain_baset &	function_end,
		const namespacet &	ns
	)

virtual

Merges just the things that have changes between "function_start" and "function_end" into "this".

To be used correctly "this" must be derived from the function call site. Anything that is not modified in the function (such as globals) will not be changed.

Parameters

function_start	The base of the diff - changes that have been made between here and the end will be retained.
function_end	The end of the merge - changes that have been made between the start and here will be retained.
ns	The global namespace

Reimplemented in variable_sensitivity_dependence_domaint.

Definition at line 419 of file variable_sensitivity_domain.cpp.

◆ output()

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

overridevirtual

Basic text output of the abstract domain.

Parameters

out	the output stream
ai	the abstract interpreter
ns	the namespace

Reimplemented from ai_domain_baset.

Definition at line 171 of file variable_sensitivity_domain.cpp.

◆ to_predicate() [1/3]

exprt variable_sensitivity_domaint::to_predicate ( void ) const

overridevirtual

Gives a Boolean condition that is true for all values represented by the domain.

This allows domains to be converted into program invariants.

Returns: exprt describing the domain

Reimplemented from ai_domain_baset.

Definition at line 179 of file variable_sensitivity_domain.cpp.

◆ to_predicate() [2/3]

exprt variable_sensitivity_domaint::to_predicate	(	const exprt &	expr,
		const namespacet &	ns
	)		const

Definition at line 184 of file variable_sensitivity_domain.cpp.

◆ to_predicate() [3/3]

exprt variable_sensitivity_domaint::to_predicate	(	const exprt::operandst &	exprs,
		const namespacet &	ns
	)		const

Definition at line 192 of file variable_sensitivity_domain.cpp.

◆ transform()

void variable_sensitivity_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
	)

overridevirtual

Compute the abstract transformer for a single instruction.

Parameters

function_from	the name of the function containing from
trace_from	the instruction before the abstract domain
function_to	the name of the function containing to
trace_to	the instruction after the abstract domain
ai	the abstract interpreter
ns	the namespace

Implements ai_domain_baset.

Definition at line 24 of file variable_sensitivity_domain.cpp.

◆ transform_function_call()

void variable_sensitivity_domaint::transform_function_call	(	locationt	from,
		locationt	to,
		ai_baset &	ai,
		const namespacet &	ns
	)

private

Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.

This is copying the values of the arguments into new symbols corresponding to the declared parameter names.

If the function call is opaque we currently top the return value and the value of any things whose address is passed into the function.

Parameters

from	the location to transform from which is a function call
to	the destination of the transform (potentially inside the function call)
ai	the abstract interpreter
ns	the namespace of the current state

Definition at line 278 of file variable_sensitivity_domain.cpp.

Member Data Documentation

◆ abstract_state

abstract_environmentt variable_sensitivity_domaint::abstract_state

private

Definition at line 245 of file variable_sensitivity_domain.h.

◆ flow_sensitivity

flow_sensitivityt variable_sensitivity_domaint::flow_sensitivity

private

Definition at line 246 of file variable_sensitivity_domain.h.

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

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

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ variable_sensitivity_domaint()

Member Function Documentation

◆ ai_simplify()

◆ assume()

◆ eval()

◆ ignore_function_call_transform()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_top()

◆ merge()

◆ merge_three_way_function_return()

◆ output()

◆ to_predicate() [1/3]

◆ to_predicate() [2/3]

◆ to_predicate() [3/3]

◆ transform()

◆ transform_function_call()

Member Data Documentation

◆ abstract_state

◆ flow_sensitivity