Loading...

Searching...

No Matches

ieee_float.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module:

4

5Author: Daniel Kroening, kroening@kroening.com

6

7\*******************************************************************/

8

9

10#ifndef CPROVER_UTIL_IEEE_FLOAT_H

11#define CPROVER_UTIL_IEEE_FLOAT_H

12

13#include <iosfwd>

14

15#include "mp_arith.h"

16#include "format_spec.h"

17

18class constant_exprt;

19class floatbv_typet;

20

21 class ieee_float_spect

22{

23public:

24 // Number of bits for fraction (excluding hidden bit)

25 // and exponent, respectively

26 std::size_t f, e;

27

28 // x86 has an extended precision format with an explicit

29 // integer bit.

30 bool x86_extended;

31

32 mp_integer bias() const;

33

34 explicit ieee_float_spect(const floatbv_typet &type)

35 {

36 from_type(type);

37 }

38

39 void from_type(const floatbv_typet &type);

40

41 ieee_float_spect():f(0), e(0), x86_extended(false)

42 {

43 }

44

45 ieee_float_spect(std::size_t _f, std::size_t _e):

46 f(_f), e(_e), x86_extended(false)

47 {

48 }

49

50 std::size_t width() const

51{

52 // Add one for the sign bit.

53 // Add one if x86 explicit integer bit is used.

54 return f+e+1+(x86_extended?1:0);

55 }

56

57 mp_integer max_exponent() const;

58 mp_integer max_fraction() const;

59

60 class floatbv_typet to_type() const;

61

62 // this is binary16 in IEEE 754-2008

63 static ieee_float_spect half_precision()

64 {

65 // 16 bits in total

66 return ieee_float_spect(10, 5);

67 }

68

69 // the well-know standard formats

70 static ieee_float_spect single_precision()

71 {

72 // 32 bits in total

73 return ieee_float_spect(23, 8);

74 }

75

76 static ieee_float_spect double_precision()

77 {

78 // 64 bits in total

79 return ieee_float_spect(52, 11);

80 }

81

82 static ieee_float_spect quadruple_precision()

83 {

84 // IEEE 754 binary128

85 return ieee_float_spect(112, 15);

86 }

87

88 static ieee_float_spect x86_80()

89 {

90 // Intel, not IEEE

91 ieee_float_spect result(63, 15);

92 result.x86_extended=true;

93 return result;

94 }

95

96 static ieee_float_spect x86_96()

97 {

98 // Intel, not IEEE

99 ieee_float_spect result(63, 15);

100 result.x86_extended=true;

101 return result;

102 }

103

104 bool operator==(const ieee_float_spect &other) const

105{

106 return f==other.f && e==other.e && x86_extended==other.x86_extended;

107 }

108

109 bool operator!=(const ieee_float_spect &other) const

110{

111 return !(*this==other);

112 }

113};

114

116 class ieee_float_valuet

117{

118public:

119 ieee_float_spect spec;

120

121 explicit ieee_float_valuet(const ieee_float_spect &_spec)

122 : spec(_spec),

123 sign_flag(false),

124 exponent(0),

125 fraction(0),

126 NaN_flag(false),

127 infinity_flag(false)

128 {

129 }

130

131 explicit ieee_float_valuet(const floatbv_typet &type)

132 : spec(ieee_float_spect(type)),

133 sign_flag(false),

134 exponent(0),

135 fraction(0),

136 NaN_flag(false),

137 infinity_flag(false)

138 {

139 }

140

141 explicit ieee_float_valuet(const constant_exprt &expr)

142 {

143 from_expr(expr);

144 }

145

146 ieee_float_valuet()

147 : sign_flag(false),

148 exponent(0),

149 fraction(0),

150 NaN_flag(false),

151 infinity_flag(false)

152 {

153 }

154

155 void negate()

156 {

157 sign_flag=!sign_flag;

158 }

159

160 void set_sign(bool _sign)

161 { sign_flag = _sign; }

162

163 void make_zero()

164 {

165 sign_flag=false;

166 exponent=0;

167 fraction=0;

168 NaN_flag=false;

169 infinity_flag=false;

170 }

171

172 static ieee_float_valuet zero(const floatbv_typet &type)

173 {

174 ieee_float_valuet result(type);

175 result.make_zero();

176 return result;

177 }

178

179 static ieee_float_valuet zero(const ieee_float_spect &spec)

180 {

181 ieee_float_valuet result(spec);

182 result.make_zero();

183 return result;

184 }

185

186 static ieee_float_valuet one(const floatbv_typet &);

187 static ieee_float_valuet one(const ieee_float_spect &);

188

189 void make_NaN();

190 void make_plus_infinity();

191 void make_minus_infinity();

192 void make_fltmax(); // maximum representable finite floating-point number

193 void make_fltmin(); // minimum normalized positive floating-point number

194

195 static ieee_float_valuet NaN(const ieee_float_spect &_spec)

196 {

197 ieee_float_valuet c(_spec);

198 c.make_NaN();

199 return c;

200 }

201

202 static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)

