Frama-Clang

Frama-Clang logo

Overview

Frama-Clang is a plugin that allows Frama-C to take as input C++ programs. As its name implies, it is based on the clang compiler, the C/C++/Objective-C front-end of the llvm platform. More precisely, Frama-Clang is composed of two parts: a clang plugin (written in C++) that produces a simplified version of the clang AST, and a normal Frama-C plugin that takes as input this simplified version and produces a normal Frama-C AST.

When this plug-in is in use, Frama-C will consider all files ending in .cpp, .c++, .C, .cxx, .cc and .ii (considered as already pre-processed) as C++ files and give them to Frama-Clang to translate them into Frama-C’s internal representation (i.e. a plain C AST). Once this has been done, any existing analyses can be launched as usual.

Caveat: Frama-Clang is currently in an early stage of development. It is known to be incomplete and comes without any bug-freeness guarantees. Moreover, the translation from C++ to C does not make any attempts to optimize the resulting code for the back-end analyzers such as Eva or WP. Further work is thus needed before Frama-Clang can claim to be a grown-up plug-in. Feel free to contact us if you’re interested in participating in its maturation.

Further Reading

For more details about Frama-Clang plug-in, please consult the Frama-Clang manual.

Installation

Download

The current version is 0.0.9. The frama-clang plugin can be downloaded here.

Requirements

  • Frama-C 21.x Scandium
  • OCaml 4.05.0 or higher, the same version as the one used to compile Frama-C itself
  • camlp5 (a version compatible with the OCaml version you’re using)
  • clang and libclang >= 6 (preferably 9 or 10)

You also need llvm-config (llvm-config-x.y for Debian and Ubuntu users, as explained in this bug report).

Installation steps

tar xzvf frama-clang-0.0.9.tar.gz
cd frama-clang-0.0.9
./configure
make
make install

Depending on your Frama-C installation, this last step might require root permissions.

Changes

v0.0.9

  • Compatibility with Frama-C 21.x Scandium
  • Compatibility with Clang 10.0
  • Support for implicit initialization of POD objects.

v0.0.8

  • Compatibility with Frama-C 20.0 Calcium
  • Compatibility with Clang 9.0
  • Proper conversion of ghost statements
  • Support for \exit_status in ACSL++
  • C++ part of the plug-in is now free from g++ warnings
  • move away from camlp4 in favor of camlp5

v0.0.7

  • Compatibility with Frama-C 19.x Potassium
  • Compatibility with Clang 6.0, 7.0 and 8.0
  • Rewritten ACSL++ parser, providing easier extensibility and maintenance
  • Frama-Clang now has a manual
  • Improved support of STL
  • Preliminary support for lambdas
  • Improved support of template instantiations

v0.0.6

  • Compatibility with Frama-C 17 Chlorine

v0.0.5

  • Compatibility with Clang/LLVM as packaged by Debian/Ubuntu

v0.0.4

  • Compatibility with Frama-C 16 Sulfur
  • Compatibility with Clang/LLVM 5.0.0
  • Improved translation for const-qualified objects
  • Fixes translation of implicit functions for classes with virtual inheritance

v0.0.3

  • Compatibility with Frama-C 15 Phosphorus
  • Improved handling of constructors and destructors for local variables

v0.0.2

  • Compatibility with Frama-C 14 Silicon
  • Adding compatibility with Clang/LLVM 3.9.0 and 4.0.0
  • Various fixes in support of virtual inheritance and templates
  • Better support for parsing GNU STL headers

v0.0.1

  • Initial release

Previous versions

  • 0.0.8 compatible with Frama-C 20.0
  • 0.0.7 compatible with Frama-C 19.x
  • 0.0.6 compatible with Frama-C 17.0
  • 0.0.5 compatible with Frama-C Sulfur-20171101
  • 0.0.5 compatible with Frama-C Sulfur-20171101
  • 0.0.3 compatible with Frama-C Phosphorus-20170501
  • 0.0.2 compatible with Frama-C Silicon-20161101
  • 0.0.1 compatible with Frama-C Aluminium-20160502

The llvm wyvern logo is © Apple, inc