CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
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_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
 

Detailed Description

Definition at line 38 of file full_slicer_class.h.

Member Typedef Documentation

◆ cfgt

typedef cfg_baset<cfg_nodet> full_slicert::cfgt
protected

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: