Account Options

  1. Sign in
The old Google Groups will be going away soon.
Switch to the new Google Groups.
Google Groups Home
« Groups Home
Outil d'analyse de code C
There are currently too many topics in this group that display first. To make this topic appear first, remove this option from another topic.
There was an error processing your request. Please try again.
flag
  2 messages - Collapse all  -  Translate all to Translated (View all originals)
The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 
From:
To:
Cc:
Followup To:
Add Cc | Add Followup-to | Edit Subject
Subject:
Validation:
For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon. Listen and type the numbers you hear
 
Jean-Marc Desperrier  
View profile   Translate to Translated (View Original)
 More options Nov 27 2008, 7:58 am
Newsgroups: fr.comp.lang.c, fr.comp.lang.c++, fr.comp.developpement
Followup-To: fr.comp.developpement
From: Jean-Marc Desperrier <jmd...@alussinan.org>
Date: Thu, 27 Nov 2008 13:58:36 +0100
Local: Thurs, Nov 27 2008 7:58 am
Subject: Re: [Pub] Outil d'analyse de code C

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.

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


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
David MENTRE  
View profile   Translate to Translated (View Original)
 More options Nov 27 2008, 1:50 pm
Newsgroups: fr.comp.developpement
From: David MENTRE <david.men...@gmail.com>
Date: Thu, 27 Nov 2008 19:50:06 +0100
Local: Thurs, Nov 27 2008 1:50 pm
Subject: Re: [Pub] Outil d'analyse de code C
Bonjour,

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é


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
End of messages
« Back to Discussions « Newer topic     Older topic »