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 ?

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>