Abstract FR:

De nombreux langages de programmation fournissent un support natif pour les exceptions : lever une exception a un endroit du programme transfere le controle au gestionnaire pour cette exception le plus proche dans la pile des appels dynamiques du programme. Les exceptions fournissent donc un moyen simple et flexible de gestion des erreurs dans les applications. Neanmoins, en l'absence de gestionnaire pour une exception levee, celle-ci mettra fin prematurement a l'execution du programme. Ce style de terminaison sur erreur affaiblit donc la robustesse et la fiabilite des programmes. Le but de cette these est donc de realiser un outil d'analyse permettant de predire les exceptions pouvant mettre terme a l'execution des programmes. Ce travail etudie donc la theorie et l'implementation d'un tel analyseur base sur un systeme de types et d'effets utilisant un mecanisme de rangees afin d'approximer a la fois le flot des exceptions non rattrapees et le flot des valeurs. Il expose le cadre theorique de l'analyse, etablit formellement ses proprietes et montre sa capacite a etre etendu a un langage de taille reelle comme objective caml. Par ailleurs cette these decrit un nouvel algorithme d'inference de types en presence de recursion polymorphe pour ml. En effet, il apparait que cette technique peut servir a rendre plus precis les resultats de notre analyse. Cet algorithme presente les interets d'etre formalise dans le cadre d'un typeur avec niveaux (c'est-a-dire suivant le principe reel d'un typeur ml efficace), d'etre rapide et de rejeter extremement peu de programmes (car ce type d'inference etant connue pour etre indecidable seule une restriction des programmes acceptes peut mener a un algorithme). Ce travail aboutit a l'implantation effective d'un analyseur d'exceptions pour et en objective caml, accompagne d'une interface utilisateur rendant l'acces aux resultats de l'analyse plus aisee.