CBMC
change_impact.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data and control-dependencies of syntactic diff
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
15 #define CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
16 
17 class goto_modelt;
18 class message_handlert;
19 enum class impact_modet { FORWARD, BACKWARD, BOTH };
20 
21 void change_impact(
22  const goto_modelt &model_old,
23  const goto_modelt &model_new,
24  impact_modet impact_mode,
25  bool compact_output,
26  message_handlert &message_handler);
27 
28 #endif // CPROVER_GOTO_DIFF_CHANGE_IMPACT_H
change_impact
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output, message_handlert &message_handler)
Definition: change_impact.cpp:758
impact_modet
impact_modet
Definition: change_impact.h:19
impact_modet::BOTH
@ BOTH
impact_modet::BACKWARD
@ BACKWARD
impact_modet::FORWARD
@ FORWARD
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:27