From a975df7255e92757951e34eafb4e9aeda097e3b8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 16 Feb 2019 22:09:37 +0000 Subject: [PATCH 1/2] Fix JSON goals output This was already broken in bmc_cover. --- src/goto-checker/cover_goals_report_util.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/goto-checker/cover_goals_report_util.cpp b/src/goto-checker/cover_goals_report_util.cpp index 4804dfbada3..42df1b503a6 100644 --- a/src/goto-checker/cover_goals_report_util.cpp +++ b/src/goto-checker/cover_goals_report_util.cpp @@ -90,22 +90,28 @@ static void output_goals_json( log.status() << messaget::eom; // force end of previous message json_stream_objectt &json_result = ui_message_handler.get_json_stream().push_back_stream_object(); + json_stream_arrayt &goals_array = json_result.push_back_stream_array("goals"); for(const auto &property_pair : properties) { const property_infot &property_info = property_pair.second; - json_result["status"] = json_stringt( + json_objectt json_goal; + json_goal["status"] = json_stringt( property_info.status == property_statust::FAIL ? "satisfied" : "failed"); - json_result["goal"] = json_stringt(property_pair.first); - json_result["description"] = json_stringt(property_info.description); + json_goal["goal"] = json_stringt(property_pair.first); + json_goal["description"] = json_stringt(property_info.description); if(property_info.pc->source_location.is_not_nil()) - json_result["sourceLocation"] = json(property_info.pc->source_location); + json_goal["sourceLocation"] = json(property_info.pc->source_location); + + goals_array.push_back(std::move(json_goal)); } - json_result["totalGoals"] = json_numbert(std::to_string(properties.size())); const std::size_t goals_covered = count_properties(properties, property_statust::FAIL); - json_result["goalsCovered"] = json_numbert(std::to_string(goals_covered)); + json_result.push_back( + "goalsCovered", json_numbert(std::to_string(goals_covered))); + json_result.push_back( + "totalGoals", json_numbert(std::to_string(properties.size()))); } void output_goals( From e25a085cbda0213310ae086ff0183ad1bec5e0c0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 19 Feb 2019 21:06:11 +0000 Subject: [PATCH 2/2] Add regression test for JSON goals output Goals need to be in an array and the summary counts must be outside the array. --- regression/cbmc-cover/json-goals1/main.c | 6 ++++++ regression/cbmc-cover/json-goals1/test.desc | 9 +++++++++ 2 files changed, 15 insertions(+) create mode 100644 regression/cbmc-cover/json-goals1/main.c create mode 100644 regression/cbmc-cover/json-goals1/test.desc diff --git a/regression/cbmc-cover/json-goals1/main.c b/regression/cbmc-cover/json-goals1/main.c new file mode 100644 index 00000000000..39913b51897 --- /dev/null +++ b/regression/cbmc-cover/json-goals1/main.c @@ -0,0 +1,6 @@ +int main(int argc, char **argv) +{ + if(argc == 42) + return 0; + return 1; +} diff --git a/regression/cbmc-cover/json-goals1/test.desc b/regression/cbmc-cover/json-goals1/test.desc new file mode 100644 index 00000000000..fbbb638fb2e --- /dev/null +++ b/regression/cbmc-cover/json-goals1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--json-ui --cover location +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +\{\n\s*"goals": \[\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\} +-- +^warning: ignoring