Plugins Kernel Specification GUI Ivette

ANSI/ISO C Specification Language

Quick description

The ANSI/ISO C Specification Langage (ACSL) is a behavioral specification language for C programs. The design of ACSL is inspired of JML. It also inherits a lot from the specification language of the source code analyzer Caduceus, a previous development of one of the partners in the Frama-C project.

ACSL can express a wide range of functional properties. The paramount notion in ACSL is the function contract. While many software engineering experts advocate the "function contract mindset" when designing complex software, they generally leave the actual expression of the contract to run-time assertions, or to comments in the source code. ACSL is expressly designed for writing the kind of properties that make up a function contract. ACSL is a formal language.

#include <stddef.h>
/*@
  requires \valid(a+(0..n-1));1ACSL provides specification primitives to cover the low-level aspects of the C programming language

  assigns  a[0..n-1];

  ensures2As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.
  \forall integer i;
    0 <= i < n ==> a[i] == 0;
*/
void set_to_0(int* a, size_t n){
  size_t i;

  /*@
    loop invariant 0 <= i <= n;
    loop invariant
    \forall integer j;3It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expects a valid linked list".
      0 <= j < i ==> a[j] == 0;
    loop assigns i, a[0..n-1];
    loop variant n-i;
  */
  for(i = 0; i < n; ++i)
    a[i] = 0;
}
ACSL provides specification primitives to cover the low-level aspects of the C programming language
As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.
It also allows more abstract reasoning through mathematical or logic types, or through the definition of high level ideas, like "the function expects a valid linked list".

WP and the older Jessie plug-ins use Hoare-style weakest precondition computations to formally prove ACSL properties. The process can be quite automatic, thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4, or more interactive, with WP's built-in interactive prover or the use of the Coq proof assistant. Other plug-ins, such as the Eva plug-in, may also contribute to the verification of ACSL properties. They may also report static analysis results in terms of new asserted ACSL properties inside the source code.

More information

  • The ACSL manual has its own repository, together with ACSL++ (its companion language for specifying C++ programs and analyzing them with the frama-clang plug-in. Pdf versions of the manual are available on the release page.
  • A comprehensive tutorial on the WP plugin and ACSL specifications is available here.
  • Another tutorial, with specifications inspired notably from C++ containers is available here.

Manuals