Volatile

Overview

This plug-in is meant to instrument volatile accesses so that one can specify the behavior of the volatile values. Without such a plug-in, Frama-C static analyzers basically consider that any read to a volatile location results in a value that covers the entire range of the corresponding C type.

Example

Let us illustrate the behavior with the following short program:

volatile unsigned index ;
int array[100] ;

int main(void){
  unsigned cur = 0 ;
  //@ loop \eva::unroll 100 ;
  while(cur < 100){
    cur = index ;
    array[cur] = 42 ;
    index = ++cur ;
  }
}

If we try to analyze this program with Eva, it fails to validate the access array[cur] = 42. Indeed, since its value is read from index, which is volatile, Eva considers that it can contain any unsigned integer. Thus, the condition cur < 100 cannot be guaranteed.

Now, we can instrument the volatile index with the following additional code:

/* Instrumentation for the volatile index:
   - last is the last written value,
   - read() returns the last written value,
   - write() can be used only to increase the value, up to 100, and updates last
*/
unsigned last ;

unsigned read(volatile unsigned* p){
  return last ;
}

//@ requires last < value <= 100 ;
unsigned write(volatile unsigned* p, unsigned value){
  last = value ;
  return value ;
}

//@ volatile index reads read writes write ;

and use the Volatile plug-in to introduce the instrumentation on read and write operations to index, and see how the results compare:

frama-c-gui volatile.c \
  -eva
  -then -volatile
  -then-last -eva
  • first, try to analyze the original code with Eva,
  • then, create a new project with instrumented volatile accesses,
  • finally on this new project, run Eva.

Usage

Note that Volatile builds a new project, thus subsequent analyses must be run on the resulting project.

Options:

  • -volatile-h: plug-in help message
  • -volatile: builds a new project (named “Volatile”) where volatile accesses are simulated by function calls
  • -volatile-basetype: use base types for int, float and enums for the instrumentation related to -volatile-binding option
  • -volatile-binding <f,...>: allows binding of volatile accesses to functions <f,...>
  • -volatile-binding-auto: allows automatic binding of volatile accesses to functions: <prefix>Rd_<typename> and <prefix>Wr_<typename>
  • -volatile-binding-call-pointer: replaces calls through function pointers by direct calls to functions: <prefix>Call_<result-type>_<param-types>
  • -volatile-binding-prefix <str>: adds <str> as prefix to function names for automatic binding
  • -volatile-call-pointer <f,...>: stub calls to pointer functions to the provided functions (indexed by type)
  • -volatile-fct <f,...>: Only process the given function(s)