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
bluemessagetstatic
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, ui_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, ui_message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)bmctinlineprotected
boldmessagetstatic
bright_bluemessagetstatic
bright_cyanmessagetstatic
bright_greenmessagetstatic
bright_magentamessagetstatic
bright_redmessagetstatic
bright_yellowmessagetstatic
command(unsigned c)messagetinlinestatic
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) constmessaget
cover(const goto_functionst &goto_functions)bmctprotected
cyanmessagetstatic
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, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)bmctstatic
driver_callback_after_symexbmctprivate
eommessagetstatic
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
faintmessagetstatic
freeze_program_variables()bmctprotectedvirtual
get_memory_model()bmctprotected
get_message_handler()messagetinline
get_mstream(unsigned message_level) constmessagetinline
greenmessagetstatic
italicmessagetstatic
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
magentamessagetstatic
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, ui_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
redmessagetstatic
report_failure()bmctprotectedvirtual
report_failure(messaget &, ui_message_handlert &)bmctprotectedstatic
report_success()bmctprotectedvirtual
report_success(messaget &, ui_message_handlert &)bmctprotectedstatic
resetmessagetstatic
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
setup()bmct
show()bmctprotected
slice()bmctprotected
statistics() constmessagetinline
status() constmessagetinline
stop_on_fail(prop_convt &solver)bmctprotectedvirtual
symexbmctprotected
symex_symbol_tablebmctprotected
trace_options()bmctinlineprotected
ui_message_handlerbmctprotected
underlinemessagetstatic
warning() constmessagetinline
yellowmessagetstatic
~bmct()bmctinlinevirtual
~messaget()messagetvirtual