diff --git a/tests/float/oracle/special_floats.res.oracle b/tests/float/oracle/special_floats.res.oracle index 653af4625c63f0bc09500f9a1a31b85f3d6c2fba..2cdcf9695086ecd4f8b8ed1fa5aaff28bd1eeb6d 100644 --- a/tests/float/oracle/special_floats.res.oracle +++ b/tests/float/oracle/special_floats.res.oracle @@ -8,11 +8,11 @@ global_infinity ∈ {inf} global_nan ∈ NaN [eva] computing for function nan_comparisons <- main. - Called from tests/float/special_floats.c:94. + Called from tests/float/special_floats.c:117. [eva] Recording results for nan_comparisons [eva] Done for function nan_comparisons [eva] computing for function is_infinite <- main. - Called from tests/float/special_floats.c:95. + Called from tests/float/special_floats.c:118. [eva] tests/float/special_floats.c:29: check 'true' got status valid. [eva:alarm] tests/float/special_floats.c:30: Warning: check 'false' got status invalid. @@ -20,53 +20,80 @@ check 'false' got status invalid. [eva:alarm] tests/float/special_floats.c:32: Warning: check 'false' got status invalid. -[eva:alarm] tests/float/special_floats.c:34: Warning: +[eva:alarm] tests/float/special_floats.c:33: Warning: check 'false' got status invalid. -[eva] tests/float/special_floats.c:35: check 'true' got status valid. -[eva] tests/float/special_floats.c:36: check 'true' got status valid. -[eva:alarm] tests/float/special_floats.c:37: Warning: +[eva:alarm] tests/float/special_floats.c:35: Warning: check 'false' got status invalid. +[eva] tests/float/special_floats.c:36: check 'true' got status valid. +[eva] tests/float/special_floats.c:37: check 'true' got status valid. +[eva] tests/float/special_floats.c:38: check 'true' got status valid. [eva:alarm] tests/float/special_floats.c:39: Warning: check 'false' got status invalid. -[eva] tests/float/special_floats.c:40: check 'true' got status valid. [eva:alarm] tests/float/special_floats.c:41: Warning: check 'false' got status invalid. -[eva:alarm] tests/float/special_floats.c:42: Warning: +[eva] tests/float/special_floats.c:42: check 'true' got status valid. +[eva:alarm] tests/float/special_floats.c:43: Warning: check 'false' got status invalid. -[eva:alarm] tests/float/special_floats.c:46: Warning: - assertion got status unknown. -[eva] tests/float/special_floats.c:47: Frama_C_show_each_pos_infinity: {inf} +[eva:alarm] tests/float/special_floats.c:44: Warning: + check 'false' got status invalid. +[eva:alarm] tests/float/special_floats.c:45: Warning: + check 'false' got status invalid. +[eva:alarm] tests/float/special_floats.c:49: Warning: + check 'unknown' got status unknown. [eva:alarm] tests/float/special_floats.c:50: Warning: + check 'unknown' got status unknown. +[eva:alarm] tests/float/special_floats.c:51: Warning: + check 'unknown' got status unknown. +[eva:alarm] tests/float/special_floats.c:52: Warning: + check 'false' got status invalid. +[eva:alarm] tests/float/special_floats.c:53: Warning: + check 'unknown' got status unknown. +[eva:alarm] tests/float/special_floats.c:57: Warning: assertion got status unknown. -[eva] tests/float/special_floats.c:51: Frama_C_show_each_neg_infinity: {-inf} -[eva:alarm] tests/float/special_floats.c:54: Warning: +[eva] tests/float/special_floats.c:58: Frama_C_show_each_pos_infinity: {inf} +[eva:alarm] tests/float/special_floats.c:61: Warning: assertion got status unknown. -[eva:alarm] tests/float/special_floats.c:55: Warning: +[eva] tests/float/special_floats.c:62: Frama_C_show_each_neg_infinity: {-inf} +[eva:alarm] tests/float/special_floats.c:65: Warning: assertion got status unknown. -[eva] tests/float/special_floats.c:56: +[eva] tests/float/special_floats.c:66: + Frama_C_show_each_infinities: [-inf .. inf] +[eva:alarm] tests/float/special_floats.c:69: Warning: + assertion got status unknown. +[eva:alarm] tests/float/special_floats.c:70: Warning: + assertion got status unknown. +[eva] tests/float/special_floats.c:71: + Frama_C_show_each_finite_nan: + [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN} +[eva:alarm] tests/float/special_floats.c:74: Warning: + assertion got status unknown. +[eva] tests/float/special_floats.c:75: Frama_C_show_each_finite_nan: [-1.79769313486e+308 .. 1.79769313486e+308] ∪ {NaN} -[eva:alarm] tests/float/special_floats.c:59: Warning: +[eva:alarm] tests/float/special_floats.c:78: Warning: assertion got status unknown. -[eva] tests/float/special_floats.c:60: +[eva] tests/float/special_floats.c:79: Frama_C_show_each_top: [-inf .. inf] ∪ {NaN} -[eva:alarm] tests/float/special_floats.c:63: Warning: +[eva:alarm] tests/float/special_floats.c:82: Warning: + assertion got status unknown. +[eva] tests/float/special_floats.c:83: Frama_C_show_each_pos_infinity: {inf;NaN} +[eva:alarm] tests/float/special_floats.c:86: Warning: assertion got status unknown. -[eva] tests/float/special_floats.c:64: Frama_C_show_each_pos_infinity: {inf;NaN} +[eva] tests/float/special_floats.c:87: Frama_C_show_each_neg_infinity: {-inf} [eva] Recording results for is_infinite [eva] Done for function is_infinite [eva] computing for function macro_infinity <- main. - Called from tests/float/special_floats.c:96. -[eva] tests/float/special_floats.c:74: Frama_C_show_each_infinity: {inf} -[eva] tests/float/special_floats.c:75: assertion got status valid. + Called from tests/float/special_floats.c:119. +[eva] tests/float/special_floats.c:97: Frama_C_show_each_infinity: {inf} +[eva] tests/float/special_floats.c:98: assertion got status valid. [eva] Recording results for macro_infinity [eva] Done for function macro_infinity [eva] computing for function macro_nan <- main. - Called from tests/float/special_floats.c:97. -[eva] tests/float/special_floats.c:84: Frama_C_show_each_nan: NaN -[eva] tests/float/special_floats.c:85: assertion got status valid. -[eva] tests/float/special_floats.c:86: assertion got status valid. -[eva] tests/float/special_floats.c:87: assertion got status valid. + Called from tests/float/special_floats.c:120. +[eva] tests/float/special_floats.c:107: Frama_C_show_each_nan: NaN +[eva] tests/float/special_floats.c:108: assertion got status valid. +[eva] tests/float/special_floats.c:109: assertion got status valid. +[eva] tests/float/special_floats.c:110: assertion got status valid. [eva] Recording results for macro_nan [eva] Done for function macro_nan [eva] Recording results for main diff --git a/tests/float/special_floats.c b/tests/float/special_floats.c index 1e07cd3a6ba385e0b3eec0bda2eb0aa1381200d3..732c2cc3e5814adf905a8ddf711e7188b5749e9b 100644 --- a/tests/float/special_floats.c +++ b/tests/float/special_floats.c @@ -28,19 +28,30 @@ void is_infinite () { double zero = -0.; /*@ check true: \is_finite(zero); */ /*@ check false: !\is_finite(zero); */ + /*@ check false: \is_infinite(zero); */ /*@ check false: \is_plus_infinity(zero); */ /*@ check false: \is_minus_infinity(zero); */ double inf = INFINITY; /*@ check false: \is_finite(inf); */ /*@ check true: !\is_finite(inf); */ + /*@ check true: \is_infinite(inf); */ /*@ check true: \is_plus_infinity(inf); */ /*@ check false: \is_minus_infinity(inf); */ double nan = NAN; /*@ check false: \is_finite(nan); */ /*@ check true: !\is_finite(nan); */ + /*@ check false: \is_infinite(nan); */ /*@ check false: \is_plus_infinity(nan); */ /*@ check false: \is_minus_infinity(nan); */ - double d = any_double; + double d; + /* Tests the evaluation on imprecise values. */ + d = rand ? zero : (rand ? -inf : nan); + /*@ check unknown: \is_finite(d); */ + /*@ check unknown: !\is_finite(d); */ + /*@ check unknown: \is_infinite(d); */ + /*@ check false: \is_plus_infinity(d); */ + /*@ check unknown: \is_minus_infinity(d); */ + d = any_double; /* Tests the reduction by assertions. */ if (rand) { /*@ assert \is_plus_infinity(d); */ @@ -50,11 +61,19 @@ void is_infinite () { /*@ assert \is_minus_infinity(d); */ Frama_C_show_each_neg_infinity(d); } + if (rand) { + /*@ assert \is_infinite(d); */ + Frama_C_show_each_infinities(d); + } if (rand) { /*@ assert !\is_plus_infinity(d); */ /*@ assert !\is_minus_infinity(d); */ Frama_C_show_each_finite_nan(d); } + if (rand) { + /*@ assert !\is_infinite(d); */ + Frama_C_show_each_finite_nan(d); + } if (rand) { /*@ assert !\is_finite(d); */ Frama_C_show_each_top(d); @@ -63,6 +82,10 @@ void is_infinite () { /*@ assert !\is_finite(d); */ Frama_C_show_each_pos_infinity(d); } + if (d < 0.) { + /*@ assert \is_infinite(d); */ + Frama_C_show_each_neg_infinity(d); + } } float global_infinity = INFINITY;