CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
json_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expressions in JSON
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
13#define CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
14
15#include <util/irep.h>
16#include <util/json.h>
17
18class typet;
19class exprt;
20class namespacet;
21
22json_objectt json(const exprt &, const namespacet &, const irep_idt &mode);
23
24json_objectt json(const typet &, const namespacet &, const irep_idt &mode);
25
26#endif // CPROVER_GOTO_PROGRAMS_JSON_EXPR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
exprt
Base class for all expressions.
Definition expr.h:56
json_objectt
Definition json.h:298
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
typet
The type of an expression, extends irept.
Definition type.h:29
json
json_objectt json(const exprt &, const namespacet &, const irep_idt &mode)
Output a CBMC expression in json.
Definition json_expr.cpp:205