cprover
json_expr.cpp File Reference

Expressions in JSON. More...

#include "json_expr.h"
#include "namespace.h"
#include "expr.h"
#include "json.h"
#include "arith_tools.h"
#include "ieee_float.h"
#include "fixedbv.h"
#include "std_expr.h"
#include "config.h"
#include "identifier.h"
#include "invariant.h"
#include <langapi/mode.h>
#include <langapi/language.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, const namespacet &ns)
 
json_objectt json (const source_locationt &location)
 
json_objectt json (const typet &type, const namespacet &ns, const irep_idt &mode)
 Output a CBMC type in json. More...
 
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

◆ json() [1/3]

◆ 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 115 of file json_expr.cpp.

References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), json(), jsont::make_array(), jsont::make_object(), json_arrayt::push_back(), typet::subtype(), to_bv_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_fixedbv_type(), to_floatbv_type(), to_signedbv_type(), to_string(), to_struct_type(), to_union_type(), to_unsignedbv_type(), and to_vector_type().

◆ json() [3/3]

◆ simplify_json_expr()