Calculating function summary using Frama-C's value analysis

120 Views Asked by At

Let's say we have the following code sample:

int a(int x){
    if (x < 0){
        return -50;
    }
    if (x >= 0 && x <= 3600){
        return x - 100;
    }

    return x + 100;
}

int main(){
    int q = Frama_C_interval(50, 5000); 

    return a(q);
}

By running the frama-c value analysis tool I can deduce the interval of the result of a() which turns out to be [-50, 5100] as expected. What I'd like to calculate now is the function summary of a() i.e. the relation between the input and the output. The result I am looking for in the above example would look something like this:

[50,3600] -> [-50, 3500]
[3601,5000] -> [3701, 5100]

Note that I am interested in a context based summary so other cases in function a() are of less interest.

What would be the best way to achieve this?

0

There are 0 best solutions below