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-bindingoption-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)
