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

>
> 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