finite_float.res.oracle

[kernel] Parsing tests/rte/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(0x1p10000); */
  double d = 0x1p10000;
  d = 0.;
  /*@ assert rte: is_nan_or_infinite: \is_finite((double)(d / d)); */
  /*@ assert
      rte: is_nan_or_infinite: \is_finite((double)((double)(d / d) + d));
  */
  double e = d / d + d;
  return;
}