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. More...

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. 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 (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 (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...

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 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.

◆ 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.

Functions