CBMC
|
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>
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. 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... | |
Expressions in JSON.
Definition in file json_expr.cpp.
|
static |
Definition at line 187 of file json_expr.cpp.
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.
expr | an expression |
ns | a namespace |
mode | language in which the code was written |
Definition at line 205 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.
type | a type |
ns | a namespace |
mode | language in which the code was written |
Definition at line 80 of file json_expr.cpp.
Definition at line 31 of file json_expr.cpp.