cprover
adjust_float_expressions.cpp File Reference

Symbolic Execution. More...

#include "adjust_float_expressions.h"
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/ieee_float.h>
#include <util/arith_tools.h>
#include "goto_model.h"
Include dependency graph for adjust_float_expressions.cpp:

Go to the source code of this file.

Functions

static bool have_to_adjust_float_expressions (const exprt &expr, const namespacet &ns)
 
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 (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.cpp.

Function Documentation

◆ adjust_float_expressions() [1/4]

◆ adjust_float_expressions() [2/4]

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

◆ adjust_float_expressions() [3/4]

void adjust_float_expressions ( goto_functionst goto_functions,
const namespacet ns 
)

◆ adjust_float_expressions() [4/4]

void adjust_float_expressions ( goto_modelt goto_model)

◆ have_to_adjust_float_expressions()

static bool have_to_adjust_float_expressions ( const exprt expr,
const namespacet ns 
)
static