Sujet : Représentation de programmes sous forme d'automates



Responsable : Emmanuel Fleury

Présentation du sujet : Afin de permettre la vérification de code, nous cherchons à traduire les programmes livrés sous la forme d'un code source qui compile en un automate qui manipule des entiers et des flottants.
Pour ce faire, nous voudrions pouvoir utiliser GCC pour traduire les codes source qu'il compile directement en automate (au format texte). Il se trouve que GCC traduit la plupart des langages qu'il compile en un format intermédiaire (GIMPLE) qui ressemble à un C simplifié.
On peut voir ce format en faisant par exemple: gcc -O2 -fdump-tree-all-blocks-lineno moncode.c
Le fichier supplémentaire qui apparaît fait apparaître les fonctions du fichier moncode.c sous la forme d'un CFG (Control Flow Graph) qui n'a pas tout à fait le format d'un automate.
Il existe de plus, un projet non-officiel de GCC permettant de lui adjoindre des plugins. Ce projet est stocké sous la forme d'une branche sur le dépôt officiel SVN de GCC:
svn co svn://gcc.gnu.org/svn/gcc/branches/plugin gcc-plugin
Voir: http://gcc.gnu.org/svn.html
Une documentation (succinte) pour ce framework peut être trouvée sur: http://www.labri.fr/~fleury/courses/misc/GCC-Plugins.pdf
Le but de ce projet est de faire un plugin pour GCC qui permet de construire l'automate correspondant à une fonction C contenue dans un fichier.