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] context depth and pointer

  • Subject: [Frama-c-discuss] context depth and pointer
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Thu Aug 21 01:49:39 2008
  • References: <48AC5D93.2060905@cs.utah.edu>
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