package frama-c-typestates

Typestates

Install

make && make install

Specification

First, we need to declare the typestate on a C type, along with a list of associated states. For example, we declare below a typestate on the FILE type with states C (closed file), R (opened in read-mode) and W (opened in write-mode).

//@ typestate \def, (FILE) fd == C | R | W;

Then, we define transitions on API functions, with pre- and post-conditions separated by the function name between brackets. In pre- and post-conditions we specify the typestates of formal parameters. For example, here we define a transition on init from Undef to C, and two transitions on close: one from W to C an the other from R to C.

//@ typestate \trans, f==Undef, {init}, f==C;
//@ typestate \trans, f==W, {close}, f==C;
//@ typestate \trans, f==R, {close}, f==C;

Note that the Undef state is a builtin to denote the typestate of a declared object which has not been initialized yet, thus we do not need to declare it explicitly in the states list.

Guard conditions

//@ typestate \trans, f==C, {open}, \post(\result!=0), f==C;
//@ typestate \trans, f==C, \guard(mode=='R'), {open}, \post(\result==0), f==R;
//@ typestate \trans, f==C, \guard(mode=='W'), {open}, \post(\result==0), f==W;

Typestates of objects in interaction

It is also possible to specify objects interactions in typestate transitions.

We can use the \ref predicate on two objects, for example \ref(src,tgt) to say that src references tgt; or on a single object to denote the state of the referenced object. Note that the two objects are not necessary of the same type, and thus can mix different typestates.

In the example below, the pipe function builds a reference from src to tgt, and the close_pipe function makes them go into their previous state: R for the src file and W for the referenced tgt file.

//@ typestate \trans, src==R, tgt==W, {pipe}, src==P, \ref(src,tgt), \ref(src)==P;
//@ typestate \trans, src==P, \ref(src)==P, {close_pipe}, src==R, \ref(src)==W;

We can also use the \link predicate on two objects to denote a bidirectional link between these. In this case, \ref on an object still denotes the state of the referenced object, but we can also use \biref on a single object to say that it references an object which references back the first one.

Multiple objects in interaction

The \addref predicate allows to add a new reference from one object to another, thus the source object can reference multiple objects.

In this case, \ref(f1,f2) means that f2 is one of the objects referenced by f1, and \ref(f1)==S means that every referenced object should have the state S.

We can then use \rmref(f1,f2) to remove a reference from f1 to f2 , or \rmrefs(f1) to remove all references from ̀f1`.

Loop invariants

We can use \ts and \tsref to denote typestates in loop invariants, these invariants must be introduced with the keywords loop ts_invariant instead of loop invariant. The predicate \ts(f) denotes the typestate of f, while \tsref(f1,f2) means that f2 is referenced from f1.

/*@
    loop assigns i,*t1[0..1],*t2[0..1];
    loop invariant 0<=i<=2;
    loop invariant \forall integer j; 0<=j<2 ==> \valid(t1[j]) && \valid(t2[j]);
    loop ts_invariant \forall integer j; i<=j<2 ==> \ts(*t1[j])==R && \ts(*t2[j])==W;
    loop ts_invariant \forall integer j; 0<=j<i ==> \ts(*t1[j])==P && \ts(*t2[j])==P;
    loop ts_invariant \forall integer j; 0<=j<i ==> \tsref(*t1[j],t2[j]);
    loop variant 3-i;
  */
  for (int i = 0; i < 2; i++)
  {
    pipe(t1[i],t2[i]);
  }

All typestates predicates

Usage

frama-c -typestates [-typestates-alloc-eva] FILENAME.c -then-last [-eva] [-wp] 

The code instrumented by the Typestates plug-in, can be verified with Eva, WP or E-ACSL (unless the option typetates-alloc-eva is used, cf Dynamic Allocation).

The -eva and -wp options controls the activation of the Eva and WP plug-ins. Note that it is possible to use both options: the two plug-ins will cooperate.

The verification of the instrumented code with E-ACSL is done via a bash script: test_eacsl.sh, and its usage is described in the next section.

Runtime verification with E-ACSL

sh test_eacsl.sh FILENAME.c

The script prints the results of the test on standard output, it also produces 3 auxiliary files: FILENAME.out.frama.c (the code instrumented by the plug-ins Typestates and E-ACSL), FILENAME.out.e-acsl (the binary compiled from FILENAME.out.frama.c), and FILENAME.eacsl.log the full output including the compilation and execution of FILENAME.out.frama.c.

Dynamic allocation

If a transition function returns type points to a tracked type, it is considered as a dynamic allocation function. Therefore, an allocation method must be selected.

For example, in the following specification, new is an allocation function :

//@ typestate \def, (FILE) fd == C | R | W;
//@ typestate \trans, {new}, "\result" == C;

At the moment, only one allocation method is available: allocation for Eva. This allocation method can be activated with the option -typestates-alloc-eva, and the resulting code is only compatible with the Eva plugin.

Debug options

-typestates-msg-key <k1[,...,kn]> enables message display for categories <k1>,...,<kn>. Use -typestates-msg-key help to get a list of available categories, and '*' to enable all categories