Skip to Main content Skip to Navigation
Conference papers

Rester statique pour devenir plus rapide, plus précis et plus mince

Arvid Jakobsson 1, 2 Nikolai Kosmatov 1 Julien Signoles 1, *
* Corresponding author
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Résumé : 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.Cet article présente deux analyses statiques qui améliorent grandement la précision de cette transformation de programme 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 permettant de distinguer les entiers (mathématiques) pouvant être convertis en des expressions C de type <> de ceux devant être traduits vers des entiers en précision arbitraire. La seconde analyse est une analyse flot de données arrière 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/hal-01096352
Contributor : David Baelde <>
Submitted on : Wednesday, December 17, 2014 - 12:30:12 PM
Last modification on : Saturday, May 1, 2021 - 3:49:14 AM
Long-term archiving on: : Monday, March 23, 2015 - 3:00:41 PM

File

jfla15_submission_1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01096352, version 1

Citation

Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles. Rester statique pour devenir plus rapide, plus précis et plus mince. Vingt-sixièmes journées francophones des langages applicatifs, Jan 2015, Le Val d'Ajol, France. ⟨hal-01096352⟩

Share

Metrics

Record views

260

Files downloads

129