cprover
|
This is the complete list of members for path_explorert, including all inherited members.
add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler) | bmct | inline |
add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler) | bmct | inline |
all_properties(const goto_functionst &goto_functions, prop_convt &solver) | bmct | protectedvirtual |
blue | messaget | static |
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) | bmct | inline |
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) | bmct | inlineprotected |
bold | messaget | static |
bright_blue | messaget | static |
bright_cyan | messaget | static |
bright_green | messaget | static |
bright_magenta | messaget | static |
bright_red | messaget | static |
bright_yellow | messaget | static |
command(unsigned c) | messaget | inlinestatic |
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const | messaget | |
cover(const goto_functionst &goto_functions) | bmct | protected |
cyan | messaget | static |
debug() const | messaget | inline |
decide(const goto_functionst &, prop_convt &) | bmct | protectedvirtual |
do_conversion() | bmct | protected |
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) | bmct | static |
eom | messaget | static |
equation | bmct | protected |
error() const | messaget | inline |
error_trace() | bmct | protectedvirtual |
safety_checkert::error_trace | safety_checkert | |
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest) | messaget | static |
execute(abstract_goto_modelt &) | bmct | |
faint | messaget | static |
freeze_program_variables() | bmct | protectedvirtual |
get_memory_model() | bmct | protected |
get_message_handler() | messaget | inline |
get_mstream(unsigned message_level) const | messaget | inline |
green | messaget | static |
italic | messaget | static |
M_DEBUG enum value | messaget | |
M_ERROR enum value | messaget | |
M_PROGRESS enum value | messaget | |
M_RESULT enum value | messaget | |
M_STATISTICS enum value | messaget | |
M_STATUS enum value | messaget | |
M_WARNING enum value | messaget | |
magenta | messaget | static |
memory_model | bmct | protected |
message_handler | messaget | protected |
message_levelt enum name | messaget | |
messaget() | messaget | inline |
messaget(const messaget &other) | messaget | inline |
messaget(message_handlert &_message_handler) | messaget | inlineexplicit |
mstream | messaget | mutableprotected |
ns | bmct | protected |
operator()(const goto_functionst &goto_functions) | bmct | inlinevirtual |
operator=(const messaget &other) | messaget | inline |
options | bmct | protected |
outer_symbol_table | bmct | protected |
output_graphml(resultt result) | bmct | protected |
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_explorert | inline |
path_storage | bmct | protected |
perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override | path_explorert | privatevirtual |
progress() const | messaget | inline |
prop_conv | bmct | protected |
red | messaget | static |
report_failure() | bmct | protectedvirtual |
report_failure(messaget &, ui_message_handlert &) | bmct | protectedstatic |
report_success() | bmct | protectedvirtual |
report_success(messaget &, ui_message_handlert &) | bmct | protectedstatic |
reset | messaget | static |
result() const | messaget | inline |
resultt enum name | safety_checkert | |
run(const goto_functionst &goto_functions) | bmct | inlinevirtual |
run(abstract_goto_modelt &) | bmct | |
run_decision_procedure(prop_convt &prop_conv) | bmct | protectedvirtual |
safety_checkert(const namespacet &_ns) | safety_checkert | explicit |
safety_checkert(const namespacet &_ns, message_handlert &_message_handler) | safety_checkert | explicit |
saved_state | path_explorert | protected |
set_message_handler(message_handlert &_message_handler) | messaget | inlinevirtual |
setup() | bmct | |
show() | bmct | protected |
slice() | bmct | protected |
statistics() const | messaget | inline |
status() const | messaget | inline |
stop_on_fail(prop_convt &solver) | bmct | protectedvirtual |
symex | bmct | protected |
symex_symbol_table | bmct | protected |
trace_options() | bmct | inlineprotected |
ui_message_handler | bmct | protected |
underline | messaget | static |
warning() const | messaget | inline |
yellow | messaget | static |
~bmct() | bmct | inlinevirtual |
~messaget() | messaget | virtual |