cprover
Loading...
Searching...
No Matches
adjust_float_expressions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
17class exprt;
18class namespacet;
19class goto_modelt;
20
24void adjust_float_expressions(
25 exprt &expr,
26 const namespacet &ns);
27
39void adjust_float_expressions(exprt &expr, const exprt &rounding_mode);
40
44void adjust_float_expressions(
45 goto_functionst::goto_functiont &goto_function,
46 const namespacet &ns);
47
51void adjust_float_expressions(
52 goto_functionst &goto_functions,
53 const namespacet &ns);
54
57void adjust_float_expressions(goto_modelt &goto_model);
58
61irep_idt rounding_mode_identifier();
62
63#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
rounding_mode_identifier
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Definition adjust_float_expressions.cpp:24
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:203
exprt
Base class for all expressions.
Definition expr.h:57
goto_functionst
A collection of goto functions.
Definition goto_functions.h:25
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition goto_functions.h:27
goto_modelt
Definition goto_model.h:27
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
goto_functions.h
Goto Programs with Functions.
irep_idt
dstringt irep_idt
Definition verification_result.h:16