Nondet-initialize variables in clinit_wrapper constructor

If nondet-static option is used

Author: svorenova

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -184,7 +184,7 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
 static void clinit_wrapper_do_recursive_calls(
-  const symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &class_name,
   code_blockt &init_body,
   const bool nondet_static,
@@ -208,9 +208,43 @@ static void clinit_wrapper_do_recursive_calls(
   auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
   if(find_sym_it != symbol_table.symbols.end())
   {
-    code_function_callt call_real_init;
-    call_real_init.function() = find_sym_it->second.symbol_expr();
-    init_body.move_to_operands(call_real_init);
+    if(!nondet_static)
+    {
+      code_function_callt call_real_init;
+      call_real_init.function() = find_sym_it->second.symbol_expr();
+      init_body.move_to_operands(call_real_init);
+    }
+    else
+    {
+      object_factory_parameterst parameters = object_factory_parameters;
+      parameters.function_id = real_clinit_name;
+
+      for(const auto &symbol : symbol_table.symbols)
+      {
+        if(
+          symbol.second.is_static_lifetime &&
+          symbol.second.type.get(ID_C_class) == class_name)
+        {
+          const symbol_exprt new_global_symbol = symbol.second.symbol_expr();
+
+          parameters.max_nonnull_tree_depth =
+            is_non_null_library_global(symbol.first)
+              ? object_factory_parameters.max_nonnull_tree_depth + 1
+              : object_factory_parameters.max_nonnull_tree_depth;
+
+          gen_nondet_init(
+            new_global_symbol,
+            init_body,
+            symbol_table,
+            source_locationt(),
+            false,
+            allocation_typet::DYNAMIC,
+            parameters,
+            pointer_type_selector,
+            update_in_placet::NO_UPDATE_IN_PLACE);
+        }
+      }
+    }
   }
 }