cprover
json.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "json.h"
10 
11 #include <algorithm>
12 #include <ostream>
13 
15 
16 void jsont::escape_string(const std::string &src, std::ostream &out)
17 {
18  for(const auto &ch : src)
19  {
20  switch(ch)
21  {
22  case '\\':
23  case '"':
24  out << '\\';
25  out << ch;
26  break;
27 
28  case '\b':
29  out << "\\b";
30  break;
31 
32  case '\f':
33  out << "\\f";
34  break;
35 
36  case '\n':
37  out << "\\n";
38  break;
39 
40  case '\r':
41  out << "\\r";
42  break;
43 
44  case '\t':
45  out << "\\t";
46  break;
47 
48  default:
49  out << ch;
50  }
51  }
52 }
53 
57 void jsont::output_rec(std::ostream &out, unsigned indent) const
58 {
59  switch(kind)
60  {
61  case kindt::J_STRING:
62  out << '"';
63  escape_string(value, out);
64  out << '"';
65  break;
66 
67  case kindt::J_NUMBER:
68  out << value;
69  break;
70 
71  case kindt::J_OBJECT:
72  out << '{';
73  output_object(out, object, indent);
74  if(!object.empty())
75  {
76  out << '\n';
77  out << std::string(indent*2, ' ');
78  }
79  out << '}';
80  break;
81 
82  case kindt::J_ARRAY:
83  out << '[';
84 
85  if(array.empty())
86  out << ' ';
87  else
88  {
89  for(arrayt::const_iterator a_it=array.begin();
90  a_it!=array.end();
91  a_it++)
92  {
93  if(a_it!=array.begin())
94  out << ',';
95 
96  if(a_it->is_object())
97  {
98  out << '\n';
99  out << std::string((indent+1)*2, ' ');
100  }
101  else
102  out << ' ';
103 
104  a_it->output_rec(out, indent+1);
105  }
106 
107  if(array.back().is_object())
108  out << '\n' << std::string(indent*2, ' ');
109  else
110  out << ' ';
111  }
112 
113  out << ']';
114  break;
115 
116  case kindt::J_TRUE: out << "true"; break;
117 
118  case kindt::J_FALSE: out << "false"; break;
119 
120  case kindt::J_NULL: out << "null"; break;
121  }
122 }
123 
131  std::ostream &out,
132  const objectt &object,
133  unsigned indent)
134 {
135  for(objectt::const_iterator o_it = object.begin(); o_it != object.end();
136  o_it++)
137  {
138  if(o_it != object.begin())
139  out << ',';
140 
141  // A JSON object always starts with an opening brace,
142  // after which we put a newline.
143  out << '\n';
144 
145  out << std::string((indent + 1) * 2, ' ');
146 
147  jsont::output_key(out, o_it->first);
148  o_it->second.output_rec(out, indent + 1);
149  }
150 }
151 
152 void jsont::output_key(std::ostream &out, const std::string &key)
153 {
154  out << '"';
155  jsont::escape_string(key, out);
156  out << "\": ";
157 }
158 
159 void jsont::swap(jsont &other)
160 {
161  std::swap(other.kind, kind);
162  other.array.swap(array);
163  other.object.swap(object);
164  other.value.swap(value);
165 }
166 
167 bool operator==(const jsont &left, const jsont &right)
168 {
169  if(left.kind != right.kind)
170  return false;
171  switch(left.kind)
172  {
174  return true;
176  return true;
178  return true;
180  return left.value == right.value;
182  return left.value == right.value;
184  {
185  const auto &left_array = static_cast<const json_arrayt &>(left);
186  const auto &right_array = static_cast<const json_arrayt &>(right);
187  return left_array.size() == right_array.size() &&
188  std::equal(
189  left_array.begin(), left_array.end(), right_array.begin());
190  }
192  {
193  const auto &left_object = static_cast<const json_objectt &>(left);
194  const auto &right_object = static_cast<const json_objectt &>(right);
195  if(left_object.size() != left_object.size())
196  return false;
197  return std::all_of(
198  left_object.begin(),
199  left_object.end(),
200  [&](const std::pair<std::string, jsont> &pair) {
201  return right_object[pair.first] == pair.second;
202  });
203  }
204  }
205  UNREACHABLE;
206 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
jsont::object
objectt object
Definition: json.h:134
jsont::kindt::J_FALSE
@ J_FALSE
operator==
bool operator==(const jsont &left, const jsont &right)
Definition: json.cpp:167
jsont::null_json_object
static const jsont null_json_object
Definition: json.h:123
jsont::escape_string
static void escape_string(const std::string &, std::ostream &)
Definition: json.cpp:16
jsont
Definition: json.h:25
jsont::kindt::J_ARRAY
@ J_ARRAY
jsont::kindt::J_NUMBER
@ J_NUMBER
json_arrayt
Definition: json.h:163
jsont::kindt::J_OBJECT
@ J_OBJECT
json_objectt
Definition: json.h:298
jsont::output_rec
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition: json.cpp:57
jsont::kindt::J_STRING
@ J_STRING
jsont::kindt::J_TRUE
@ J_TRUE
jsont::swap
void swap(jsont &other)
Definition: json.cpp:159
jsont::objectt
std::map< std::string, jsont > objectt
Definition: json.h:28
jsont::output_object
static void output_object(std::ostream &out, const objectt &object, unsigned indent)
Basic handling of the printing of a JSON object.
Definition: json.cpp:130
jsont::kindt::J_NULL
@ J_NULL
json_arrayt::size
std::size_t size() const
Definition: json.h:200
jsont::array
arrayt array
Definition: json.h:133
json.h
jsont::kind
kindt kind
Definition: json.h:42
jsont::output_key
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:152
jsont::value
std::string value
Definition: json.h:130