#include <interval_domain.h>

Inheritance diagram for interval_domaint:

Collaboration diagram for interval_domaint:

Public Member Functions
	interval_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
	how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...

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

bool	merge (const interval_domaint &b, trace_ptrt, trace_ptrt)

void	make_bottom () final override
	no states More...

void	make_top () final override
	all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it. More...

bool	is_bottom () const override final

bool	is_top () const override final

exprt	make_expression (const symbol_exprt &) const

void	assume (const exprt &, const namespacet &)

virtual bool	ai_simplify (exprt &condition, const namespacet &ns) const override
	Uses the abstract state to simplify a given expression using context- specific information. 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 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...

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

Static Public Member Functions
static bool	is_int (const typet &src)

static bool	is_float (const typet &src)

Protected Types
typedef std::map< irep_idt, integer_intervalt >	int_mapt

typedef std::map< irep_idt, ieee_float_intervalt >	float_mapt

Protected Member Functions
bool	join (const interval_domaint &b)
	Sets *this to the mathematical join between the two domains. More...

void	havoc_rec (const exprt &)

void	assume_rec (const exprt &, bool negation=false)

void	assume_rec (const exprt &lhs, irep_idt id, const exprt &rhs)

void	assign (const exprt &lhs, const exprt &rhs)

integer_intervalt	get_int_rec (const exprt &)

ieee_float_intervalt	get_float_rec (const exprt &)

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

Protected Attributes
bool	bottom

int_mapt	int_map

float_mapt	float_map

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

typedef ai_history_baset::trace_ptrt	trace_ptrt

Detailed Description

Definition at line 23 of file interval_domain.h.

Member Typedef Documentation

◆ float_mapt

typedef std::map<irep_idt, ieee_float_intervalt> interval_domaint::float_mapt

protected

Definition at line 110 of file interval_domain.h.

◆ int_mapt

typedef std::map<irep_idt, integer_intervalt> interval_domaint::int_mapt

protected

Definition at line 109 of file interval_domain.h.

Constructor & Destructor Documentation

◆ interval_domaint()

interval_domaint::interval_domaint ( )

inline

Definition at line 30 of file interval_domain.h.

Member Function Documentation

◆ ai_simplify()

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

overridevirtual

Uses the abstract state to simplify a given expression using context- specific information.

parameters: The expression to simplify.

Returns: A simplified version of the expression.

Reimplemented from ai_domain_baset.

Definition at line 488 of file interval_domain.cpp.

◆ assign()

void interval_domaint::assign	(	const exprt &	lhs,
		const exprt &	rhs
	)

protected

Definition at line 211 of file interval_domain.cpp.

◆ assume()

void interval_domaint::assume	(	const exprt &	cond,
		const namespacet &	ns
	)

Definition at line 351 of file interval_domain.cpp.

◆ assume_rec() [1/2]

void interval_domaint::assume_rec	(	const exprt &	cond,
		bool	negation = `false`
	)

protected

Definition at line 358 of file interval_domain.cpp.

◆ assume_rec() [2/2]

void interval_domaint::assume_rec	(	const exprt &	lhs,
		irep_idt	id,
		const exprt &	rhs
	)

protected

Definition at line 239 of file interval_domain.cpp.

◆ get_float_rec()

ieee_float_intervalt interval_domaint::get_float_rec ( const exprt & )

protected

◆ get_int_rec()

integer_intervalt interval_domaint::get_int_rec ( const exprt & )

protected

◆ havoc_rec()

void interval_domaint::havoc_rec ( const exprt & lhs )

protected

Definition at line 217 of file interval_domain.cpp.

◆ is_bottom()

bool interval_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 72 of file interval_domain.h.

◆ is_float()

static bool interval_domaint::is_float ( const typet & src )

inlinestatic

Definition at line 97 of file interval_domain.h.

◆ is_int()

static bool interval_domaint::is_int ( const typet & src )

inlinestatic

Definition at line 92 of file interval_domain.h.

◆ is_top()

bool interval_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 83 of file interval_domain.h.

◆ join()

bool interval_domaint::join ( const interval_domaint & b )

protected

Sets *this to the mathematical join between the two domains.

This can be thought of as an abstract version of union; *this is increased so that it contains all of the values that are represented by b as well as its original intervals. The result is an overapproximation, for example: "[0,1]".join("[3,4]") --> "[0,4]" includes 2 which isn't in [0,1] or [3,4].

     Join is used in several places, the most significant being
     merge, which uses it to bring together two different paths
     of analysis.

parameters: The interval domain, b, to join to this domain.

Returns: True if the join increases the set represented by *this, False if there is no change.

Definition at line 153 of file interval_domain.cpp.

◆ make_bottom()

void interval_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 57 of file interval_domain.h.

◆ make_expression()

exprt interval_domaint::make_expression ( const symbol_exprt & src ) const

Definition at line 408 of file interval_domain.cpp.

◆ make_top()

void interval_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 65 of file interval_domain.h.

◆ merge()

bool interval_domaint::merge	(	const interval_domaint &	b,
		trace_ptrt	,
		trace_ptrt
	)

inline

Definition at line 51 of file interval_domain.h.

◆ output()

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

overridevirtual

Reimplemented from ai_domain_baset.

Definition at line 23 of file interval_domain.cpp.

◆ transform()

void interval_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	from,
		const irep_idt &	function_to,
		trace_ptrt	to,
		ai_baset &	ai,
		const namespacet &	ns
	)

finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implements ai_domain_baset.

Definition at line 59 of file interval_domain.cpp.

Member Data Documentation

◆ bottom

bool interval_domaint::bottom

protected

Definition at line 107 of file interval_domain.h.

◆ float_map

float_mapt interval_domaint::float_map

protected

Definition at line 113 of file interval_domain.h.

◆ int_map

int_mapt interval_domaint::int_map

protected

Definition at line 112 of file interval_domain.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/interval_domain.h
/home/runner/work/cbmc/cbmc/src/analyses/interval_domain.cpp

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ float_mapt

◆ int_mapt

Constructor & Destructor Documentation

◆ interval_domaint()

Member Function Documentation

◆ ai_simplify()

◆ assign()

◆ assume()

◆ assume_rec() [1/2]

◆ assume_rec() [2/2]

◆ get_float_rec()

◆ get_int_rec()

◆ havoc_rec()

◆ is_bottom()

◆ is_float()

◆ is_int()

◆ is_top()

◆ join()

◆ make_bottom()

◆ make_expression()

◆ make_top()

◆ merge()

◆ output()

◆ transform()

Member Data Documentation

◆ bottom

◆ float_map

◆ int_map