--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds



Hello,

I am doing some Value analysis (with Frama-C Nitrogen) on a code that
has the same structure that the attached example. Roughly, this code
is made of two for loops, j and k, one inside the other.

* First basic analysis

I run:
   frama-c -cpp-command 'gcc -E -C -I. ' -val -slevel 100
/usr/local/share/frama-c/builtin.c array_loop.c

The loop bounds are correctly computed, with acceptable approximation.

[value] Values for function F:
          min ? {15}
          max ? {35}
          j ? {35}
          k ? [34..50]


* Addition of an array access

Now, if I add a simple array access, that simply reads k:
  frama-c -cpp-command 'gcc -E -C -I. -DOUT_ACCESS' -val -slevel 100
/usr/local/share/frama-c/builtin.c array_loop.c

Then the loop bound for k is wrongly approximated, k ? [34..143]. The
143 upper bound is clearly far from the real bound, 50.

[value] Values for function F:
          Frama_C_entropy_source ? [--..--]
          min ? {15}
          max ? {35}
          j ? {35}
          k ? [34..143]

The point I don't understand is why adding a *read* access on k
variable makes the bound computation on k so bad? I am not modifying k
in any way, so that for me Value analysis should give the same
approximation (k ? [34..50]).

Of course, if I increase slevel to 620 ( j range * k range == (35-15)
* 31) ) the k value is correctly computed.

I am asking this question because the real code I am analysing has the
same overall structure (the two loops with the same numerical bound in
a first step) but with a lot of linear computations inside them : it
computes the value of several variables, the new ones form the
previous ones, reading the 'in' array and writing the 'out' one. I
need to increase a *lot* slevel, up to 10,000, to get a correct result
on k bound. Using the 620 slevel value does not compute the correct
bound on k. I don't understand why.

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: array_loop.c
Type: text/x-csrc
Size: 1101 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120427/5d255684/attachment.c>