Runtime Annotation Checking with Frama-C: The E-ACSL Plug-in

Runtime Annotation Checking (RAC) is a lightweight formal method consisting in checking code annotations written in the source code during the program execution. While static formal methods aim for guarantees that hold for any execution of the analyzed program, RAC only provides guarantees about the particular execution it monitors. This allows RAC-based tools to be used to check a wide range of properties with minimum intervention from the user. Frama-C can perform RAC on C programs with the plug-in E-ACSLE-ACSL . This chapter presents RAC through practical use with E-ACSLE-ACSL , shows advanced uses of E-ACSLE-ACSL leveraging the collaboration with other plug-ins, and sheds some light on the internals of E-ACSLE-ACSL and the technical difficulties of implementing RAC.