File: extract_bits.i

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 42,324 kB
  • ctags: 35,695
  • sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (26 lines) | stat: -rw-r--r-- 667 bytes parent folder | download | duplicates (2) 
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
 
/* run.config*
  OPT: -val @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep ppc_32 -float-normal -warn-decimal-float all
  OPT: -val @VALUECONFIG@ -slevel 10 -big-ints-hex 0 -machdep x86_32 -float-normal -warn-decimal-float all
*/

float f = 3.14;
double d = 2.71;

double stdtod_bug = 1.8254370818746402660437411213933955878019332885742187;
/*
http://www.exploringbinary.com/a-bug-in-the-bigcomp-function-of-david-gays-strtod/
*/

int fr[4];
int dr[8];

void main() {
  int i;
  for (i=0; i<4; i++)
    fr[i] = ((unsigned char*) &f)[i];
  for (i=0; i<8; i++)
    dr[i] = ((unsigned char*) &d)[i];

  long double x = 1.;
  Frama_C_show_each(*(unsigned char *)&x);
}