2015-jfla-jks.md

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.