cprover
expr_initializer.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Expression Initialization
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_UTIL_EXPR_INITIALIZER_H
13
#define CPROVER_UTIL_EXPR_INITIALIZER_H
14
15
#include "
expr.h
"
16
#include "
optional.h
"
17
18
class
message_handlert
;
19
class
namespacet
;
20
class
source_locationt
;
21
22
optionalt<exprt>
23
zero_initializer
(
const
typet
&,
const
source_locationt
&,
const
namespacet
&);
24
25
optionalt<exprt>
nondet_initializer
(
26
const
typet
&type,
27
const
source_locationt
&source_location,
28
const
namespacet
&ns);
29
30
#endif // CPROVER_UTIL_EXPR_INITIALIZER_H
typet
The type of an expression, extends irept.
Definition:
type.h:29
optional.h
zero_initializer
optionalt< exprt > zero_initializer(const typet &, const source_locationt &, const namespacet &)
Create the equivalent of zero for type type.
Definition:
expr_initializer.cpp:318
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
nondet_initializer
optionalt< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
Definition:
expr_initializer.cpp:333
message_handlert
Definition:
message.h:28
optionalt
nonstd::optional< T > optionalt
Definition:
optional.h:35
source_locationt
Definition:
source_location.h:20
util
expr_initializer.h
Generated by
1.8.20