forked from pascal-cuoq/abstract_floats
-
Notifications
You must be signed in to change notification settings - Fork 0
/
drift.c
27 lines (20 loc) · 1023 Bytes
/
drift.c
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
#include <stdio.h>
#include <stdbool.h>
#include <string.h>
int main(void)
{
printf("%a / %a = %a\n", 1.0001, 1.0002, 1.0001/1.0002);
// prints:
// 0x1.00068db8bac71p+0 / 0x1.000d1b71758e2p+0 = 0x1.fff2e53a4e1dap-1
// Building the problem:
// We are interested in the equation:
// X / [0x1.000d1b71758e2p+0 … 2.0] == 0x1.fff2e53a4e1dbp-1
printf("%a / %a = %a\n", 0x1.00068db8bac72p+0, 0x1.000d1b71758e2p+0, 0x1.00068db8bac72p+0/ 0x1.000d1b71758e2p+0);
// This makes 0x1.fff2e53a4e1dcp-1: too high
printf("%a / %a = %a\n", 0x1.00068db8bac72p+0, 0x1.000d1b71758e3p+0, 0x1.00068db8bac72p+0/ 0x1.000d1b71758e3p+0);
// This makes 0x1.fff2e53a4e1dap-1: too low
printf("%a / %a = %a\n", 0x1.00068db8bac73p+0, 0x1.000d1b71758e3p+0, 0x1.00068db8bac73p+0/ 0x1.000d1b71758e3p+0);
// This makes 0x1.fff2e53a4e1dcp-1: too high again
printf("%a / %a = %a\n", 0x1.00068db8bac73p+0, 0x1.000d1b71758e4p+0, 0x1.00068db8bac73p+0/ 0x1.000d1b71758e4p+0);
// This makes 0x1.fff2e53a4e1dap-1: too low again
}