A lesson on runtime assertion checking with Frama-C

Abstract : Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834991
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:55 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

N. Kosmatov, J. Signoles. A lesson on runtime assertion checking with Frama-C. Runtime Verification. RV 2013. Lecture Notes in Computer Science, Sep 2013, Rennes, France. pp.386-399, ⟨10.1007/978-3-642-40787-1_29⟩. ⟨cea-01834991⟩

Share

Metrics

Record views

69