adjust_float_expressions.h File Reference

Symbolic Execution. More...

#include <goto-programs/goto_functions.h>

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)
	This adds the rounding mode to floating-point operations, including those in vectors and complex numbers. More...
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 (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)

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

adjust_float_expressions() [2/5]

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.

Definition at line 78 of file adjust_float_expressions.cpp.

adjust_float_expressions() [3/5]

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

Definition at line 189 of file adjust_float_expressions.cpp.

adjust_float_expressions() [4/5]

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

Definition at line 200 of file adjust_float_expressions.cpp.

adjust_float_expressions() [5/5]

void adjust_float_expressions

(

goto_modelt &

goto_model

)

Definition at line 208 of file adjust_float_expressions.cpp.