Is it possible to inject values in the frama-c value analyzer?

Question

I'm experimenting with the frama-c value analyzer to evaluate C-Code, which is actually threaded. I want to ignore any threading problems that might occur und just inspect the possible values for a single thread. So far this works by setting the entry point to where the thread starts.

Now to my problem: Inside one thread I read values that are written by another thread, because frama-c does not (and should not?) consider threading (currently) it assumes my variable is in some broad range, but I know that the range is in fact much smaller. Is it possible to tell the value analyzer the value range of this variable?

Example:

volatile int x = 0;

void f() {
    while(x==0)
        sleep(100);
    ...
}

Here frama-c detects that x is volatile and thus has range [--..--], but I know what the other thread will write into x, and I want to tell the analyzer that x can only be 0 or 1. Is this possible with frama-c, especially in the gui?

Thanks in advance Christian

Answer 1

This is currently not possible automatically. The value analysis considers that volatile variables always contain the full range of values included in their underlying type. There however exists a proprietary plug-in that transforms accesses to volatile variables into calls to user-supplied function. In your case, your code would be transformed into essentially this:

int x = 0;

void f() {
while(1) {
    x = f_volatile_x();
    if (x == 0)
    sleep(100);
...
}

By specifying f_volatile_x correctly, you can ensure it returns values between 0 and 1 only.

Answer 2

If the variable 'x' is not modified in the thread you are studying, you could also initialize it at the beginning of the 'main' function with :

x = Frama_C_interval (0, 1);

This is a function defined by Frama-C in ...../share/frama-c/builtin.c so you have to add this file to your inputs when you use it.