salle A. Turing CE4
5 juillet 2012 - 14h00
Collaboration d'analyses dans Frama-C
par Pascal Cuoq de CEA
Résumé : Frama-C est une plateforme collaborative d'analyse statique pour le langage C. Chaque technique ou idée peut être implémentée dans Frama-C sous la forme d'un greffon.
Un premier moyen de collaboration entre greffons est par le langage de spécification ACSL : l'analyse de valeurs, un greffon d'interprétation abstraite, insère dans le programme cible des assertions ACSL pour chaque comportement indéfini qu'elle est incapable d'exclure. Ces assertions peuvent être vérifiées par un autre greffon, tel qu'un greffon basé sur la logique de Hoare.
Un greffon particulier peut aussi rendre ses résultats disponibles à travers une interface programmatique adaptée. C'est ainsi que l'analyse de valeurs est utilisée par les greffons d'analyses de flots de contrôle et de données dont les résultats sont in fine exploités par des greffons de vérification propriétaires [1].
Cette présentation se concentrera sur l'analyse de valeurs de Frama-C et ses interfaces programmatiques.
[1] Fan-C, a Frama-C plug-in for data flow verification http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf
