cprover
|
#include <full_slicer_class.h>
Classes | |
struct | cfg_nodet |
Public Member Functions | |
void | operator() (goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion) |
Protected Types | |
typedef cfg_baset< cfg_nodet > | cfgt |
typedef std::vector< cfgt::entryt > | dep_node_to_cfgt |
typedef std::stack< cfgt::entryt > | queuet |
typedef std::list< cfgt::entryt > | jumpst |
typedef std::unordered_map< irep_idt, queuet > | decl_deadt |
Protected Member Functions | |
void | fixedpoint (goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph) |
void | add_dependencies (const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg) |
void | add_function_calls (const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions) |
void | add_decl_dead (const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead) |
void | add_jumps (queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators) |
void | add_to_queue (queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason) |
Protected Attributes | |
cfgt | cfg |
Definition at line 38 of file full_slicer_class.h.
|
protected |
Definition at line 59 of file full_slicer_class.h.
|
protected |
Definition at line 65 of file full_slicer_class.h.
|
protected |
Definition at line 62 of file full_slicer_class.h.
|
protected |
Definition at line 64 of file full_slicer_class.h.
|
protected |
Definition at line 63 of file full_slicer_class.h.
|
protected |
Definition at line 62 of file full_slicer.cpp.
References add_to_queue(), and find_symbols().
Referenced by fixedpoint().
|
protected |
Definition at line 22 of file full_slicer.cpp.
References add_to_queue(), and graph_nodet< E >::in.
Referenced by fixedpoint().
|
protected |
Definition at line 38 of file full_slicer.cpp.
References add_to_queue(), cfg, cfg_baset< T, P, I >::entry_map, goto_functionst::function_map, and grapht< N >::in().
Referenced by fixedpoint().
|
protected |
Definition at line 93 of file full_slicer.cpp.
References add_to_queue(), cfg_dominators_templatet< P, T, post_dom >::cfg, cfg, cfg_baset< T, P, I >::entry_map, INVARIANT, and grapht< N >::size().
Referenced by fixedpoint().
|
inlineprotected |
Definition at line 95 of file full_slicer_class.h.
References cfg.
Referenced by add_decl_dead(), add_dependencies(), add_function_calls(), add_jumps(), and operator()().
|
protected |
Definition at line 217 of file full_slicer.cpp.
References add_decl_dead(), add_dependencies(), add_function_calls(), add_jumps(), cfg, dependence_grapht::cfg_post_dominators(), cfg_baset< T, P, I >::entry_map, and grapht< N >::size().
Referenced by operator()().
void full_slicert::operator() | ( | goto_functionst & | goto_functions, |
const namespacet & | ns, | ||
slicing_criteriont & | criterion | ||
) |
Definition at line 286 of file full_slicer.cpp.
References add_to_queue(), cfg, criterion, cfg_baset< T, P, I >::entry_map, fixedpoint(), Forall_goto_functions, Forall_goto_program_instructions, symbol_exprt::get_identifier(), implicit(), remove_skip(), code_declt::symbol(), code_deadt::symbol(), to_code_dead(), to_code_decl(), to_string(), and to_symbol_expr().
|
protected |
Definition at line 60 of file full_slicer_class.h.
Referenced by add_function_calls(), add_jumps(), add_to_queue(), fixedpoint(), and operator()().