Add improved functionality for the construction of json_arrayt and json_objectt

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -461,7 +461,7 @@ int jbmc_parse_optionst::doit()
       break;
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_options({{"options", options.to_json()}});
+      json_objectt json_options{{"options", options.to_json()}};
       debug() << json_options;
       break;
     }

src/analyses/ai.cpp

@@ -95,11 +95,11 @@ jsont ai_baset::output_json(
     std::ostringstream out;
     goto_program.output_instruction(ns, function_id, out, *i_it);
 
-    json_objectt location(
-      {{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
-       {"sourceLocation", json_stringt(i_it->source_location.as_string())},
-       {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
-       {"instruction", json_stringt(out.str())}});
+    json_objectt location{
+      {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
+      {"sourceLocation", json_stringt(i_it->source_location.as_string())},
+      {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
+      {"instruction", json_stringt(out.str())}};
 
     contents.push_back(std::move(location));
   }

src/analyses/dependence_graph.cpp

@@ -285,19 +285,19 @@ jsont dep_graph_domaint::output_json(
 
   for(const auto &cd : control_deps)
   {
-    json_objectt link(
-      {{"locationNumber", json_numbert(std::to_string(cd->location_number))},
-       {"sourceLocation", json(cd->source_location)},
-       {"type", json_stringt("control")}});
+    json_objectt link{
+      {"locationNumber", json_numbert(std::to_string(cd->location_number))},
+      {"sourceLocation", json(cd->source_location)},
+      {"type", json_stringt("control")}};
     graph.push_back(std::move(link));
   }
 
   for(const auto &dd : data_deps)
   {
-    json_objectt link(
-      {{"locationNumber", json_numbert(std::to_string(dd->location_number))},
-       {"sourceLocation", json(dd->source_location)},
-       {"type", json_stringt("data")}});
+    json_objectt link{
+      {"locationNumber", json_numbert(std::to_string(dd->location_number))},
+      {"sourceLocation", json(dd->source_location)},
+      {"type", json_stringt("data")}};
     graph.push_back(std::move(link));
   }
 

src/cbmc/bmc_cover.cpp

@@ -383,7 +383,7 @@ bool bmc_covert::operator()()
           {
             if(step.is_input())
             {
-              json_objectt json_input({{"id", json_stringt(step.io_id)}});
+              json_objectt json_input{{"id", json_stringt(step.io_id)}};
               if(step.io_args.size()==1)
                 json_input["value"]=
                   json(step.io_args.front(), bmc.ns, ID_unknown);

src/goto-analyzer/static_verifier.cpp

@@ -12,6 +12,7 @@ Author: Martin Brain, [email protected]
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/options.h>
+#include <util/range.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -20,48 +21,42 @@ Author: Martin Brain, [email protected]
 struct static_verifier_resultt
 {
   // clang-format off
-  enum { TRUE, FALSE, BOTTOM, UNKNOWN } status;
+  enum statust { TRUE, FALSE, BOTTOM, UNKNOWN } status;
   // clang-format on
   source_locationt source_location;
   irep_idt function_id;
 };
 
+/// Makes a status message string from a status.
+static const char *message(const static_verifier_resultt::statust &status)
+{
+  switch(status)
+  {
+  case static_verifier_resultt::TRUE:
+    return "SUCCESS";
+  case static_verifier_resultt::FALSE:
+    return "FAILURE (if reachable)";
+  case static_verifier_resultt::BOTTOM:
+    return "SUCCESS (unreachable)";
+  case static_verifier_resultt::UNKNOWN:
+    return "UNKNOWN";
+  }
+  UNREACHABLE;
+}
+
 static void static_verifier_json(
   const std::vector<static_verifier_resultt> &results,
   messaget &m,
   std::ostream &out)
 {
   m.status() << "Writing JSON report" << messaget::eom;
-
-  json_arrayt json_result;
-
-  for(const auto &result : results)
-  {
-    json_objectt &j = json_result.push_back().make_object();
-
-    switch(result.status)
-    {
-    case static_verifier_resultt::TRUE:
-      j["status"] = json_stringt("SUCCESS");
-      break;
-
-    case static_verifier_resultt::FALSE:
-      j["status"] = json_stringt("FAILURE (if reachable)");
-      break;
-
-    case static_verifier_resultt::BOTTOM:
-      j["status"] = json_stringt("SUCCESS (unreachable)");
-      break;
-
-    case static_verifier_resultt::UNKNOWN:
-      j["status"] = json_stringt("UNKNOWN");
-      break;
-    }
-
-    j["sourceLocation"] = json(result.source_location);
-  }
-
-  out << json_result;
+  out << make_range(results)
+           .map([](const static_verifier_resultt &result) {
+             return json_objectt{
+               {"status", json_stringt{message(result.status)}},
+               {"sourceLocation", json(result.source_location)}};
+           })
+           .collect<json_arrayt>();
 }
 
 static void static_verifier_xml(

src/goto-analyzer/taint_analysis.cpp

@@ -355,12 +355,12 @@ bool taint_analysist::operator()(
 
         if(use_json)
         {
-          json_objectt json(
-            {{"bugClass",
-              json_stringt(i_it->source_location.get_property_class())},
-             {"file", json_stringt(i_it->source_location.get_file())},
-             {"line",
-              json_numbert(id2string(i_it->source_location.get_line()))}});
+          json_objectt json{
+            {"bugClass",
+             json_stringt(i_it->source_location.get_property_class())},
+            {"file", json_stringt(i_it->source_location.get_file())},
+            {"line",
+             json_numbert(id2string(i_it->source_location.get_line()))}};
           json_result.push_back(std::move(json));
         }
         else

src/goto-analyzer/unreachable_instructions.cpp

@@ -114,12 +114,12 @@ static void add_to_json(
   DATA_INVARIANT(end_function->is_end_function(),
                  "The last instruction in a goto-program must be END_FUNCTION");
 
-  json_objectt entry(
-    {{"function", json_stringt(function_identifier)},
-     {"fileName",
-      json_stringt(concat_dir_file(
-        id2string(end_function->source_location.get_working_directory()),
-        id2string(end_function->source_location.get_file())))}});
+  json_objectt entry{
+    {"function", json_stringt(function_identifier)},
+    {"fileName",
+     json_stringt(concat_dir_file(
+       id2string(end_function->source_location.get_working_directory()),
+       id2string(end_function->source_location.get_file())))}};
 
   json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
 
@@ -142,8 +142,8 @@ static void add_to_json(
 
     // print info for file actually with full path
     const source_locationt &l=it->second->source_location;
-    json_objectt i_entry(
-      {{"sourceLocation", json(l)}, {"statement", json_stringt(s)}});
+    json_objectt i_entry{{"sourceLocation", json(l)},
+                         {"statement", json_stringt(s)}};
     dead_ins.push_back(std::move(i_entry));
   }
 
@@ -246,14 +246,14 @@ static void json_output_function(
   const source_locationt &last_location,
   json_arrayt &dest)
 {
-  json_objectt entry(
-    {{"function", json_stringt(function)},
-     {"file name",
-      json_stringt(concat_dir_file(
-        id2string(first_location.get_working_directory()),
-        id2string(first_location.get_file())))},
-     {"first line", json_numbert(id2string(first_location.get_line()))},
-     {"last line", json_numbert(id2string(last_location.get_line()))}});
+  json_objectt entry{
+    {"function", json_stringt(function)},
+    {"file name",
+     json_stringt(concat_dir_file(
+       id2string(first_location.get_working_directory()),
+       id2string(first_location.get_file())))},
+    {"first line", json_numbert(id2string(first_location.get_line()))},
+    {"last line", json_numbert(id2string(last_location.get_line()))}};
 
   dest.push_back(std::move(entry));
 }

src/goto-diff/goto_diff_base.cpp

@@ -38,9 +38,9 @@ void goto_difft::output_functions() const
     }
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result(
-        {{"totalNumberOfFunctions",
-          json_stringt(std::to_string(total_functions_count))}});
+      json_objectt json_result{
+        {"totalNumberOfFunctions",
+         json_stringt(std::to_string(total_functions_count))}};
       convert_function_group_json(
         json_result["newFunctions"].make_array(), new_functions, goto_model2);
       convert_function_group_json(

src/goto-instrument/unwind.cpp

@@ -346,11 +346,10 @@ jsont goto_unwindt::unwind_logt::output_log_json() const
     goto_programt::const_targett target=it->first;
     unsigned location_number=it->second;
 
-    json_objectt object(
-      {{"originalLocationNumber",
-        json_numbert(std::to_string(location_number))},
-       {"newLocationNumber",
-        json_numbert(std::to_string(target->location_number))}});
+    json_objectt object{
+      {"originalLocationNumber", json_numbert(std::to_string(location_number))},
+      {"newLocationNumber",
+       json_numbert(std::to_string(target->location_number))}};
 
     json_unwound.push_back(std::move(object));
   }

src/goto-programs/goto_inline_class.cpp

@@ -887,17 +887,17 @@ jsont goto_inlinet::goto_inline_logt::output_inline_log_json() const
 
     PRECONDITION(start->location_number <= end->location_number);
 
-    json_arrayt json_orig(
-      {json_numbert(std::to_string(info.begin_location_number)),
-       json_numbert(std::to_string(info.end_location_number))});
-    json_arrayt json_new({json_numbert(std::to_string(start->location_number)),
-                          json_numbert(std::to_string(end->location_number))});
-
-    json_objectt object(
-      {{"call", json_numbert(std::to_string(info.call_location_number))},
-       {"function", json_stringt(info.function.c_str())},
-       {"originalSegment", std::move(json_orig)},
-       {"inlinedSegment", std::move(json_new)}});
+    json_arrayt json_orig{
+      json_numbert(std::to_string(info.begin_location_number)),
+      json_numbert(std::to_string(info.end_location_number))};
+    json_arrayt json_new{json_numbert(std::to_string(start->location_number)),
+                         json_numbert(std::to_string(end->location_number))};
+
+    json_objectt object{
+      {"call", json_numbert(std::to_string(info.call_location_number))},
+      {"function", json_stringt(info.function.c_str())},
+      {"originalSegment", std::move(json_orig)},
+      {"inlinedSegment", std::move(json_new)}};
 
     json_inlined.push_back(std::move(object));
   }

src/goto-programs/json_expr.cpp

@@ -172,8 +172,8 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
       to_struct_type(type).components();
     for(const auto &component : components)
     {
-      json_objectt e({{"name", json_stringt(component.get_name())},
-                      {"type", json(component.type(), ns, mode)}});
+      json_objectt e{{"name", json_stringt(component.get_name())},
+                     {"type", json(component.type(), ns, mode)}};
       members.push_back(std::move(e));
     }
   }
@@ -185,8 +185,8 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
       to_union_type(type).components();
     for(const auto &component : components)
     {
-      json_objectt e({{"name", json_stringt(component.get_name())},
-                      {"type", json(component.type(), ns, mode)}});
+      json_objectt e{{"name", json_stringt(component.get_name())},
+                     {"type", json(component.type(), ns, mode)}};
       members.push_back(std::move(e));
     }
   }
@@ -348,8 +348,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
 
     forall_operands(it, expr)
     {
-      json_objectt e({{"index", json_numbert(std::to_string(index))},
-                      {"value", json(*it, ns, mode)}});
+      json_objectt e{{"index", json_numbert(std::to_string(index))},
+                     {"value", json(*it, ns, mode)}};
       elements.push_back(std::move(e));
       index++;
     }
@@ -370,8 +370,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
       json_arrayt &members = result["members"].make_array();
       for(std::size_t m = 0; m < expr.operands().size(); m++)
       {
-        json_objectt e({{"value", json(expr.operands()[m], ns, mode)},
-                        {"name", json_stringt(components[m].get_name())}});
+        json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
+                       {"name", json_stringt(components[m].get_name())}};
         members.push_back(std::move(e));
       }
     }

src/goto-programs/show_goto_functions_json.cpp

@@ -70,8 +70,8 @@ json_objectt show_goto_functions_jsont::convert(
       for(const goto_programt::instructiont &instruction :
         function.body.instructions)
       {
-        json_objectt instruction_entry(
-          {{"instructionId", json_stringt(instruction.to_string())}});
+        json_objectt instruction_entry{
+          {"instructionId", json_stringt(instruction.to_string())}};
 
         if(instruction.code.source_location().is_not_nil())
         {

src/goto-programs/show_properties.cpp

@@ -129,12 +129,12 @@ void convert_properties_json(
 
     irep_idt property_id=source_location.get_property_id();
 
-    json_objectt json_property(
-      {{"name", json_stringt(property_id)},
-       {"class", json_stringt(property_class)},
-       {"sourceLocation", json(source_location)},
-       {"description", json_stringt(description)},
-       {"expression", json_stringt(from_expr(ns, identifier, ins.guard))}});
+    json_objectt json_property{
+      {"name", json_stringt(property_id)},
+      {"class", json_stringt(property_class)},
+      {"sourceLocation", json(source_location)},
+      {"description", json_stringt(description)},
+      {"expression", json_stringt(from_expr(ns, identifier, ins.guard))}};
 
     if(!source_location.get_basic_block_covered_lines().empty())
       json_property["coveredLines"] =
@@ -155,7 +155,7 @@ void show_properties_json(
   for(const auto &fct : goto_functions.function_map)
     convert_properties_json(json_properties, ns, fct.first, fct.second.body);
 
-  json_objectt json_result({{"properties", json_properties}});
+  json_objectt json_result{{"properties", json_properties}};
   msg.result() << json_result;
 }