Common Specification Language for Static and Dynamic Analysis of C Programs

Mickaël Delahaye 1 Nikolai Kosmatov 2 Julien Signoles 2
1 VASCO
LIG - Laboratoire d'Informatique de Grenoble
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.
Type de document :
Communication dans un congrès
Sung Y. Shin and José Carlos Maldonado. SAC 2013 - 28th ACM Symposium on Applied Computing, Mar 2013, Coimbra, Portugal. ACM, 2, pp.1230-1235, 2013, Proceedings of the 28th Annual ACM Symposium on Applied Computing (SAC 2013). 〈10.1145/248062.2480593〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00853721
Contributeur : Mickaël Delahaye <>
Soumis le : vendredi 23 août 2013 - 16:33:24
Dernière modification le : vendredi 16 mars 2018 - 01:12:42

Identifiants

Collections

CEA | LIG_GLSI_VASCO | LIG_GLSI | LIG | UGA | DRT | LIG_SRCPR | LIST

Citation

Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles. Common Specification Language for Static and Dynamic Analysis of C Programs. Sung Y. Shin and José Carlos Maldonado. SAC 2013 - 28th ACM Symposium on Applied Computing, Mar 2013, Coimbra, Portugal. ACM, 2, pp.1230-1235, 2013, Proceedings of the 28th Annual ACM Symposium on Applied Computing (SAC 2013). 〈10.1145/248062.2480593〉. 〈hal-00853721〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

230

Contact


archive-ouverte@inria.fr