--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2010 ---
Hello Pascal, 2010/10/6 Pascal Cuoq <pascal.cuoq at gmail.com>: > The value analysis will require much less memory for many large > analyses, along with other less striking improvements. The ratios > range from 4 to 100 for the existing memory consumption benchmarks > that I had lying around (that is, from 4 times less memory required to > 100 times less memory required). Very good! I assume this is the result of the rangemap work. BTW, are there any figures about the size of C code that can be handled by Frama-C? 1,000 lines? 10,000 lines? 100,000 lines? In which time? I am more interested in possible results obtained by applying "automatic" plug-ins like value analysis. I can easily imagine that annotating and proving 100,000 lines of C with ACSL and Jessie is not that easy! ;-) I'm asking this because I recently attended a DGA-MI presentation where DGA people said they use PolySpace. They limit the analyzed code size to 60,000 lines otherwise it takes a too long time (> 3 days). They are not entirely satisfied with the result. They are considering using Frama-C (amongst other tools). > Note that no date is fixed for a Carbon release and that while it is > unlikely that these changes do not happen, many others could be added > to the list in the meantime. As usual. While a precise roadmap is probably not needed, having some hints on content of future release is always useful, especially if you are trying to sell Frama-C within your company. ;-) Many thanks for the answer Pascal, Best regards, david