cprover
adjust_float_expressions.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Symbolic Execution
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
13
#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
14
15
#include <
goto-programs/goto_functions.h
>
16
17
class
exprt
;
18
class
namespacet
;
19
class
goto_modelt
;
20
24
void
adjust_float_expressions
(
25
exprt
&expr,
26
const
namespacet
&ns);
27
39
void
adjust_float_expressions
(
exprt
&expr,
const
exprt
&rounding_mode);
40
44
void
adjust_float_expressions
(
45
goto_functionst::goto_functiont
&goto_function,
46
const
namespacet
&ns);
47
51
void
adjust_float_expressions
(
52
goto_functionst
&
goto_functions
,
53
const
namespacet
&ns);
54
57
void
adjust_float_expressions
(
goto_modelt
&goto_model);
58
59
#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
exprt
Base class for all expressions.
Definition:
expr.h:53
goto_modelt
Definition:
goto_model.h:26
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition:
goto_functions.h:25
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const namespacet &ns)
Adjust floating point subexpressions in the passed expr with the rounding mode from the ns.
Definition:
adjust_float_expressions.cpp:183
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition:
goto_model.h:33
goto_functions.h
Goto Programs with Functions.
goto-programs
adjust_float_expressions.h
Generated by
1.8.20