CBMC
full_slicert Class Reference

#include <full_slicer_class.h>

+ Collaboration diagram for full_slicert:

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_nodetcfgt
 
typedef std::vector< cfgt::entrytdep_node_to_cfgt
 
typedef std::stack< cfgt::entrytqueuet
 
typedef std::list< cfgt::entrytjumpst
 
typedef std::unordered_map< irep_idt, queuetdecl_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
 

Detailed Description

Definition at line 38 of file full_slicer_class.h.

Member Typedef Documentation

◆ cfgt

Definition at line 61 of file full_slicer_class.h.

◆ decl_deadt

typedef std::unordered_map<irep_idt, queuet> full_slicert::decl_deadt
protected

Definition at line 67 of file full_slicer_class.h.

◆ dep_node_to_cfgt

typedef std::vector<cfgt::entryt> full_slicert::dep_node_to_cfgt
protected

Definition at line 64 of file full_slicer_class.h.

◆ jumpst

typedef std::list<cfgt::entryt> full_slicert::jumpst
protected

Definition at line 66 of file full_slicer_class.h.

◆ queuet

typedef std::stack<cfgt::entryt> full_slicert::queuet
protected

Definition at line 65 of file full_slicer_class.h.

Member Function Documentation

◆ add_decl_dead()

void full_slicert::add_decl_dead ( const cfgt::nodet node,
queuet queue,
decl_deadt decl_dead 
)
protected

Definition at line 54 of file full_slicer.cpp.

◆ add_dependencies()

void full_slicert::add_dependencies ( const cfgt::nodet node,
queuet queue,
const dependence_grapht dep_graph,
const dep_node_to_cfgt dep_node_to_cfg 
)
protected

Definition at line 20 of file full_slicer.cpp.

◆ add_function_calls()

void full_slicert::add_function_calls ( const cfgt::nodet node,
queuet queue,
const goto_functionst goto_functions 
)
protected

Definition at line 36 of file full_slicer.cpp.

◆ add_jumps()

void full_slicert::add_jumps ( queuet queue,
jumpst jumps,
const dependence_grapht::post_dominators_mapt post_dominators 
)
protected

Definition at line 85 of file full_slicer.cpp.

◆ add_to_queue()

void full_slicert::add_to_queue ( queuet queue,
const cfgt::entryt entry,
goto_programt::const_targett  reason 
)
inlineprotected

Definition at line 97 of file full_slicer_class.h.

◆ fixedpoint()

void full_slicert::fixedpoint ( goto_functionst goto_functions,
queuet queue,
jumpst jumps,
decl_deadt decl_dead,
const dependence_grapht dep_graph 
)
protected

Definition at line 190 of file full_slicer.cpp.

◆ operator()()

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.

Member Data Documentation

◆ cfg

cfgt full_slicert::cfg
protected

Definition at line 62 of file full_slicer_class.h.


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