cprover
|
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>
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... | |
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 224 of file json_expr.cpp.
json_objectt json | ( | const source_locationt & | location | ) |
Definition at line 87 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; for now ID_C and ID_java are supported |
Definition at line 119 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; for now ID_C and ID_java are supported |
Definition at line 238 of file json_expr.cpp.
|
static |
Definition at line 30 of file json_expr.cpp.