Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis: resulting intervals after loop

  • Subject: [Frama-c-discuss] Value analysis: resulting intervals after loop
  • From: matthieu.lemerre at cea.fr (Matthieu Lemerre)
  • Date: Thu, 06 Apr 2017 14:00:12 +0200
  • In-reply-to: <CAK2NOcUOtCjhHQNBEc7rOBGk-Bm7=vt0ERkQ3OiZvKseLZyTLA@mail.gmail.com>
  • References: <CAK2NOcUOtCjhHQNBEc7rOBGk-Bm7=vt0ERkQ3OiZvKseLZyTLA@mail.gmail.com>
Dear Sergio,

The code that you are analyzing is incorrect: the C standards forbides
overflow of signed integers on a left shift operation. Value simplifies
the approximation of possible values based on this, which explains why
you do not have the result that you expected.

You have to replace the bogus code i <<= 1; by (unsigned int) i <<=
1. If you do this, you will have ix ∈ [-149..128] as you expected.

Best regards,
Matthieu Lemerre

Sergio Feo <sergio.feo at gmail.com> writes:

> Dear all,
> we have a particular scenario where we are unable to explain the results
> reported by Frama-C. Any pointers would be greatly appreciated.
>
> We are analyzing the sun newlib math library (
> ftp://sourceware.org/pub/newlib/newlib-2.4.0.tar.gz) from where we have
> extracted the following snippet:
>
> #include <stdint.h>
>
> typedef union {
>     float value;
>     int32_t word;
> } ieee_float_shape_type;
>
> void main(float x) {
>     int32_t hx;
>     ieee_float_shape_type temp_u;
>
>     temp_u.value = x;
>     hx = temp_u.word;
>     hx &= 0x7FFFFFFF;
>
>     int i, ix;
>
>     if (hx < 0x0080000L) {
>         ix = -126;
>         Frama_C_show_each_ix_before(ix);
>         i = hx << 8;
>         while (i > 0) {
>             ix --;
>             Frama_C_show_each_ix_loop(ix);
>             i <<= 1;
>         }
>     }
>     else {
>         ix = (hx >> 23) - 127;
>         Frama_C_show_each_ix_else(ix);
>     }
>     Frama_C_show_each_ix_after(ix);
> }
>
> we are interested in the possible values of variable 'ix' at the end of the
> function.
>
> Running value analysis with a sufficiently large slevel (30 for example)
> outputs:
>
> [value] Called Frama_C_show_each_ix_before({-126})
> [value] Called Frama_C_show_each_ix_else([-127..128])
> [value] Called Frama_C_show_each_ix_loop({-127})
> [value] Called Frama_C_show_each_ix_loop({-128})
> [value] Called Frama_C_show_each_ix_loop({-129})
> [value] Called Frama_C_show_each_ix_loop({-130})
> [value] Called Frama_C_show_each_ix_loop({-131})
> (...)
> [value] Called Frama_C_show_each_ix_loop({-132})
> [value] Called Frama_C_show_each_ix_loop({-133})
> [value] Called Frama_C_show_each_ix_loop({-134})
> [value] Called Frama_C_show_each_ix_loop({-135})
> [value] Called Frama_C_show_each_ix_loop({-136})
> [value] Called Frama_C_show_each_ix_loop({-137})
> [value] Called Frama_C_show_each_ix_loop({-138})
> [value] Called Frama_C_show_each_ix_loop({-139})
> [value] Called Frama_C_show_each_ix_loop({-140})
> [value] Called Frama_C_show_each_ix_loop({-141})
> [value] Called Frama_C_show_each_ix_loop({-142})
> [value] Called Frama_C_show_each_ix_loop({-143})
> [value] Called Frama_C_show_each_ix_loop({-144})
> [value] Called Frama_C_show_each_ix_loop({-145})
> [value] Called Frama_C_show_each_ix_loop({-146})
> [value] Called Frama_C_show_each_ix_loop({-147})
> [value] Called Frama_C_show_each_ix_loop({-148})
> [value] Called Frama_C_show_each_ix_loop({-149})
> [value] Called Frama_C_show_each_ix_after([-127..128])
> [value] Called Frama_C_show_each_ix_after({-126})
> [value] Recording results for main
> [value] done for function main
> [value] ====== VALUES COMPUTED ======
> [value] Values at end of function main:
>   hx ∈ [0..2147483647]
>   temp_u{.value; .word} ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
>   i ∈ {0} or UNINITIALIZED
>   ix ∈ [-127..128]
>
> Observing the if branch, that is, the 'before' and 'loop' values for ix,
> one would expect that the corresponding 'after' value is the interval
> [-149,-126]. However, it is reported to be only {-126}.
>
> The result for the else branch is correctly reported as [-127..128] and
> thus, the resulting values of ix at the end of the function are reported as
> [-127..128], where the expected values would be [-149,128].
>
> The consequences of this issue are incorrect reports of dead code in the
> library we are analyzing.
>
> Again, we would greatly appreciate any pointers to what could be happening
> in this case.
>
> Best regards,
> -- Sergio
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss