ACSL Importer

Overview

The plug-in allows importing external ACSL specifications written in files, separated from the C source files. That provides more flexibility in the use of ACSL in the life cycle of software since the merge between the specifications and the source code is done by the plug-in.

Therefore, ACSL Importer plug-in is useful only to people that intend to write ACSL specifications and do not want to write them inside comments of the C source files.

Usage

The use of the plug-in could be the following, except if the given options lead to run analysis (analysis should be launched through the graphical interface):

• frama-c-gui <importing options> <C files>

Otherwise, options have to be split into two groups and given as follows:

• frama-c-gui <importing options> <C files> -then <analysis options>

Once the plugin installed, the next command gives the up-to-date list of the plug-in options:

• frama-c -acsl-importer-help

All options of the plug-in are prefixed by -acsl-.

The main options are:

• -acsl-importer-help: lists all options specific to the plug-in
• -acsl-import <filename list>: analyzes the content of files listed in its arguments and inserts the correctly typed specifications in the abstract syntax tree of Frama-C for further processing.
• -acsl-Idir <dirname list>: specifies the list of directories where the relative file names mentioned in include directives are searched.
• -acsl-keep-unsed-symbols: configures Frama-C kernel such that unused C symbols aren’t removed before the import.
• -acsl-parse-only: parses the ACSL files without typing nor imports.
• -acsl-typing-only: parses and types the ACSL files without imports.
• -acsl-version: pretty prints a text containing the version ID of the plugin.

Example

The plug-in can be used as follows. From a C file:

int f ( int i );
int g ( int j );
void job ( int *t , int A) {
  for ( int i = 0; i < 50; i ++) t[i] = f (i );
  for ( int j = A; j < 100; j ++) t[j ] = g(j );
}

and a specification file:

module demo :
 axiomatic A {
 type event = B | C(integer);
 predicate P(integer x);
 logic integer phi(event e);
 }

function f:
  contract:
    ensures P(phi(C(\result)));
    assigns \nothing ;

function g:
  contract: assigns \nothing ;

function job:
  at 1: assert 50 <= A <= 100;
  at loop 1:
    loop invariant 0 <= i <= 50;
    loop invariant \forall integer k; 0 <= k < i == > P(t[k]);
    loop assigns i,t[0..49];
  at loop body 1:
    contract:
      ensures i == \old(i);
  at loop stmt 1:
    contract:
      requires i==0;
      ensures i==50;
  at loop 2:
    loop invariant A <= j <= 100;
    loop assigns j,t[A ..99];
  at return:
    assert \forall integer k; 0 <= k < 50 == > P(t[k]);
  at call f:
    contract:
      ensures P(phi(C(t[i])));

The following command line:

frama-c -acsl-import demo.acsl demo.c -print -no-unicode

generates the following output:

# frama-c -acsl-import demo.acsl demo.c -print -no-unicode
[kernel] Parsing demo.c (with preprocessing)
[acsl-importer] Success for demo.acsl
[acsl-importer] Done: 1 file.
[kernel] Parsing demo.c (with preprocessing)
[acsl-importer] Success for demo.acsl
[acsl-importer] Done: 1 file.
/* Generated by Frama-C */
/*@
axiomatic A {
  type event = B | C(integer);
  predicate P(integer x) ;
  logic integer phi(event e) ;
  }
 */
/*@ ensures P(phi(C(\result)));
    assigns \nothing; */
int f(int i);

/*@ assigns \nothing; */
int g(int j);

void job(int *t, int A) {
  /*@ assert 50 <= A <= 100; */
  {
    int i = 0;
    /*@ requires i == 0;
        ensures i == 50; */
    /*@ loop invariant 0 <= i <= 50;
        loop invariant \forall integer k; 0 <= k < i ==> P(*(t + k));
        loop assigns i, *(t + (0 .. 49));
    */
    while (i < 50) {
      /*@ ensures i == \old(i); */
      {
        /*@ ensures P(phi(C(*(t + i)))); */
        *(t + i) = f(i);
      }
      i ++;
    }
  }
  {
    int j = A;
    /*@ loop invariant A <= j <= 100;
        loop assigns j, *(t + (A .. 99)); */
    while (j < 100) {
      {
        *(t + j) = g(j);
      }
      j ++;
    }
  }
  /*@ assert \forall integer k; 0 <= k < 50 ==> P(*(t + k)); */
  return;
}

int T[100];
void main(void) {
  job(T,50);
  return;
}

Contact

The plug-in is currently available under a proprietary license. For any questions, remarks or suggestions, please contact Allan Blanchard.