cprover
unified_diff.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unified diff (using LCSS) of goto functions
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_DIFF_UNIFIED_DIFF_H
15 #define CPROVER_GOTO_DIFF_UNIFIED_DIFF_H
16 
17 #include <iosfwd>
18 #include <list>
19 #include <map>
20 #include <vector>
21 
22 #include <util/namespace.h>
23 
25 
26 class goto_functionst;
27 class goto_modelt;
28 class goto_programt;
29 
31 {
32 public:
33  unified_difft(const goto_modelt &model_old, const goto_modelt &model_new);
34 
35  bool operator()();
36 
37  void output(std::ostream &os) const;
38 
39  enum class differencet
40  {
41  SAME,
42  DELETED,
43  NEW
44  };
45 
46  typedef std::list<std::pair<goto_programt::const_targett, differencet>>
48 
49  goto_program_difft get_diff(const irep_idt &function) const;
50 
51 private:
56 
57  typedef std::vector<differencet> differencest;
58  typedef std::map<irep_idt, differencest> differences_mapt;
59 
60  void unified_diff(
61  const irep_idt &identifier,
62  const goto_programt &old_goto_program,
63  const goto_programt &new_goto_program);
64 
65  static differencest lcss(
66  const goto_programt &old_goto_program,
67  const goto_programt &new_goto_program);
68 
70  const goto_programt &old_goto_program,
71  const goto_programt &new_goto_program,
72  const differencest &differences);
73 
74  void output_diff(
75  const irep_idt &identifier,
76  const goto_programt &old_goto_program,
77  const goto_programt &new_goto_program,
78  const differencest &differences,
79  std::ostream &os) const;
80 
81  static bool instructions_equal(
82  const goto_programt::instructiont &ins1,
83  const goto_programt::instructiont &ins2);
84 
85  const differences_mapt &differences_map() const;
86 
88 };
89 
90 #endif // CPROVER_GOTO_DIFF_UNIFIED_DIFF_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
unified_difft::output
void output(std::ostream &os) const
Definition: unified_diff.cpp:367
unified_difft::differencet::SAME
@ SAME
goto_modelt
Definition: goto_model.h:26
namespace.h
unified_difft
Definition: unified_diff.h:31
unified_difft::operator()
bool operator()()
Definition: unified_diff.cpp:328
unified_difft::differences_mapt
std::map< irep_idt, differencest > differences_mapt
Definition: unified_diff.h:58
unified_difft::new_goto_functions
const goto_functionst & new_goto_functions
Definition: unified_diff.h:54
unified_difft::ns_new
const namespacet ns_new
Definition: unified_diff.h:55
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
unified_difft::differences_map_
differences_mapt differences_map_
Definition: unified_diff.h:87
unified_difft::instructions_equal
static bool instructions_equal(const goto_programt::instructiont &ins1, const goto_programt::instructiont &ins2)
Definition: unified_diff.cpp:391
unified_difft::old_goto_functions
const goto_functionst & old_goto_functions
Definition: unified_diff.h:52
unified_difft::differencet::DELETED
@ DELETED
unified_difft::differencest
std::vector< differencet > differencest
Definition: unified_diff.h:57
unified_difft::differencet
differencet
Definition: unified_diff.h:40
unified_difft::lcss
static differencest lcss(const goto_programt &old_goto_program, const goto_programt &new_goto_program)
Definition: unified_diff.cpp:147
goto_program.h
Concrete Goto Program.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
unified_difft::unified_difft
unified_difft(const goto_modelt &model_old, const goto_modelt &model_new)
Definition: unified_diff.cpp:20
unified_difft::differencet::NEW
@ NEW
unified_difft::output_diff
void output_diff(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program, const differencest &differences, std::ostream &os) const
Definition: unified_diff.cpp:103
unified_difft::ns_old
const namespacet ns_old
Definition: unified_diff.h:53
unified_difft::differences_map
const differences_mapt & differences_map() const
Definition: unified_diff.cpp:400
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
unified_difft::get_diff
goto_program_difft get_diff(const irep_idt &function) const
Definition: unified_diff.cpp:31
unified_difft::goto_program_difft
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:47
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
unified_difft::unified_diff
void unified_diff(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program)
Definition: unified_diff.cpp:305