Frama-C

Architecture

• Value analysis computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation techniques and many other plugins make use of its results.
• Jessie verifies properties in a deductive manner. Jessie relies on the Why or Why3 back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Coq or Why. Using Jessie, or can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic.
• WP similar to Jessie, verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. WP can optionally use the Why3 platform to invoke many other automated and interactive provers.
• Impact analysis highlights the impacts of a modification in the C source code.
• Slicing enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties.
• Spare code removes useless code from a C program.

• Dominators computes dominators and postdominators of statements.
• From analysis computes functional dependencies.

  Features

• To understand C code which you have not written. In particular, Frama-C enables one to observe a set of values, slice the program into shorter programs, and navigate in the program.
• To prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers.
• To enforce coding standards or code conventions on C source code, by means of custom plugin
• To instrument C code against some security flaws