bmc_covert Class Reference

Inheritance diagram for bmc_covert:

Collaboration diagram for bmc_covert:

Classes
struct	goalt
struct	testt

Public Types
typedef std::map< irep_idt, goalt >	goal_mapt
typedef std::vector< testt >	testst
Public Types inherited from messaget
enum	message_levelt {   M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,   M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Public Member Functions
	bmc_covert (const goto_functionst &_goto_functions, bmct &_bmc)
bool	operator() ()
virtual void	satisfying_assignment ()
irep_idt	id (goto_programt::const_targett loc)
std::string	get_test (const goto_tracet &goto_trace) const
Public Member Functions inherited from cover_goalst::observert
virtual void	goal_covered (const goalt &)
Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)
message_handlert &	get_message_handler ()
	messaget ()
	messaget (const messaget &other)
messaget &	operator= (const messaget &other)
	messaget (message_handlert &_message_handler)
virtual	~messaget ()
mstreamt &	get_mstream (unsigned message_level) const
mstreamt &	error () const
mstreamt &	warning () const
mstreamt &	result () const
mstreamt &	status () const
mstreamt &	statistics () const
mstreamt &	progress () const
mstreamt &	debug () const
void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...

Public Attributes
goal_mapt	goal_map
testst	tests

Protected Attributes
const goto_functionst &	goto_functions
prop_convt &	solver
bmct &	bmc
Protected Attributes inherited from messaget
message_handlert *	message_handler
mstreamt	mstream

Additional Inherited Members
Static Public Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
Static Public Attributes inherited from messaget
static eomt	eom
static const commandt	reset
	return to default formatting, as defined by the terminal More...
static const commandt	red
	render text with red foreground color More...
static const commandt	green
	render text with green foreground color More...
static const commandt	yellow
	render text with yellow foreground color More...
static const commandt	blue
	render text with blue foreground color More...
static const commandt	magenta
	render text with magenta foreground color More...
static const commandt	cyan
	render text with cyan foreground color More...
static const commandt	bright_red
	render text with bright red foreground color More...
static const commandt	bright_green
	render text with bright green foreground color More...
static const commandt	bright_yellow
	render text with bright yellow foreground color More...
static const commandt	bright_blue
	render text with bright blue foreground color More...
static const commandt	bright_magenta
	render text with bright magenta foreground color More...
static const commandt	bright_cyan
	render text with bright cyan foreground color More...
static const commandt	bold
	render text with bold font More...
static const commandt	faint
	render text with faint font More...
static const commandt	italic
	render italic text More...
static const commandt	underline
	render underlined text More...

Detailed Description

Definition at line 32 of file bmc_cover.cpp.

Member Typedef Documentation

goal_mapt

typedef std::map<irep_idt, goalt> bmc_covert::goal_mapt

Definition at line 112 of file bmc_cover.cpp.

testst

typedef std::vector<testt> bmc_covert::testst

Definition at line 114 of file bmc_cover.cpp.

Constructor & Destructor Documentation

bmc_covert()

bmc_covert::bmc_covert ( const goto_functionst &  _goto_functions, bmct &  _bmc  )

inline

Definition at line 37 of file bmc_cover.cpp.

Member Function Documentation

get_test()

std::string bmc_covert::get_test ( const goto_tracet &  goto_trace ) const

inline

Definition at line 117 of file bmc_cover.cpp.

id()

irep_idt bmc_covert::id ( goto_programt::const_targett  loc )

inline

Definition at line 107 of file bmc_cover.cpp.

operator()()

bool bmc_covert::operator()

(

void

)

Definition at line 185 of file bmc_cover.cpp.

satisfying_assignment()

void bmc_covert::satisfying_assignment ( )

virtual

Reimplemented from cover_goalst::observert.

Definition at line 152 of file bmc_cover.cpp.

Member Data Documentation

bmc

bmct& bmc_covert::bmc

protected

Definition at line 142 of file bmc_cover.cpp.

goal_map

goal_mapt bmc_covert::goal_map

Definition at line 113 of file bmc_cover.cpp.

goto_functions

const goto_functionst& bmc_covert::goto_functions

protected

Definition at line 140 of file bmc_cover.cpp.

solver

prop_convt& bmc_covert::solver

protected

Definition at line 141 of file bmc_cover.cpp.

tests

testst bmc_covert::tests

Definition at line 115 of file bmc_cover.cpp.

---

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

• cbmc/bmc_cover.cpp