CBMC
json_stream.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_JSON_STREAM_H
10 #define CPROVER_UTIL_JSON_STREAM_H
11 
12 #include <iosfwd>
13 #include <memory>
14 
15 #include "json.h"
16 #include "invariant.h"
17 
19 class json_stream_arrayt;
20 
37 {
38 public:
40  void close()
41  {
42  if(open)
43  {
46  open = false;
47  }
48  }
49 
50  virtual ~json_streamt() = default;
51 
52 protected:
56  json_streamt(std::ostream &_out, unsigned _indent)
57  : open(true), out(_out), indent(_indent), first(true), child_stream(nullptr)
58  {
59  }
60 
62  bool open;
63  std::ostream &out;
64  unsigned indent;
65 
68  bool first;
69 
72  typedef std::map<std::string, jsont> objectt;
74 
79  std::unique_ptr<json_streamt> child_stream;
82 
84  void output_delimiter();
85 
86  // To be overridden by derived classes:
87  virtual void output_child_stream() = 0;
88  virtual void output_finalizer() = 0;
89 };
90 
93 {
94 public:
95  explicit json_stream_arrayt(std::ostream &out, unsigned indent = 0);
96 
99  {
100  close();
101  }
102 
106  void push_back(const jsont &json)
107  {
109  // To ensure consistency of the output, we flush and
110  // close the current child stream before printing the given element.
113  json.output_rec(out, indent + 1);
114  }
115 
121  {
123  // To ensure consistency of the output, we flush and
124  // close the current child stream before adding the given element.
126  // We store the new element in the object map.
127  return object["array_element"];
128  }
129 
132 
133 protected:
134  void output_child_stream() override;
135  void output_finalizer() override;
136 };
137 
140 {
141 public:
142  explicit json_stream_objectt(std::ostream &out, unsigned indent = 0);
143 
148  jsont &operator[](const std::string &key)
149  {
150  return object[key];
151  }
152 
154  {
155  close();
156  }
157 
163  const jsont &operator[](const std::string &key) const
164  {
165  objectt::const_iterator it = object.find(key);
166  if(it == object.end())
168  else
169  return it->second;
170  }
171 
178  void push_back(const std::string &key, const jsont &json)
179  {
181  // Check the key is not already due to be output later:
182  PRECONDITION(!object.count(key));
183  // To ensure consistency of the output, we flush and
184  // close the current child stream before printing the given element.
187  jsont::output_key(out, key);
188  json.output_rec(out, indent + 1);
189  }
190 
191  json_stream_objectt &push_back_stream_object(const std::string &key);
192  json_stream_arrayt &push_back_stream_array(const std::string &key);
193 
194 protected:
195  void output_child_stream() override;
196  void output_finalizer() override;
197 };
198 
199 #endif // CPROVER_UTIL_JSON_STREAM_H
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
jsont & push_back()
Push back and return a new non-streaming JSON element into the current array stream.
Definition: json_stream.h:120
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
~json_stream_arrayt() override
Flushes and closes the stream on destruction.
Definition: json_stream.h:98
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
const jsont & operator[](const std::string &key) const
Lookup the key of a non-streaming JSON element.
Definition: json_stream.h:163
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
Definition: json_stream.h:178
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.
jsont & operator[](const std::string &key)
Provide key-value lookup capabilities for the JSON object.
Definition: json_stream.h:148
~json_stream_objectt() override
Definition: json_stream.h:153
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
virtual void output_child_stream()=0
void close()
Outputs the current current child stream and closes this JSON stream.
Definition: json_stream.h:40
json_stream_objectt & create_child_stream_object()
Create a new JSON object child stream.
Definition: json_stream.cpp:74
virtual void output_finalizer()=0
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
std::map< std::string, jsont > objectt
Non-streaming JSON elements These will be printed when closing the stream or creating a child stream.
Definition: json_stream.h:72
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
virtual ~json_streamt()=default
json_streamt(std::ostream &_out, unsigned _indent)
Constructor to be used by derived classes.
Definition: json_stream.h:56
std::ostream & out
Definition: json_stream.h:63
std::unique_ptr< json_streamt > child_stream
The current child stream.
Definition: json_stream.h:79
Definition: json.h:27
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:154
static const jsont null_json_object
Definition: json.h:125
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
#define PRECONDITION(CONDITION)
Definition: invariant.h:463