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