Re: [Pub] Outil d'analyse de code C
Jean-Marc Desperrier
> [...]
> un peu de pub. Je sors d'une présentation de l'outil
> coccinelle. C'est un truc qui fait de la détection
> de patern suspect dans un code (un kmalloc sans
> le kfree associé par exemple).
>
> Pour ceux que les avancées sur l'analyse de code C
> intéressent.
>
> http://www.emn.fr/x-info/coccinelle/
Hum, franchement aujourd'hui, je pense que ce type d'outils a peu de
perspectives d'avenir, quand on voit les perspectives qu'ouvrent
Dehydra, Treehydra (diagnostique), et Oink/Pork (réécriture) dans le
domaine.
https://developer.mozilla.org/en/Dehydra
https://developer.mozilla.org/en/Treehydra
https://developer.mozilla.org/en/Pork
http://www.cubewano.org/oink
Un "super diff/patch" n'a plus trop d'avenir quand il existe par
ailleurs des outils qui s'appuient sur gcc (un parseur C/C++ indépendant
pour Oink/Pork) pour travailler avec la structure interprétée *exacte*
du code.
Il y a quelques exemples d'utilisation ici:
http://hg.mozilla.org/mozilla-central/file/fdd5e4e34241/xpcom/analysis/
L'un des gros trucs qui est fait actuellement avec ces outils dans le
code Mozilla est de s'assurer qu'une fonction soit retourne un code
d'erreur OK et fixe la valeur de tous les arguments, ou bien renvoie un
code d'erreur et ne touche à aucun argument en sortie.
Voir à ce sujet la description de la technique ESP pour analyser le flux
d'une fonction en temps polynomial:
http://www.cs.cornell.edu/courses/cs711/2005fa/papers/dls-pldi02.pdf
https://developer.mozilla.org/Treehydra_Manual#section_8
Je pense que ces outils ne peuvent que prendre beaucoup d'importance,
car le fait qu'ils donnent des résultats exacts (au besoin, en
s'appuyant sur des techniques de récursivité) change complètement la
perspective.
Suivi redirigé vers fr.comp.developpement
David MENTRE
Jean-Marc Desperrier <jmd...@alussinan.org> writes:
> Marc Boyer wrote:
>> [...]
>> un peu de pub. Je sors d'une présentation de l'outil
>> coccinelle. C'est un truc qui fait de la détection
>> de patern suspect dans un code (un kmalloc sans
>> le kfree associé par exemple).
>>
>> Pour ceux que les avancées sur l'analyse de code C
>> intéressent.
>>
>> http://www.emn.fr/x-info/coccinelle/
>
> Hum, franchement aujourd'hui, je pense que ce type d'outils a peu de
> perspectives d'avenir, quand on voit les perspectives qu'ouvrent
> Dehydra, Treehydra (diagnostique), et Oink/Pork (réécriture) dans le
> domaine.
>
> https://developer.mozilla.org/en/Dehydra
> https://developer.mozilla.org/en/Treehydra
> https://developer.mozilla.org/en/Pork
> http://www.cubewano.org/oink
>
> Un "super diff/patch" n'a plus trop d'avenir quand il existe par
> ailleurs des outils qui s'appuient sur gcc (un parseur C/C++ indépendant
> pour Oink/Pork) pour travailler avec la structure interprétée *exacte*
> du code.
Je ne suis pas sûr que les outils cités soient antinomiques.
En tout état de cause, si ces outils de vérification formelle de code
vous intéressent, je vous invite à jeter un coup d'oeil sur la partie «
Tools to help verification of real programs » de la page suivante :
http://gulliver.eu.org/wiki/FreeSoftwareForFormalVerification
On y trouve des outils comme Why, Frama-C, Sparse, ...
Si vous connaissez d'autres outils libres répondant à ces besoins, dites
le moi ou mieux éditez directement la page, c'est un wiki.
Amicalement,
d.
--
David Mentré