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).
- Follow-Ups:
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: moy at adacore.com (Yannick Moy)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Prev by Date: [Frama-c-discuss] Valid physical address
- Next by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Previous by thread: [Frama-c-discuss] Valid physical address
- Next by thread: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Index(es):