203 {

204 ieee_float_valuet c(_spec);

205 c.make_plus_infinity();

206 return c;

207 }

208

209 static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)

210 {

211 ieee_float_valuet c(_spec);

212 c.make_minus_infinity();

213 return c;

214 }

215

216 // maximum representable finite floating-point number

217 static ieee_float_valuet fltmax(const ieee_float_spect &_spec)

218 {

219 ieee_float_valuet c(_spec);

220 c.make_fltmax();

221 return c;

222 }

223

224 // minimum normalized positive floating-point number

225 static ieee_float_valuet fltmin(const ieee_float_spect &_spec)

226 {

227 ieee_float_valuet c(_spec);

228 c.make_fltmin();

229 return c;

230 }

231

232 // set to next representable number towards plus infinity

233 void increment(bool distinguish_zero=false)

234 {

235 if(is_zero() && get_sign() && distinguish_zero)

236 negate();

237 else

238 next_representable(true);

239 }

240

241 // set to previous representable number towards minus infinity

242 void decrement(bool distinguish_zero=false)

243 {

244 if(is_zero() && !get_sign() && distinguish_zero)

245 negate();

246 else

247 next_representable(false);

248 }

249

250 bool is_zero() const

251{

252 return !NaN_flag && !infinity_flag && fraction==0 && exponent==0;

253 }

254 bool get_sign() const { return sign_flag; }

255 bool is_negative() const

256{

257 return sign_flag;

258 }

259 bool is_NaN() const { return NaN_flag; }

260 bool is_infinity() const { return !NaN_flag && infinity_flag; }

261 bool is_normal() const;

262

263 const mp_integer &get_exponent() const { return exponent; }

264 const mp_integer &get_fraction() const { return fraction; }

265

266 // Construct IEEE floating point value

267 void unpack(const mp_integer &);

268 void from_double(double);

269 void from_float(float);

270

271 // performs conversions from IEEE float-point format

272 // to something else

273

280 double to_double() const;

281

290 float to_float() const;

291

293 bool is_double() const;

295 bool is_float() const;

296 mp_integer pack() const;

297 void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const;

298 void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const;

299

311 mp_integer to_integer() const;

312

313 // output

314 void print(std::ostream &out) const;

315

316 std::string to_ansi_c_string() const

317{

318 return format(format_spect());

319 }

320

321 std::string to_string_decimal(std::size_t precision) const;

322 std::string to_string_scientific(std::size_t precision) const;

323 std::string format(const format_spect &format_spec) const;

324

325 // expressions

326 constant_exprt to_expr() const;

327 void from_expr(const constant_exprt &expr);

328

329 bool operator<(const ieee_float_valuet &) const;

330 bool operator<=(const ieee_float_valuet &) const;

331 bool operator>(const ieee_float_valuet &) const;

332 bool operator>=(const ieee_float_valuet &) const;

333

334 ieee_float_valuet abs() const;

335

336 // warning: these do packed equality, not IEEE equality

337 // e.g., NAN==NAN

338 bool operator==(const ieee_float_valuet &) const;

339 bool operator!=(const ieee_float_valuet &) const;

340 bool operator==(int) const;

341 bool operator==(double) const;

342 bool operator==(float) const;

343

344 // these do IEEE equality, i.e., NAN!=NAN

345 bool ieee_equal(const ieee_float_valuet &) const;

346 bool ieee_not_equal(const ieee_float_valuet &) const;

347

348protected:

349 // we store the number unpacked

350 bool sign_flag;

