1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
#ifdef __GNUC__
#include <assert.h>
#include <math.h>
#include <fenv.h>
float nondet_value();
// Should work without this as it defaults to off.
// It is explicitly ignored by GCC
#pragma STDC FENV_ACCESS OFF
void roundingTest (float f1, float f2) {
// (Re)Set to the default rounding mode.
fesetround(FE_TONEAREST);
// With round to nearest, should get 0x1.000002p+0f
float roundToNearestSum = f1 + f2;
assert(roundToNearestSum == 0x1.000002p+0f);
#ifdef FE_DOWNWARD
// Change the rounding mode
fesetround(FE_DOWNWARD);
// Should now round down to 0x1p+0;
float roundDownSum = f1 + f2;
assert(roundDownSum == 0x1.0p+0f);
#endif
return;
}
#endif
int main (void)
{
#ifdef __GNUC__
float f1 = 0x1.0p+0;
float f2 = 0x1.8p-24;
// Test with constant folding
roundingTest(f1,f2);
// Test with bitwise model
float f3 = nondet_value();
float f4 = nondet_value();
__CPROVER_assume((0x1.fffffep-1f < f3) && (f3 < 0x1.000002p+0f));
__CPROVER_assume((0x1.7ffffep-24f < f4) && (f4 < 0x1.800002p-24f));
roundingTest(f3,f4);
#endif
return 0;
}
|
