Merge pull request #2180 from thomasspriggs/json_id2string

 Remove `id2string` from inside calls to the `json_stringt` constructor.

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -214,8 +214,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
       for(const auto &g : goal_map)
       {
         json_stream_objectt &result = result_array.push_back_stream_object();
-        result["property"]=json_stringt(id2string(g.first));
-        result["description"]=json_stringt(id2string(g.second.description));
+        result["property"] = json_stringt(g.first);
+        result["description"] = json_stringt(g.second.description);
         result["status"]=json_stringt(g.second.status_string());
 
         if(g.second.status==goalt::statust::FAILURE)

src/cbmc/bmc.cpp

@@ -74,10 +74,10 @@ void bmct::error_trace()
       json_stream_objectt &json_result =
         status().json_stream().push_back_stream_object();
       const goto_trace_stept &step=goto_trace.steps.back();
-      json_result["property"]=
-        json_stringt(id2string(step.pc->source_location.get_property_id()));
-      json_result["description"]=
-        json_stringt(id2string(step.pc->source_location.get_comment()));
+      json_result["property"] =
+        json_stringt(step.pc->source_location.get_property_id());
+      json_result["description"] =
+        json_stringt(step.pc->source_location.get_comment());
       json_result["status"]=json_stringt("failed");
       json_stream_arrayt &json_trace =
         json_result.push_back_stream_array("trace");

src/cbmc/bmc_cover.cpp

@@ -355,7 +355,7 @@ bool bmc_covert::operator()()
 
         json_result["status"] =
           json_stringt(goal.satisfied ? "satisfied" : "failed");
-        json_result["goal"] = json_stringt(id2string(goal_pair.first));
+        json_result["goal"] = json_stringt(goal_pair.first);
         json_result["description"] = json_stringt(goal.description);
 
         if(goal.source_location.is_not_nil())
@@ -382,7 +382,7 @@ bool bmc_covert::operator()()
             if(step.is_input())
             {
               json_objectt json_input;
-              json_input["id"]=json_stringt(id2string(step.io_id));
+              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);
@@ -393,7 +393,7 @@ bool bmc_covert::operator()()
         json_arrayt &goal_refs=result["coveredGoals"].make_array();
         for(const auto &goal_id : test.covered_goals)
         {
-          goal_refs.push_back(json_stringt(id2string(goal_id)));
+          goal_refs.push_back(json_stringt(goal_id));
         }
       }
 

src/goto-analyzer/static_analyzer.cpp

@@ -153,10 +153,9 @@ void static_analyzert::json_report(const std::string &file_name)
       else
         j["status"]=json_stringt("UNKNOWN");
 
-      j["file"]=json_stringt(id2string(i_it->source_location.get_file()));
+      j["file"] = json_stringt(i_it->source_location.get_file());
       j["line"]=json_numbert(id2string(i_it->source_location.get_line()));
-      j["description"]=json_stringt(id2string(
-        i_it->source_location.get_comment()));
+      j["description"] = json_stringt(i_it->source_location.get_comment());
     }
   }
 

src/goto-analyzer/taint_analysis.cpp

