Tools for Program Understanding

Frama-C can operate as an exploration framework: several plug-ins and scripts have been created to enable tool-assisted code exploration and understanding. Unassisted reviews of C code require deep expertise and knowledge of many of C ’s pitfalls; Frama-C should help overcome many of its quirks, to help ensure that “all bugs are shallow”. Whether you want some simple metrics and an overview; or you need to quickly evaluate code written by others; or you seek deep understanding about the origin of a complex bug, several Frama-C plug-ins are available to help you. This chapter presents these plug-ins and provides pointers for further details.