cprover
path_searcht Class Reference

#include <path_search.h>

Inheritance diagram for path_searcht:
[legend]
Collaboration diagram for path_searcht:
[legend]

Classes

struct  loc_datat
 
struct  property_entryt
 

Public Types

enum  statust { NOT_REACHED, SUCCESS, FAILURE }
 
typedef std::map< irep_idt, property_entrytproperty_mapt
 
- Public Types inherited from safety_checkert
enum  resultt { resultt::SAFE, resultt::UNSAFE, resultt::ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

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 ()
 
- Public Member Functions inherited from safety_checkert
 safety_checkert (const namespacet &_ns)
 
 safety_checkert (const namespacet &_ns, message_handlert &_message_handler)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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
 
- Public Attributes inherited from safety_checkert
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< statetqueuet
 

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_datatloc_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
 
- Protected Attributes inherited from safety_checkert
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 24 of file path_search.h.

Member Typedef Documentation

§ property_mapt

Definition at line 102 of file path_search.h.

§ queuet

typedef std::list<statet> path_searcht::queuet
protected

Definition at line 110 of file path_search.h.

§ statet

Definition at line 106 of file path_search.h.

Member Enumeration Documentation

§ search_heuristict

enum path_searcht::search_heuristict
strongprotected
Enumerator
DFS 
BFS 
LOCS 

Definition at line 143 of file path_search.h.

§ statust

Enumerator
NOT_REACHED 
SUCCESS 
FAILURE 

Definition at line 84 of file path_search.h.

Constructor & Destructor Documentation

§ path_searcht()

path_searcht::path_searcht ( const namespacet _ns)
inlineexplicit

Definition at line 27 of file path_search.h.

References operator()().

Member Function Documentation

§ check_assertion()

§ do_show_vcc()

§ drop_state()

§ execute()

bool path_searcht::execute ( queuet::iterator  state)
protected

§ initialize_property_map()

§ is_feasible()

§ operator()()

§ pick_state()

void path_searcht::pick_state ( )
protected

Definition at line 193 of file path_search.cpp.

References BFS, DFS, LOCS, queue, and search_heuristic.

Referenced by operator()().

§ report_statistics()

§ set_bfs()

void path_searcht::set_bfs ( )
inline

Definition at line 99 of file path_search.h.

References BFS, and search_heuristic.

Referenced by symex_parse_optionst::doit().

§ set_branch_bound()

void path_searcht::set_branch_bound ( int  limit)
inline

Definition at line 53 of file path_search.h.

References branch_bound.

Referenced by symex_parse_optionst::doit().

§ set_context_bound()

void path_searcht::set_context_bound ( int  limit)
inline

Definition at line 48 of file path_search.h.

References context_bound.

Referenced by symex_parse_optionst::doit().

§ set_depth_limit()

void path_searcht::set_depth_limit ( int  limit)
inline

Definition at line 43 of file path_search.h.

References depth_limit.

Referenced by symex_parse_optionst::doit().

§ set_dfs()

void path_searcht::set_dfs ( )
inline

Definition at line 98 of file path_search.h.

References DFS, and search_heuristic.

Referenced by symex_parse_optionst::doit().

§ set_locs()

void path_searcht::set_locs ( )
inline

Definition at line 100 of file path_search.h.

References LOCS, and search_heuristic.

Referenced by symex_parse_optionst::doit().

§ set_time_limit()

void path_searcht::set_time_limit ( int  limit)
inline

Definition at line 63 of file path_search.h.

References time_limit.

Referenced by symex_parse_optionst::doit().

§ set_unwind_limit()

void path_searcht::set_unwind_limit ( int  limit)
inline

Definition at line 58 of file path_search.h.

References unwind_limit.

Referenced by symex_parse_optionst::doit().

Member Data Documentation

§ branch_bound

unsigned path_searcht::branch_bound
protected

Definition at line 139 of file path_search.h.

Referenced by drop_state(), and set_branch_bound().

§ context_bound

unsigned path_searcht::context_bound
protected

Definition at line 138 of file path_search.h.

Referenced by drop_state(), and set_context_bound().

§ depth_limit

unsigned path_searcht::depth_limit
protected

Definition at line 137 of file path_search.h.

Referenced by drop_state(), and set_depth_limit().

§ eager_infeasibility

bool path_searcht::eager_infeasibility

Definition at line 69 of file path_search.h.

Referenced by symex_parse_optionst::doit(), and operator()().

§ last_source_location

source_locationt path_searcht::last_source_location
protected

Definition at line 145 of file path_search.h.

Referenced by drop_state().

§ loc_data

expanding_vectort<loc_datat> path_searcht::loc_data
protected

Definition at line 122 of file path_search.h.

Referenced by operator()(), and report_statistics().

§ number_of_dropped_states

std::size_t path_searcht::number_of_dropped_states

Definition at line 72 of file path_search.h.

Referenced by operator()(), and report_statistics().

§ number_of_failed_properties

std::size_t path_searcht::number_of_failed_properties

Definition at line 79 of file path_search.h.

Referenced by check_assertion(), and operator()().

§ number_of_feasible_paths

std::size_t path_searcht::number_of_feasible_paths

Definition at line 75 of file path_search.h.

Referenced by operator()().

§ number_of_infeasible_paths

std::size_t path_searcht::number_of_infeasible_paths

Definition at line 76 of file path_search.h.

Referenced by operator()(), and report_statistics().

§ number_of_locs

std::size_t path_searcht::number_of_locs

Definition at line 80 of file path_search.h.

Referenced by operator()(), and report_statistics().

§ number_of_paths

std::size_t path_searcht::number_of_paths

Definition at line 73 of file path_search.h.

Referenced by operator()(), and report_statistics().

§ number_of_steps

std::size_t path_searcht::number_of_steps

Definition at line 74 of file path_search.h.

Referenced by operator()().

§ number_of_VCCs

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().

§ number_of_VCCs_after_simplification

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_map

property_mapt path_searcht::property_map

§ queue

queuet path_searcht::queue
protected

Definition at line 111 of file path_search.h.

Referenced by operator()(), and pick_state().

§ sat_time

time_periodt path_searcht::sat_time

Definition at line 82 of file path_search.h.

Referenced by check_assertion(), is_feasible(), and report_statistics().

§ search_heuristic

enum path_searcht::search_heuristict path_searcht::search_heuristic
protected

Referenced by pick_state(), set_bfs(), set_dfs(), and set_locs().

§ show_vcc

bool path_searcht::show_vcc

Definition at line 68 of file path_search.h.

Referenced by symex_parse_optionst::doit(), and operator()().

§ start_time

absolute_timet path_searcht::start_time

Definition at line 81 of file path_search.h.

Referenced by drop_state(), operator()(), and report_statistics().

§ time_limit

unsigned path_searcht::time_limit
protected

Definition at line 141 of file path_search.h.

Referenced by drop_state(), and set_time_limit().

§ unwind_limit

unsigned path_searcht::unwind_limit
protected

Definition at line 140 of file path_search.h.

Referenced by drop_state(), and set_unwind_limit().


The documentation for this class was generated from the following files: