This class provides a facility for streaming JSON objects directly to the output instead of waiting for the object to be fully formed in memory and then print it (as done using jsont).
More...
#include <json_stream.h>
Inheritance diagram for json_streamt: Collaboration diagram for json_streamt:Public Member Functions | |
| void | close () |
| Outputs the current current child stream and closes this JSON stream. More... | |
| virtual | ~json_streamt ()=default |
Protected Types | |
| typedef std::map< std::string, jsont > | objectt |
| Non-streaming JSON elements These will be printed when closing the stream or creating a child stream. More... | |
Protected Member Functions | |
| json_streamt (std::ostream &_out, unsigned _indent) | |
| Constructor to be used by derived classes. More... | |
| json_stream_arrayt & | create_child_stream_array () |
| Create a new JSON array child stream. More... | |
| json_stream_objectt & | create_child_stream_object () |
| Create a new JSON object child stream. More... | |
| void | output_delimiter () |
| Outputs the delimiter between JSON elements. More... | |
| virtual void | output_child_stream ()=0 |
| virtual void | output_finalizer ()=0 |
Protected Attributes | |
| bool | open |
| Denotes whether the current stream is open or has been invalidated. More... | |
| std::ostream & | out |
| unsigned | indent |
| bool | first |
| Is the current element the first element in the object or array? This is required to know whether a delimiter must be output or not. More... | |
| objectt | object |
| std::unique_ptr< json_streamt > | child_stream |
| The current child stream. More... | |
Detailed Description
This class provides a facility for streaming JSON objects directly to the output instead of waiting for the object to be fully formed in memory and then print it (as done using jsont).
This reduces memory consumption when preparing e.g. large traces for output.
json_streamt is the base class from which the classes for streaming arrays (json_stream_arrayt) and objects (json_stream_objectt) are derived. json_streamt wraps an output stream and stores the current element to be output. This can be either a child stream (of type json_streamt that outputs JSON objects incrementally) or a non-streaming JSON object (of type jsont that will be output as a whole) To ensure consistency of the output, a class invariant is that there is at most one child stream at any time. For this reason, the existing child stream is flushed and closed when creating a new child stream.
Definition at line 36 of file json_stream.h.
Member Typedef Documentation
◆ objectt
|
protected |
Non-streaming JSON elements These will be printed when closing the stream or creating a child stream.
Definition at line 72 of file json_stream.h.
Constructor & Destructor Documentation
◆ ~json_streamt()
|
virtualdefault |
◆ json_streamt()
|
inlineprotected |
Constructor to be used by derived classes.
- Parameters
-
_out output stream _indent indentation level
Definition at line 56 of file json_stream.h.
Member Function Documentation
◆ close()
|
inline |
Outputs the current current child stream and closes this JSON stream.
Definition at line 40 of file json_stream.h.
◆ create_child_stream_array()
|
protected |
Create a new JSON array child stream.
Definition at line 66 of file json_stream.cpp.
◆ create_child_stream_object()
|
protected |
Create a new JSON object child stream.
Definition at line 74 of file json_stream.cpp.
◆ output_child_stream()
|
protectedpure virtual |
Implemented in json_stream_objectt, and json_stream_arrayt.
◆ output_delimiter()
|
protected |
Outputs the delimiter between JSON elements.
Output the element delimiter to the output stream.
Definition at line 14 of file json_stream.cpp.
◆ output_finalizer()
|
protectedpure virtual |
Implemented in json_stream_objectt, and json_stream_arrayt.
Member Data Documentation
◆ child_stream
|
protected |
The current child stream.
One can create and close many child streams sequentially (timewise), e.g. for each element in an array or each property in an object. The invariant is that there can only be at most child one stream at a time.
Definition at line 79 of file json_stream.h.
◆ first
|
protected |
Is the current element the first element in the object or array? This is required to know whether a delimiter must be output or not.
Definition at line 68 of file json_stream.h.
◆ indent
|
protected |
Definition at line 64 of file json_stream.h.
◆ object
|
protected |
Definition at line 73 of file json_stream.h.
◆ open
|
protected |
Denotes whether the current stream is open or has been invalidated.
Definition at line 62 of file json_stream.h.
◆ out
|
protected |
Definition at line 63 of file json_stream.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/util/json_stream.h
- /home/runner/work/cbmc/cbmc/src/util/json_stream.cpp
