Various goto-diff fixes and a java regression test

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;
+  }
+}

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;
+  }
+}

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

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));
 }

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;

src/goto-programs/goto_convert_functions.cpp

@@ -16,6 +16,7 @@ Date: June 2003
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 #include <util/prefix.h>
+#include <util/fresh_symbol.h>
 
 #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);