Loading...

Searching...

No Matches

adjust_float_expressions.cpp File Reference

Symbolic Execution. More...

#include "adjust_float_expressions.h"
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include "goto_model.h"

+ Include dependency graph for adjust_float_expressions.cpp:

[フレーム]

Go to the source code of this file.

Functions

irep_idt rounding_mode_identifier ()

Return the identifier of the program symbol used to store the current rounding mode.

static bool have_to_adjust_float_expressions (const exprt &expr)

Iterate over an expression and check it or any of its subexpressions are floating point operations that haven't been adjusted with a rounding mode yet.

void adjust_float_expressions (exprt &expr, const exprt &rounding_mode)

Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent floatbv version, for example a plus expression (ID_plus) turns into a floatbv_plus expression (ID_floatbv_plus).

void adjust_float_expressions (exprt &expr, const namespacet &ns)

Adjust floating point subexpressions in the passed expr with the rounding mode from the ns.

void adjust_float_expressions (goto_functionst::goto_functiont &goto_function, const namespacet &ns)

Adjust floating point expressions in the body of a given function.

void adjust_float_expressions (goto_functionst &goto_functions, const namespacet &ns)

Adjust float expressions in all goto function bodies.

void adjust_float_expressions (goto_modelt &goto_model)

Adjust float expressions in a given goto_model.

Detailed Description

Symbolic Execution.

Definition in file adjust_float_expressions.cpp.

Function Documentation

◆ adjust_float_expressions() [1/5]

void adjust_float_expressions ( exprt & expr,

const exprt & rounding_mode

)

Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent floatbv version, for example a plus expression (ID_plus) turns into a floatbv_plus expression (ID_floatbv_plus).

These versions of the operators hold the current rounding mode as an additional operand, which affects how these expressions have to be evaluated. (Note that these floating point versions of arithmetic operators do not have corresponding exprt classes at the moment).

Parameters: expr The expression to adjust

rounding_mode The rounding mode to set on floating point subexpressions of this expression.

Definition at line 91 of file adjust_float_expressions.cpp.

◆ adjust_float_expressions() [2/5]

void adjust_float_expressions ( exprt & expr,

const namespacet & ns

)

Adjust floating point subexpressions in the passed expr with the rounding mode from the ns.

See also: adjust_float_expressions(exprt &, const namespacet &)

Definition at line 203 of file adjust_float_expressions.cpp.

◆ adjust_float_expressions() [3/5]

void adjust_float_expressions ( goto_functionst & goto_functions,

const namespacet & ns

)

Adjust float expressions in all goto function bodies.

See also: adjust_float_expressions( goto_functionst::goto_functiont &, const namespacet &)

Definition at line 232 of file adjust_float_expressions.cpp.

◆ adjust_float_expressions() [4/5]

void adjust_float_expressions ( goto_functionst::goto_functiont & goto_function,

const namespacet & ns

)

Adjust floating point expressions in the body of a given function.

See also: adjust_float_expressions(exprt &, namespacet &); adjust_float_expressions(exprt &, const exprt &)

Definition at line 216 of file adjust_float_expressions.cpp.

◆ adjust_float_expressions() [5/5]

void adjust_float_expressions ( goto_modelt & goto_model )

Adjust float expressions in a given goto_model.

See also: adjust_float_expressions(goto_functionst &, const namespacet &)

Definition at line 240 of file adjust_float_expressions.cpp.

◆ have_to_adjust_float_expressions()

static bool have_to_adjust_float_expressions ( const exprt & expr )

static

Iterate over an expression and check it or any of its subexpressions are floating point operations that haven't been adjusted with a rounding mode yet.

Definition at line 32 of file adjust_float_expressions.cpp.

◆ rounding_mode_identifier()

irep_idt rounding_mode_identifier ( )

Return the identifier of the program symbol used to store the current rounding mode.

Definition at line 24 of file adjust_float_expressions.cpp.