Functions

Output a CBMC expression in json.

Output a CBMC type in json.

Detailed Description

Expressions in JSON.

Definition in file json_expr.h.

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

Definition at line 203 of file json_expr.cpp.

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

Definition at line 78 of file json_expr.cpp.