351 mp_integer exponent; // this is unbiased

352 mp_integer fraction; // this _does_ include the hidden bit

353 bool NaN_flag, infinity_flag;

354

355 // number of digits of an integer >=1 in base 10

356 static mp_integer base10_digits(const mp_integer &src);

357

358 void next_representable(bool greater);

359};

360

361 inline std::ostream &operator<<(std::ostream &out, const ieee_float_valuet &f)

362{

363 return out << f.to_ansi_c_string();

364}

365

368 class ieee_floatt : public ieee_float_valuet

369{

370public:

371 // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and

372 // is the IEEE default.

373 // ROUND_TO_AWAY is also known as "round to nearest, ties away from zero".

374 // The numbering below is what x86 uses in the control word and

375 // what is recommended in C11 5.2.4.2.2.

376 // The numbering of ROUND_TO_AWAY is not specified in C11 5.2.4.2.2.

377 enum rounding_modet

378 {

379 ROUND_TO_EVEN = 0,

380 ROUND_TO_MINUS_INF = 1,

381 ROUND_TO_PLUS_INF = 2,

382 ROUND_TO_ZERO = 3,

383 ROUND_TO_AWAY = 4,

384 UNKNOWN,

385 NONDETERMINISTIC

386 };

387

388 rounding_modet rounding_mode() const

389{

390 return _rounding_mode;

391 }

392

393 // A helper to turn a rounding mode into a constant bitvector expression

394 static constant_exprt rounding_mode_expr(rounding_modet);

395

396 ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)

397 : ieee_float_valuet(__spec), _rounding_mode(__rounding_mode)

398 {

399 }

400

401 ieee_floatt(

402 ieee_float_spect __spec,

403 rounding_modet __rounding_mode,

404 const mp_integer &value)

405 : ieee_float_valuet(__spec), _rounding_mode(__rounding_mode)

406 {

407 from_integer(value);

408 }

409

410 ieee_floatt(const floatbv_typet &type, rounding_modet __rounding_mode)

411 : ieee_float_valuet(type), _rounding_mode(__rounding_mode)

412 {

413 }

414

415 ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)

416 : ieee_float_valuet(expr), _rounding_mode(__rounding_mode)

417 {

418 }

419

420 ieee_floatt(ieee_float_valuet __value, rounding_modet __rounding_mode)

421 : ieee_float_valuet(__value), _rounding_mode(__rounding_mode)

422 {

423 }

424

425 // performs conversion to IEEE floating point format,

426 // with rounding.

427 void from_integer(const mp_integer &i);

428 void from_base10(const mp_integer &exp, const mp_integer &frac);

429 void build(const mp_integer &exp, const mp_integer &frac);

430

431 // conversions

432 void change_spec(const ieee_float_spect &dest_spec);

433

434 // Rounds according to the configured rounding mode

435 ieee_floatt round_to_integral() const;

436

437 // the usual operators

438 ieee_floatt &operator/=(const ieee_floatt &other);

439 ieee_floatt &operator*=(const ieee_floatt &other);

440 ieee_floatt &operator+=(const ieee_floatt &other);

441 ieee_floatt &operator-=(const ieee_floatt &other);

442

443protected:

444 rounding_modet _rounding_mode;

445

446 void divide_and_round(mp_integer &dividend, const mp_integer &divisor);

447 void align();

448};

449

450#endif // CPROVER_UTIL_IEEE_FLOAT_H

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

constant_exprt

A constant literal expression.

Definition std_expr.h:3007

floatbv_typet

Fixed-width bit-vector with IEEE floating-point interpretation.

Definition bitvector_types.h:404

format_spect

Definition format_spec.h:16

ieee_float_spect

Definition ieee_float.h:22

ieee_float_spect::max_fraction

mp_integer max_fraction() const

Definition ieee_float.cpp:40

ieee_float_spect::ieee_float_spect

ieee_float_spect(std::size_t _f, std::size_t _e)

Definition ieee_float.h:45

ieee_float_spect::half_precision

static ieee_float_spect half_precision()

Definition ieee_float.h:63

ieee_float_spect::ieee_float_spect

ieee_float_spect(const floatbv_typet &type)

Definition ieee_float.h:34

ieee_float_spect::operator!=

bool operator!=(const ieee_float_spect &other) const

