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