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: moy at adacore.com (Yannick Moy)
- Date: Mon, 07 May 2012 10:26:29 +0200
- In-reply-to: <CAOH62JhAyq8W1m8T-U6Sb7hddQS2hW6LqrM2jP7JUf29yhbfxQ@mail.gmail.com>
- References: <CAOH62JhAyq8W1m8T-U6Sb7hddQS2hW6LqrM2jP7JUf29yhbfxQ@mail.gmail.com>
On 05/05/2012 12:24 AM, Pascal Cuoq wrote: > 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?. Hi David and Pascal, At the risk of saying something wrong, I'll try to explain what I think -slevel does. Abstract interpretation works by abstracting state. In Frama-C, state is abstracted at each program point using the value abstract domain, which, for integer values, is the same as the widely used interval abstract domain. So every integer value X in your code is abstracted as a range min..max at every program point. So, without slevel, the analysis of the following program only knows that i and j are in 0..1 after the if-statement, not that they are equal: //@ requires 0 <= i <= 1; void main(int i) { int j; if (i == 0) { j = 0; } else { j = 1; } //@ assert i == j; return; } This is because, at the join point after the if-statement, the analyzer "joins" (this is the abstract join operator of abstract interpretation) two states, one where i = j = 0 and one where i = j = 1. Now, if you set -slevel to 1, then the analyzer keeps these two states separate instead of merging them, so that it now knows that the assertion holds. The explanation of -slevel in Frama-C manual says this in a slightly more abstract way, and it also says that it has a similar effect as unrolling loops. Indeed, join points are everywhere the flow of control encounters another path, which occurs at the start of loops. > >> 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 believe that it is clear once you understand that -slevel has only an effect on the number of states that are kept separate at join points. On your example, David, there are no join points at all, so no effect of -slevel. > 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). One thing I found quite effective at conveying how the tool works, without going into the details of how it is implemented, is to show/discuss the detailed results on small examples. I have done it for our static analyzer CodePeer, and this works very well in trainings. Here is the online version if you want to have a look at it: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html (And it is quite fast to do for someone very familiar with the tool, it took me just one week. One thing you'd like though is that the document is generated from actual runs of the tool on the examples, so that it is kept up-to-date easily, which is what we did.) > 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). I don't think you need to read highly mathematical descriptions of abstract domains to understand what -slevel does. And I believe David knows much more than what is needed already. I agree with you that a tool has many tradeoffs that cannot be all documented (except in the code!), but surely that question of David can be answered simply like I just did. -- Yannick Moy, Senior Software Engineer, AdaCore
- 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
- References:
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Prev by Date: [Frama-c-discuss] Transformation of if-statements
- Next by Date: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Previous by thread: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Next by thread: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
- Index(es):