@@ -351,10 +351,9 @@ bool taint_analysist::operator()(
         if(use_json)
         {
           json_objectt json;
-          json["bugClass"]=
-            json_stringt(id2string(i_it->source_location.get_property_class()));
-          json["file"]=
-            json_stringt(id2string(i_it->source_location.get_file()));
+          json["bugClass"] =
+            json_stringt(i_it->source_location.get_property_class());
+          json["file"] = json_stringt(i_it->source_location.get_file());
           json["line"]=
             json_numbert(id2string(i_it->source_location.get_line()));
           json_result.array.push_back(json);

src/goto-analyzer/unreachable_instructions.cpp

@@ -127,7 +127,7 @@ static void add_to_json(
   DATA_INVARIANT(end_function->is_end_function(),
                  "The last instruction in a goto-program must be END_FUNCTION");
 
-  entry["function"]=json_stringt(id2string(end_function->function));
+  entry["function"] = json_stringt(end_function->function);
   entry["fileName"]=
     json_stringt(concat_dir_file(
         id2string(end_function->source_location.get_working_directory()),
@@ -261,7 +261,7 @@ static void json_output_function(
 {
   json_objectt &entry=dest.push_back().make_object();
 
-  entry["function"]=json_stringt(id2string(function));
+  entry["function"] = json_stringt(function);
   entry["file name"]=
     json_stringt(concat_dir_file(
         id2string(first_location.get_working_directory()),

src/goto-diff/goto_diff_base.cpp

@@ -136,7 +136,7 @@ void goto_difft::convert_function_json(
   namespacet ns(goto_model.symbol_table);
   const symbolt &symbol = ns.lookup(function_name);
 
-  result["name"] = json_stringt(id2string(function_name));
+  result["name"] = json_stringt(function_name);
   result["sourceLocation"] = json(symbol.location);
 
   if(options.get_bool_option("show-properties"))

src/goto-programs/json_goto_trace.cpp

@@ -52,8 +52,8 @@ void convert_assert(
   json_failure["hidden"] = jsont::json_boolean(step.hidden);
   json_failure["internal"] = jsont::json_boolean(step.internal);
   json_failure["thread"] = json_numbert(std::to_string(step.thread_nr));
-  json_failure["reason"] = json_stringt(id2string(step.comment));
-  json_failure["property"] = json_stringt(id2string(property_id));
+  json_failure["reason"] = json_stringt(step.comment);
+  json_failure["property"] = json_stringt(property_id);
 
   if(!location.is_null())
     json_failure["sourceLocation"] = location;
@@ -133,7 +133,7 @@ void convert_decl(
     if(type_string == "")
       type_string = from_type(ns, identifier, symbol->type);
 
-    json_assignment["mode"] = json_stringt(id2string(symbol->mode));
+    json_assignment["mode"] = json_stringt(symbol->mode);
     exprt simplified = simplify_expr(step.full_lhs_value, ns);
 
     full_lhs_value = json(simplified, ns, symbol->mode);
@@ -183,7 +183,7 @@ void convert_output(
   json_output["hidden"] = jsont::json_boolean(step.hidden);
   json_output["internal"] = jsont::json_boolean(step.internal);
   json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
-  json_output["outputID"] = json_stringt(id2string(step.io_id));
+  json_output["outputID"] = json_stringt(step.io_id);
 
   // Recovering the mode from the function
   irep_idt mode;
@@ -193,7 +193,7 @@ void convert_output(
     mode = ID_unknown;
   else
     mode = function_name->mode;
-  json_output["mode"] = json_stringt(id2string(mode));
+  json_output["mode"] = json_stringt(mode);
   json_arrayt &json_values = json_output["values"].make_array();
 
   for(const auto &arg : step.io_args)
@@ -226,7 +226,7 @@ void convert_input(
   json_input["hidden"] = jsont::json_boolean(step.hidden);
   json_input["internal"] = jsont::json_boolean(step.internal);
   json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
-  json_input["inputID"] = json_stringt(id2string(step.io_id));
+  json_input["inputID"] = json_stringt(step.io_id);
 
   // Recovering the mode from the function
   irep_idt mode;
@@ -236,7 +236,7 @@ void convert_input(
     mode = ID_unknown;
   else
     mode = function_name->mode;
-  json_input["mode"] = json_stringt(id2string(mode));
+  json_input["mode"] = json_stringt(mode);
   json_arrayt &json_values = json_input["values"].make_array();
 
   for(const auto &arg : step.io_args)
@@ -275,8 +275,8 @@ void convert_return(
 
   const symbolt &symbol = ns.lookup(step.identifier);
   json_objectt &json_function = json_call_return["function"].make_object();
-  json_function["displayName"] = json_stringt(id2string(symbol.display_name()));
-  json_function["identifier"] = json_stringt(id2string(step.identifier));
+  json_function["displayName"] = json_stringt(symbol.display_name());
+  json_function["identifier"] = json_stringt(step.identifier);
   json_function["sourceLocation"] = json(symbol.location);
 
   if(!location.is_null())

src/goto-programs/show_goto_functions_json.cpp

@@ -48,7 +48,7 @@ json_objectt show_goto_functions_jsont::convert(
 
     json_objectt &json_function=
       json_functions.push_back(jsont()).make_object();
-    json_function["name"]=json_stringt(id2string(function_name));
+    json_function["name"] = json_stringt(function_name);
     json_function["isBodyAvailable"]=
       jsont::json_boolean(function.body_available());
     bool is_internal=

src/goto-programs/show_properties.cpp

@@ -131,14 +131,13 @@ void convert_properties_json(
 
     json_objectt &json_property=
       json_properties.push_back(jsont()).make_object();
-    json_property["name"]=json_stringt(id2string(property_id));
-    json_property["class"]=json_stringt(id2string(property_class));
+    json_property["name"] = json_stringt(property_id);
+    json_property["class"] = json_stringt(property_class);
     if(!source_location.get_basic_block_covered_lines().empty())
-      json_property["coveredLines"]=
-        json_stringt(
-          id2string(source_location.get_basic_block_covered_lines()));
+      json_property["coveredLines"] =
+        json_stringt(source_location.get_basic_block_covered_lines());
     json_property["sourceLocation"]=json(source_location);
-    json_property["description"]=json_stringt(id2string(description));
+    json_property["description"] = json_stringt(description);
     json_property["expression"]=
       json_stringt(from_expr(ns, identifier, ins.guard));
   }