|
16 | 16 | #include <goto-programs/goto_model.h>
|
17 | 17 |
|
18 | 18 | #include <analyses/ai.h>
|
| 19 | +#include <util/range.h> |
19 | 20 |
|
20 | 21 | struct static_verifier_resultt
|
21 | 22 | {
|
22 | 23 | // clang-format off
|
23 |
| - enum { TRUE, FALSE, BOTTOM, UNKNOWN } status; |
| 24 | + enum statust { TRUE, FALSE, BOTTOM, UNKNOWN } status; |
24 | 25 | // clang-format on
|
25 | 26 | source_locationt source_location;
|
26 | 27 | irep_idt function_id;
|
27 | 28 | };
|
28 | 29 |
|
| 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 | + |
29 | 47 | static void static_verifier_json(
|
30 | 48 | const std::vector<static_verifier_resultt> &results,
|
31 | 49 | messaget &m,
|
32 | 50 | std::ostream &out)
|
33 | 51 | {
|
34 | 52 | 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>(); |
65 | 60 | }
|
66 | 61 |
|
67 | 62 | static void static_verifier_xml(
|
|
0 commit comments