CBMC
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 
30 {
31 public:
32  unified_difft(const goto_modelt &model_old, const goto_modelt &model_new);
33 
34  bool operator()();
35 
36  void output(std::ostream &os) const;
37 
38  enum class differencet
39  {
40  SAME,
41  DELETED,
42  NEW
43  };
44 
45  typedef std::list<std::pair<goto_programt::const_targett, differencet>>
47 
48  goto_program_difft get_diff(const irep_idt &function) const;
49 
50 private:
55 
56  typedef std::vector<differencet> differencest;
57  typedef std::map<irep_idt, differencest> differences_mapt;
58 
59  void unified_diff(
60  const irep_idt &identifier,
61  const goto_programt &old_goto_program,
62  const goto_programt &new_goto_program);
63 
64  static differencest lcss(
65  const goto_programt &old_goto_program,
66  const goto_programt &new_goto_program);
67 
69  const goto_programt &old_goto_program,
70  const goto_programt &new_goto_program,
71  const differencest &differences);
72 
73  void output_diff(
74  const irep_idt &identifier,
75  const goto_programt &old_goto_program,
76  const goto_programt &new_goto_program,
77  const differencest &differences,
78  std::ostream &os) const;
79 
80  static bool instructions_equal(
81  const goto_programt::instructiont &ins1,
82  const goto_programt::instructiont &ins2);
83 
84  const differences_mapt &differences_map() const;
85 
87 };
88 
89 #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:36
unified_difft::output
void output(std::ostream &os) const
Definition: unified_diff.cpp:375
unified_difft::differencet::SAME
@ SAME
goto_modelt
Definition: goto_model.h:25
namespace.h
unified_difft
Definition: unified_diff.h:29
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:57
unified_difft::new_goto_functions
const goto_functionst & new_goto_functions
Definition: unified_diff.h:53
unified_difft::ns_new
const namespacet ns_new
Definition: unified_diff.h:54
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
unified_difft::differences_map_
differences_mapt differences_map_
Definition: unified_diff.h:86
unified_difft::instructions_equal
static bool instructions_equal(const goto_programt::instructiont &ins1, const goto_programt::instructiont &ins2)
Definition: unified_diff.cpp:399
unified_difft::old_goto_functions
const goto_functionst & old_goto_functions
Definition: unified_diff.h:51
unified_difft::differencet::DELETED
@ DELETED
unified_difft::differencest
std::vector< differencet > differencest
Definition: unified_diff.h:56
unified_difft::differencet
differencet
Definition: unified_diff.h:38
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
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
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:52
unified_difft::differences_map
const differences_mapt & differences_map() const
Definition: unified_diff.cpp:408
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
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:46
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
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