12 #ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
13 #define 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.
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
goto_functionst goto_functions
GOTO functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Goto Programs with Functions.