Make replace_nondet a non-member function

This makes the information flow more obvious.

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -22,23 +22,24 @@ void goto_symext::do_simplify(exprt &expr)
     simplify(expr, ns);
 }
 
-nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type)
+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count)
 {
   irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
   nondet_symbol_exprt new_expr(identifier, type);
   return new_expr;
 }
 
-void goto_symext::replace_nondet(exprt &expr)
+void replace_nondet(exprt &expr, unsigned &nondet_count)
 {
   if(expr.id()==ID_side_effect &&
      expr.get(ID_statement)==ID_nondet)
   {
-    nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
+    nondet_symbol_exprt new_expr =
+      build_symex_nondet(expr.type(), nondet_count);
     new_expr.add_source_location()=expr.source_location();
     expr.swap(new_expr);
   }
   else
     Forall_operands(it, expr)
-      replace_nondet(*it);
+      replace_nondet(*it, nondet_count);
 }

src/goto-symex/goto_symex.h

@@ -320,8 +320,6 @@ class goto_symext
     statet &,
     const goto_functionst::goto_functiont &);
 
-  nondet_symbol_exprt build_symex_nondet(typet &type);
-
   // exceptions
   void symex_throw(statet &);
   void symex_catch(statet &);
@@ -404,7 +402,6 @@ class goto_symext
   static unsigned nondet_count;
   static unsigned dynamic_counter;
 
-  void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
 
   path_storaget &path_storage;
@@ -452,6 +449,10 @@ class goto_symext
   }
 };
 
+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);
+
+void replace_nondet(exprt &, unsigned &);
+
 void symex_transition(goto_symext::statet &state);
 
 void symex_transition(

src/goto-symex/symex_builtin_functions.cpp

@@ -177,7 +177,7 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    const exprt nondet = build_symex_nondet(object_type);
+    const exprt nondet = build_symex_nondet(object_type, nondet_count);
     const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }

src/goto-symex/symex_clean_expr.cpp

@@ -140,7 +140,7 @@ void goto_symext::clean_expr(
   statet &state,
   const bool write)
 {
-  replace_nondet(expr);
+  replace_nondet(expr, nondet_count);
   dereference(expr, state, write);
 
   // make sure all remaining byte extract operations use the root