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] Issue understanding Value analysis approximation on loop bounds

  • Subject: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Fri, 27 Apr 2012 10:06:23 +0200
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>