Abstract FR:

Nous proposons dans cette these une technique d'analyse semantique statique des programmes c elaboree a partir de l'evaluation partielle et de l'evaluation symbolique. La premiere methode consiste a reduire un programme en fixant la valeur d'un sous-ensemble de ses parametres pour obtenir un programme residuel ayant la meme semantique que l'original pour ces valeurs ; la seconde consiste a evaluer le programme en propageant dans son code des symboles de valeurs donnes arbitrairement a ses variables d'entree. L'evaluation partielle symbolique (eps) que nous proposons est une synthese de ces deux methodes. Son but est non seulement de verifier statiquement la semantique d'un programme c donne, en detectant statiquement des erreurs run-time comme dans l'evaluation symbolique, mais egalement de calculer un programme residuel dont la semantique est une abstraction de celle du programme original (et non pas une semantique equivalente comme dans le cas de l'evaluation partielle). Cette methode presente le caractere statique (off-line) de l'evaluation partielle et le caractere flow sensitive de l'evaluation symbolique. Ainsi l'interet du programme residuel est double: d'une part sa representation est debarrassee de tout ce qui ne contribue pas directement a sa semantique, d'autre part chacun de ses chemins d'executions possibles est distingue des autres ; ainsi il se prete a diverses utilisations ulterieures, par exemple d'autres analyses ou des series de tests, une bonne partie du travail etant alors deja effectuee