CBMC
|
#include <full_slicer_class.h>
Classes | |
struct | cfg_nodet |
Public Member Functions | |
void | operator() (goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler) |
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 61 of file full_slicer_class.h.
|
protected |
Definition at line 67 of file full_slicer_class.h.
|
protected |
Definition at line 64 of file full_slicer_class.h.
|
protected |
Definition at line 66 of file full_slicer_class.h.
|
protected |
Definition at line 65 of file full_slicer_class.h.
|
protected |
Definition at line 54 of file full_slicer.cpp.
|
protected |
Definition at line 20 of file full_slicer.cpp.
|
protected |
Definition at line 36 of file full_slicer.cpp.
|
protected |
Definition at line 85 of file full_slicer.cpp.
|
inlineprotected |
Definition at line 97 of file full_slicer_class.h.
|
protected |
Definition at line 190 of file full_slicer.cpp.
void full_slicert::operator() | ( | goto_functionst & | goto_functions, |
const namespacet & | ns, | ||
const slicing_criteriont & | criterion, | ||
message_handlert & | message_handler | ||
) |
Definition at line 254 of file full_slicer.cpp.
|
protected |
Definition at line 62 of file full_slicer_class.h.