From 8c2d622f57189e19efef8b0b7cdd6a30c5c10b9a Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Tue, 19 Dec 2017 15:45:10 +0000
Subject: [PATCH 1/2] Fix the problem where two static functions with the same
 name would cause the dependency graph to fail.

---
 src/goto-programs/read_goto_binary.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index 717da589d2f..eaffee85a75 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -214,6 +214,7 @@ bool is_goto_binary(const std::string &filename)
 
 static void rename_symbols_in_function(
   goto_functionst::goto_functiont &function,
+  irep_idt &new_function_name,
   const rename_symbolt &rename_symbol)
 {
   goto_programt &program=function.body;
@@ -223,6 +224,9 @@ static void rename_symbols_in_function(
   {
     rename_symbol(iit->code);
     rename_symbol(iit->guard);
+    // we need to update the instruction's function field as
+    // well, with the new symbol for the function
+    iit->function=new_function_name;
   }
 }
 
@@ -256,7 +260,7 @@ static bool link_functions(
 
     if(dest_f_it==dest_functions.function_map.end()) // not there yet
     {
-      rename_symbols_in_function(src_it->second, rename_symbol);
+      rename_symbols_in_function(src_it->second, final_id, rename_symbol);
 
       goto_functionst::goto_functiont &in_dest_symbol_table=
         dest_functions.function_map[final_id];
@@ -275,7 +279,7 @@ static bool link_functions(
          weak_symbols.find(final_id)!=weak_symbols.end())
       {
         // the one with body wins!
-        rename_symbols_in_function(src_func, rename_symbol);
+        rename_symbols_in_function(src_func, final_id, rename_symbol);
 
         in_dest_symbol_table.body.swap(src_func.body);
         in_dest_symbol_table.type=src_func.type;
@@ -323,7 +327,10 @@ static bool link_functions(
 
   if(!macro_application.expr_map.empty())
     Forall_goto_functions(dest_it, dest_functions)
-      rename_symbols_in_function(dest_it->second, macro_application);
+    {
+      irep_idt final_id=dest_it->first;
+      rename_symbols_in_function(dest_it->second, final_id, macro_application);
+    }
 
   if(!object_type_updates.expr_map.empty())
   {

From 8cb7ff596db34d5c3ae403fb090be2c36b6bef83 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Wed, 20 Dec 2017 13:54:55 +0000
Subject: [PATCH 2/2] Add a test for the same-named static functions crashing
 dependence graph in the goto-analyser

---
 regression/goto-analyzer/dependence-graph6/file1.c   | 11 +++++++++++
 regression/goto-analyzer/dependence-graph6/file2.c   | 11 +++++++++++
 regression/goto-analyzer/dependence-graph6/main.c    |  8 ++++++++
 regression/goto-analyzer/dependence-graph6/test.desc |  9 +++++++++
 4 files changed, 39 insertions(+)
 create mode 100644 regression/goto-analyzer/dependence-graph6/file1.c
 create mode 100644 regression/goto-analyzer/dependence-graph6/file2.c
 create mode 100644 regression/goto-analyzer/dependence-graph6/main.c
 create mode 100644 regression/goto-analyzer/dependence-graph6/test.desc

diff --git a/regression/goto-analyzer/dependence-graph6/file1.c b/regression/goto-analyzer/dependence-graph6/file1.c
new file mode 100644
index 00000000000..c0b9f9063a5
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph6/file1.c
@@ -0,0 +1,11 @@
+extern int s1;
+static void sub(void)
+{
+  if (s1) {
+  }
+}
+
+void f1(void)
+{
+  sub();
+}
diff --git a/regression/goto-analyzer/dependence-graph6/file2.c b/regression/goto-analyzer/dependence-graph6/file2.c
new file mode 100644
index 00000000000..00f8455364d
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph6/file2.c
@@ -0,0 +1,11 @@
+extern int s2;
+static void sub(void)
+{
+  if (s2) {
+  }
+}
+
+void f2(void)
+{
+  sub();
+}
diff --git a/regression/goto-analyzer/dependence-graph6/main.c b/regression/goto-analyzer/dependence-graph6/main.c
new file mode 100644
index 00000000000..a6341efc83e
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph6/main.c
@@ -0,0 +1,8 @@
+void f1(void);
+void f2(void);
+
+void main(void)
+{
+  f1();
+  f2();
+}
diff --git a/regression/goto-analyzer/dependence-graph6/test.desc b/regression/goto-analyzer/dependence-graph6/test.desc
new file mode 100644
index 00000000000..01f458b5088
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph6/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+file1.c file2.c --dependence-graph
+^EXIT=0$
+^SIGNAL=0$
+--
+Assertion .+ failed
+--
+