Make get_user_specified_clinit_body json arg non optional

No user specified static initializer should appear if the static-values
is not set anyway. So this if condition can be replaced by an invariant
at the call site.

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1210,9 +1210,11 @@ bool java_bytecode_languaget::convert_single_method(
         declaring_class(symbol_table.lookup_ref(function_id));
       INVARIANT(
         class_name, "user_specified_clinit must be declared by a class.");
+      INVARIANT(
+        static_values_json.has_value(), "static-values JSON must be available");
       writable_symbol.value = get_user_specified_clinit_body(
         *class_name,
-        static_values_json,
+        *static_values_json,
         symbol_table,
         get_message_handler(),
         needed_lazy_methods,

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -769,57 +769,54 @@ code_ifthenelset get_clinit_wrapper_body(
 
 code_blockt get_user_specified_clinit_body(
   const irep_idt &class_id,
-  const optionalt<json_objectt> &static_values_json,
+  const json_objectt &static_values_json,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   size_t max_user_array_length,
   std::unordered_map<std::string, object_creation_referencet> &references)
 {
   const irep_idt &real_clinit_name = clinit_function_name(class_id);
-  if(static_values_json.has_value())
+  const auto class_entry =
+    static_values_json.find(id2string(strip_java_namespace_prefix(class_id)));
+  if(class_entry != static_values_json.end())
   {
-    const auto class_entry =
-      static_values_json->find(id2string(strip_java_namespace_prefix(class_id)));
-    if(class_entry != static_values_json->end())
+    const auto &class_json_value = class_entry->second;
+    if(class_json_value.is_object())
     {
-      const auto &class_json_value = class_entry->second;
-      if(class_json_value.is_object())
+      const auto &class_json_object = to_json_object(class_json_value);
+      std::map<symbol_exprt, jsont> static_field_values;
+      for(const auto &symbol_pair : symbol_table)
       {
-        const auto &class_json_object = to_json_object(class_json_value);
-        std::map<symbol_exprt, jsont> static_field_values;
-        for(const auto &symbol_pair : symbol_table)
+        const symbolt &symbol = symbol_pair.second;
+        if(
+          declaring_class(symbol) && *declaring_class(symbol) == class_id &&
+          symbol.is_static_lifetime)
         {
-          const symbolt &symbol = symbol_pair.second;
-          if(
-            declaring_class(symbol) && *declaring_class(symbol) == class_id &&
-            symbol.is_static_lifetime)
+          const symbol_exprt &static_field_expr = symbol.symbol_expr();
+          const auto &static_field_entry =
+            class_json_object.find(id2string(symbol.base_name));
+          if(static_field_entry != class_json_object.end())
           {
-            const symbol_exprt &static_field_expr = symbol.symbol_expr();
-            const auto &static_field_entry =
-              class_json_object.find(id2string(symbol.base_name));
-            if(static_field_entry != class_json_object.end())
-            {
-              static_field_values.insert(
-                {static_field_expr, static_field_entry->second});
-            }
+            static_field_values.insert(
+              {static_field_expr, static_field_entry->second});
           }
         }
-        code_blockt body;
-        for(const auto &value_pair : static_field_values)
-        {
-          assign_from_json(
-            value_pair.first,
-            value_pair.second,
-            real_clinit_name,
-            body,
-            symbol_table,
-            needed_lazy_methods,
-            max_user_array_length,
-            references);
-        }
-        return body;
       }
+      code_blockt body;
+      for(const auto &value_pair : static_field_values)
+      {
+        assign_from_json(
+          value_pair.first,
+          value_pair.second,
+          real_clinit_name,
+          body,
+          symbol_table,
+          needed_lazy_methods,
+          max_user_array_length,
+          references);
+      }
+      return body;
     }
   }
   if(const auto clinit_func = symbol_table.lookup(real_clinit_name))

jbmc/src/java_bytecode/java_static_initializers.h

@@ -76,7 +76,7 @@ code_ifthenelset get_clinit_wrapper_body(
 /// \return the body of the user_specified_clinit function as a code block.
 code_blockt get_user_specified_clinit_body(
   const irep_idt &class_id,
-  const optionalt<json_objectt> &static_values_json,
+  const json_objectt &static_values_json,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,