[kernel] Parsing array_size_float.i (no preprocessing)
[kernel:parser:decimal-float] array_size_float.i:1: Warning:
Floating-point constant 50.1 is not represented exactly. Will use 0x1.90ccccccccccdp5.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[kernel] array_size_float.i:2: Warning:
Unable to do constant-folding on array length (int)6000000000000.1. Some CIL operations on this array may fail.
/* Generated by Frama-C */
int t1[(int)50.1];
int t2[(int)6000000000000.1];
|