Provides methods for streaming JSON objects. More...

#include <json_stream.h>

Inheritance diagram for json_stream_objectt:

Collaboration diagram for json_stream_objectt:

Public Member Functions
	json_stream_objectt (std::ostream &out, unsigned indent=0)
	Constructor for json_stream_objectt. More...

jsont &	operator[] (const std::string &key)
	Provide key-value lookup capabilities for the JSON object. More...

	~json_stream_objectt () override

const jsont &	operator[] (const std::string &key) const
	Lookup the key of a non-streaming JSON element. More...

void	push_back (const std::string &key, const jsont &json)
	Push back a JSON element into the current object stream. More...

json_stream_objectt &	push_back_stream_object (const std::string &key)
	Add a JSON object stream for a specific key. More...

json_stream_arrayt &	push_back_stream_array (const std::string &key)
	Add a JSON array stream for a specific key. More...

Public Member Functions inherited from json_streamt
void	close ()
	Outputs the current current child stream and closes this JSON stream. More...

virtual	~json_streamt ()=default

Protected Member Functions
void	output_child_stream () override
	Output non-streaming JSON properties and flushes and closes the child stream. More...

void	output_finalizer () override
	Output the finalizing character for a JSON object. More...

Protected Member Functions inherited from json_streamt
	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...

Additional Inherited Members
Protected Types inherited from json_streamt
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 Attributes inherited from json_streamt
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

Provides methods for streaming JSON objects.

Definition at line 139 of file json_stream.h.

Constructor & Destructor Documentation

◆ json_stream_objectt()

json_stream_objectt::json_stream_objectt	(	std::ostream &	out,
		unsigned	indent = `0`
	)

explicit

Constructor for json_stream_objectt.

Parameters

out	The stream that is to be used to output the JSON object.
indent	Current indentation level.

Definition at line 59 of file json_stream.cpp.

◆ ~json_stream_objectt()

json_stream_objectt::~json_stream_objectt ( )

inlineoverride

Definition at line 153 of file json_stream.h.

Member Function Documentation

◆ operator[]() [1/2]

jsont& json_stream_objectt::operator[] ( const std::string & key )

inline

Provide key-value lookup capabilities for the JSON object.

Provided for compatibility with jsont.

Parameters

key	The key to be looked up inside the attributes of the JSON object.

Definition at line 148 of file json_stream.h.

◆ operator[]() [2/2]

const jsont& json_stream_objectt::operator[] ( const std::string & key ) const

inline

Lookup the key of a non-streaming JSON element.

Parameters

key	The key to be looked up inside the attributes of the JSON object.

Returns: The value that corresponds to the key if found, a null_json_object otherwise.

Definition at line 163 of file json_stream.h.

◆ output_child_stream()

void json_stream_objectt::output_child_stream ( )

overrideprotectedvirtual

Output non-streaming JSON properties and flushes and closes the child stream.

Implements json_streamt.

Definition at line 133 of file json_stream.cpp.

◆ output_finalizer()

void json_stream_objectt::output_finalizer ( )

overrideprotectedvirtual

Output the finalizing character for a JSON object.

Implements json_streamt.

Definition at line 150 of file json_stream.cpp.

◆ push_back()

void json_stream_objectt::push_back	(	const std::string &	key,
		const jsont &	json
	)

inline

Push back a JSON element into the current object stream.

Note the pushed key won't be available via operator[], as it has been output already. Provided for compatibility with jsont.

Parameters

key	new key to create in the streamed object
json	a non-streaming JSON element

Definition at line 178 of file json_stream.h.

◆ push_back_stream_array()

json_stream_arrayt & json_stream_objectt::push_back_stream_array ( const std::string & key )

Add a JSON array stream for a specific key.

Parameters

key	key of the JSON property

Definition at line 120 of file json_stream.cpp.

◆ push_back_stream_object()

json_stream_objectt & json_stream_objectt::push_back_stream_object ( const std::string & key )

Add a JSON object stream for a specific key.

Parameters

key	key of the JSON property

Definition at line 106 of file json_stream.cpp.

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

Public Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ json_stream_objectt()

◆ ~json_stream_objectt()

Member Function Documentation

◆ operator[]() [1/2]

◆ operator[]() [2/2]

◆ output_child_stream()

◆ output_finalizer()

◆ push_back()

◆ push_back_stream_array()

◆ push_back_stream_object()