#include "json_expr.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/expr_util.h>
#include <util/fixedbv.h>
#include <util/identifier.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/json.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <memory>

Include dependency graph for json_expr.cpp:

Functions
static exprt	simplify_json_expr (const exprt &src)

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

static std::string	binary (const constant_exprt &src)

json_objectt	json (const exprt &expr, const namespacet &ns, const irep_idt &mode)
	Output a CBMC expression in json. More...

Detailed Description

Expressions in JSON

Definition in file json_expr.cpp.

Function Documentation

◆ binary()

static std::string binary ( const constant_exprt & src )

static

Definition at line 189 of file json_expr.cpp.

◆ 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.

◆ simplify_json_expr()

static exprt simplify_json_expr ( const exprt & src )