--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on October 2013 ---
[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 ?



Dear Boris,

Your solution is extremely helpful. I sincerely appreciate for your help
and patience.
By setting the -context-deps option to 0, a lot of time can be saved.

Thanks again.

Best regards.

Yours sincerely,
-David



On 11 October 2013 19:07, Boris Yakobowski <boris at yakobowski.org> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131011/41ef71dc/attachment.html>