From 05f46a9938ddd0d5ecc9fb764fc2f4e36b80a5ad Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Wed, 20 Dec 2017 14:58:55 +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/link_goto_model.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp
index 2c8b49f74b7..8c2de974e8d 100644
--- a/src/goto-programs/link_goto_model.cpp
+++ b/src/goto-programs/link_goto_model.cpp
@@ -23,6 +23,7 @@ Author: Michael Tautschnig, Daniel Kroening
 
 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;
@@ -32,6 +33,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;
   }
 }
 
@@ -67,7 +71,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];
@@ -86,7 +90,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;
@@ -136,7 +140,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 acac776c573d27f13743f8d1de216ff2a39a32b0 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..7a44f5be38d
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph6/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+file1.c file2.c --dependence-graph --show
+^EXIT=0$
+^SIGNAL=0$
+--
+Assertion .+ failed
+--
+