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