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] Value analysis plug-in algorithms
- Subject: [Frama-c-discuss] Value analysis plug-in algorithms
- From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
- Date: Fri Nov 14 16:21:33 2008
- In-reply-to: <bacfeaa40811140556i5d398caby18ce9b6fc562e302@mail.gmail.com>
- References: <bacfeaa40811140556i5d398caby18ce9b6fc562e302@mail.gmail.com>
> > I'm very impressed by the accuracy of the variation domains this > plugin can compute and I would be very interested to know which > techniques are used to achieve this, even more interested in good > papers describing those techniques. So if anyone here have a few > hints on this, it would be of a great help to me. Hi! The value analysis plug-in uses the "Abstract Interpretation" techniques introduced in the seminal article available here: http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml The integer values and the offsets of addresses are sometimes represented as intervals with additional congruence information. The use of this last part of the information as an abstract domain was first described by Granger in an article named "Static analysis of arithmetical congruences" (1989). Gentle introductions to the general theory of abstract interpretation are for instance the slides on this page: http://www.labri.fr/perso/sutre/Teaching/INF555/ or the course notes available on this page: http://www.di.ens.fr/~cousot/Marktoberdorf98.shtml The design of better abstract domains is the topic of active research, but the new domains being defined nowadays are pretty much all relational domains -- that is, these domains are able to represent relations between variables, such as for instance "x == (y + 2)". When interpreting variables as intervals individually (for instance y -> [0..10] and x -> [2..12]), this information is typically lost. The value analysis plug-in inside Frama-C is able to represent only a few such relations, and only so as to be able to tell that two pointers point to the same memory location (please see the file test/misc/alias.c for some examples where the analysis is able to extract some relations). I would be personally interested in seeing examples where the value analysis produces useful results, and even more in examples where it could be improved, inasmuch as it would be possible for you to show us these examples. Pascal
- References:
- [Frama-c-discuss] Value analysis plug-in algorithms
- From: jsdslml at gmail.com (jsd slml)
- [Frama-c-discuss] Value analysis plug-in algorithms
- Prev by Date: [Frama-c-discuss] Value analysis plug-in algorithms
- Next by Date: [Frama-c-discuss] RE: [Why-discuss] New Frama-C release
- Previous by thread: [Frama-c-discuss] Value analysis plug-in algorithms
- Next by thread: [Frama-c-discuss] Jessie-patch release ???
- Index(es):