ACSL Importer

Overview

This plug-in allows importing external ACSL specifications written in files, separated from the C source files. it provides more flexibility in the use of ACSL in the life cycle of software since merging the specifications and the source code is done automatically 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 in comments of the C source files.

Example

The plug-in can be used as follows. From a C file (demo.c):

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 (demo.acsl):

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-import] Success for demo.acsl
[acsl-import] 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;
}

Usage

Basic plug-in usage is as follows, assuming no analyses are executed:

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

If you wish to run analyses, separate them in a group after a -then:

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

To obtain the full list of options for the plug-in, run:

• frama-c -acsl-import-help

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

The main options are:

• -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-import-dirs <dirname list>: specifies the list of directories where the relative file names mentioned in include directives are searched.
• -acsl-import-keep-unused-symbols: configures Frama-C kernel such that unused C symbols are not removed before importing annotations.
• -acsl-import-parse-only: parses the ACSL files without typing nor importing.
• -acsl-import-type-only: parses and types the ACSL files without importing.