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
.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.
For more details about Frama-Clang plug-in, please consult the Frama-Clang manual.
Frama-Clang has an Opam package. Hence, if you already have Opam, installing Frama-Clang can be done easily with
opam install frama-clang (see Frama-C’s own installation instructions for more details on how to install opam if needed)
The current version is 0.0.14. The frama-clang plugin can be downloaded here.
Frama-Clang has its own public git repository, whose
master branch should always be synchronized with Frama-C’s own
- Frama-C 27.x Cobalt
- OCaml, 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 >= 11
You also need llvm-config (llvm-config-x.y for Debian and Ubuntu users, as explained in this bug report).
tar xjvf frama-clang-0.0.14.tar.bz2
Depending on your Frama-C installation, this last step might require root permissions.
- Compatibility with Frama-C 27.x Cobalt
- Compatibility with Clang 15 and 16
- Minimal supported Clang version is 11
- Compatibility with Frama-C 25.0 Manganese
libc++ (contributed by T-Gruber)
- Compatiblity with Frama-C 24.0 Chromium
- Compatibility with Clang 13.0 and 14.0
- Minimal supported Clang version is 10.0
- support for C++14 generic lambdas (contributed by S. Gränitz)
- options for printing reparseable code and using demangling on non-C++ sources
- Compatibility with Frama-C 23.x Vanadium
- Compatibility with Clang 12.0
- Slightly improved ACSL++ parsing
- Various bug fixes
- Compatibility with Frama-C 22.x Titanium
- Compatibility with Clang 11.0
- Don’t generate code for implicit member functions and operators when they’re not used.
- Don’t generate code for templated member functions that are in fact never instantiated.
false if they are macros (partial fix for https://git.frama-c.com/pub/frama-c/#2546)
- Compatibility with Frama-C 21.x Scandium
- Compatibility with Clang 10.0
- Support for implicit initialization of POD objects.
- Compatibility with Frama-C 20.0 Calcium
- Compatibility with Clang 9.0
- Proper conversion of ghost statements
- Support for _status in ACSL++
- C++ part of the plug-in is now free from g++ warnings
- move away from camlp4 in favor of camlp5
- 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
- Compatibility with Frama-C 17 Chlorine
- Compatibility with Clang/LLVM as packaged by Debian/Ubuntu
- Compatibility with Frama-C 16 Sulfur
- Compatibility with Clang/LLVM 5.0.0
- Improved translation for
- Fixes translation of implicit functions for classes with virtual inheritance
- Compatibility with Frama-C 15 Phosphorus
- Improved handling of constructors and destructors for local variables
- 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
- 0.0.13 compatible with Frama-C 25.0
- 0.0.12 compatible with Frama-C 24.0
- 0.0.11 compatible with Frama-C 23.0
- 0.0.10 compatible with Frama-C 22.0
- 0.0.9 compatible with Frama-C 21.0
- 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