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
|
/* run.config*
STDOPT: #"-warn-decimal-float all -float-hex"
*/
volatile v;
int main() {
if (v) {
double d = 0.0E9999999999999999999;
Frama_C_show_each(d, "reached");
}
if (v) {
double d = 0.0E-9999999999999999999;
Frama_C_show_each(d, "reached");
}
if (v) {
double d1 = 0e500;
double d2 = 0.0e500;
Frama_C_show_each(d1, d2, "reached");
}
if (v) {
double d = 0.00000000000000000000000000000000000000001e310;
Frama_C_show_each(d, "reached");
}
if (v) {
double d = 0.0000001E9999999999999999999;
Frama_C_show_each("unreached");
}
}
|
