CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
change_impactt Class Reference
+ Collaboration diagram for change_impactt:

Public Member Functions

 change_impactt (const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output, message_handlert &message_handler)
 
void operator() ()
 

Protected Types

enum  mod_flagt {
  SAME =0 , NEW =1<<0 , DELETED =1<<1 , NEW_DATA_DEP =1<<2 ,
  DEL_DATA_DEP =1<<3 , NEW_CTRL_DEP =1<<4 , DEL_CTRL_DEP =1<<5
}
 
typedef std::map< goto_programt::const_targett, unsigned, goto_programt::target_less_than > goto_program_change_impactt
 
typedef std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
 

Protected Member Functions

void change_impact (const irep_idt &function_id)
 
void change_impact (const irep_idt &function_id, const goto_programt &old_goto_program, const goto_programt &new_goto_program, const unified_difft::goto_program_difft &diff, goto_program_change_impactt &old_impact, goto_program_change_impactt &new_impact)
 
void propogate_dep_back (const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
 
void propogate_dep_forward (const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
 
void output_change_impact (const irep_idt &function_id, const goto_program_change_impactt &c_i, const goto_functionst &goto_functions, const namespacet &ns) const
 
void output_change_impact (const irep_idt &function_id, const goto_program_change_impactt &o_c_i, const goto_functionst &o_goto_functions, const namespacet &o_ns, const goto_program_change_impactt &n_c_i, const goto_functionst &n_goto_functions, const namespacet &n_ns) const
 
void output_instruction (char prefix, const goto_programt &goto_program, const namespacet &ns, goto_programt::const_targett &target) const
 

Protected Attributes

impact_modet impact_mode
 
bool compact_output
 
const goto_functionst & old_goto_functions
 
const namespacet ns_old
 
const goto_functionst & new_goto_functions
 
const namespacet ns_new
 
unified_difft unified_diff
 
dependence_grapht old_dep_graph
 
dependence_grapht new_dep_graph
 
goto_functions_change_impactt old_change_impact
 
goto_functions_change_impactt new_change_impact
 

Detailed Description

Definition at line 203 of file change_impact.cpp.

Member Typedef Documentation

◆ goto_functions_change_impactt

typedef std::map<irep_idt, goto_program_change_impactt> change_impactt::goto_functions_change_impactt
protected

Definition at line 244 of file change_impact.cpp.

◆ goto_program_change_impactt

typedef std:: map<goto_programt::const_targett, unsigned, goto_programt::target_less_than> change_impactt::goto_program_change_impactt
protected

Definition at line 242 of file change_impact.cpp.

Member Enumeration Documentation

◆ mod_flagt

enum change_impactt::mod_flagt
protected
Enumerator
SAME 
NEW 
DELETED 
NEW_DATA_DEP 
DEL_DATA_DEP 
NEW_CTRL_DEP 
DEL_CTRL_DEP 

Definition at line 229 of file change_impact.cpp.

Constructor & Destructor Documentation

◆ change_impactt()

change_impactt::change_impactt ( const goto_modelt &  model_old,
const goto_modelt &  model_new,
impact_modet  impact_mode,
bool  compact_output,
message_handlert &  message_handler 
)

Definition at line 292 of file change_impact.cpp.

Member Function Documentation

◆ change_impact() [1/2]

void change_impactt::change_impact ( const irep_idt &  function_id)
protected

Definition at line 319 of file change_impact.cpp.

◆ change_impact() [2/2]

void change_impactt::change_impact ( const irep_idt &  function_id,
const goto_programt &  old_goto_program,
const goto_programt &  new_goto_program,
const unified_difft::goto_program_difft &  diff,
goto_program_change_impactt &  old_impact,
goto_program_change_impactt &  new_impact 
)
protected

Definition at line 351 of file change_impact.cpp.

◆ operator()()

void change_impactt::operator() ( void  )

Definition at line 492 of file change_impact.cpp.

◆ output_change_impact() [1/2]

void change_impactt::output_change_impact ( const irep_idt &  function_id,
const goto_program_change_impactt &  c_i,
const goto_functionst &  goto_functions,
const namespacet &  ns 
) const
protected

Definition at line 570 of file change_impact.cpp.

◆ output_change_impact() [2/2]

void change_impactt::output_change_impact ( const irep_idt &  function_id,
const goto_program_change_impactt &  o_c_i,
const goto_functionst &  o_goto_functions,
const namespacet &  o_ns,
const goto_program_change_impactt &  n_c_i,
const goto_functionst &  n_goto_functions,
const namespacet &  n_ns 
) const
protected

Definition at line 615 of file change_impact.cpp.

◆ output_instruction()

void change_impactt::output_instruction ( char  prefix,
const goto_programt &  goto_program,
const namespacet &  ns,
goto_programt::const_targett &  target 
) const
protected

Definition at line 735 of file change_impact.cpp.

◆ propogate_dep_back()

void change_impactt::propogate_dep_back ( const irep_idt &  function_id,
const dependence_grapht::nodet &  d_node,
const dependence_grapht &  dep_graph,
goto_functions_change_impactt &  change_impact,
bool  del 
)
protected

Definition at line 456 of file change_impact.cpp.

◆ propogate_dep_forward()

void change_impactt::propogate_dep_forward ( const irep_idt &  function_id,
const dependence_grapht::nodet &  d_node,
const dependence_grapht &  dep_graph,
goto_functions_change_impactt &  change_impact,
bool  del 
)
protected

Definition at line 423 of file change_impact.cpp.

Member Data Documentation

◆ compact_output

bool change_impactt::compact_output
protected

Definition at line 217 of file change_impact.cpp.

◆ impact_mode

impact_modet change_impactt::impact_mode
protected

Definition at line 216 of file change_impact.cpp.

◆ new_change_impact

goto_functions_change_impactt change_impactt::new_change_impact
protected

Definition at line 246 of file change_impact.cpp.

◆ new_dep_graph

dependence_grapht change_impactt::new_dep_graph
protected

Definition at line 227 of file change_impact.cpp.

◆ new_goto_functions

const goto_functionst& change_impactt::new_goto_functions
protected

Definition at line 221 of file change_impact.cpp.

◆ ns_new

const namespacet change_impactt::ns_new
protected

Definition at line 222 of file change_impact.cpp.

◆ ns_old

const namespacet change_impactt::ns_old
protected

Definition at line 220 of file change_impact.cpp.

◆ old_change_impact

goto_functions_change_impactt change_impactt::old_change_impact
protected

Definition at line 246 of file change_impact.cpp.

◆ old_dep_graph

dependence_grapht change_impactt::old_dep_graph
protected

Definition at line 226 of file change_impact.cpp.

◆ old_goto_functions

const goto_functionst& change_impactt::old_goto_functions
protected

Definition at line 219 of file change_impact.cpp.

◆ unified_diff

unified_difft change_impactt::unified_diff
protected

Definition at line 224 of file change_impact.cpp.

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