Abstract FR:

L'objectif est de présenter une méthode permettant d'obtenir par analyse sémantique du code source d'un programme, des informations sur ce que sera la structure des données dynamiques (c'est à "tas") à l'exécution de ce programme. Pour cela, dans un premier temps, un treillis de graphes spécialisés (les "h-graphes") est construit Nous montrons que chaque h-graphe est une approximation sémantiquement correcte d'un ensemble d'états possibles de la mémoire dynamique, et présentons les primitives abstraites correspondantes à quelques primitives classiques d'un langage LISPien. Dans un deuxième temps, la question de l'analyse d'un langage LISPien utilisant des fonctions récursives et la portée dynamique est abordée. Une méthode permettant de résoudre ce problème délicat est présentée, et les éléments nécessaires à une preuve de correction sémantique sont donnés. Dans un troisième temps, enfin, un analyseur de Le_Lisp utilisant nos techniques est présenté, et quelques exemples d'analyse sont fournis. Les idées nécessaires à une adaptation de nos méthodes pour l'analyse d'un langage PASCALien sont données dans la thèse.