--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on March 2011 ---
[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