CBMC
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 
61 irep_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:192
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
exprt
Base class for all expressions.
Definition: expr.h:56
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:94
goto_functions.h
Goto Programs with Functions.