---
plugin: "e-acsl"
authors: "Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles"
title: "Rester statique pour devenir plus rapide, plus précis et plus mince"
book: "Journées Francophones des Langages Applicatifs (JFLA)"
link: http://julien.signoles.free.fr/publis/2015_jfla.pdf
year: 2015
category: other
short: "In French"
---

E-ACSL est un greffon de Frama-C, une plateforme d'analyse de codes C qui est
développée en OCaml. Son but est de transformer un programme C formellement
annoté dans le langage de spécification éponyme E-ACSL en un autre programme C
dont le comportement à l'exécution est équivalent si toutes les spécifications
sont dynamiquement vérifiées et qui échoue sur la première spécification
fausse sinon. Pour cela, une instrumentation du programme source est notamment
effectuée afin, d'une part, de conserver les informations nécessaires à
l'évaluation des prédicats E-ACSL et, d'autre part, de traduire correctement
ces derniers.

Cet article présente deux analyses statiques qui améliorent grandement la
précision de cette transformation de programmes en réduisant l'instrumentation
effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire
lors de son exécution. La première analyse est un système de types fondé sur
une inférence d'intervalles et permettant de distinguer les entiers
(mathématiques) pouvant être convertis en des expressions C de type "entier
machine" de ceux devant être traduits vers des entiers en précision
arbitraire. La seconde analyse est une analyse flot de données arrière
sur-approximante paramétrée par une analyse d'alias. Elle permet de limiter
l'instrumentation des opérations sur la mémoire à celles ayant un impact
potentiel sur la validité d'une annotation formelle.