clinit_wrapper cont. (to be squashed later)

Instead of nondet-initializing all static variables instead of calling
clinit, call clinit and then nondet-initialize all non-final static
variables (to make sure they get the correct value from the clinit)

Author: svorenova

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -180,8 +180,9 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 
 /// Generates codet that iterates through the base types of the class specified
 /// by class_name, C, and recursively adds calls to their clinit wrapper.
-/// Finally a call to the clinit of C is made or if nondet-static option was
-/// given then all static variables of the class are nondet-initialized instead.
+/// Finally a call to the clinit of C is made. If nondet-static option was
+/// given then all static variables that are not constants (i.e. final) are
+/// then re-assigned to a nondet value.
 /// \param symbol_table: symbol table
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
@@ -216,26 +217,24 @@ 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())
   {
-    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);
+
+    // Add a standard nondet initialisation for each global declared on this
+    // class. Note this is the same invocation used in
+    // get_stub_initializer_body and java_static_lifetime_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
-    {
-      // Add a standard nondet initialisation for each global declared on this
-      // class. Note this is the same invocation used in
-      // get_stub_initializer_body and java_static_lifetime_init.
-
       object_factory_parameterst parameters = object_factory_parameters;
       parameters.function_id = clinit_wrapper_name(class_name);
 
       for(const auto &symbol : symbol_table.symbols)
       {
         if(
+          symbol.second.type.get(ID_C_class) == class_name &&
           symbol.second.is_static_lifetime &&
-          symbol.second.type.get(ID_C_class) == class_name)
+          !symbol.second.type.get_bool(ID_C_constant))
         {
           const symbol_exprt new_global_symbol = symbol.second.symbol_expr();