< Retour au sommaire
Calcul de différences entre Arbres Syntaxiques pour l'Analyse Incrémentale
Julie Brunet le
Lieu: Salle 1073
Suivre en visio
Résumé
L’analyse de programme incrémentale est un procédé qui permet d’accélérer considérablement l’analyse d’un programme lorsqu’un résultat a déjà été obtenu sur un code proche. Pour réaliser une telle analyse, il est nécessaire de comparer deux versions d’un programme afin d’identifier leurs similarités, aussi bien au niveau de sa structure (fonctions, boucles, etc.) qu’au niveau sémantique.
Dans cet objectif, nous développons un algorithme de différence d’arbres syntaxiques, plus adapté que des algorithmes de différence textuelle plus traditionnels : ils peuvent prendre en compte la structure des programmes analysés et répondre aux besoins spécifiques de l’analyse incrémentale. Par exemple, dans le cas d’un programme dans lequel seul l’ordre des fonctions a été modifié, un algorithme de différence textuelle conclura que les deux versions sont très différentes, alors qu’un algorithme de différence d’arbres syntaxiques détectera que la structure de l’arbre est inchangée. Dans cet exemple, il sera possible de réutiliser entièrement les résultats de l’analyse précédente.
Notre algorithme est destiné à être utilisé avec Frama-C / Eva, un analyseur basé sur l’interprétation abstraite qui a fait l’objet de travaux récents pour
être rendu incrémental. En particulier, nous nous intéressons aux modifications des boucles, car leur analyse est très coûteuse en temps pour Frama-C / Eva.
Dans cet exposé, je présenterai l’algorithme de correspondance d’arbres syntaxiques que j’ai conçu et implémenté dans Frama-C.