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
21
void
adjust_float_expressions
(
22
exprt
&expr,
23
const
namespacet
&ns);
24
25
void
adjust_float_expressions
(
exprt
&expr,
const
exprt
&rounding_mode);
26
27
void
adjust_float_expressions
(
28
goto_functionst::goto_functiont
&goto_function,
29
const
namespacet
&ns);
30
31
void
adjust_float_expressions
(
32
goto_functionst
&
goto_functions
,
33
const
namespacet
&ns);
34
void
adjust_float_expressions
(
goto_modelt
&goto_model);
35
36
#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
exprt
Base class for all expressions.
Definition:
expr.h:54
goto_modelt
Definition:
goto_model.h:24
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
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)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
Definition:
adjust_float_expressions.cpp:176
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:22
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition:
goto_model.h:32
goto_functions.h
goto-programs
adjust_float_expressions.h
Generated by
1.8.16