The Art of Developing Frama-C Plug-ins

One of the key features of Frama-C is its extensibility. More precisely, the platform is based on a kernel, which provides the core services and datastructures that are needed for analyzing C programs, including in particular parsing C and ACSL code. Analyses themselves are then implemented by plug-ins, that use the kernel’s API to, among other things, access the code under analysis, perform some code transformation, add ACSL annotations, and validate (or invalidate) other ACSL annotations. Furthermore, plug-ins can also export their own API to be used by other plug-ins. In this chapter, we will give an overview of Frama-C ’s general architecture and describe the main functionalities of the kernel, using as example a small plug-in that we build step by step during the course of the chapter.