Calculate reachability for a function using frama-c value analysis

Question

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 would like to do is find the range of the input variable n when initializing in main, which will lead to the achievement of the sum of the function. The correct range in this example is [1, 10].

In the example, I would like to “save” the original input in a global value in and re-enter it into the sum of the function, assigning it to the log_global variable and thus discovering the original input that led to the function being reached. When running frama-c in this example, 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 in is given at the beginning of main and it is not affected by further manipulations on n .. p>

I was wondering if there is an easy way to change this in frama-c? Perhaps a simple modification in frama-c code?

One unrelated idea was to manipulate the if statement basically:

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

I used a global variable instead of n . This does lead to the correct range, but this solution does not scale well for more complex functions and deeper call stacks.

Answer 1

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

 int n = Frama_C_interval_split(-10, 10); 

Results:

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

(In principle, this means performing a manual check of the model, so the characteristics will not be good at large values ​​of N.)