[kernel] Parsing finite_float.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
#include "errno.h"
#include "math.h"
void main(void)
{
  /*@ assert rte: is_nan_or_infinite: \is_finite((double)0x1p10000); */
  double d = 0x1p10000;
  d = 0.;
  /*@ assert rte: is_nan_or_infinite: \is_finite(\div_double(d, d)); */
  /*@ assert
      rte: is_nan_or_infinite: \is_finite(\add_double(\div_double(d, d), d));
  */
  double e = d / d + d;
  return;
}