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,

Option -no-deps has no effect if you require the computation of the pdg, as
PDG needs some sort of functional dependencies to compute the effects of
function calls. The simplest solution is to specify neither -does nor
-no-deps.

Perhaps counter-intuitively, you should set option -calldeps. Although it
will slow down the execution of Value, this will speed up the computation
of the PDG, as the modelisation of each call will be more precise. If, with
just -calldeps, the execution is still slow, you will have to send us more
information. Do you see something special in the function for which the pdg
computation take too much time ?

HTH,
 Le 9 oct. 2013 19:09, "David Yang" <abiao.yang at gmail.com> a ?crit :

> Dear all,
>
>
>
> After perform value analysis (about 3 mins), I want to get the Pdg of a specific kernel function by using following function:
>
>
>
> let pdg = !Db.Pdg.get kf in
>
>
>
>
> But this costs a lot of time. (more than an hour...)
>
>
>
>
> I really want to improve the speed of computing pdg for the specific function.
>
>
>
> As we known, pdg depends on other plugins. I can see that it depends on from plugin. So I set two options of the from plugin: -no-calldeps and -no-deps.
>
>
>
>
> Is there any other plugins that Pdg depends on ?
>
> Or is there any other options that can be set to speed up computing pdg?
>
>
>
>
> Thank you very much.
>
>
>
>
> Best regards,
>
>
>
>
> Yours sincerely,
>
> David
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131009/7a9af649/attachment.html>