finite_float.res.oracle

[kernel] Parsing finite_float.c (with preprocessing)
[kernel:parser:decimal-float] finite_float.c:8: Warning: 
  Floating-point constant 0x1p10000 is not represented exactly. Will use inf.
  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[rte:annot] 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;
}