#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	make_entry () override
	Set up a reasonable entry-point state. 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_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
	Perform a context aware merge of the changes that have been applied between function_start and the current state. 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 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...

std::vector< irep_idt >	get_modified_symbols (const variable_sensitivity_domaint &other) const
	Get symbols that have been modified since this domain and other. More...

void	apply_domain (std::vector< symbol_exprt > modified_symbols, const variable_sensitivity_domaint &target, const namespacet &ns)
	Given a domain and some symbols, apply those symbols values to the current domain. 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 116 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 119 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 245 of file variable_sensitivity_domain.cpp.

◆ apply_domain()

void variable_sensitivity_domaint::apply_domain	(	std::vector< symbol_exprt >	modified_symbols,
		const variable_sensitivity_domaint &	target,
		const namespacet &	ns
	)

private

Given a domain and some symbols, apply those symbols values to the current domain.

Parameters

modified_symbols	The symbols to write
target	The domain to take the values from
ns	The global namespace

Definition at line 462 of file variable_sensitivity_domain.cpp.

◆ assume()

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

private

Definition at line 474 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 216 of file variable_sensitivity_domain.h.

◆ get_modified_symbols()

std::vector< irep_idt > variable_sensitivity_domaint::get_modified_symbols ( const variable_sensitivity_domaint & other ) const

private

Get symbols that have been modified since this domain and other.

Parameters

other The domain that things may have been modified in

Returns: A list of symbols whose write location is different

Definition at line 282 of file variable_sensitivity_domain.cpp.

◆ 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 414 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 272 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 277 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 209 of file variable_sensitivity_domain.cpp.

◆ make_entry()

void variable_sensitivity_domaint::make_entry ( )

overridevirtual

Set up a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 220 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 215 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 225 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_call,
		const ai_domain_baset &	function_start,
		const ai_domain_baset &	function_end,
		const namespacet &	ns
	)

virtual

Perform a context aware merge of the changes that have been applied between function_start and the current state.

Anything that has not been modified will be taken from the function_call domain.

Parameters

function_call	The local of the merge - values from here will be taken if they have not been modified
function_start	The base of the merge - 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 430 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 170 of file variable_sensitivity_domain.cpp.

◆ to_predicate() [1/3]

exprt variable_sensitivity_domaint::to_predicate ( ) 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 178 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 183 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 191 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 23 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 289 of file variable_sensitivity_domain.cpp.

Member Data Documentation

◆ abstract_state

abstract_environmentt variable_sensitivity_domaint::abstract_state

private

Definition at line 266 of file variable_sensitivity_domain.h.

◆ flow_sensitivity

flow_sensitivityt variable_sensitivity_domaint::flow_sensitivity

private

Definition at line 267 of file variable_sensitivity_domain.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/variable-sensitivity/variable_sensitivity_domain.h
/home/runner/work/cbmc-documentation/cbmc-documentation/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()

◆ apply_domain()

◆ assume()

◆ eval()

◆ get_modified_symbols()

◆ ignore_function_call_transform()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ 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