-
Andre Maroneze authored
Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
Andre Maroneze authoredSome case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
finite_float.res.oracle 474 B
[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;
}