cprover
json_expr.h File Reference

Expressions in JSON. More...

#include "json.h"
#include "irep.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...
 
json_objectt json (const source_locationt &)
 

Detailed Description

Expressions in JSON.

Definition in file json_expr.h.

Function Documentation

◆ json() [1/3]

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
expran expression
nsa namespace
modelanguage in which the code was written; for now ID_C and ID_java are supported
Returns
a json object

Definition at line 238 of file json_expr.cpp.

◆ json() [2/3]

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
typea type
nsa namespace
modelanguage in which the code was written; for now ID_C and ID_java are supported
Returns
a json object

Definition at line 119 of file json_expr.cpp.

◆ json() [3/3]

json_objectt json ( const source_locationt )

Definition at line 87 of file json_expr.cpp.