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 lesson on runtime with Frama-C, publicly available toolset for analysis C programs. We illustrate how can be in executable specification language e-acsl and this automatically translated into instrumented code suitable monitoring verification show various errors detected the code, including errors, failures postconditions, assertions, preconditions called functions, memory leaks. Benefits combining other Frama-C analyzers are illustrated as well.