Definition ieee_float.h:109

ieee_float_spect::ieee_float_spect

ieee_float_spect()

Definition ieee_float.h:41

ieee_float_spect::x86_80

static ieee_float_spect x86_80()

Definition ieee_float.h:88

ieee_float_spect::single_precision

static ieee_float_spect single_precision()

Definition ieee_float.h:70

ieee_float_spect::quadruple_precision

static ieee_float_spect quadruple_precision()

Definition ieee_float.h:82

ieee_float_spect::operator==

bool operator==(const ieee_float_spect &other) const

Definition ieee_float.h:104

ieee_float_spect::to_type

class floatbv_typet to_type() const

Definition ieee_float.cpp:25

ieee_float_spect::bias

mp_integer bias() const

Definition ieee_float.cpp:20

ieee_float_spect::max_exponent

mp_integer max_exponent() const

Definition ieee_float.cpp:35

ieee_float_spect::x86_extended

bool x86_extended

Definition ieee_float.h:30

ieee_float_spect::x86_96

static ieee_float_spect x86_96()

Definition ieee_float.h:96

ieee_float_spect::from_type

void from_type(const floatbv_typet &type)

Definition ieee_float.cpp:45

ieee_float_spect::double_precision

static ieee_float_spect double_precision()

Definition ieee_float.h:76

ieee_float_spect::f

std::size_t f

Definition ieee_float.h:26

ieee_float_spect::width

std::size_t width() const

Definition ieee_float.h:50

ieee_float_spect::e

std::size_t e

Definition ieee_float.h:26

ieee_float_valuet

An IEEE 754 floating-point value, including specificiation.

Definition ieee_float.h:117

ieee_float_valuet::to_double

double to_double() const

Reinterpret this value as a native double.

Definition ieee_float.cpp:490

ieee_float_valuet::ieee_float_valuet

ieee_float_valuet(const ieee_float_spect &_spec)

Definition ieee_float.h:121

ieee_float_valuet::set_sign

void set_sign(bool _sign)

Definition ieee_float.h:160

ieee_float_valuet::minus_infinity

static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)

Definition ieee_float.h:209

ieee_float_valuet::to_float

float to_float() const

Reinterpret this value as a native float.

Definition ieee_float.cpp:525

ieee_float_valuet::ieee_equal

bool ieee_equal(const ieee_float_valuet &) const

Definition ieee_float.cpp:686

ieee_float_valuet::is_NaN

bool is_NaN() const

Definition ieee_float.h:259

ieee_float_valuet::operator>=

bool operator>=(const ieee_float_valuet &) const

Definition ieee_float.cpp:660

ieee_float_valuet::operator<

bool operator<(const ieee_float_valuet &) const

Definition ieee_float.cpp:584

ieee_float_valuet::one

static ieee_float_valuet one(const floatbv_typet &)

Definition ieee_float.cpp:483

ieee_float_valuet::exponent

mp_integer exponent

Definition ieee_float.h:351

ieee_float_valuet::operator!=

bool operator!=(const ieee_float_valuet &) const

Definition ieee_float.cpp:720

ieee_float_valuet::extract_base10

void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const

Definition ieee_float.cpp:439

ieee_float_valuet::spec

ieee_float_spect spec

Definition ieee_float.h:119

ieee_float_valuet::make_minus_infinity

void make_minus_infinity()

Definition ieee_float.cpp:1355

ieee_float_valuet::from_expr

void from_expr(const constant_exprt &expr)

Definition ieee_float.cpp:1250

ieee_float_valuet::is_float

bool is_float() const

Definition ieee_float.cpp:1366

ieee_float_valuet::ieee_not_equal

bool ieee_not_equal(const ieee_float_valuet &) const

Definition ieee_float.cpp:725

ieee_float_valuet::ieee_float_valuet

ieee_float_valuet(const constant_exprt &expr)

Definition ieee_float.h:141

ieee_float_valuet::fraction

mp_integer fraction

Definition ieee_float.h:352

ieee_float_valuet::to_expr

constant_exprt to_expr() const

Definition ieee_float.cpp:579

ieee_float_valuet::pack

mp_integer pack() const

Definition ieee_float.cpp:377

ieee_float_valuet::fltmin

static ieee_float_valuet fltmin(const ieee_float_spect &_spec)

