diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 421b8111edc..d23889242fd 100644 --- a/src/cbmc/all_properties.cpp +++ b/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) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ea7b3e17f30..4683a42d29c 100644 --- a/src/cbmc/bmc.cpp +++ b/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"); diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 72d64a184a5..2382c7d8bfa 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/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)); } } diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index df85702500d..2e763978dcb 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/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()); } } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index f2722c98e91..67539387227 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/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); diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index c691142aead..bae1266ee89 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/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()), diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index a06b13edf2b..16a8f523979 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/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")) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 1095a3ad281..5d69118a4a0 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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()) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index bfedc6250c2..1955c1edd11 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/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= diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 6df2f69bf33..54b2aa1a6ab 100644 --- a/src/goto-programs/show_properties.cpp +++ b/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)); } diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index aa8b63a0dc7..0e9147fe775 100644 --- a/src/util/json_expr.cpp +++ b/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,7 +261,7 @@ 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); @@ -271,7 +269,7 @@ json_objectt json( 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,13 +284,13 @@ 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()); } @@ -300,7 +298,7 @@ json_objectt json( { 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");