Loading...

Searching...

No Matches

json_expr.cpp File Reference

Expressions in JSON. More...

#include "json_expr.h"
#include <util/arith_tools.h>
#include <util/c_types.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:

[フレーム]

Go to the source code of this file.

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.

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.

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 185 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 203 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 78 of file json_expr.cpp.

◆ simplify_json_expr()

static exprt simplify_json_expr ( const exprt & src )

static

Definition at line 31 of file json_expr.cpp.