Skip to Main content Skip to Navigation
Conference papers

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
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:55 AM
Last modification on : Monday, February 10, 2020 - 6:14:14 PM

Links full text





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⟩



Record views