Skip to content

Commit 5777e16

Browse files
committed
Make JSON output of goto functions complete
We must include all information required to re-produce a goto program from its JSON representation.
1 parent a36793a commit 5777e16

File tree

1 file changed

+39
-13
lines changed

1 file changed

+39
-13
lines changed

src/goto-programs/show_goto_functions_json.cpp

Lines changed: 39 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,14 @@ json_objectt show_goto_functions_jsont::convert(
4848
function_name.starts_with("java::org.cprover") ||
4949
function_name.starts_with("java::java");
5050
json_function["isInternal"]=jsont::json_boolean(is_internal);
51+
json_function["isHidden"] = jsont::json_boolean(function.is_hidden());
52+
auto json_parameter_id_range =
53+
make_range(
54+
function.parameter_identifiers.begin(),
55+
function.parameter_identifiers.end())
56+
.map([](const irep_idt &id) { return json_stringt{id}; });
57+
json_function["parameterIdentifiers"] = json_arrayt{
58+
json_parameter_id_range.begin(), json_parameter_id_range.end()};
5159

5260
if(list_only)
5361
continue;
@@ -60,12 +68,14 @@ json_objectt show_goto_functions_jsont::convert(
6068
function.body.instructions)
6169
{
6270
json_objectt instruction_entry{
63-
{"instructionId", json_stringt(instruction.to_string())}};
71+
{"instructionId", json_stringt(instruction.to_string())},
72+
{"locationNumber",
73+
json_numbert{std::to_string(instruction.location_number)}}};
6474

65-
if(instruction.code().source_location().is_not_nil())
75+
if(instruction.source_location().is_not_nil())
6676
{
6777
instruction_entry["sourceLocation"] =
68-
json(instruction.code().source_location());
78+
json(instruction.source_location());
6979
}
7080

7181
std::ostringstream instruction_builder;
@@ -74,17 +84,12 @@ json_objectt show_goto_functions_jsont::convert(
7484
instruction_entry["instruction"]=
7585
json_stringt(instruction_builder.str());
7686

77-
if(!instruction.code().operands().empty())
87+
if(instruction.code().is_not_nil())
7888
{
79-
json_arrayt operand_array;
80-
for(const exprt &operand : instruction.code().operands())
81-
{
82-
json_objectt operand_object=
83-
no_comments_irep_converter.convert_from_irep(
84-
operand);
85-
operand_array.push_back(operand_object);
86-
}
87-
instruction_entry["operands"] = std::move(operand_array);
89+
json_objectt code_object =
90+
no_comments_irep_converter.convert_from_irep(instruction.code());
91+
92+
instruction_entry["code"] = std::move(code_object);
8893
}
8994

9095
if(instruction.has_condition())
@@ -96,6 +101,27 @@ json_objectt show_goto_functions_jsont::convert(
96101
instruction_entry["guard"] = std::move(guard_object);
97102
}
98103

104+
if(!instruction.targets.empty())
105+
{
106+
auto json_target_range =
107+
make_range(instruction.targets.begin(), instruction.targets.end())
108+
.map(
109+
[](const goto_programt::targett &target) {
110+
return json_numbert{std::to_string(target->location_number)};
111+
});
112+
instruction_entry["targets"] =
113+
json_arrayt{json_target_range.begin(), json_target_range.end()};
114+
}
115+
116+
if(!instruction.labels.empty())
117+
{
118+
auto json_label_range =
119+
make_range(instruction.labels.begin(), instruction.labels.end())
120+
.map([](const irep_idt &id) { return json_stringt{id}; });
121+
instruction_entry["labels"] =
122+
json_arrayt{json_label_range.begin(), json_label_range.end()};
123+
}
124+
99125
json_instruction_array.push_back(std::move(instruction_entry));
100126
}
101127

0 commit comments

Comments
 (0)