[SOS] Actualité du noyau

David MENTRE dmentre at linux-france.org
Sam 17 Sep 15:06:22 CEST 2005


Salut Thomas,

Thomas Petazzoni <thomas.petazzoni at enix.org> writes:

>  - un résumé de l'actualité du noyau de la dernière semaine [2]
> [2] http://thomas.enix.org/Blog-20050917022607-Technologie

Très intéressant, comme d'habitude.

Dans la série des analyseurs de code C, il y a :

 - CIL http://manju.cs.berkeley.edu/cil/

   C'est un framework pour parser du C (avec les extensions gcc) et en
   sortir une version normalisée pour faire des analyses dessus. Un
   certain nombre d'analyses sont déjà proposées (data flow,
   dominateurs, pointeurs, StackGuard, ...) ;

 - Cqual http://www.cs.umd.edu/~jfoster/cqual/

   Inférence de type sur du code C/C++ pour vérifier des propriétés ;


 - CCured http://manju.cs.berkeley.edu/ccured/

   Insertion de vérifications dans un programme pour garantir que les
   allocations mémoires sont sans soucis ;


 - Smatch!! http://smatch.sourceforge.net/

   La version libre du Stanford Checker.


<pub>Tout ça est sur la page que je maintiens à propos des outils libres
pour la vérif formelle
http://gulliver.eu.org/ateliers/fv-tools/fv-tool-list.html </pub>


J'ai l'impression que les développeurs du noyau ont tendance à
réinventer la roue, Linus en tête (GIT, Sparse). Je ne nie pas l'interêt
de le faire pour eux (c'est comme SOS), mais j'ai l'impression qu'ils
refont parfois ce que d'autres pourraient mieux faire qu'eux.


Amicalement,
d.
-- 
pub  1024D/A3AD7A2A 2004-10-03 David MENTRE <dmentre at linux-france.org>
 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A



Plus d'informations sur la liste de diffusion Sos