6

Here is my example:

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

What I'd like to do is to find the range of the input variable n when initialized in main that results in reaching the function sum. The correct range in this example is [1, 10].

In the sample, I'd like to "save" the original input in a global value in and reintroduce it in the function sum by assigning it into the variable log_global and thus discovering the original input that resulted in reaching the function. When running frama-c on this sample, we get that the range of log_input is [5, 14] and the range of log_global is [-10, 10]. I understand why this happens - the value of in is set at the start of main and is not affected by further manipulations on n.

I was wondering whether there is a simple way to change this in frama-c? Perhaps a simple modification in frama-c's code?

One unrelated idea I had was to manipulate the if statement in main:

if (in > 0){
    sum(in + 4);
}

I used the global variable instead of n. This indeed results in the right range but this solution doesn't scale well to more complicated function and deeper call stacks.

Maor Veitsman
  • 1,544
  • 9
  • 21

1 Answers1

3

Here is a possible solution. Use the builtin Frama_C_interval_split and an appropriate -slevel N (here, at least N=21). The function sum will be examined N times, one for each possible value of N, and the result will be precise

int n = Frama_C_interval_split(-10, 10);

The results:

 [value] Values at end of function sum:
  log_input ∈ [5..14]
  log_global ∈ [1..10]
  __retres ∈ {0}

(Basically, this amounts to performing manual model-checking, so the performances won't be good for large values of N.)

byako
  • 3,372
  • 2
  • 21
  • 36
  • I don't seem to be getting the correct results, log_input is [5, MaxInt] and log_global [MinInt, MaxInt], perhaps this is a version issue? I'm using sodium. Also if I understand correctly, this is not applicable to unknown or very large intervals, right? – Maor Veitsman Feb 04 '16 at 09:12
  • My mistake, `Frama_C_interval_split` is not part of the released version. You can obtain the same result by writing a (tedious) ACSL disjunction after the call to `Frama_C_interval`: `//@ assert n == -10 | n == -9 || ... n == 10`. And indeed, this won't work well for large intervals. On the other hand, if you do not aim for full automaticity, you can do a smart partioning: `//@ assert n <= 0 || n > 0` will work in this case. – byako Feb 04 '16 at 13:05