CBMC
adjust_float_expressions.h File Reference

Symbolic Execution. More...

+ Include dependency graph for adjust_float_expressions.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void adjust_float_expressions (exprt &expr, const namespacet &ns)
 Adjust floating point subexpressions in the passed expr with the rounding mode from the ns. More...
 
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). More...
 
void adjust_float_expressions (goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 Adjust floating point expressions in the body of a given function. More...
 
void adjust_float_expressions (goto_functionst &goto_functions, const namespacet &ns)
 Adjust float expressions in all goto function bodies. More...
 
void adjust_float_expressions (goto_modelt &goto_model)
 Adjust float expressions in a given goto_model. More...
 
irep_idt rounding_mode_identifier ()
 Return the identifier of the program symbol used to store the current rounding mode. More...
 

Detailed Description

Symbolic Execution.

Definition in file adjust_float_expressions.h.

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
exprThe expression to adjust
rounding_modeThe rounding mode to set on floating point subexpressions of this expression.

Definition at line 87 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 192 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 221 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 205 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 229 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.