This is the basic interface of the abstract interpreter with default implementations of the core functionality. More...

#include <ai.h>

Inheritance diagram for ai_baset:

Public Types
typedef ai_domain_baset	statet

Public Member Functions
	ai_baset ()=default
void	operator() (const goto_programt &goto_program, const namespacet &ns)
	Run analysis over Program.
void	operator() (const goto_functionst &goto_functions, const namespacet &ns)
	Run analysis over Module (Goto Functions).
virtual std::unique_ptr< statet >	abstract_state_before (goto_programt::const_targett l) const =0
virtual std::unique_ptr< statet >	abstract_state_after (goto_programt::const_targett l) const
virtual void	clear ()
	Resets the domain.
virtual void	output (const goto_functionst &goto_functions, std::ostream &out) const

Public Attributes
bool	continue_past_failed_assertions = false
	goto_programt::get_successors gives an ASSERT whose guard is false no successor, as though a violation ended the run.

Protected Types
typedef std::unordered_map< unsigned, goto_programt::const_targett >	working_sett

Protected Member Functions
virtual void	initialize (const goto_programt &)
virtual void	initialize (const goto_functiont &)
virtual void	initialize (const goto_functionst &)
virtual void	finalize ()
void	entry_state (const goto_programt &)
void	entry_state (const goto_functionst &)
goto_programt::const_targett	get_next (working_sett &working_set)
void	put_in_working_set (working_sett &working_set, goto_programt::const_targett l)
bool	fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
virtual void	fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)=0
void	sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
bool	visit (goto_programt::const_targett l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
bool	do_function_call_rec (goto_programt::const_targett l_call, goto_programt::const_targett l_return, const expr2tc &function, const goto_functionst &goto_functions, const namespacet &ns)
bool	do_function_call (goto_programt::const_targett l_call, goto_programt::const_targett l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const namespacet &ns)
virtual bool	merge (const statet &src, goto_programt::const_targett from, goto_programt::const_targett to)=0
virtual bool	merge_shared (const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns)=0
virtual statet &	get_state (goto_programt::const_targett l)=0
virtual const statet &	find_state (goto_programt::const_targett l) const =0
virtual std::unique_ptr< statet >	make_temporary_state (const statet &s)=0

Detailed Description

This is the basic interface of the abstract interpreter with default implementations of the core functionality.

Users of abstract interpreters should use the interface given by this class. It breaks into three categories:

Running an analysis, via operator() overloads
Accessing the results of an analysis, by looking up the state map
Outputting the results of the analysis;

Member Typedef Documentation

◆ statet

typedef ai_domain_baset ai_baset::statet

◆ working_sett

typedef std::unordered_map<unsigned, goto_programt::const_targett> ai_baset::working_sett

protected

Constructor & Destructor Documentation

◆ ai_baset()

ai_baset::ai_baset ( )

default

Member Function Documentation

◆ abstract_state_after()

virtual std::unique_ptr< statet > ai_baset::abstract_state_after ( goto_programt::const_targett l ) const

inlinevirtual

◆ abstract_state_before()

virtual std::unique_ptr< statet > ai_baset::abstract_state_before ( goto_programt::const_targett l ) const

pure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ clear()

virtual void ai_baset::clear ( )

inlinevirtual

Resets the domain.

Reimplemented in ait< domainT >, and ait< cse_domaint >.

◆ do_function_call()

bool ai_baset::do_function_call	(	goto_programt::const_targett	l_call,
		goto_programt::const_targett	l_return,
		const goto_functionst &	goto_functions,
		const goto_functionst::function_mapt::const_iterator	f_it,
		const namespacet &	ns )

protected

◆ do_function_call_rec()

bool ai_baset::do_function_call_rec	(	goto_programt::const_targett	l_call,
		goto_programt::const_targett	l_return,
		const expr2tc &	function,
		const goto_functionst &	goto_functions,
		const namespacet &	ns )

protected

◆ entry_state() [1/2]

void ai_baset::entry_state ( const goto_functionst & goto_functions )

protected

◆ entry_state() [2/2]

void ai_baset::entry_state ( const goto_programt & goto_program )

protected

◆ finalize()

void ai_baset::finalize ( )

protectedvirtual

◆ find_state()

virtual const statet & ai_baset::find_state ( goto_programt::const_targett l ) const

protectedpure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ fixedpoint() [1/2]

virtual void ai_baset::fixedpoint	(	const goto_functionst &	goto_functions,
		const namespacet &	ns )

protectedpure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ fixedpoint() [2/2]

bool ai_baset::fixedpoint	(	const goto_programt &	goto_program,
		const goto_functionst &	goto_functions,
		const namespacet &	ns )

protected

◆ get_next()

goto_programt::const_targett ai_baset::get_next ( working_sett & working_set )

protected

◆ get_state()

virtual statet & ai_baset::get_state ( goto_programt::const_targett l )

protectedpure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ initialize() [1/3]

void ai_baset::initialize ( const goto_functionst & goto_functions )

protectedvirtual

◆ initialize() [2/3]

void ai_baset::initialize ( const goto_functiont & goto_function )

protectedvirtual

◆ initialize() [3/3]

void ai_baset::initialize ( const goto_programt & goto_program )

protectedvirtual

◆ make_temporary_state()

virtual std::unique_ptr< statet > ai_baset::make_temporary_state ( const statet & s )

protectedpure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ merge()

virtual bool ai_baset::merge	(	const statet &	src,
		goto_programt::const_targett	from,
		goto_programt::const_targett	to )

protectedpure virtual

Implemented in ait< domainT >, and ait< cse_domaint >.

◆ merge_shared()

virtual bool ai_baset::merge_shared	(	const statet &	src,
		goto_programt::const_targett	from,
		goto_programt::const_targett	to,
		const namespacet &	ns )

protectedpure virtual

◆ operator()() [1/2]

void ai_baset::operator()	(	const goto_functionst &	goto_functions,
		const namespacet &	ns )

inline

Run analysis over Module (Goto Functions).

Parameters

goto_functions	functions under analysis
ns	current namespace

◆ operator()() [2/2]

void ai_baset::operator()	(	const goto_programt &	goto_program,
		const namespacet &	ns )

inline

Run analysis over Program.

Parameters

goto_program	prograam under analysis
ns	current namespace

◆ output()

void ai_baset::output	(	const goto_functionst &	goto_functions,
		std::ostream &	out ) const

virtual

◆ put_in_working_set()

void ai_baset::put_in_working_set	(	working_sett &	working_set,
		goto_programt::const_targett	l )

inlineprotected

◆ sequential_fixedpoint()

void ai_baset::sequential_fixedpoint	(	const goto_functionst &	goto_functions,
		const namespacet &	ns )

protected

◆ visit()

bool ai_baset::visit	(	goto_programt::const_targett	l,
		working_sett &	working_set,
		const goto_programt &	goto_program,
		const goto_functionst &	goto_functions,
		const namespacet &	ns )

protected

Member Data Documentation

◆ continue_past_failed_assertions

bool ai_baset::continue_past_failed_assertions = false

goto_programt::get_successors gives an ASSERT whose guard is false no successor, as though a violation ended the run.

Symex continues past a failed assertion, so a run that checks claims beyond one (–multi-property, coverage) must set this, or the states that follow the violation are missing from every invariant computed here.

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

src/goto-programs/abstract-interpretation/ai.h
src/goto-programs/abstract-interpretation/ai.cpp

Public Types

Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Detailed Description

Member Typedef Documentation

◆ statet

◆ working_sett

Constructor & Destructor Documentation

◆ ai_baset()

Member Function Documentation

◆ abstract_state_after()

◆ abstract_state_before()

◆ clear()

◆ do_function_call()

◆ do_function_call_rec()

◆ entry_state() [1/2]

◆ entry_state() [2/2]

◆ finalize()

◆ find_state()

◆ fixedpoint() [1/2]

◆ fixedpoint() [2/2]

◆ get_next()

◆ get_state()

◆ initialize() [1/3]

◆ initialize() [2/3]

◆ initialize() [3/3]

◆ make_temporary_state()

◆ merge()

◆ merge_shared()

◆ operator()() [1/2]

◆ operator()() [2/2]

◆ output()

◆ put_in_working_set()

◆ sequential_fixedpoint()

◆ visit()

Member Data Documentation

◆ continue_past_failed_assertions