frexp.c File Reference

#include <fenv.h>
#include <math.h>
#include <stdint.h>
#include <float.h>
#include <limits.h>

Include dependency graph for frexp.c:

Macros
#define	FLT_BITS   32
#define	FLT_EXP_BITS   8
#define	FLT_MANT_BITS   (FLT_MANT_DIG - 1)
#define	DBL_BITS   64
#define	DBL_EXP_BITS   11
#define	DBL_MANT_BITS   (DBL_MANT_DIG - 1)
#define	LDBL_BITS   128
#define	LDBL_EXP_BITS   15
#define	LDBL_MANT_BITS   112
#define	TYPE1(n)
#define	TYPE0(n)
#define	BITS(pre)
#define	TYPE(pre)
#define	EXP_BIAS(pre)
#define	MANT_BITS(pre)
#define	EXP_BITS(pre)
#define	EXP_MASK(pre)
#define	FREXP(name, type, pre)
#define	LDEXP(name, type, pre, suff, SUFF)

Typedefs
typedef __uint128_t	__UINT128_TYPE__

Macro Definition Documentation

BITS

#define BITS

(

pre

)

Value:

pre##_BITS

DBL_BITS

#define DBL_BITS   64

DBL_EXP_BITS

#define DBL_EXP_BITS   11

DBL_MANT_BITS

#define DBL_MANT_BITS   (DBL_MANT_DIG - 1)

EXP_BIAS

#define EXP_BIAS

(

pre

)

Value:

((pre##_MAX_EXP - pre##_MIN_EXP + 1) / 2)

EXP_BITS

#define EXP_BITS

(

pre

)

Value:

(pre##_EXP_BITS)

EXP_MASK

#define EXP_MASK

(

pre

)

Value:

((((TYPE(pre))1 << EXP_BITS(pre)) - 1) << MANT_BITS(pre))

FLT_BITS

#define FLT_BITS   32

FLT_EXP_BITS

#define FLT_EXP_BITS   8

FLT_MANT_BITS

#define FLT_MANT_BITS   (FLT_MANT_DIG - 1)

FREXP

#define FREXP	(		name,
			type,
			pre )

Value:

  type name(type x, int *exp)                                                  \
  {                                                                            \
  __ESBMC_HIDE:;                                                               \
    if (!isfinite(x))                                                          \
      return x;                                                                \
    if (x == 0)                                                                \
    {                                                                          \
      *exp = 0;                                                                \
      return x;                                                                \
    }                                                                          \
    int off = 0;                                                               \
    if (!isnormal(x))                                                          \
    {                                                                          \
      x *= (TYPE(pre))1 << MANT_BITS(pre);                                     \
      off -= MANT_BITS(pre);                                                   \
    }                                                                          \
    TYPE(pre) v;                                                               \
    __ESBMC_bitcast(&v, &x);                                                   \
    int e = (v & EXP_MASK(pre)) >> MANT_BITS(pre);                             \
    *exp = e - (EXP_BIAS(pre) - 1) + off; /* range [0.5, 1) */                 \
    v &= ~EXP_MASK(pre);                  /* clear exponent */                 \
    v |= (TYPE(pre))(EXP_BIAS(pre) - 1)                                        \
         << MANT_BITS(pre); /* set exponent to -1 */                           \
    __ESBMC_bitcast(&x, &v);                                                   \
    return x;                                                                  \
  }

LDBL_BITS

#define LDBL_BITS   128

LDBL_EXP_BITS

#define LDBL_EXP_BITS   15

LDBL_MANT_BITS

#define LDBL_MANT_BITS   112

LDEXP

#define LDEXP	(		name,
			type,
			pre,
			suff,
			SUFF )

MANT_BITS

#define MANT_BITS

(

pre

)

Value:

(pre##_MANT_BITS)

TYPE

#define TYPE

(

pre

)

Value:

TYPE0(BITS(pre))

TYPE0

#define TYPE0

(

n

)

Value:

TYPE1(n)

TYPE1

#define TYPE1

(

n

)

Value:

__UINT##n##_TYPE__

Typedef Documentation

__UINT128_TYPE__

typedef __uint128_t __UINT128_TYPE__