Skip to content

Commit 8d65dba

Browse files
committed
Refactor static_verifier_json using range
This commit is included in this PR, as a demonstration of the coding style which is enabled by the proceeding commits.
1 parent ada9d27 commit 8d65dba

File tree

1 file changed

+26
-31
lines changed

1 file changed

+26
-31
lines changed

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 std::string 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(

0 commit comments

Comments
 (0)