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