cprover
goto_diff.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO-DIFF Base Class
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_H
13 #define CPROVER_GOTO_DIFF_GOTO_DIFF_H
14 
16 #include <langapi/language_ui.h>
17 #include <util/message.h>
18 #include <util/json.h>
19 
20 #include <ostream>
21 
22 class goto_difft:public messaget
23 {
24 public:
25  explicit goto_difft(
26  const goto_modelt &_goto_model1,
27  const goto_modelt &_goto_model2,
28  message_handlert &_message_handler
29  )
30  :
31  messaget(_message_handler),
32  goto_model1(_goto_model1),
33  goto_model2(_goto_model2),
34  ui(ui_message_handlert::uit::PLAIN),
36  {}
37 
38  virtual bool operator()()=0;
39 
40  void set_ui(language_uit::uit _ui) { ui=_ui; }
41 
42  virtual std::ostream &output_functions(std::ostream &out) const;
43 
44 protected:
48 
50  typedef std::set<irep_idt> irep_id_sett;
52 
55  const irep_id_sett &function_group) const;
56  void convert_function(
58  const irep_idt &function_name) const;
59 };
60 
61 #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_H
virtual std::ostream & output_functions(std::ostream &out) const
mstreamt & result()
Definition: message.h:233
const goto_modelt & goto_model1
Definition: goto_diff.h:45
const goto_modelt & goto_model2
Definition: goto_diff.h:46
void convert_function(json_objectt &result, const irep_idt &function_name) const
void set_ui(language_uit::uit _ui)
Definition: goto_diff.h:40
Symbol Table + CFG.
unsigned total_functions_count
Definition: goto_diff.h:49
irep_id_sett modified_functions
Definition: goto_diff.h:51
goto_difft(const goto_modelt &_goto_model1, const goto_modelt &_goto_model2, message_handlert &_message_handler)
Definition: goto_diff.h:25
void convert_function_group(json_arrayt &result, const irep_id_sett &function_group) const
language_uit::uit ui
Definition: goto_diff.h:47
std::set< irep_idt > irep_id_sett
Definition: goto_diff.h:50
virtual bool operator()()=0
irep_id_sett new_functions
Definition: goto_diff.h:51
irep_id_sett deleted_functions
Definition: goto_diff.h:51