Skip to content

Commit 41def9f

Browse files
committed
Use common implementation of instruction/goto program equality
1 parent 405b12b commit 41def9f

File tree

3 files changed

+5
-40
lines changed

3 files changed

+5
-40
lines changed

jbmc/src/jdiff/java_syntactic_diff.cpp

Lines changed: 2 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,7 @@ bool java_syntactic_difft::operator()()
7070
continue;
7171
}
7272

73-
if(
74-
it->second.body.instructions.size() !=
75-
f_it->second.body.instructions.size())
73+
if(!it->second.body.equals(f_it->second.body))
7674
{
7775
modified_functions.insert(it->first);
7876
continue;
@@ -86,22 +84,7 @@ bool java_syntactic_difft::operator()()
8684
i_it2 != f_it->second.body.instructions.end();
8785
++i_it1, ++i_it2)
8886
{
89-
long jump_difference1 = 0;
90-
if(!i_it1->targets.empty())
91-
{
92-
jump_difference1 =
93-
i_it1->get_target()->location_number - i_it1->location_number;
94-
}
95-
long jump_difference2 = 0;
96-
if(!i_it2->targets.empty())
97-
{
98-
jump_difference2 =
99-
i_it2->get_target()->location_number - i_it2->location_number;
100-
}
101-
if(
102-
i_it1->code != i_it2->code || i_it1->function != i_it2->function ||
103-
i_it1->type != i_it2->type || i_it1->guard != i_it2->guard ||
104-
jump_difference1 != jump_difference2)
87+
if(i_it1->function != i_it2->function)
10588
{
10689
modified_functions.insert(it->first);
10790
break;

src/goto-diff/syntactic_diff.cpp

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,7 @@ bool syntactic_difft::operator()()
6969
continue;
7070
}
7171

72-
if(it->second.body.instructions.size() !=
73-
f_it->second.body.instructions.size())
72+
if(!it->second.body.equals(f_it->second.body))
7473
{
7574
modified_functions.insert(it->first);
7675
continue;
@@ -84,22 +83,7 @@ bool syntactic_difft::operator()()
8483
i_it2!=f_it->second.body.instructions.end();
8584
++i_it1, ++i_it2)
8685
{
87-
long jump_difference1 = 0;
88-
if(!i_it1->targets.empty())
89-
{
90-
jump_difference1 =
91-
i_it1->get_target()->location_number - i_it1->location_number;
92-
}
93-
long jump_difference2 = 0;
94-
if(!i_it2->targets.empty())
95-
{
96-
jump_difference2 =
97-
i_it2->get_target()->location_number - i_it2->location_number;
98-
}
99-
if(
100-
i_it1->code != i_it2->code || i_it1->function != i_it2->function ||
101-
i_it1->type != i_it2->type || i_it1->guard != i_it2->guard ||
102-
jump_difference1 != jump_difference2)
86+
if(i_it1->function != i_it2->function)
10387
{
10488
modified_functions.insert(it->first);
10589
break;

src/goto-diff/unified_diff.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -392,9 +392,7 @@ bool unified_difft::instructions_equal(
392392
const goto_programt::instructiont &ins1,
393393
const goto_programt::instructiont &ins2)
394394
{
395-
return ins1.code == ins2.code && ins1.function == ins2.function &&
396-
ins1.type == ins2.type && ins1.guard == ins2.guard &&
397-
ins1.targets.size() == ins2.targets.size() &&
395+
return ins1.equals(ins2) && ins1.function == ins2.function &&
398396
(ins1.targets.empty() ||
399397
instructions_equal(*ins1.get_target(), *ins2.get_target()));
400398
}

0 commit comments

Comments
 (0)