Remove id2string from inside calls to the json_stringt constructor.

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));
   }

src/util/json_expr.cpp

@@ -85,24 +85,22 @@ json_objectt json(const source_locationt &location)
   json_objectt result;
 
   if(!location.get_working_directory().empty())
-    result["workingDirectory"]=
-      json_stringt(id2string(location.get_working_directory()));
+    result["workingDirectory"] = json_stringt(location.get_working_directory());
 
   if(!location.get_file().empty())
-    result["file"]=json_stringt(id2string(location.get_file()));
+    result["file"] = json_stringt(location.get_file());
 
   if(!location.get_line().empty())
-    result["line"]=json_stringt(id2string(location.get_line()));
+    result["line"] = json_stringt(location.get_line());
 
   if(!location.get_column().empty())
-    result["column"]=json_stringt(id2string(location.get_column()));
+    result["column"] = json_stringt(location.get_column());
 
   if(!location.get_function().empty())
-    result["function"]=json_stringt(id2string(location.get_function()));
+    result["function"] = json_stringt(location.get_function());
 
   if(!location.get_java_bytecode_index().empty())
-    result["bytecodeIndex"]=
-      json_stringt(id2string(location.get_java_bytecode_index()));
+    result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
 
   return result;
 }
@@ -193,7 +191,7 @@ json_objectt json(
     for(const auto &component : components)
     {
       json_objectt &e=members.push_back().make_object();
-      e["name"]=json_stringt(id2string(component.get_name()));
+      e["name"] = json_stringt(component.get_name());
       e["type"]=json(component.type(), ns, mode);
     }
   }
@@ -206,7 +204,7 @@ json_objectt json(
     for(const auto &component : components)
     {
       json_objectt &e=members.push_back().make_object();
-      e["name"]=json_stringt(id2string(component.get_name()));
+      e["name"] = json_stringt(component.get_name());
       e["type"]=json(component.type(), ns, mode);
     }
   }
@@ -263,15 +261,15 @@ json_objectt json(
       std::size_t width=to_bitvector_type(type).get_width();
 
       result["name"]=json_stringt("integer");
-      result["binary"]=json_stringt(id2string(constant_expr.get_value()));
+      result["binary"] = json_stringt(constant_expr.get_value());
       result["width"]=json_numbert(std::to_string(width));
       result["type"]=json_stringt(type_string);
       result["data"]=json_stringt(value_string);
     }
     else if(type.id()==ID_c_enum)
     {
       result["name"]=json_stringt("integer");
-      result["binary"]=json_stringt(id2string(constant_expr.get_value()));
+      result["binary"] = json_stringt(constant_expr.get_value());
       result["width"]=json_numbert(type.subtype().get_string(ID_width));
       result["type"]=json_stringt("enum");
       result["data"]=json_stringt(value_string);
@@ -286,21 +284,21 @@ json_objectt json(
     else if(type.id()==ID_bv)
     {
       result["name"]=json_stringt("bitvector");
-      result["binary"]=json_stringt(id2string(constant_expr.get_value()));
+      result["binary"] = json_stringt(constant_expr.get_value());
     }
     else if(type.id()==ID_fixedbv)
     {
       result["name"]=json_stringt("fixed");
       result["width"]=json_numbert(type.get_string(ID_width));
-      result["binary"]=json_stringt(id2string(constant_expr.get_value()));
+      result["binary"] = json_stringt(constant_expr.get_value());
       result["data"]=
         json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
     }
     else if(type.id()==ID_floatbv)
     {
       result["name"]=json_stringt("float");
       result["width"]=json_numbert(type.get_string(ID_width));
-      result["binary"]=json_stringt(id2string(constant_expr.get_value()));
+      result["binary"] = json_stringt(constant_expr.get_value());
       result["data"]=
         json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
     }
@@ -341,7 +339,7 @@ json_objectt json(
     else if(type.id()==ID_string)
     {
       result["name"]=json_stringt("string");
-      result["data"]=json_stringt(id2string(constant_expr.get_value()));
+      result["data"] = json_stringt(constant_expr.get_value());
     }
     else
     {
@@ -381,7 +379,7 @@ json_objectt json(
       {
         json_objectt &e=members.push_back().make_object();
         e["value"]=json(expr.operands()[m], ns, mode);
-        e["name"]=json_stringt(id2string(components[m].get_name()));
+        e["name"] = json_stringt(components[m].get_name());
       }
     }
   }
@@ -392,7 +390,7 @@ json_objectt json(
     const union_exprt &union_expr=to_union_expr(expr);
     json_objectt &e=result["member"].make_object();
     e["value"]=json(union_expr.op(), ns, mode);
-    e["name"]=json_stringt(id2string(union_expr.get_component_name()));
+    e["name"] = json_stringt(union_expr.get_component_name());
   }
   else
     result["name"]=json_stringt("unknown");