The Frama-Clang plugin

frama-clang logo 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 an 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 analysis 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 guarantee. Moreover, the translation from C++ to C does not make any attempt to optimize the resulting code for the back-end analyzers such as Value Analysis 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 to its maturation.

Installation

Download

Current version is 0.0.3. The frama-clang plugin can be downloaded here

Requirements

Installation steps

tar xzvf frama-clang-0.0.3.tar.gz
cd frama-clang-0.0.3
./configure
make
make install
Depending on your Frama-C installation, this last step might require root permissions

Changes

v0.0.3

v0.0.2

v0.0.1

Previous versions

Command-line options

ACSL++

It is possible to annotate C++ code with a language very similar to ACSL. The only distinction is currently that C++ scoping rules apply for global identifiers. Classes can have member logic functions and member predicates. They are never static, and take an implicit \this object as receiver argument, similar to the this pointer in the code (which is of course accessible in function contracts, assertions and loop annotations). Finally, it is possible to define class invariant, similar to ACSL's type invariants for the current class. The following class provides a short example of ACSL++ annotations:

class A {
public:
  int x;
  /*@ class invariant pos = \this.x >= 0; */

  /*@ predicate bigger(A a) = x > a.x; */

  /*@ requires \valid(a);
      // The 'this' pointer is always valid within a method.
      // No need to add a requires for that
      requires this->bigger(*a);
      assigns this->x;
      ensures this->x == \at(this->x, Pre) - a->x;
   */
   void f(A* a) { x -= a -> x; }
};

 

The llvm wyvern logo is © Apple, inc