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