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

Arvid Jakobsson 1, 2 Nikolai Kosmatov 1 Julien Signoles 1, *
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes journées francophones des langages applicatifs, Jan 2015, Le Val d'Ajol, France. Actes des vingt-sixièmes journées francophones des langages applicatifs, 〈http://jfla.inria.fr/2015〉
Liste complète des métadonnées

Littérature citée [3 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01096352
Contributeur : David Baelde <>
Soumis le : mercredi 17 décembre 2014 - 12:30:12
Dernière modification le : lundi 25 juin 2018 - 13:17:21
Document(s) archivé(s) le : lundi 23 mars 2015 - 15:00:41

Fichier

jfla15_submission_1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. David Baelde; Jade Alglave. Vingt-sixièmes journées francophones des langages applicatifs, Jan 2015, Le Val d'Ajol, France. Actes des vingt-sixièmes journées francophones des langages applicatifs, 〈http://jfla.inria.fr/2015〉. 〈hal-01096352〉

Partager

Métriques

Consultations de la notice

175

Téléchargements de fichiers

95