Frama-C Framework for Modular Analysis of C programs

[1van]

Available plug-ins (https://frama-c.com/plugins.html)

Three heavyweight plug-ins that are used by the other plug-ins:

• Evolved Value analysis (EVA)
  This plug-in computes variation domains for variables. It is quite automatic, although the user may guide the analysis in places. It handles a wide spectrum of C constructs. This plug-in uses abstract interpretation techniques.
  
  
  
  
• Jessie and Wp, two deductive verification plug-ins
  These plug-ins are based on weakest precondition computation techniques. They allow to prove that C functions satisfy their specification as expressed in ACSL. These proofs are modular: the specifications of the called functions are used to establish the proof without looking at their code.
  
  
  

The availability of the above three plug-ins make it possible to write additional plug-ins that provide a wide palette of possibilities with relatively little effort. Here is a non-exhaustive list of plug-ins that have already been written and are distributed with Frama-C. Note that some of these plug-ins are still in development.

For browsing unfamiliar code:

• Impact analysis
  This plug-in highlights the locations in the source code that are impacted by a modification.
  
  
• Scope & Data-flow browsing
  This plug-in allows the user to navigate the dataflow of the program, from definition to use or from use to definition.
  
  
• Variable occurrence browsing
  Also provided as a simple example for new plug-in development, this plug-in allows the user to reach the statements where a given variable is used.
  
  
  
  
• Metrics calculation
  This plug-in allows the user to compute various metrics from the source code.
  

For code transformation:

• Semantic constant folding
  This plug-in makes use of the results of the evolved value analysis plug-in to replace, in the source code, the constant expressions by their values. Because it relies on EVA, it is able to do more of these simplifications than a syntactic analysis would.
  
  
• Slicing
  This plug-in slices the code according to a user-provided criterion: it creates a copy of the program, but keeps only those parts which are necessary with respect to the given criterion.
  
  
• Spare code: remove "spare code", code that does not contribute to the final results of the program.
  
  
• E-ACSL: translate annotations into C code for runtime assertion checking.
  
  
  

For verifying functional specifications:

• Aoraï: verify specifications expressed as LTL (Linear Temporal Logic) formulas
  
  
• Other functionalities documented together with the EVA plug-in can be considered as verifying low-level functional specifications (inputs, outputs, dependencies,…)
  

For test-case generation:

• PathCrawler automatically finds test-case inputs to ensure coverage of a C function. It can be used for structural unit testing, as a complement to static analysis or to study the feasible execution paths of the function.
  
  

For concurrent programs:

• Mthread
  This plug-in automatically analyzes concurrent C programs, using the EVA plug-in, taking into account all possible thread interactions. At the end of its execution, the concurrent behavior of each thread is over-approximated, resulting in precise information about shared variables, which mutex protects a part of the code, etc.
  

Front-end for other languages

• Frama-Clang
  This plug-in provides a C++ front-end to Frama-C, based on the clang compiler. It transforms C++ code into a Frama-C AST, which can then be analyzed by the plug-ins above. Note however that it is very experimental and only supports a subset of C++11