Ensure JSON file is JSON object just after parsing

There is no reason to delay this check, and we can provide useful
warning messages right at the start of the bytecode analysis.

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -204,8 +204,21 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
   {
     const std::string filename = options.get_option("static-values");
     jsont tmp_json;
-    if(!parse_json(filename, *message_handler, tmp_json))
-      static_values_json = std::move(tmp_json);
+    if(parse_json(filename, *message_handler, tmp_json))
+    {
+      warning() << "Provided JSON file for static-values cannot be parsed; it"
+                << " will be ignored." << messaget::eom;
+    }
+    else
+    {
+      if(!tmp_json.is_object())
+      {
+        warning() << "Provided JSON file for static-values is not a JSON "
+                  << "object; it will be ignored." << messaget::eom;
+      }
+      else
+        static_values_json = std::move(to_json_object(tmp_json));
+    }
   }
 
   if(options.is_set("context-include") || options.is_set("context-exclude"))

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -232,7 +232,7 @@ class java_bytecode_languaget:public languaget
   /// JSON which contains initial values of static fields (right
   /// after the static initializer of the class was run). This is read from the
   /// --static-values command-line option.
-  optionalt<jsont> static_values_json;
+  optionalt<json_objectt> static_values_json;
 
   // list of classes to force load even without reference from the entry point
   std::vector<irep_idt> java_load_classes;

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -769,20 +769,19 @@ code_ifthenelset get_clinit_wrapper_body(
 
 code_blockt get_user_specified_clinit_body(
   const irep_idt &class_id,
-  const optionalt<jsont> &static_values_json,
+  const optionalt<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() && static_values_json->is_object())
+  if(static_values_json.has_value())
   {
-    const auto &json_object = to_json_object(*static_values_json);
     const auto class_entry =
-      json_object.find(id2string(strip_java_namespace_prefix(class_id)));
-    if(class_entry != json_object.end())
+      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())

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<jsont> &static_values_json,
+  const optionalt<json_objectt> &static_values_json,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,