Definition ieee_float.h:225

ieee_float_valuet::ieee_float_valuet

ieee_float_valuet()

Definition ieee_float.h:146

ieee_float_valuet::operator==

bool operator==(const ieee_float_valuet &) const

Definition ieee_float.cpp:665

ieee_float_valuet::make_zero

void make_zero()

Definition ieee_float.h:163

ieee_float_valuet::abs

ieee_float_valuet abs() const

Definition ieee_float.cpp:60

ieee_float_valuet::get_sign

bool get_sign() const

Definition ieee_float.h:254

ieee_float_valuet::fltmax

static ieee_float_valuet fltmax(const ieee_float_spect &_spec)

Definition ieee_float.h:217

ieee_float_valuet::to_ansi_c_string

std::string to_ansi_c_string() const

Definition ieee_float.h:316

ieee_float_valuet::to_string_decimal

std::string to_string_decimal(std::size_t precision) const

Definition ieee_float.cpp:141

ieee_float_valuet::get_fraction

const mp_integer & get_fraction() const

Definition ieee_float.h:264

ieee_float_valuet::to_string_scientific

std::string to_string_scientific(std::size_t precision) const

format as [-]d.ddde+-d Note that printf always produces at least two digits for the exponent.

Definition ieee_float.cpp:235

ieee_float_valuet::is_negative

bool is_negative() const

Definition ieee_float.h:255

ieee_float_valuet::print

void print(std::ostream &out) const

Definition ieee_float.cpp:67

ieee_float_valuet::make_NaN

void make_NaN()

Definition ieee_float.cpp:1325

ieee_float_valuet::next_representable

void next_representable(bool greater)

Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...

Definition ieee_float.cpp:739

ieee_float_valuet::is_zero

bool is_zero() const

Definition ieee_float.h:250

ieee_float_valuet::zero

static ieee_float_valuet zero(const floatbv_typet &type)

Definition ieee_float.h:172

ieee_float_valuet::from_float

void from_float(float)

Definition ieee_float.cpp:1301

ieee_float_valuet::base10_digits

static mp_integer base10_digits(const mp_integer &src)

Definition ieee_float.cpp:132

ieee_float_valuet::NaN

static ieee_float_valuet NaN(const ieee_float_spect &_spec)

Definition ieee_float.h:195

ieee_float_valuet::is_double

bool is_double() const

Definition ieee_float.cpp:1361

ieee_float_valuet::operator<=

bool operator<=(const ieee_float_valuet &) const

Definition ieee_float.cpp:632

ieee_float_valuet::to_integer

mp_integer to_integer() const

Convert to an integer, always rounding towards zero (truncation), i.e.

Definition ieee_float.cpp:1256

ieee_float_valuet::decrement

void decrement(bool distinguish_zero=false)

Definition ieee_float.h:242

ieee_float_valuet::format

std::string format(const format_spect &format_spec) const

Definition ieee_float.cpp:72

ieee_float_valuet::plus_infinity

static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)

Definition ieee_float.h:202

ieee_float_valuet::unpack

void unpack(const mp_integer &)

Definition ieee_float.cpp:322

ieee_float_valuet::make_plus_infinity

void make_plus_infinity()

Definition ieee_float.cpp:1346

ieee_float_valuet::increment

void increment(bool distinguish_zero=false)

Definition ieee_float.h:233

ieee_float_valuet::sign_flag

bool sign_flag

Definition ieee_float.h:350

ieee_float_valuet::is_normal

bool is_normal() const

Definition ieee_float.cpp:372

ieee_float_valuet::from_double

void from_double(double)

Definition ieee_float.cpp:1277

ieee_float_valuet::ieee_float_valuet

ieee_float_valuet(const floatbv_typet &type)

Definition ieee_float.h:131

ieee_float_valuet::NaN_flag

bool NaN_flag

Definition ieee_float.h:353

ieee_float_valuet::extract_base2

void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const

Definition ieee_float.cpp:415

ieee_float_valuet::infinity_flag

bool infinity_flag

Definition ieee_float.h:353

ieee_float_valuet::make_fltmax

void make_fltmax()

Definition ieee_float.cpp:1334

ieee_float_valuet::negate

void negate()

Definition ieee_float.h:155

ieee_float_valuet::operator>

bool operator>(const ieee_float_valuet &) const

