Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Plugins in next Frama-C?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 6 Oct 2010 22:21:54 +0200
  • In-reply-to: <AANLkTimrtkSEWFs5br=YJn8QXa5Y8pbr8KbKwQv6tDkA@mail.gmail.com>
  • References: <AANLkTikw8pjgcE3LS1tqDebwktuECBkoFfLLRAw=UEFu@mail.gmail.com> <AANLkTimrtkSEWFs5br=YJn8QXa5Y8pbr8KbKwQv6tDkA@mail.gmail.com>
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