9 #ifndef CPROVER_UTIL_JSON_STREAM_H 10 #define CPROVER_UTIL_JSON_STREAM_H 72 typedef std::map<std::string, jsont>
objectt;
127 return object[
"array_element"];
165 objectt::const_iterator it =
object.find(key);
166 if(it ==
object.end())
199 #endif // CPROVER_UTIL_JSON_STREAM_H
json_streamt(std::ostream &_out, unsigned _indent)
Constructor to be used by derived classes.
void close()
Outputs the current current child stream and closes this JSON stream.
Provides methods for streaming JSON objects.
static void output_key(std::ostream &out, const std::string &key)
json_stream_arrayt(std::ostream &out, unsigned indent=0)
Construct a new JSON array stream.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
json_stream_objectt & create_child_stream_object()
Create a new JSON object child stream.
json_stream_objectt(std::ostream &out, unsigned indent=0)
Constructor for json_stream_objectt.
jsont & operator[](const std::string &key)
Provide key-value lookup capabilities for the JSON object.
This class provides a facility for streaming JSON objects directly to the output instead of waiting f...
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
json_stream_arrayt & push_back_stream_array()
Add a JSON array child stream.
void output_finalizer() override
Output the finalizing character for a JSON object.
bool first
Is the current element the first element in the object or array? This is required to know whether a d...
bool open
Denotes whether the current stream is open or has been invalidated.
void output_child_stream() override
Output the non-streaming JSON objects and closes the current child stream.
json_stream_arrayt & create_child_stream_array()
Create a new JSON array child stream.
std::unique_ptr< json_streamt > child_stream
The current child stream.
Provides methods for streaming JSON arrays.
#define PRECONDITION(CONDITION)
virtual void output_child_stream()=0
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
json_stream_objectt & push_back_stream_object(const std::string &key)
Add a JSON object stream for a specific key.
virtual void output_finalizer()=0
void output_delimiter()
Outputs the delimiter between JSON elements.
const jsont & operator[](const std::string &key) const
Lookup the key of a non-streaming JSON element.
std::map< std::string, jsont > objectt
Non-streaming JSON elements These will be printed when closing the stream or creating a child stream...
virtual ~json_streamt()=default
void output_finalizer() override
Output the finalizing character for a JSON array.
static const jsont null_json_object
~json_stream_objectt() override
jsont & push_back()
Push back and return a new non-streaming JSON element into the current array stream.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
~json_stream_arrayt() override
Flushes and closes the stream on destruction.
void output_child_stream() override
Output non-streaming JSON properties and flushes and closes the child stream.
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
json_objectt json(const source_locationt &location)