cprover
json_expr.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Expressions in JSON
4
5
Author: Peter Schrammel
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_UTIL_JSON_EXPR_H
13
#define CPROVER_UTIL_JSON_EXPR_H
14
15
#include "
json.h
"
16
#include "
irep.h
"
17
18
class
source_locationt
;
19
class
typet
;
20
class
exprt
;
21
class
namespacet
;
22
23
json_objectt
json
(
24
const
exprt
&,
25
const
namespacet
&,
26
const
irep_idt
&mode);
27
28
json_objectt
json
(
29
const
typet
&,
30
const
namespacet
&,
31
const
irep_idt
&mode);
32
33
json_objectt
json
(
const
source_locationt
&);
34
35
#endif // CPROVER_UTIL_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:35
json
json_objectt json(const exprt &, const namespacet &, const irep_idt &mode)
Output a CBMC expression in json.
Definition:
json_expr.cpp:238
typet
The type of an expression, extends irept.
Definition:
type.h:27
exprt
Base class for all expressions.
Definition:
expr.h:54
json_objectt
Definition:
json.h:244
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
source_locationt
Definition:
source_location.h:20
json.h
irep.h
util
json_expr.h
Generated by
1.8.16