--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugins in next Frama-C?



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