cprover
bmct Class Reference

#include <bmc.h>

Inheritance diagram for bmct:
[legend]
Collaboration diagram for bmct:
[legend]

Public Member Functions

 bmct (const optionst &_options, const symbol_tablet &_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv)
 
virtual resultt run (const goto_functionst &goto_functions)
 
virtual ~bmct ()
 
void set_ui (language_uit::uit _ui)
 
virtual resultt operator() (const goto_functionst &goto_functions)
 
- Public Member Functions inherited from safety_checkert
 safety_checkert (const namespacet &_ns)
 
 safety_checkert (const namespacet &_ns, message_handlert &_message_handler)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Public Attributes

expr_listt bmc_constraints
 
- Public Attributes inherited from safety_checkert
goto_tracet error_trace
 

Protected Member Functions

virtual decision_proceduret::resultt run_decision_procedure (prop_convt &prop_conv)
 
virtual resultt decide (const goto_functionst &, prop_convt &)
 
virtual void setup_unwind ()
 
virtual void do_unwind_module ()
 
void do_conversion ()
 
virtual void show_vcc ()
 
virtual void show_vcc_plain (std::ostream &out)
 
virtual void show_vcc_json (std::ostream &out)
 
virtual resultt all_properties (const goto_functionst &goto_functions, prop_convt &solver)
 
virtual resultt stop_on_fail (const goto_functionst &goto_functions, prop_convt &solver)
 
virtual void show_program ()
 
virtual void report_success ()
 
virtual void report_failure ()
 
virtual void error_trace ()
 
void output_graphml (resultt result, const goto_functionst &goto_functions)
 outputs witnesses in graphml format More...
 
bool cover (const goto_functionst &goto_functions, const optionst::value_listt &criteria)
 Try to cover all goals. More...
 

Protected Attributes

const optionstoptions
 
symbol_tablet new_symbol_table
 
namespacet ns
 
symex_target_equationt equation
 
symex_bmct symex
 
prop_convtprop_conv
 
language_uit::uit ui
 
- Protected Attributes inherited from safety_checkert
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Friends

class bmc_all_propertiest
 
class bmc_covert
 
class fault_localizationt
 

Additional Inherited Members

- Public Types inherited from safety_checkert
enum  resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR }
 
- 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
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 32 of file bmc.h.

Constructor & Destructor Documentation

§ bmct()

bmct::bmct ( const optionst _options,
const symbol_tablet _symbol_table,
message_handlert _message_handler,
prop_convt _prop_conv 
)
inline

§ ~bmct()

virtual bmct::~bmct ( )
inlinevirtual

Definition at line 54 of file bmc.h.

Member Function Documentation

§ all_properties()

safety_checkert::resultt bmct::all_properties ( const goto_functionst goto_functions,
prop_convt solver 
)
protectedvirtual

Definition at line 233 of file all_properties.cpp.

References messaget::get_message_handler(), and messaget::set_message_handler().

Referenced by decide().

§ cover()

bool bmct::cover ( const goto_functionst goto_functions,
const optionst::value_listt criteria 
)
protected

Try to cover all goals.

Definition at line 435 of file bmc_cover.cpp.

References messaget::get_message_handler(), and messaget::set_message_handler().

Referenced by run().

§ decide()

safety_checkert::resultt bmct::decide ( const goto_functionst goto_functions,
prop_convt prop_conv 
)
protectedvirtual

§ do_conversion()

§ do_unwind_module()

void bmct::do_unwind_module ( )
protectedvirtual

Definition at line 46 of file bmc.cpp.

Referenced by do_conversion().

§ error_trace()

§ operator()()

virtual resultt bmct::operator() ( const goto_functionst goto_functions)
inlinevirtual

Implements safety_checkert.

Definition at line 62 of file bmc.h.

References run().

§ output_graphml()

void bmct::output_graphml ( resultt  result,
const goto_functionst goto_functions 
)
protected

outputs witnesses in graphml format

Definition at line 93 of file bmc.cpp.

References equation, safety_checkert::error_trace, optionst::get_option(), graphml_witnesst::graph(), ns, options, safety_checkert::SAFE, safety_checkert::UNSAFE, and write_graphml().

Referenced by run(), and stop_on_fail().

§ report_failure()

§ report_success()

§ run()

§ run_decision_procedure()

§ set_ui()

void bmct::set_ui ( language_uit::uit  _ui)
inline

Definition at line 59 of file bmc.h.

References ui.

Referenced by cbmc_parse_optionst::do_bmc().

§ setup_unwind()

§ show_program()

void bmct::show_program ( )
protectedvirtual

Definition at line 221 of file bmc.cpp.

References equation, languagest::from_expr(), languages, new_ansi_c_language(), ns, and symex_target_equationt::SSA_steps.

Referenced by run().

§ show_vcc()

§ show_vcc_json()

§ show_vcc_plain()

void bmct::show_vcc_plain ( std::ostream &  out)
protectedvirtual

§ stop_on_fail()

Friends And Related Function Documentation

§ bmc_all_propertiest

friend class bmc_all_propertiest
friend

Definition at line 114 of file bmc.h.

§ bmc_covert

friend class bmc_covert
friend

Definition at line 115 of file bmc.h.

§ fault_localizationt

friend class fault_localizationt
friend

Definition at line 116 of file bmc.h.

Member Data Documentation

§ bmc_constraints

expr_listt bmct::bmc_constraints

Definition at line 57 of file bmc.h.

Referenced by do_conversion().

§ equation

§ new_symbol_table

symbol_tablet bmct::new_symbol_table
protected

Definition at line 70 of file bmc.h.

§ ns

§ options

const optionst& bmct::options
protected

§ prop_conv

§ symex

symex_bmct bmct::symex
protected

Definition at line 73 of file bmc.h.

Referenced by bmct(), run(), and setup_unwind().

§ ui


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