Merge pull request diffblue#1961 from danpoe/slice-global-inits-fix

Fix a bug in slice global inits where guard expressions were disregarded

Author: tautschnig

regression/goto-instrument/slice-global-inits2/main.c

@@ -0,0 +1,13 @@
+
+int x;
+int y;
+
+int main()
+{
+  if(x)
+  {
+    y = 1;
+  }
+
+  return 0;
+}

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

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

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

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;