--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2008 ---
Hi, > In changelog I see context depth mentioned with pointer >initialization. Can somebody points me to a paper or elaborate on it >please? I believe you are alluding to the options -context-depth n : use n as the depth of the default context for value analyses. (defaults to 2) -context-width n : use n as the width of the default context for value analyses. (defaults to 2) -context-valid-pointers : context generation will only allocate valid pointers until the -context-depth and then use NULL (defaults to false) These options of the value analysis decide what happens for the variables for which Frama-C is supposed to build a "generic" value, with only their respective types as information. These variables are the arguments of the entry point function in any case, and all the global variables in "-lib-entry" mode. When not in "-lib-entry" mode, the globals are assumed to be initialized to zero, which is not as far as I remember a property that is guaranteed by the C standard, but one offered on many platforms anyway because it coincides with something that the loader can do easily. The best way to see what these options do is by example. I suggest the following program: int *p; int *****q; struct list { int content; struct list * tail; } L; struct tree { int content; struct tree * left; struct tree *right; } T; void main(void) { Frama_C_dump_each(); } and to start with the following command-line (and then fiddle with the previous three options' value): bin/toplevel.opt -lib-entry -val t.c Here are some highlights for the results with the default values of the options: p ? {{ &NULL ; &star_p ;}} star_p[0..1] ? [--..--] (the [0..1] interval has to do with the context-width option) q ? {{ &NULL ; &star_q ;}} star_q[0] ? {{ &NULL ; &star_star_q_0nth ;}} [1] ? {{ &NULL ; &star_star_q_1nth ;}} star_star_q_0nth[0] ? {{ &NULL ; &star_star_star_q_0nth_0nth ;}} [1] ? {{ &NULL ; &star_star_star_q_0nth_1nth ;}} star_star_star_q_0nth_0nth[0] ? {{ garbled mix of &{star_star_star_q_0nth_0nth_0nth_WELL; } (origin: Well) }} ... star_star_star_q_0nth_0nth_0nth_WELL[bits 0 to 549755813887] ? {{ garbled mix of &{star_star_star_q_0nth_0nth_0nth_WELL; } (origin: Well) }} ... (the depth at which base addresses are allocated before representing using a "well" for the representation has to do with the context-depth option) If the datatypes you were interested in were list and trees such as those in my example, you would definitely use "-context-width 1" so that the analyzer knew that the fields tail, left and right are pointers to a single substructure instead of an array of them. The result would then look like: L.content ? [--..--] .tail ? {{ &NULL ; &star_L__tail ;}} star_L__tail[0].content ? [--..--] [0].tail ? {{ &NULL ; &star_star_L__tail_0nth__tail ;}} star_star_L__tail_0nth__tail[0].content ? [--..--] [0].tail ? {{ &NULL ; &star_star_star_L__tail_0nth__tail_0nth__tail ;}} star_star_star_L__tail_0nth__tail_0nth__tail[0].content ? [--..--] [0].tail ? {{ garbled mix of &{star_star_star_L__tail_0nth__tail_0nth__tail_0nth__tail_WELL; } (origin: Well) }} star_star_star_L__tail_0nth__tail_0nth__tail_0nth__tail_WELL[bits 0 to 549755813887] ? {{ garbled mix of & {star_star_star_L__tail_0nth__tail_0nth__tail_0nth__tail_WELL; } (origin: Well) }} Pascal