Plugins Kernel Specification Ivette (GUI)

Frama-Clang

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

Opam

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)

Download

Frama-Clang has its own public git repository, whose master branch should always be synchronized with Frama-C’s own master branch. Since v0.0.12, all releases are available on this repository, together with their respective Changelog. Previous versions are kept below for historical purposes.

Old Versions

Changes

v0.0.12 and newer

See Public repository’s releases page

v0.0.11

  • Compatibility with Frama-C 23.x Vanadium
  • Compatibility with Clang 12.0
  • Slightly improved ACSL++ parsing
  • Various bug fixes

v0.0.10

  • 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.
  • header <cstdbool> undefines bool, true and false if they are macros (partial fix for https://git.frama-c.com/pub/frama-c/#2546)

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 _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.12: See public repository’s releases page
  • 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