CBMC
json_stream.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
9 #include "json_stream.h"
10 
11 #include <ostream>
12 
15 {
16  if(!first)
17  out << ',';
18  else
19  first = false;
20  out << '\n';
21  out << std::string((indent + 1) * 2, ' ');
22 }
23 
27 json_stream_arrayt::json_stream_arrayt(std::ostream &out, unsigned indent)
28  : json_streamt(out, indent)
29 {
30  out << '[';
31 }
32 
35 {
36  if(!object.empty())
37  {
39  object["array_element"].output_rec(out, indent + 1);
40  object.clear();
41  }
42  if(child_stream)
43  {
44  child_stream->close();
45  child_stream = nullptr;
46  }
47 }
48 
51 {
52  out << '\n' << std::string(indent * 2, ' ');
53  out << ']';
54 }
55 
59 json_stream_objectt::json_stream_objectt(std::ostream &out, unsigned indent)
60  : json_streamt(out, indent)
61 {
62  out << '{';
63 }
64 
67 {
68  child_stream =
69  std::unique_ptr<json_streamt>(new json_stream_arrayt(out, indent + 1));
70  return static_cast<json_stream_arrayt &>(*child_stream);
71 }
72 
75 {
76  child_stream =
77  std::unique_ptr<json_streamt>(new json_stream_objectt(out, indent + 1));
78  return static_cast<json_stream_objectt &>(*child_stream);
79 }
80 
83 {
85  // To ensure consistency of the output, we flush and
86  // close the current child stream before creating the new one.
90 }
91 
94 {
96  // To ensure consistency of the output, we flush and
97  // close the current child stream before creating the new one.
100  return create_child_stream_array();
101 }
102 
107 {
109  // To ensure consistency of the output, we flush and
110  // close the current child stream before creating the new one.
113  jsont::output_key(out, key);
115 }
116 
121 {
123  // To ensure consistency of the output, we flush and
124  // close the current child stream before creating the new one.
127  jsont::output_key(out, key);
128  return create_child_stream_array();
129 }
130 
134 {
135  for(const auto &obj : object)
136  {
138  jsont::output_key(out, obj.first);
139  obj.second.output_rec(out, indent + 1);
140  }
141  object.clear();
142  if(child_stream)
143  {
144  child_stream->close();
145  child_stream = nullptr;
146  }
147 }
148 
151 {
152  jsont::output_object(out, object, indent);
153  out << '\n' << std::string(indent * 2, ' ');
154  out << '}';
155 }
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
json_stream_arrayt & push_back_stream_array()
Add a JSON array child stream.
Definition: json_stream.cpp:93
void output_finalizer() override
Output the finalizing character for a JSON array.
Definition: json_stream.cpp:50
void output_child_stream() override
Output the non-streaming JSON objects and closes the current child stream.
Definition: json_stream.cpp:34
json_stream_arrayt(std::ostream &out, unsigned indent=0)
Construct a new JSON array stream.
Definition: json_stream.cpp:27
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
void output_finalizer() override
Output the finalizing character for a JSON object.
json_stream_objectt & push_back_stream_object(const std::string &key)
Add a JSON object stream for a specific key.
void output_child_stream() override
Output non-streaming JSON properties and flushes and closes the child stream.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
json_stream_objectt(std::ostream &out, unsigned indent=0)
Constructor for json_stream_objectt.
Definition: json_stream.cpp:59
This class provides a facility for streaming JSON objects directly to the output instead of waiting f...
Definition: json_stream.h:37
json_stream_arrayt & create_child_stream_array()
Create a new JSON array child stream.
Definition: json_stream.cpp:66
json_stream_objectt & create_child_stream_object()
Create a new JSON object child stream.
Definition: json_stream.cpp:74
bool first
Is the current element the first element in the object or array? This is required to know whether a d...
Definition: json_stream.h:68
bool open
Denotes whether the current stream is open or has been invalidated.
Definition: json_stream.h:62
void output_delimiter()
Outputs the delimiter between JSON elements.
Definition: json_stream.cpp:14
unsigned indent
Definition: json_stream.h:64
std::ostream & out
Definition: json_stream.h:63
std::unique_ptr< json_streamt > child_stream
The current child stream.
Definition: json_stream.h:79
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:154
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:463