build_full_trace() const override | single_path_symex_checkert | virtual |
build_shortest_trace() const override | single_path_symex_checkert | virtual |
build_trace(const irep_idt &) const override | single_path_symex_checkert | virtual |
equation_output(const symex_bmct &symex, const symex_target_equationt &equation) | single_path_symex_only_checkert | protected |
final_update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties) | single_path_symex_only_checkert | protectedvirtual |
get_namespace() const override | single_path_symex_checkert | virtual |
goto_model | single_path_symex_only_checkert | protected |
guard_manager | single_path_symex_only_checkert | protected |
has_finished_exploration(const propertiest &) | single_path_symex_only_checkert | protectedvirtual |
incremental_goto_checkert()=delete | incremental_goto_checkert | |
incremental_goto_checkert(const incremental_goto_checkert &)=delete | incremental_goto_checkert | |
incremental_goto_checkert(const optionst &, ui_message_handlert &) | incremental_goto_checkert | protected |
initialize_worklist() | single_path_symex_only_checkert | protectedvirtual |
is_ready_to_decide(const symex_bmct &, const path_storaget::patht &) override | single_path_symex_checkert | protectedvirtual |
log | incremental_goto_checkert | protected |
ns | single_path_symex_only_checkert | protected |
operator()(propertiest &) override | single_path_symex_checkert | virtual |
options | incremental_goto_checkert | protected |
output_error_witness(const goto_tracet &) override | single_path_symex_checkert | virtual |
output_proof() override | single_path_symex_checkert | virtual |
prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider) | single_path_symex_checkert | protectedvirtual |
property_decider | single_path_symex_checkert | protected |
report() | incremental_goto_checkert | inlinevirtual |
resume_path(path_storaget::patht &path) | single_path_symex_only_checkert | protectedvirtual |
run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, std::chrono::duration< double > solver_runtime) | single_path_symex_checkert | protectedvirtual |
setup_symex(symex_bmct &symex) | single_path_symex_only_checkert | protectedvirtual |
single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | single_path_symex_checkert | |
single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model) | single_path_symex_only_checkert | |
symex_initialized | single_path_symex_checkert | protected |
symex_runtime | single_path_symex_only_checkert | protected |
symex_symbol_table | single_path_symex_only_checkert | protected |
ui_message_handler | incremental_goto_checkert | protected |
unwindset | single_path_symex_only_checkert | protected |
update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation) | single_path_symex_only_checkert | protectedvirtual |
worklist | single_path_symex_only_checkert | protected |
~goto_trace_providert()=default | goto_trace_providert | virtual |
~incremental_goto_checkert()=default | incremental_goto_checkert | virtual |
~single_path_symex_checkert()=default | single_path_symex_checkert | virtual |
~single_path_symex_only_checkert()=default | single_path_symex_only_checkert | virtual |
~witness_providert()=default | witness_providert | virtual |