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.
References adjust_float_expressions(), from_integer(), have_to_adjust_float_expressions(), irept::id(), make_binary(), unary_exprt::op(), exprt::op1(), exprt::op2(), exprt::operands(), ieee_floatt::ROUND_TO_ZERO, typet::subtype(), to_typecast_expr(), and exprt::type().
Referenced by adjust_float_expressions(), c_typecheck_baset::make_constant(), goto_analyzer_parse_optionst::perform_analysis(), jbmc_parse_optionst::process_goto_function(), goto_diff_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
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 171 of file adjust_float_expressions.cpp.
References exprt::add_source_location(), adjust_float_expressions(), CPROVER_PREFIX, have_to_adjust_float_expressions(), namespacet::lookup(), and exprt::source_location().
void adjust_float_expressions | ( | goto_functionst::goto_functiont & | goto_function, |
const namespacet & | ns | ||
) |
Definition at line 184 of file adjust_float_expressions.cpp.
References adjust_float_expressions(), and Forall_goto_program_instructions.
void adjust_float_expressions | ( | goto_functionst & | goto_functions, |
const namespacet & | ns | ||
) |
Definition at line 195 of file adjust_float_expressions.cpp.
References adjust_float_expressions(), and Forall_goto_functions.
void adjust_float_expressions | ( | goto_modelt & | goto_model | ) |
Definition at line 203 of file adjust_float_expressions.cpp.
References adjust_float_expressions(), goto_modelt::goto_functions, and goto_modelt::symbol_table.
|
static |
Definition at line 23 of file adjust_float_expressions.cpp.
References forall_operands, irept::id(), unary_exprt::op(), typet::subtype(), to_typecast_expr(), and exprt::type().
Referenced by adjust_float_expressions().