Plugins Kernel Specification GUI Ivette

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

The current stable version is 0.0.17. The frama-clang plugin can be downloaded here.
sha512: 2402446802b8369225dbfff15e0646b4b4567f7addb18fc633c6effac86b2abb9e9a35111189ad71e5aaf6acafd7b51436c898ed50283f52a435ffcafaada33. Installation instructions are available in the README

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.

Changes

v0.0.17

  • Compatibility with Frama-C 30.x Zinc

v0.0.16

  • Better handling of ACSL constructions
  • Compatibility with Clang 18
  • Compatibility with Frama-C 29.x Copper

v0.0.15

  • Better handling of mixed C/C++ code and extern "C" declarations
  • Compatibility with Clang 17
  • Compatibility with Frama-C 28.x Nickel

v0.0.14

  • Compatibility with Frama-C 27.x Cobalt
  • Compatibility with Clang 15 and 16
  • Minimal supported Clang version is 11

v0.0.13

  • Compatibility with Frama-C 25.0 Manganese
  • added limits and ratio in libc++ (contributed by T-Gruber)

v0.0.12

  • 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

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.15 compatible with Frama-C 28.0
  • 0.0.14 compatible with Frama-C 27.0
  • 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