CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
16
17class exprt;
18class namespacet;
19class goto_modelt;
20
25 exprt &expr,
26 const namespacet &ns);
27
39void adjust_float_expressions(exprt &expr, const exprt &rounding_mode);
40
46 const namespacet &ns);
47
53 const namespacet &ns);
54
58
62
63#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
void adjust_float_expressions(exprt &expr, const namespacet &ns)
Adjust floating point subexpressions in the passed expr with the rounding mode from the ns.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Goto Programs with Functions.