--- layout: fc_discuss_archives title: Message 31 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,

Thank you very  much  for your prompt reply.
"-does"  option seems not exist.

Besides, i also output the codes to test.c for testing.

attached pleased find:
1. the source code : test.c
2. the temp project of the first command: temp.prj

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

command 2 for computing pdg of function close_io :
~# frama-c -load temp.prj -fct-pdg close_io

the first command cost nearly 16 secs.
but the second command seems not to stop...


Thanks again.
-David



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

> 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
>>
>
> _______________________________________________
> 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/d95b13ad/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: text/x-csrc
Size: 248863 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131009/d95b13ad/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.prj
Type: application/octet-stream
Size: 2559413 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131009/d95b13ad/attachment-0001.obj>