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] integer overflow

> Precise analysis of bit-style code such as 
> safe_signed_add_1() may be somewhat challenging for your abstract 
> domains.

To tell the truth, the analysis currently does not even try to compute
an abstract value for the results of | and ^, although there
would be things to say despite the fact the arguments are intervals and 
the result is expected as an interval.
Actually, I realize as I write this that all bitwise abstract functions
could be implemented with a generic function
that would morally be equivalent to
on-the-fly translation to bit-vector of the argument intervals and
translation of the result back to interval. This would be an excellent
occasion to get rid of the current (ugly, ad-hoc) implementation for &
and a welcome improvement for the other (unimplemented) bitwise
abstract functions.

But yes, even if the value analysis tried, it would have a hard time with
most of your functions.

>   However it would seem that purely arithmetic code such as 
> safe_signed_add_2() should be analyzable using a framework like Frama-C. 
>  Are octagons sufficient to precisely analyze safe_signed_add_2()?

Octagons should be sufficient, provided that all the appropriate
syntactic patterns for "octogonalisation" have been implemented.
I know that I am often disappointed that one is missing in Interproc
http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
when I go there to check something, but it is tedious to get
them all right.
We have plans to interface to APRON (a library from the authors
of Astr?e and others, which implements octagons
and other relational domains), but there are several refactoring steps
that need to be done before it's even possible to start the
interfacing per se.

> I can't tell if something a bit more powerful is needed, such as the 
>"decision tree abstract domain" described in the Astree PLDI paper.

As far as I can tell, the decision tree abstract domain uses boolean
variables (from the program) as nodes, by opposition to
boolean expressions, or even bits from integer program variables,
which is what analyzing your functions would need.
If that domain works as I understand it does, it would not help here
(but it works great for C code with a lot of if(c) statements,
which happens to be common in code generated by Scade,
and Astr?e was primarily designed to do well on code that had been
generated by Scade).

Pascal
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: application/ms-tnef
Taille: 4039 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090614/5d49bcaf/attachment.bin