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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Sat, 5 May 2012 00:24:55 +0200
David Mentr? wrote:

> So, if I understand correctly, using an array t[] in a code will
> multiply the number of propagated states, because the possible values
> for the array are taken into account.

No.

You have seen a few examples where the presence of an array t[]
was a catalyst in multiplying the number of propagated states. One
was your original example with nested loops. Another was specially
crafted by my facetious colleague Boris to illustrate one other particularity.
Your statement above, as a general statement about Frama-C's
value analysis, is extremely misleading and is a bad way to
summarize or remember how it works. The slevel option separates
abstract paths, and optionally user-provided ACSL disjuncts,
not ?possible values for the array?.

> So if I have code linear like:
> """
> ... = ... t1[i] ....
> ...
> t2[j] = ...
> """
> then all possible values for t1[] and t2[] arrays will be taken into
> account, thus increasing the need for a high -slevel for a precise
> analysis.

No. Unlike the previous statement which, despite being generally false,
is true about some particular examples, this statement is simply
always false. The -slevel option has no effects at all on the analysis
of a linear code without ACSL disjunctions. If you identify a piece of
linear code on which the option -slevel has an effect, feel free
to report it as a bug.

I do not think that the Q&A format is going to work to transmit the
fundamentals. My case rests on recent discussions on this list
(including this thread).
I would recommend that anyone interested in the subject reads up
on abstract interpretation, the technique on which the value analysis
is loosely based (as I think the manual mentions).