Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] A question on Frama-C input/output analysis

>> Recently I used Frama-C to analyze the input/output information for each C
>> function. However, I found for some functions, there are many inputs (more
>> than 200, but most of them are similar).
>
> These variables are generated by the value analysis to act as target
> for pointers (using -lib-entry, all global pointer variables; without
> -lib-entry, only the entry point's arguments).

Here is an example where you can see perhaps more easily what is happening:

struct S { int a; int *b; } t[10];

int f(int i){
  return 1 + *(t[i].b);
}

frama-c -lib-entry -main f -input t.c

The generated initial state, according to the documentation, is:

[value] Values of globals at initialization
        t[0].a ? [--..--]
         [0].b ? {‌{ &NULL ; &S_b_0_t ;}‌}
         [1].a ? [--..--]
         [1].b ? {‌{ &NULL ; &S_b_1_t ;}‌}
         [2].a ? [--..--]
         [2].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [3].a ? [--..--]
         [3].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [4].a ? [--..--]
         [4].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [5].a ? [--..--]
         [5].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [6].a ? [--..--]
         [6].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [7].a ? [--..--]
         [7].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [8].a ? [--..--]
         [8].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
         [9].a ? [--..--]
         [9].b ? {‌{ &NULL ; &S_b_0_t ; &S_b_1_t ;}‌}
        S_b_0_t[0..1] ? [--..--]
        S_b_1_t[0..1] ? [--..--]

Although the function is very simple, if you compute precisely its
inputs and list them, you get a long list:

[inout] Inputs for function f:

          t{[0].b; [1].b; [2].b; [3].b; [4].b; [5].b; [6].b; [7].b;
[8].b; [9].b; };
-> each field is an input. A less precisely analysis would tell you
that "t" is an input. If this is the kind of result you would prefer,
use such an imprecise analysis (I am sure there are plenty available
elsewhere).

          S_b_0_t[0]; S_b_1_t[0]
-> with your version, which I think is the version some in this
mailing list (but not me) have been saying is so inferior to Boron
that you should not even try to use it, you would get a list of ten
target locations, one for each .b field in array t. With Carbon, only
two target locations are generated, and all the t[i].b pointers are
made to point to one, or the other, or both of these locations.

Pascal