CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
json_stream.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
27json_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
59json_stream_objectt::json_stream_objectt(std::ostream &out, unsigned indent)
60 : json_streamt(out, indent)
61{
62 out << '{';
63}
64
67{
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{
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.
101}
102
107{
109 // To ensure consistency of the output, we flush and
110 // close the current child stream before creating the new one.
115}
116
121{
123 // To ensure consistency of the output, we flush and
124 // close the current child stream before creating the new one.
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{
153 out << '\n' << std::string(indent * 2, ' ');
154 out << '}';
155}
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Provides methods for streaming JSON arrays.
Definition json_stream.h:93
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
json_stream_arrayt & push_back_stream_array()
Add a JSON array child stream.
void output_finalizer() override
Output the finalizing character for a JSON array.
void output_child_stream() override
Output the non-streaming JSON objects and closes the current child stream.
json_stream_arrayt(std::ostream &out, unsigned indent=0)
Construct a new JSON array stream.
Provides methods for streaming JSON objects.
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.
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.
json_stream_objectt & create_child_stream_object()
Create a new JSON object child stream.
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
objectt object
Definition json_stream.h:73
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.
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