Skip to content

Commit d5e12be

Browse files
Fix JSON goals output
This was already broken in bmc_cover.
1 parent 79ea945 commit d5e12be

File tree

1 file changed

+12
-6
lines changed

1 file changed

+12
-6
lines changed

src/goto-checker/cover_goals_report_util.cpp

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -90,22 +90,28 @@ static void output_goals_json(
9090
log.status() << messaget::eom; // force end of previous message
9191
json_stream_objectt &json_result =
9292
ui_message_handler.get_json_stream().push_back_stream_object();
93+
json_stream_arrayt &goals_array = json_result.push_back_stream_array("goals");
9394
for(const auto &property_pair : properties)
9495
{
9596
const property_infot &property_info = property_pair.second;
9697

97-
json_result["status"] = json_stringt(
98+
json_objectt json_goal;
99+
json_goal["status"] = json_stringt(
98100
property_info.status == property_statust::FAIL ? "satisfied" : "failed");
99-
json_result["goal"] = json_stringt(property_pair.first);
100-
json_result["description"] = json_stringt(property_info.description);
101+
json_goal["goal"] = json_stringt(property_pair.first);
102+
json_goal["description"] = json_stringt(property_info.description);
101103

102104
if(property_info.pc->source_location.is_not_nil())
103-
json_result["sourceLocation"] = json(property_info.pc->source_location);
105+
json_goal["sourceLocation"] = json(property_info.pc->source_location);
106+
107+
goals_array.push_back(std::move(json_goal));
104108
}
105-
json_result["totalGoals"] = json_numbert(std::to_string(properties.size()));
106109
const std::size_t goals_covered =
107110
count_properties(properties, property_statust::FAIL);
108-
json_result["goalsCovered"] = json_numbert(std::to_string(goals_covered));
111+
json_result.push_back(
112+
"goalsCovered", json_numbert(std::to_string(goals_covered)));
113+
json_result.push_back(
114+
"totalGoals", json_numbert(std::to_string(properties.size())));
109115
}
110116

111117
void output_goals(

0 commit comments

Comments
 (0)