Skip to content

Commit 085fd6a

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #3862 from thomasspriggs/tas/json_construction
Add improved functionality for the construction of json_arrayt and json_objectt
2 parents d4e627b + 2a4d8ff commit 085fd6a

21 files changed

+365
-153
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -450,7 +450,7 @@ int jbmc_parse_optionst::doit()
450450
break;
451451
case ui_message_handlert::uit::JSON_UI:
452452
{
453-
json_objectt json_options({{"options", options.to_json()}});
453+
json_objectt json_options{{"options", options.to_json()}};
454454
debug() << json_options;
455455
break;
456456
}

‎src/analyses/ai.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -95,11 +95,11 @@ jsont ai_baset::output_json(
9595
std::ostringstream out;
9696
goto_program.output_instruction(ns, function_id, out, *i_it);
9797

98-
json_objectt location(
99-
{{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
100-
{"sourceLocation", json_stringt(i_it->source_location.as_string())},
101-
{"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
102-
{"instruction", json_stringt(out.str())}});
98+
json_objectt location{
99+
{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
100+
{"sourceLocation", json_stringt(i_it->source_location.as_string())},
101+
{"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
102+
{"instruction", json_stringt(out.str())}};
103103

104104
contents.push_back(std::move(location));
105105
}

‎src/analyses/dependence_graph.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -285,19 +285,19 @@ jsont dep_graph_domaint::output_json(
285285

286286
for(const auto &cd : control_deps)
287287
{
288-
json_objectt link(
289-
{{"locationNumber", json_numbert(std::to_string(cd->location_number))},
290-
{"sourceLocation", json(cd->source_location)},
291-
{"type", json_stringt("control")}});
288+
json_objectt link{
289+
{"locationNumber", json_numbert(std::to_string(cd->location_number))},
290+
{"sourceLocation", json(cd->source_location)},
291+
{"type", json_stringt("control")}};
292292
graph.push_back(std::move(link));
293293
}
294294

295295
for(const auto &dd : data_deps)
296296
{
297-
json_objectt link(
298-
{{"locationNumber", json_numbert(std::to_string(dd->location_number))},
299-
{"sourceLocation", json(dd->source_location)},
300-
{"type", json_stringt("data")}});
297+
json_objectt link{
298+
{"locationNumber", json_numbert(std::to_string(dd->location_number))},
299+
{"sourceLocation", json(dd->source_location)},
300+
{"type", json_stringt("data")}};
301301
graph.push_back(std::move(link));
302302
}
303303

‎src/cbmc/bmc_cover.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -383,7 +383,7 @@ bool bmc_covert::operator()()
383383
{
384384
if(step.is_input())
385385
{
386-
json_objectt json_input({{"id", json_stringt(step.io_id)}});
386+
json_objectt json_input{{"id", json_stringt(step.io_id)}};
387387
if(step.io_args.size()==1)
388388
json_input["value"]=
389389
json(step.io_args.front(), bmc.ns, ID_unknown);

‎src/goto-analyzer/static_verifier.cpp

Lines changed: 26 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Martin Brain, [email protected]
1212
#include <util/message.h>
1313
#include <util/namespace.h>
1414
#include <util/options.h>
15+
#include <util/range.h>
1516

1617
#include <goto-programs/goto_model.h>
1718

@@ -20,48 +21,42 @@ Author: Martin Brain, [email protected]
2021
struct static_verifier_resultt
2122
{
2223
// clang-format off
23-
enum { TRUE, FALSE, BOTTOM, UNKNOWN } status;
24+
enum statust { TRUE, FALSE, BOTTOM, UNKNOWN } status;
2425
// clang-format on
2526
source_locationt source_location;
2627
irep_idt function_id;
2728
};
2829

30+
/// Makes a status message string from a status.
31+
static const char *message(const static_verifier_resultt::statust &status)
32+
{
33+
switch(status)
34+
{
35+
case static_verifier_resultt::TRUE:
36+
return "SUCCESS";
37+
case static_verifier_resultt::FALSE:
38+
return "FAILURE (if reachable)";
39+
case static_verifier_resultt::BOTTOM:
40+
return "SUCCESS (unreachable)";
41+
case static_verifier_resultt::UNKNOWN:
42+
return "UNKNOWN";
43+
}
44+
UNREACHABLE;
45+
}
46+
2947
static void static_verifier_json(
3048
const std::vector<static_verifier_resultt> &results,
3149
messaget &m,
3250
std::ostream &out)
3351
{
3452
m.status() << "Writing JSON report" << messaget::eom;
35-
36-
json_arrayt json_result;
37-
38-
for(const auto &result : results)
39-
{
40-
json_objectt &j = json_result.push_back().make_object();
41-
42-
switch(result.status)
43-
{
44-
case static_verifier_resultt::TRUE:
45-
j["status"] = json_stringt("SUCCESS");
46-
break;
47-
48-
case static_verifier_resultt::FALSE:
49-
j["status"] = json_stringt("FAILURE (if reachable)");
50-
break;
51-
52-
case static_verifier_resultt::BOTTOM:
53-
j["status"] = json_stringt("SUCCESS (unreachable)");
54-
break;
55-
56-
case static_verifier_resultt::UNKNOWN:
57-
j["status"] = json_stringt("UNKNOWN");
58-
break;
59-
}
60-
61-
j["sourceLocation"] = json(result.source_location);
62-
}
63-
64-
out << json_result;
53+
out << make_range(results)
54+
.map([](const static_verifier_resultt &result) {
55+
return json_objectt{
56+
{"status", json_stringt{message(result.status)}},
57+
{"sourceLocation", json(result.source_location)}};
58+
})
59+
.collect<json_arrayt>();
6560
}
6661

6762
static void static_verifier_xml(

‎src/goto-analyzer/taint_analysis.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -355,12 +355,12 @@ bool taint_analysist::operator()(
355355

356356
if(use_json)
357357
{
358-
json_objectt json(
359-
{{"bugClass",
360-
json_stringt(i_it->source_location.get_property_class())},
361-
{"file", json_stringt(i_it->source_location.get_file())},
362-
{"line",
363-
json_numbert(id2string(i_it->source_location.get_line()))}});
358+
json_objectt json{
359+
{"bugClass",
360+
json_stringt(i_it->source_location.get_property_class())},
361+
{"file", json_stringt(i_it->source_location.get_file())},
362+
{"line",
363+
json_numbert(id2string(i_it->source_location.get_line()))}};
364364
json_result.push_back(std::move(json));
365365
}
366366
else

‎src/goto-analyzer/unreachable_instructions.cpp

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -114,12 +114,12 @@ static void add_to_json(
114114
DATA_INVARIANT(end_function->is_end_function(),
115115
"The last instruction in a goto-program must be END_FUNCTION");
116116

117-
json_objectt entry(
118-
{{"function", json_stringt(function_identifier)},
119-
{"fileName",
120-
json_stringt(concat_dir_file(
121-
id2string(end_function->source_location.get_working_directory()),
122-
id2string(end_function->source_location.get_file())))}});
117+
json_objectt entry{
118+
{"function", json_stringt(function_identifier)},
119+
{"fileName",
120+
json_stringt(concat_dir_file(
121+
id2string(end_function->source_location.get_working_directory()),
122+
id2string(end_function->source_location.get_file())))}};
123123

124124
json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
125125

@@ -142,8 +142,8 @@ static void add_to_json(
142142

143143
// print info for file actually with full path
144144
const source_locationt &l=it->second->source_location;
145-
json_objectt i_entry(
146-
{{"sourceLocation", json(l)}, {"statement", json_stringt(s)}});
145+
json_objectt i_entry{{"sourceLocation", json(l)},
146+
{"statement", json_stringt(s)}};
147147
dead_ins.push_back(std::move(i_entry));
148148
}
149149

@@ -246,14 +246,14 @@ static void json_output_function(
246246
const source_locationt &last_location,
247247
json_arrayt &dest)
248248
{
249-
json_objectt entry(
250-
{{"function", json_stringt(function)},
251-
{"file name",
252-
json_stringt(concat_dir_file(
253-
id2string(first_location.get_working_directory()),
254-
id2string(first_location.get_file())))},
255-
{"first line", json_numbert(id2string(first_location.get_line()))},
256-
{"last line", json_numbert(id2string(last_location.get_line()))}});
249+
json_objectt entry{
250+
{"function", json_stringt(function)},
251+
{"file name",
252+
json_stringt(concat_dir_file(
253+
id2string(first_location.get_working_directory()),
254+
id2string(first_location.get_file())))},
255+
{"first line", json_numbert(id2string(first_location.get_line()))},
256+
{"last line", json_numbert(id2string(last_location.get_line()))}};
257257

258258
dest.push_back(std::move(entry));
259259
}

‎src/goto-diff/goto_diff_base.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,9 @@ void goto_difft::output_functions() const
3838
}
3939
case ui_message_handlert::uit::JSON_UI:
4040
{
41-
json_objectt json_result(
42-
{{"totalNumberOfFunctions",
43-
json_stringt(std::to_string(total_functions_count))}});
41+
json_objectt json_result{
42+
{"totalNumberOfFunctions",
43+
json_stringt(std::to_string(total_functions_count))}};
4444
convert_function_group_json(
4545
json_result["newFunctions"].make_array(), new_functions, goto_model2);
4646
convert_function_group_json(

‎src/goto-instrument/unwind.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -346,11 +346,10 @@ jsont goto_unwindt::unwind_logt::output_log_json() const
346346
goto_programt::const_targett target=it->first;
347347
unsigned location_number=it->second;
348348

349-
json_objectt object(
350-
{{"originalLocationNumber",
351-
json_numbert(std::to_string(location_number))},
352-
{"newLocationNumber",
353-
json_numbert(std::to_string(target->location_number))}});
349+
json_objectt object{
350+
{"originalLocationNumber", json_numbert(std::to_string(location_number))},
351+
{"newLocationNumber",
352+
json_numbert(std::to_string(target->location_number))}};
354353

355354
json_unwound.push_back(std::move(object));
356355
}

‎src/goto-programs/goto_inline_class.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -887,17 +887,17 @@ jsont goto_inlinet::goto_inline_logt::output_inline_log_json() const
887887

888888
PRECONDITION(start->location_number <= end->location_number);
889889

890-
json_arrayt json_orig(
891-
{json_numbert(std::to_string(info.begin_location_number)),
892-
json_numbert(std::to_string(info.end_location_number))});
893-
json_arrayt json_new({json_numbert(std::to_string(start->location_number)),
894-
json_numbert(std::to_string(end->location_number))});
895-
896-
json_objectt object(
897-
{{"call", json_numbert(std::to_string(info.call_location_number))},
898-
{"function", json_stringt(info.function.c_str())},
899-
{"originalSegment", std::move(json_orig)},
900-
{"inlinedSegment", std::move(json_new)}});
890+
json_arrayt json_orig{
891+
json_numbert(std::to_string(info.begin_location_number)),
892+
json_numbert(std::to_string(info.end_location_number))};
893+
json_arrayt json_new{json_numbert(std::to_string(start->location_number)),
894+
json_numbert(std::to_string(end->location_number))};
895+
896+
json_objectt object{
897+
{"call", json_numbert(std::to_string(info.call_location_number))},
898+
{"function", json_stringt(info.function.c_str())},
899+
{"originalSegment", std::move(json_orig)},
900+
{"inlinedSegment", std::move(json_new)}};
901901

902902
json_inlined.push_back(std::move(object));
903903
}

‎src/goto-programs/json_expr.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -172,8 +172,8 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
172172
to_struct_type(type).components();
173173
for(const auto &component : components)
174174
{
175-
json_objectt e({{"name", json_stringt(component.get_name())},
176-
{"type", json(component.type(), ns, mode)}});
175+
json_objectt e{{"name", json_stringt(component.get_name())},
176+
{"type", json(component.type(), ns, mode)}};
177177
members.push_back(std::move(e));
178178
}
179179
}
@@ -185,8 +185,8 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
185185
to_union_type(type).components();
186186
for(const auto &component : components)
187187
{
188-
json_objectt e({{"name", json_stringt(component.get_name())},
189-
{"type", json(component.type(), ns, mode)}});
188+
json_objectt e{{"name", json_stringt(component.get_name())},
189+
{"type", json(component.type(), ns, mode)}};
190190
members.push_back(std::move(e));
191191
}
192192
}
@@ -348,8 +348,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
348348

349349
forall_operands(it, expr)
350350
{
351-
json_objectt e({{"index", json_numbert(std::to_string(index))},
352-
{"value", json(*it, ns, mode)}});
351+
json_objectt e{{"index", json_numbert(std::to_string(index))},
352+
{"value", json(*it, ns, mode)}};
353353
elements.push_back(std::move(e));
354354
index++;
355355
}
@@ -370,8 +370,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
370370
json_arrayt &members = result["members"].make_array();
371371
for(std::size_t m = 0; m < expr.operands().size(); m++)
372372
{
373-
json_objectt e({{"value", json(expr.operands()[m], ns, mode)},
374-
{"name", json_stringt(components[m].get_name())}});
373+
json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
374+
{"name", json_stringt(components[m].get_name())}};
375375
members.push_back(std::move(e));
376376
}
377377
}

‎src/goto-programs/show_goto_functions_json.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -70,8 +70,8 @@ json_objectt show_goto_functions_jsont::convert(
7070
for(const goto_programt::instructiont &instruction :
7171
function.body.instructions)
7272
{
73-
json_objectt instruction_entry(
74-
{{"instructionId", json_stringt(instruction.to_string())}});
73+
json_objectt instruction_entry{
74+
{"instructionId", json_stringt(instruction.to_string())}};
7575

7676
if(instruction.code.source_location().is_not_nil())
7777
{

‎src/goto-programs/show_properties.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -129,12 +129,12 @@ void convert_properties_json(
129129

130130
irep_idt property_id=source_location.get_property_id();
131131

132-
json_objectt json_property(
133-
{{"name", json_stringt(property_id)},
134-
{"class", json_stringt(property_class)},
135-
{"sourceLocation", json(source_location)},
136-
{"description", json_stringt(description)},
137-
{"expression", json_stringt(from_expr(ns, identifier, ins.guard))}});
132+
json_objectt json_property{
133+
{"name", json_stringt(property_id)},
134+
{"class", json_stringt(property_class)},
135+
{"sourceLocation", json(source_location)},
136+
{"description", json_stringt(description)},
137+
{"expression", json_stringt(from_expr(ns, identifier, ins.guard))}};
138138

139139
if(!source_location.get_basic_block_covered_lines().empty())
140140
json_property["coveredLines"] =
@@ -155,7 +155,7 @@ void show_properties_json(
155155
for(const auto &fct : goto_functions.function_map)
156156
convert_properties_json(json_properties, ns, fct.first, fct.second.body);
157157

158-
json_objectt json_result({{"properties", json_properties}});
158+
json_objectt json_result{{"properties", json_properties}};
159159
msg.result() << json_result;
160160
}
161161

0 commit comments

Comments
 (0)