cprover
|
#include <instrumenter_pensieve.h>
Public Member Functions | |
instrumenter_pensievet (symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &message) | |
void | collect_pairs_naive (namespacet &ns) |
void | collect_pairs (namespacet &ns) |
![]() | |
void | print_map_function_graph () const |
instrumentert (symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &_message) | |
unsigned | goto2graph_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body) |
goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions More... | |
void | collect_cycles (memory_modelt model) |
void | collect_cycles_by_SCCs (memory_modelt model) |
Note: can be distributed (#define DISTRIBUTED) More... | |
void | cfg_cycles_filter () |
void | set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false) |
void | instrument_with_strategy (instrumentation_strategyt strategy) |
void | instrument_my_events (const std::set< event_idt > &events) |
void | set_rendering_options (bool aligned, bool file, bool function) |
void | print_outputs (memory_modelt model, bool hide_internals) |
Definition at line 22 of file instrumenter_pensieve.h.
|
inline |
Definition at line 25 of file instrumenter_pensieve.h.
|
inline |
Definition at line 37 of file instrumenter_pensieve.h.
References event_grapht::collect_pairs(), instrumentert::egraph, and instrumentert::ns.
Referenced by fence_pensieve().
|
inline |
Definition at line 31 of file instrumenter_pensieve.h.
References event_grapht::collect_pairs_naive(), instrumentert::egraph, and instrumentert::ns.
Referenced by fence_pensieve().