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.