|
cprover
|
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 |
Definition at line 203 of file change_impact.cpp.
|
protected |
Definition at line 244 of file change_impact.cpp.
|
protected |
Definition at line 242 of file change_impact.cpp.
|
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.
| 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.
|
protected |
Definition at line 319 of file change_impact.cpp.
|
protected |
Definition at line 351 of file change_impact.cpp.
| void change_impactt::operator() | ( | ) |
Definition at line 492 of file change_impact.cpp.
|
protected |
Definition at line 570 of file change_impact.cpp.
|
protected |
Definition at line 615 of file change_impact.cpp.
|
protected |
Definition at line 735 of file change_impact.cpp.
|
protected |
Definition at line 456 of file change_impact.cpp.
|
protected |
Definition at line 423 of file change_impact.cpp.
|
protected |
Definition at line 217 of file change_impact.cpp.
|
protected |
Definition at line 216 of file change_impact.cpp.
|
protected |
Definition at line 246 of file change_impact.cpp.
|
protected |
Definition at line 227 of file change_impact.cpp.
|
protected |
Definition at line 221 of file change_impact.cpp.
|
protected |
Definition at line 222 of file change_impact.cpp.
|
protected |
Definition at line 220 of file change_impact.cpp.
|
protected |
Definition at line 246 of file change_impact.cpp.
|
protected |
Definition at line 226 of file change_impact.cpp.
|
protected |
Definition at line 219 of file change_impact.cpp.
|
protected |
Definition at line 224 of file change_impact.cpp.