cprover
|
Symbolic Execution. More...
#include "adjust_float_expressions.h"
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/ieee_float.h>
#include <util/arith_tools.h>
#include "goto_model.h"
Go to the source code of this file.
Functions | |
static bool | have_to_adjust_float_expressions (const exprt &expr) |
void | adjust_float_expressions (exprt &expr, const exprt &rounding_mode) |
This adds the rounding mode to floating-point operations, including those in vectors and complex numbers. More... | |
void | adjust_float_expressions (exprt &expr, const namespacet &ns) |
This adds the rounding mode to floating-point operations, including those in vectors and complex numbers. More... | |
void | adjust_float_expressions (goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
void | adjust_float_expressions (goto_functionst &goto_functions, const namespacet &ns) |
void | adjust_float_expressions (goto_modelt &goto_model) |
Symbolic Execution.
Definition in file adjust_float_expressions.cpp.
This adds the rounding mode to floating-point operations, including those in vectors and complex numbers.
Definition at line 78 of file adjust_float_expressions.cpp.
void adjust_float_expressions | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
This adds the rounding mode to floating-point operations, including those in vectors and complex numbers.
Definition at line 176 of file adjust_float_expressions.cpp.
void adjust_float_expressions | ( | goto_functionst::goto_functiont & | goto_function, |
const namespacet & | ns | ||
) |
Definition at line 189 of file adjust_float_expressions.cpp.
void adjust_float_expressions | ( | goto_functionst & | goto_functions, |
const namespacet & | ns | ||
) |
Definition at line 200 of file adjust_float_expressions.cpp.
void adjust_float_expressions | ( | goto_modelt & | goto_model | ) |
Definition at line 208 of file adjust_float_expressions.cpp.
|
static |
Definition at line 23 of file adjust_float_expressions.cpp.