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 ?

  • Subject: [Frama-c-discuss] How to speed up computing Pdg for a specific kernel function ?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Wed, 9 Oct 2013 21:19:23 +0100
  • In-reply-to: <CABbVA-Cfj=HnoNqfKzHEXNH-+4YfccsRxjLgRLso6bSXkg_Jww@mail.gmail.com>
  • References: <CAA1cxuhPgkhUDop59dwaSzUK5f5Pd9j9mnnS+rvU0Vnm6auBRQ@mail.gmail.com> <CABbVA-Cfj=HnoNqfKzHEXNH-+4YfccsRxjLgRLso6bSXkg_Jww@mail.gmail.com>
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>