Skip to Main content Skip to Navigation
Conference papers

Common Specification Language for Static and Dynamic Analysis of C Programs

Mickaël Delahaye 1 Nikolai Kosmatov 2 Julien Signoles 2
1 VASCO - Validation de Systèmes, Composants et Objets logiciels
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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/hal-00853721
Contributor : Mickaël Delahaye <>
Submitted on : Friday, August 23, 2013 - 4:33:24 PM
Last modification on : Friday, June 25, 2021 - 9:52:03 AM

Identifiers

Collections

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

Citation

Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles. Common Specification Language for Static and Dynamic Analysis of C Programs. SAC 2013 - 28th ACM Symposium on Applied Computing, Polytechnic Institute of Coimbra (IPC), Mar 2013, Coimbra, Portugal. pp.1230-1235, ⟨10.1145/248062.2480593⟩. ⟨hal-00853721⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

440

 

Contact                    Legal Notice                    Personal Data