From a403fdda3cdc093ca027fc4834d8aae23eb8444f Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Thu, 22 Mar 2018 16:01:34 +0000
Subject: [PATCH] Fix a bug in slice global inits where guard expressions were
 disregarded

---
 .../slice-global-inits2/main.c                | 13 +++++++++
 .../slice-global-inits2/test.desc             |  9 +++++++
 .../slice-global-inits3/main.c                | 14 ++++++++++
 .../slice-global-inits3/test.desc             |  9 +++++++
 src/goto-programs/slice_global_inits.cpp      | 27 ++++---------------
 5 files changed, 50 insertions(+), 22 deletions(-)
 create mode 100644 regression/goto-instrument/slice-global-inits2/main.c
 create mode 100644 regression/goto-instrument/slice-global-inits2/test.desc
 create mode 100644 regression/goto-instrument/slice-global-inits3/main.c
 create mode 100644 regression/goto-instrument/slice-global-inits3/test.desc

diff --git a/regression/goto-instrument/slice-global-inits2/main.c b/regression/goto-instrument/slice-global-inits2/main.c
new file mode 100644
index 00000000000..0039503f2c3
--- /dev/null
+++ b/regression/goto-instrument/slice-global-inits2/main.c
@@ -0,0 +1,13 @@
+
+int x;
+int y;
+
+int main()
+{
+  if(x)
+  {
+    y = 1;
+  }
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice-global-inits2/test.desc b/regression/goto-instrument/slice-global-inits2/test.desc
new file mode 100644
index 00000000000..8d2e0699012
--- /dev/null
+++ b/regression/goto-instrument/slice-global-inits2/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--slice-global-inits
+x = 0;$
+y = 0;$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/slice-global-inits3/main.c b/regression/goto-instrument/slice-global-inits3/main.c
new file mode 100644
index 00000000000..fa2e5939e3f
--- /dev/null
+++ b/regression/goto-instrument/slice-global-inits3/main.c
@@ -0,0 +1,14 @@
+
+int x;
+int y;
+
+void func(int a, int b)
+{
+}
+
+int main()
+{
+  func(x, y);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice-global-inits3/test.desc b/regression/goto-instrument/slice-global-inits3/test.desc
new file mode 100644
index 00000000000..8d2e0699012
--- /dev/null
+++ b/regression/goto-instrument/slice-global-inits3/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--slice-global-inits
+x = 0;$
+y = 0;$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp
index 33679d8a9d5..87d92c33a6d 100644
--- a/src/goto-programs/slice_global_inits.cpp
+++ b/src/goto-programs/slice_global_inits.cpp
@@ -13,10 +13,9 @@ Date:   December 2016
 
 #include "slice_global_inits.h"
 
-#include <unordered_set>
-
 #include <analyses/call_graph.h>
 
+#include <util/find_symbols.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/cprover_prefix.h>
@@ -46,23 +45,7 @@ void slice_global_inits(goto_modelt &goto_model)
 
   // gather all symbols used by reachable functions
 
-  class symbol_collectort:public const_expr_visitort
-  {
-  public:
-    virtual void operator()(const exprt &expr)
-    {
-      if(expr.id()==ID_symbol)
-      {
-        const symbol_exprt &symbol_expr=to_symbol_expr(expr);
-        const irep_idt id=symbol_expr.get_identifier();
-        symbols.insert(id);
-      }
-    }
-
-    std::unordered_set<irep_idt, irep_id_hash> symbols;
-  };
-
-  symbol_collectort visitor;
+  find_symbols_sett symbols;
 
   for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
   {
@@ -76,12 +59,12 @@ void slice_global_inits(goto_modelt &goto_model)
     forall_goto_program_instructions(i_it, goto_program)
     {
       const codet &code=i_it->code;
-      code.visit(visitor);
+      find_symbols(code, symbols, true, false);
+      const exprt &expr = i_it->guard;
+      find_symbols(expr, symbols, true, false);
     }
   }
 
-  const std::unordered_set<irep_idt, irep_id_hash> &symbols=visitor.symbols;
-
   // now remove unnecessary initializations
 
   goto_functionst::function_mapt::iterator f_it;