Nondet static: update the symbol table

Update the symbol table and auto-generate __CPROVER_initialize instead
of hand-tweaking the function. This will ensure that any further
rebuilding of __CPROVER_initialize preserves those changes.

Author: tautschnig

src/goto-instrument/nondet_static.cpp

@@ -77,7 +77,7 @@ bool is_nondet_initializable_static(
 /// \param ns: Namespace for resolving type information.
 /// \param [out] goto_functions: Existing goto-functions to be updated.
 /// \param fct_name: Name of the goto-function to be updated.
-void nondet_static(
+static void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions,
   const irep_idt &fct_name)
@@ -188,6 +188,10 @@ void nondet_static(
     {
       symbol.value.set(ID_C_no_nondet_initialization, 1);
     }
+    else if(is_nondet_initializable_static(symbol.symbol_expr(), ns))
+    {
+      symbol.value = side_effect_expr_nondett(symbol.type, symbol.location);
+    }
   }
 
   nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);