CBMC
Loading...
Searching...
No Matches
json.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "json.h"
10
11#include "structured_data.h"
12
13#include <algorithm>
14#include <ostream>
15
17
18void jsont::escape_string(const std::string &src, std::ostream &out)
19{
20 for(const auto &ch : src)
21 {
22 switch(ch)
23 {
24 case '\\':
25 case '"':
26 out << '\\';
27 out << ch;
28 break;
29
30 case '\b':
31 out << "\\b";
32 break;
33
34 case '\f':
35 out << "\\f";
36 break;
37
38 case '\n':
39 out << "\\n";
40 break;
41
42 case '\r':
43 out << "\\r";
44 break;
45
46 case '\t':
47 out << "\\t";
48 break;
49
50 default:
51 out << ch;
52 }
53 }
54}
55
59void jsont::output_rec(std::ostream &out, unsigned indent) const
60{
61 switch(kind)
62 {
63 case kindt::J_STRING:
64 out << '"';
65 escape_string(value, out);
66 out << '"';
67 break;
68
69 case kindt::J_NUMBER:
70 out << value;
71 break;
72
73 case kindt::J_OBJECT:
74 out << '{';
75 output_object(out, object, indent);
76 if(!object.empty())
77 {
78 out << '\n';
79 out << std::string(indent*2, ' ');
80 }
81 out << '}';
82 break;
83
84 case kindt::J_ARRAY:
85 out << '[';
86
87 if(array.empty())
88 out << ' ';
89 else
90 {
91 for(arrayt::const_iterator a_it=array.begin();
92 a_it!=array.end();
93 a_it++)
94 {
95 if(a_it!=array.begin())
96 out << ',';
97
98 if(a_it->is_object())
99 {
100 out << '\n';
101 out << std::string((indent+1)*2, ' ');
102 }
103 else
104 out << ' ';
105
106 a_it->output_rec(out, indent+1);
107 }
108
109 if(array.back().is_object())
110 out << '\n' << std::string(indent*2, ' ');
111 else
112 out << ' ';
113 }
114
115 out << ']';
116 break;
117
118 case kindt::J_TRUE: out << "true"; break;
119
120 case kindt::J_FALSE: out << "false"; break;
121
122 case kindt::J_NULL: out << "null"; break;
123 }
124}
125
133 std::ostream &out,
134 const objectt &object,
135 unsigned indent)
136{
137 for(objectt::const_iterator o_it = object.begin(); o_it != object.end();
138 o_it++)
139 {
140 if(o_it != object.begin())
141 out << ',';
142
143 // A JSON object always starts with an opening brace,
144 // after which we put a newline.
145 out << '\n';
146
147 out << std::string((indent + 1) * 2, ' ');
148
149 jsont::output_key(out, o_it->first);
150 o_it->second.output_rec(out, indent + 1);
151 }
152}
153
154void jsont::output_key(std::ostream &out, const std::string &key)
155{
156 out << '"';
158 out << "\": ";
159}
160
161void jsont::swap(jsont &other)
162{
163 std::swap(other.kind, kind);
164 other.array.swap(array);
165 other.object.swap(object);
166 other.value.swap(value);
167}
168
169bool operator==(const jsont &left, const jsont &right)
170{
171 if(left.kind != right.kind)
172 return false;
173 switch(left.kind)
174 {
176 return true;
178 return true;
180 return true;
182 return left.value == right.value;
184 return left.value == right.value;
186 {
187 const auto &left_array = static_cast<const json_arrayt &>(left);
188 const auto &right_array = static_cast<const json_arrayt &>(right);
189 return left_array.size() == right_array.size() &&
190 std::equal(
191 left_array.begin(), left_array.end(), right_array.begin());
192 }
194 {
195 const auto &left_object = static_cast<const json_objectt &>(left);
196 const auto &right_object = static_cast<const json_objectt &>(right);
197 if(left_object.size() != left_object.size())
198 return false;
199 return std::all_of(
200 left_object.begin(),
201 left_object.end(),
202 [&](const std::pair<std::string, jsont> &pair) {
203 return right_object[pair.first] == pair.second;
204 });
205 }
206 }
208}
209
211{
212 if(entry.is_leaf())
213 return entry.leaf_object();
214 else
215 {
216 json_objectt result;
217 for(const auto &sub_entry : entry.children())
218 {
219 result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
220 }
221 return std::move(result);
222 }
223}
224
226{
227 if(data.data().size() == 0)
228 return jsont{};
229
230 json_objectt result;
231 for(const auto &sub_entry : data.data())
232 {
233 result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
234 }
235 return std::move(result);
236}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Definition json.h:27
arrayt array
Definition json.h:135
static void escape_string(const std::string &, std::ostream &)
Definition json.cpp:18
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition json.cpp:59
void swap(jsont &other)
Definition json.cpp:161
static void output_key(std::ostream &out, const std::string &key)
Definition json.cpp:154
std::string value
Definition json.h:132
std::map< std::string, jsont > objectt
Definition json.h:30
static const jsont null_json_object
Definition json.h:125
kindt kind
Definition json.h:44
static void output_object(std::ostream &out, const objectt &object, unsigned indent)
Basic handling of the printing of a JSON object.
Definition json.cpp:132
objectt object
Definition json.h:136
A way of representing nested key/value data.
const std::map< labelt, structured_data_entryt > & data() const
jsont to_json(const structured_datat &data)
Convert the structured_datat into an json object.
Definition json.cpp:225
bool operator==(const jsont &left, const jsont &right)
Definition json.cpp:169
jsont json_node(const structured_data_entryt &entry)
Definition json.cpp:210
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
const std::map< labelt, structured_data_entryt > & children() const