diff --git a/regression/goto-diff/syntactic-diff-java1/new.jar b/regression/goto-diff/syntactic-diff-java1/new.jar new file mode 100644 index 00000000000..2966f962517 Binary files /dev/null and b/regression/goto-diff/syntactic-diff-java1/new.jar differ diff --git a/regression/goto-diff/syntactic-diff-java1/new/Test.java b/regression/goto-diff/syntactic-diff-java1/new/Test.java new file mode 100644 index 00000000000..2fb52b24ee1 --- /dev/null +++ b/regression/goto-diff/syntactic-diff-java1/new/Test.java @@ -0,0 +1,16 @@ +public class Test { + + public int run() { + int x = 42; + + return x; + } + + public void bar() { + int y = 0; + } + + public void unchanged() { + int z = 0; + } +} diff --git a/regression/goto-diff/syntactic-diff-java1/old.jar b/regression/goto-diff/syntactic-diff-java1/old.jar new file mode 100644 index 00000000000..0d1d5acf794 Binary files /dev/null and b/regression/goto-diff/syntactic-diff-java1/old.jar differ diff --git a/regression/goto-diff/syntactic-diff-java1/old/Test.java b/regression/goto-diff/syntactic-diff-java1/old/Test.java new file mode 100644 index 00000000000..43b8e717aad --- /dev/null +++ b/regression/goto-diff/syntactic-diff-java1/old/Test.java @@ -0,0 +1,16 @@ +public class Test { + + public int run() { + int x = 0; + + return x; + } + + public void unchanged() { + int z = 0; + } + + public void foo() { + int y = 0; + } +} diff --git a/regression/goto-diff/syntactic-diff-java1/test.desc b/regression/goto-diff/syntactic-diff-java1/test.desc new file mode 100644 index 00000000000..c9fd2393b08 --- /dev/null +++ b/regression/goto-diff/syntactic-diff-java1/test.desc @@ -0,0 +1,10 @@ +CORE +old.jar +new.jar +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +new functions:\n Test\.java: java::Test\.foo:\(\)V\nmodified functions:\n Test\.java: java::Test\.run:\(\)I\ndeleted functions:\n Test\.java: java::Test\.bar:\(\)V +-- +^warning: ignoring diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index 1ad26dbee7f..32b6b2949af 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -15,6 +15,8 @@ Author: Peter Schrammel std::ostream &goto_difft::output_functions(std::ostream &out) const { + namespacet ns1(goto_model1.symbol_table); + namespacet ns2(goto_model2.symbol_table); switch(ui) { case ui_message_handlert::uit::PLAIN: @@ -24,33 +26,24 @@ std::ostream &goto_difft::output_functions(std::ostream &out) const for(irep_id_sett::const_iterator it=new_functions.begin(); it!=new_functions.end(); ++it) { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns2.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } out << "modified functions:\n"; for(irep_id_sett::const_iterator it=modified_functions.begin(); it!=modified_functions.end(); ++it) { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns2.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } out << "deleted functions:\n"; for(irep_id_sett::const_iterator it=deleted_functions.begin(); it!=deleted_functions.end(); ++it) { - const goto_programt &program= - goto_model1.goto_functions.function_map.at(*it).body; - out << " " - << program.instructions.begin()->source_location.get_file() - << ": " << *it << "\n"; + const symbolt &symbol = ns1.lookup(*it); + out << " " << symbol.location.get_file() << ": " << *it << "\n"; } break; } @@ -91,12 +84,22 @@ void goto_difft::convert_function( json_objectt &result, const irep_idt &function_name) const { - const goto_programt &program= - goto_model2.goto_functions.function_map.at(function_name).body; - if(!program.instructions.empty()) + // the function may be in goto_model1 or goto_model2 + if( + goto_model1.goto_functions.function_map.find(function_name) != + goto_model1.goto_functions.function_map.end()) { - result["sourceLocation"]= - json(program.instructions.begin()->source_location); + const symbolt &symbol = + namespacet(goto_model1.symbol_table).lookup(function_name); + result["sourceLocation"] = json(symbol.location); + } + else if( + goto_model2.goto_functions.function_map.find(function_name) != + goto_model2.goto_functions.function_map.end()) + { + const symbolt &symbol = + namespacet(goto_model2.symbol_table).lookup(function_name); + result["sourceLocation"] = json(symbol.location); } result["name"]=json_stringt(id2string(function_name)); } diff --git a/src/goto-diff/syntactic_diff.cpp b/src/goto-diff/syntactic_diff.cpp index 030d35e0f3c..68b7379b688 100644 --- a/src/goto-diff/syntactic_diff.cpp +++ b/src/goto-diff/syntactic_diff.cpp @@ -42,11 +42,22 @@ bool syntactic_difft::operator()() i_it2!=f_it->second.body.instructions.end(); ++i_it1, ++i_it2) { - if(i_it1->code != i_it2->code || - i_it1->function != i_it2->function || - i_it1->type != i_it2->type || - i_it1->guard != i_it2->guard || - i_it1->targets != i_it2->targets) + long jump_difference1 = 0; + if(!i_it1->targets.empty()) + { + jump_difference1 = + i_it1->get_target()->location_number - i_it1->location_number; + } + long jump_difference2 = 0; + if(!i_it2->targets.empty()) + { + jump_difference2 = + i_it2->get_target()->location_number - i_it2->location_number; + } + if( + i_it1->code != i_it2->code || i_it1->function != i_it2->function || + i_it1->type != i_it2->type || i_it1->guard != i_it2->guard || + jump_difference1 != jump_difference2) { modified_functions.insert(it->first); break; diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 8a4f28c4dd7..4aa3c8d90ee 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -16,6 +16,7 @@ Date: June 2003 #include #include #include +#include #include "goto_inline.h" @@ -145,6 +146,7 @@ void goto_convert_functionst::convert_function( // make tmp variables local to function tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::"; temporary_counter=0; + reset_temporary_counter(); f.type=to_code_type(symbol.type);