--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] context depth and pointer



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