cprover
|
Public Member Functions | |
change_impactt (const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output) | |
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_program_change_impactt |
typedef std::map< irep_idt, goto_program_change_impactt > | goto_functions_change_impactt |
Definition at line 205 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 230 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 | ||
) |
Definition at line 289 of file change_impact.cpp.
References new_dep_graph, new_goto_functions, ns_new, ns_old, old_dep_graph, old_goto_functions, and unified_diff.
|
protected |
Definition at line 315 of file change_impact.cpp.
References goto_functionst::function_map, unified_difft::get_diff(), new_change_impact, new_goto_functions, old_change_impact, old_goto_functions, and unified_diff.
Referenced by operator()(), propogate_dep_back(), and propogate_dep_forward().
|
protected |
Definition at line 346 of file change_impact.cpp.
References BACKWARD, BOTH, unified_difft::DELETED, DELETED, FORWARD, impact_mode, goto_programt::instructions, unified_difft::NEW, NEW, new_change_impact, new_dep_graph, old_change_impact, old_dep_graph, propogate_dep_back(), propogate_dep_forward(), unified_difft::SAME, and SAME.
void change_impactt::operator() | ( | void | ) |
Definition at line 483 of file change_impact.cpp.
References change_impact(), forall_goto_functions, new_change_impact, new_goto_functions, ns_new, ns_old, old_change_impact, old_goto_functions, and output_change_impact().
|
protected |
Definition at line 553 of file change_impact.cpp.
References compact_output, DEL_CTRL_DEP, DEL_DATA_DEP, DELETED, forall_goto_program_instructions, goto_functionst::function_map, goto_program, NEW, NEW_CTRL_DEP, NEW_DATA_DEP, output_instruction(), SAME, and UNREACHABLE.
Referenced by operator()().
|
protected |
Definition at line 598 of file change_impact.cpp.
References compact_output, DEL_CTRL_DEP, DEL_DATA_DEP, DELETED, forall_goto_program_instructions, goto_functionst::function_map, goto_program, goto_programt::instructions, NEW, NEW_CTRL_DEP, NEW_DATA_DEP, output_instruction(), SAME, and UNREACHABLE.
|
protected |
Definition at line 714 of file change_impact.cpp.
References compact_output, dstringt::empty(), goto_program, id2string(), and goto_programt::output_instruction().
Referenced by output_change_impact().
|
protected |
Definition at line 453 of file change_impact.cpp.
References dep_edget::BOTH, change_impact(), dep_edget::DATA, DEL_CTRL_DEP, DEL_DATA_DEP, NEW_CTRL_DEP, and NEW_DATA_DEP.
Referenced by change_impact().
|
protected |
Definition at line 426 of file change_impact.cpp.
References dep_edget::BOTH, change_impact(), dep_edget::DATA, DEL_CTRL_DEP, DEL_DATA_DEP, NEW_CTRL_DEP, and NEW_DATA_DEP.
Referenced by change_impact().
|
protected |
Definition at line 218 of file change_impact.cpp.
Referenced by output_change_impact(), and output_instruction().
|
protected |
Definition at line 217 of file change_impact.cpp.
Referenced by change_impact().
|
protected |
Definition at line 246 of file change_impact.cpp.
Referenced by change_impact(), and operator()().
|
protected |
Definition at line 228 of file change_impact.cpp.
Referenced by change_impact(), and change_impactt().
|
protected |
Definition at line 222 of file change_impact.cpp.
Referenced by change_impact(), change_impactt(), and operator()().
|
protected |
Definition at line 223 of file change_impact.cpp.
Referenced by change_impactt(), and operator()().
|
protected |
Definition at line 221 of file change_impact.cpp.
Referenced by change_impactt(), and operator()().
|
protected |
Definition at line 246 of file change_impact.cpp.
Referenced by change_impact(), and operator()().
|
protected |
Definition at line 227 of file change_impact.cpp.
Referenced by change_impact(), and change_impactt().
|
protected |
Definition at line 220 of file change_impact.cpp.
Referenced by change_impact(), change_impactt(), and operator()().
|
protected |
Definition at line 225 of file change_impact.cpp.
Referenced by change_impact(), and change_impactt().