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] How to speed up computing Pdg for a specific kernel function ?

HI,

On Wed, Oct 9, 2013 at 10:19 PM, David Yang <abiao.yang at gmail.com> wrote:
> Thank you very  much  for your prompt reply.
> "-does"  option seems not exist.

My phone decided to autocorrect -deps into -does.

> Besides, i also output the codes to test.c for testing.
>
> attached pleased find:
> 1. the source code : test.c

Thanks, this is helpful.

> 2. the temp project of the first command: temp.prj

This is less useful, as it is not easy to share binary saves between
two machines and Frama-C versions. Also, this is a big attachment for
a public mailing-list.

> command 1 for value analysis by close_io entry point:
> ~# frama-c -lib-entry -main close_io -val test.c -val-use-spec close_redir
> -val-use-spec warning -val-use-spec strerror -val-use-spec __errno_location
> -save temp.prj

The 'culprit' is option -lib-entry, but it is doing exactly what it is
designed for. The recursive datastructures in your projects cause the
generation of tons of variables to model the initial state. Consider
the number of lines in the initial state, depending on the option
-context-depth:
-context-depth / nb of lines
0 /   2552
1 /   6334
2 /  25526
3 / 118662
Although there is not a variable by line, this gives you an idea of
the size increase with different context depths. (The default value is
2)

Given the very broad assigns for the sub-functions called by main, you
essentially assigns everything reachable from red_head, and this
assignment also depends on everything reachable from red_head. This
means that the size of the PDG is inherently quadratic in the number
of variables that are in the initial state of red_head, which is a
recursive (and complicated) structure. You should probably use option
-context-depth 0, as this gives you essentially the same level of
generality, and a much more reasonable initial state. You could also
write your own initial state.

HTH,

-- 
Boris