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_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
13
#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
14
15
class
exprt
;
16
class
namespacet
;
17
class
goto_functionst
;
18
class
goto_modelt
;
19
20
void
adjust_float_expressions
(
21
exprt
&expr,
22
const
namespacet
&ns);
23
24
void
adjust_float_expressions
(
25
goto_functionst
&
goto_functions
,
26
const
namespacet
&ns);
27
void
adjust_float_expressions
(
goto_modelt
&goto_model);
28
29
#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
goto_modelt
Definition:
goto_model.h:22
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
goto_functionst
Definition:
goto_functions.h:20
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:80
exprt
Base class for all expressions.
Definition:
expr.h:46
goto_modelt::goto_functions
goto_functionst goto_functions
Definition:
goto_model.h:26
goto-symex
adjust_float_expressions.h
Generated by
1.8.12