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