A Lesson on Runtime Assertion Checking with Frama-C

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.