cprover
path_explorert Member List

This is the complete list of members for path_explorert, including all inherited members.

add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)bmctinline
add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler)bmctinline
all_properties(const goto_functionst &goto_functions, prop_convt &solver)bmctprotectedvirtual
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)bmctinline
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)bmctinlineprotected
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) constmessaget
cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)bmctprotected
debug() constmessagetinline
decide(const goto_functionst &, prop_convt &)bmctprotectedvirtual
do_conversion()bmctprotected
do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)bmctstatic
endl(mstreamt &m)messagetinlinestatic
eom(mstreamt &m)messagetinlinestatic
equationbmctprotected
error() constmessagetinline
error_trace()bmctprotectedvirtual
safety_checkert::error_tracesafety_checkert
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)messagetstatic
execute(abstract_goto_modelt &)bmct
freeze_program_variables()bmctprotectedvirtual
get_memory_model()bmctprotected
get_message_handler()messagetinline
get_mstream(unsigned message_level) constmessagetinline
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
memory_modelbmctprotected
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetmutableprotected
nsbmctprotected
operator()(const goto_functionst &goto_functions)bmctinlinevirtual
operator=(const messaget &other)messagetinline
optionsbmctprotected
outer_symbol_tablebmctprotected
output_graphml(resultt result)bmctprotected
path_explorert(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, std::function< bool(void)> callback_after_symex)path_explorertinline
path_storagebmctprotected
perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) overridepath_explorertprivatevirtual
progress() constmessagetinline
prop_convbmctprotected
report_failure()bmctprotectedvirtual
report_success()bmctprotectedvirtual
result() constmessagetinline
resultt enum namesafety_checkert
run(const goto_functionst &goto_functions)bmctinlinevirtual
run(abstract_goto_modelt &)bmct
run_decision_procedure(prop_convt &prop_conv)bmctprotectedvirtual
safety_checkert(const namespacet &_ns)safety_checkertexplicit
safety_checkert(const namespacet &_ns, message_handlert &_message_handler)safety_checkertexplicit
saved_statepath_explorertprotected
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
set_ui(ui_message_handlert::uit _ui)bmctinline
setup()bmct
show()bmctprotected
show_program()bmctprotectedvirtual
show_vcc()bmctprotectedvirtual
show_vcc_json(std::ostream &out)bmctprotectedvirtual
show_vcc_plain(std::ostream &out)bmctprotectedvirtual
slice()bmctprotected
statistics() constmessagetinline
status() constmessagetinline
stop_on_fail(prop_convt &solver)bmctprotectedvirtual
symexbmctprotected
symex_symbol_tablebmctprotected
trace_options()bmctinlineprotected
uibmctprotected
warning() constmessagetinline
~bmct()bmctinlinevirtual
~messaget()messagetvirtual