Skip to content

Commit 48b9ce6

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

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

src/goto-checker/cover_goals_report_util.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,17 +90,21 @@ 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
}
105109
json_result["totalGoals"] = json_numbert(std::to_string(properties.size()));
106110
const std::size_t goals_covered =

0 commit comments

Comments
 (0)