json_expr.h File Reference

#include <util/irep.h>
#include <util/json.h>

Include dependency graph for json_expr.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
json_objectt	json (const exprt &, const namespacet &, const irep_idt &mode)
	Output a CBMC expression in json. More...
json_objectt	json (const typet &, const namespacet &, const irep_idt &mode)
	Output a CBMC type in json. More...

Detailed Description

Expressions in JSON

Definition in file json_expr.h.

Function Documentation

json() [1/2]

json_objectt json	(	const exprt &	expr,
		const namespacet &	ns,
		const irep_idt &	mode
	)

Output a CBMC expression in json.

The mode is used to correctly report types.

Parameters

expr	an expression
ns	a namespace
mode	language in which the code was written

Returns

a json object

Definition at line 207 of file json_expr.cpp.

json() [2/2]

json_objectt json	(	const typet &	type,
		const namespacet &	ns,
		const irep_idt &	mode
	)

Output a CBMC type in json.

The mode argument is used to correctly report types.

Parameters

type	a type
ns	a namespace
mode	language in which the code was written

Returns

a json object

Definition at line 82 of file json_expr.cpp.