cprover
|
#include <path_search.h>
Classes | |
struct | loc_datat |
struct | property_entryt |
Public Types | |
enum | statust { NOT_REACHED, SUCCESS, FAILURE } |
typedef std::map< irep_idt, property_entryt > | property_mapt |
![]() | |
enum | resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR } |
Public Member Functions | |
path_searcht (const namespacet &_ns) | |
virtual resultt | operator() (const goto_functionst &goto_functions) |
void | set_depth_limit (int limit) |
void | set_context_bound (int limit) |
void | set_branch_bound (int limit) |
void | set_unwind_limit (int limit) |
void | set_time_limit (int limit) |
void | set_dfs () |
void | set_bfs () |
void | set_locs () |
![]() | |
safety_checkert (const namespacet &_ns) | |
safety_checkert (const namespacet &_ns, message_handlert &_message_handler) | |
Public Attributes | |
bool | show_vcc |
bool | eager_infeasibility |
std::size_t | number_of_dropped_states |
std::size_t | number_of_paths |
std::size_t | number_of_steps |
std::size_t | number_of_feasible_paths |
std::size_t | number_of_infeasible_paths |
std::size_t | number_of_VCCs |
std::size_t | number_of_VCCs_after_simplification |
std::size_t | number_of_failed_properties |
std::size_t | number_of_locs |
absolute_timet | start_time |
time_periodt | sat_time |
property_mapt | property_map |
![]() | |
goto_tracet | error_trace |
Protected Types | |
enum | search_heuristict { search_heuristict::DFS, search_heuristict::BFS, search_heuristict::LOCS } |
typedef path_symex_statet | statet |
typedef std::list< statet > | queuet |
Protected Member Functions | |
void | pick_state () |
bool | execute (queuet::iterator state) |
void | check_assertion (statet &state) |
bool | is_feasible (statet &state) |
void | do_show_vcc (statet &state) |
bool | drop_state (const statet &state) |
decide whether to drop a state More... | |
void | report_statistics () |
void | initialize_property_map (const goto_functionst &goto_functions) |
Protected Attributes | |
queuet | queue |
expanding_vectort< loc_datat > | loc_data |
unsigned | depth_limit |
unsigned | context_bound |
unsigned | branch_bound |
unsigned | unwind_limit |
unsigned | time_limit |
enum path_searcht::search_heuristict | search_heuristic |
source_locationt | last_source_location |
![]() | |
const namespacet & | ns |
Additional Inherited Members |
Definition at line 24 of file path_search.h.
typedef std::map<irep_idt, property_entryt> path_searcht::property_mapt |
Definition at line 102 of file path_search.h.
|
protected |
Definition at line 110 of file path_search.h.
|
protected |
Definition at line 106 of file path_search.h.
|
strongprotected |
Enumerator | |
---|---|
DFS | |
BFS | |
LOCS |
Definition at line 143 of file path_search.h.
Enumerator | |
---|---|
NOT_REACHED | |
SUCCESS | |
FAILURE |
Definition at line 84 of file path_search.h.
|
inlineexplicit |
Definition at line 27 of file path_search.h.
|
protected |
Definition at line 375 of file path_search.cpp.
References build_goto_trace(), path_symex_statet::check_assertion(), current_time(), messaget::eom(), path_searcht::property_entryt::error_trace, FAILURE, path_symex_statet::get_instruction(), messaget::get_message_handler(), exprt::is_true(), NOT_REACHED, safety_checkert::ns, number_of_failed_properties, number_of_VCCs, number_of_VCCs_after_simplification, property_map, path_symex_statet::read(), sat_time, messaget::set_message_handler(), path_searcht::property_entryt::status, messaget::status(), and SUCCESS.
Referenced by operator()().
|
protected |
Definition at line 213 of file path_search.cpp.
References path_symex_step_reft::build_history(), messaget::eom(), from_expr(), source_locationt::get_comment(), path_symex_statet::get_instruction(), path_symex_statet::history, exprt::is_true(), safety_checkert::ns, number_of_VCCs, number_of_VCCs_after_simplification, path_symex_statet::read(), messaget::result(), and messaget::mstreamt::source_location.
Referenced by operator()().
|
protected |
decide whether to drop a state
Definition at line 266 of file path_search.cpp.
References branch_bound, context_bound, current_time(), messaget::debug(), depth_limit, dstringt::empty(), messaget::eom(), code_function_callt::function(), path_symex_statet::get_current_thread(), path_symex_statet::get_depth(), source_locationt::get_file(), source_locationt::get_function(), path_symex_statet::get_instruction(), source_locationt::get_line(), path_symex_statet::get_no_branches(), path_symex_statet::get_no_thread_interleavings(), fine_timet::get_t(), exprt::is_false(), irept::is_nil(), last_source_location, goto_program_templatet< codet, exprt >::loop_id(), safety_checkert::ns, path_symex_statet::pc(), path_symex_statet::recursion_map, simplify_expr(), messaget::mstreamt::source_location, start_time, time_limit, to_code_function_call(), unwind_limit, and path_symex_statet::unwinding_map.
Referenced by operator()().
|
protected |
|
protected |
Definition at line 442 of file path_search.cpp.
References path_searcht::property_entryt::description, forall_goto_functions, forall_goto_program_instructions, source_locationt::get_comment(), source_locationt::get_property_id(), NOT_REACHED, property_map, path_searcht::property_entryt::source_location, and path_searcht::property_entryt::status.
Referenced by operator()().
|
protected |
Definition at line 422 of file path_search.cpp.
References current_time(), messaget::eom(), messaget::get_message_handler(), path_symex_statet::is_feasible(), safety_checkert::ns, messaget::result(), sat_time, messaget::set_message_handler(), and messaget::status().
Referenced by operator()().
|
virtual |
Implements safety_checkert.
Definition at line 23 of file path_search.cpp.
References locst::build(), check_assertion(), current_time(), messaget::debug(), do_show_vcc(), drop_state(), eager_infeasibility, messaget::eom(), messaget::error(), path_symex_statet::get_current_thread(), path_symex_statet::get_depth(), path_symex_statet::get_instruction(), initial_state(), initialize_property_map(), path_symex_statet::is_executable(), is_feasible(), path_symex_statet::last_was_branch(), loc_data, loc_reft::loc_number, safety_checkert::ns, number_of_dropped_states, number_of_failed_properties, number_of_feasible_paths, number_of_infeasible_paths, number_of_locs, number_of_paths, number_of_steps, number_of_VCCs, number_of_VCCs_after_simplification, path_symex(), path_symex_statet::pc(), pick_state(), property_map, queue, report_statistics(), safety_checkert::SAFE, show_vcc, locst::size(), start_time, messaget::status(), path_symex_statet::threads, and safety_checkert::UNSAFE.
|
protected |
Definition at line 193 of file path_search.cpp.
References BFS, DFS, LOCS, queue, and search_heuristic.
Referenced by operator()().
|
protected |
Definition at line 156 of file path_search.cpp.
References current_time(), messaget::eom(), loc_data, number_of_dropped_states, number_of_infeasible_paths, number_of_locs, number_of_paths, number_of_VCCs, number_of_VCCs_after_simplification, sat_time, start_time, and messaget::status().
Referenced by operator()().
|
inline |
Definition at line 99 of file path_search.h.
References BFS, and search_heuristic.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 53 of file path_search.h.
References branch_bound.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 48 of file path_search.h.
References context_bound.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 43 of file path_search.h.
References depth_limit.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 98 of file path_search.h.
References DFS, and search_heuristic.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 100 of file path_search.h.
References LOCS, and search_heuristic.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 63 of file path_search.h.
References time_limit.
Referenced by symex_parse_optionst::doit().
|
inline |
Definition at line 58 of file path_search.h.
References unwind_limit.
Referenced by symex_parse_optionst::doit().
|
protected |
Definition at line 139 of file path_search.h.
Referenced by drop_state(), and set_branch_bound().
|
protected |
Definition at line 138 of file path_search.h.
Referenced by drop_state(), and set_context_bound().
|
protected |
Definition at line 137 of file path_search.h.
Referenced by drop_state(), and set_depth_limit().
bool path_searcht::eager_infeasibility |
Definition at line 69 of file path_search.h.
Referenced by symex_parse_optionst::doit(), and operator()().
|
protected |
Definition at line 145 of file path_search.h.
Referenced by drop_state().
|
protected |
Definition at line 122 of file path_search.h.
Referenced by operator()(), and report_statistics().
std::size_t path_searcht::number_of_dropped_states |
Definition at line 72 of file path_search.h.
Referenced by operator()(), and report_statistics().
std::size_t path_searcht::number_of_failed_properties |
Definition at line 79 of file path_search.h.
Referenced by check_assertion(), and operator()().
std::size_t path_searcht::number_of_feasible_paths |
Definition at line 75 of file path_search.h.
Referenced by operator()().
std::size_t path_searcht::number_of_infeasible_paths |
Definition at line 76 of file path_search.h.
Referenced by operator()(), and report_statistics().
std::size_t path_searcht::number_of_locs |
Definition at line 80 of file path_search.h.
Referenced by operator()(), and report_statistics().
std::size_t path_searcht::number_of_paths |
Definition at line 73 of file path_search.h.
Referenced by operator()(), and report_statistics().
std::size_t path_searcht::number_of_steps |
Definition at line 74 of file path_search.h.
Referenced by operator()().
std::size_t path_searcht::number_of_VCCs |
Definition at line 77 of file path_search.h.
Referenced by check_assertion(), do_show_vcc(), operator()(), and report_statistics().
std::size_t path_searcht::number_of_VCCs_after_simplification |
Definition at line 78 of file path_search.h.
Referenced by check_assertion(), do_show_vcc(), operator()(), and report_statistics().
property_mapt path_searcht::property_map |
Definition at line 103 of file path_search.h.
Referenced by check_assertion(), symex_parse_optionst::doit(), initialize_property_map(), and operator()().
|
protected |
Definition at line 111 of file path_search.h.
Referenced by operator()(), and pick_state().
time_periodt path_searcht::sat_time |
Definition at line 82 of file path_search.h.
Referenced by check_assertion(), is_feasible(), and report_statistics().
|
protected |
Referenced by pick_state(), set_bfs(), set_dfs(), and set_locs().
bool path_searcht::show_vcc |
Definition at line 68 of file path_search.h.
Referenced by symex_parse_optionst::doit(), and operator()().
absolute_timet path_searcht::start_time |
Definition at line 81 of file path_search.h.
Referenced by drop_state(), operator()(), and report_statistics().
|
protected |
Definition at line 141 of file path_search.h.
Referenced by drop_state(), and set_time_limit().
|
protected |
Definition at line 140 of file path_search.h.
Referenced by drop_state(), and set_unwind_limit().