Definition ieee_float.cpp:655

ieee_float_valuet::is_infinity

bool is_infinity() const

Definition ieee_float.h:260

ieee_float_valuet::zero

static ieee_float_valuet zero(const ieee_float_spect &spec)

Definition ieee_float.h:179

ieee_float_valuet::get_exponent

const mp_integer & get_exponent() const

Definition ieee_float.h:263

ieee_float_valuet::make_fltmin

void make_fltmin()

Definition ieee_float.cpp:1341

ieee_floatt

An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.

Definition ieee_float.h:369

ieee_floatt::operator*=

ieee_floatt & operator*=(const ieee_floatt &other)

Definition ieee_float.cpp:1097

ieee_floatt::ieee_floatt

ieee_floatt(ieee_float_valuet __value, rounding_modet __rounding_mode)

Definition ieee_float.h:420

ieee_floatt::ieee_floatt

ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode, const mp_integer &value)

Definition ieee_float.h:401

ieee_floatt::operator+=

ieee_floatt & operator+=(const ieee_floatt &other)

Definition ieee_float.cpp:1133

ieee_floatt::divide_and_round

void divide_and_round(mp_integer &dividend, const mp_integer &divisor)

Definition ieee_float.cpp:954

ieee_floatt::rounding_mode_expr

static constant_exprt rounding_mode_expr(rounding_modet)

Definition ieee_float.cpp:561

ieee_floatt::ieee_floatt

ieee_floatt(const floatbv_typet &type, rounding_modet __rounding_mode)

Definition ieee_float.h:410

ieee_floatt::operator-=

ieee_floatt & operator-=(const ieee_floatt &other)

Definition ieee_float.cpp:1224

ieee_floatt::operator/=

ieee_floatt & operator/=(const ieee_floatt &other)

Definition ieee_float.cpp:1023

ieee_floatt::ieee_floatt

ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)

Definition ieee_float.h:415

ieee_floatt::_rounding_mode

rounding_modet _rounding_mode

Definition ieee_float.h:444

ieee_floatt::from_integer

void from_integer(const mp_integer &i)

Definition ieee_float.cpp:813

ieee_floatt::rounding_mode

rounding_modet rounding_mode() const

Definition ieee_float.h:388

ieee_floatt::rounding_modet

rounding_modet

Definition ieee_float.h:378

ieee_floatt::NONDETERMINISTIC

@ NONDETERMINISTIC

Definition ieee_float.h:385

ieee_floatt::ROUND_TO_ZERO

@ ROUND_TO_ZERO

Definition ieee_float.h:382

ieee_floatt::ROUND_TO_PLUS_INF

@ ROUND_TO_PLUS_INF

Definition ieee_float.h:381

ieee_floatt::UNKNOWN

@ UNKNOWN

Definition ieee_float.h:384

ieee_floatt::ROUND_TO_AWAY

@ ROUND_TO_AWAY

Definition ieee_float.h:383

ieee_floatt::ROUND_TO_EVEN

@ ROUND_TO_EVEN

Definition ieee_float.h:379

ieee_floatt::ROUND_TO_MINUS_INF

@ ROUND_TO_MINUS_INF

Definition ieee_float.h:380

ieee_floatt::build

void build(const mp_integer &exp, const mp_integer &frac)

Definition ieee_float.cpp:566

ieee_floatt::ieee_floatt

ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)

Definition ieee_float.h:396

ieee_floatt::from_base10

void from_base10(const mp_integer &exp, const mp_integer &frac)

compute f * (10^e)

Definition ieee_float.cpp:784

ieee_floatt::change_spec

void change_spec(const ieee_float_spect &dest_spec)

Definition ieee_float.cpp:1231

ieee_floatt::align

void align()

Definition ieee_float.cpp:821

ieee_floatt::round_to_integral

ieee_floatt round_to_integral() const

Definition ieee_float.cpp:1371

format_spec.h

operator<<

std::ostream & operator<<(std::ostream &out, const ieee_float_valuet &f)

Definition ieee_float.h:361

exp

double exp(double x)

Definition math.c:2186

mp_arith.h

mp_integer

BigInt mp_integer

Definition smt_terms.h:17

CBMC: /home/runner/work/cbmc/cbmc/src/util/ieee_float.h Source File