cprover
Loading...
Searching...
No Matches
unified_diff.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unified diff (using LCSS) of goto functions
4
5Author: Michael Tautschnig
6
7Date: 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
26class goto_functionst;
27class goto_modelt;
28
30{
31public:
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
50private:
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(
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 has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
static bool instructions_equal(const goto_programt::instructiont &ins1, const goto_programt::instructiont &ins2)
std::map< irep_idt, differencest > differences_mapt
Definition: unified_diff.h:57
std::vector< differencet > differencest
Definition: unified_diff.h:56
const namespacet ns_old
Definition: unified_diff.h:52
const goto_functionst & old_goto_functions
Definition: unified_diff.h:51
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:46
const goto_functionst & new_goto_functions
Definition: unified_diff.h:53
goto_program_difft get_diff(const irep_idt &function) const
void unified_diff(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program)
const namespacet ns_new
Definition: unified_diff.h:54
const differences_mapt & differences_map() const
static differencest lcss(const goto_programt &old_goto_program, const goto_programt &new_goto_program)
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
differences_mapt differences_map_
Definition: unified_diff.h:86
void output(std::ostream &os) const
Concrete Goto Program.