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] Frama-c-discuss Digest, Vol 135, Issue 2

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 135, Issue 2
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 17 Sep 2019 16:50:11 +0200
  • In-reply-to: <CADR7Ut1qYQyVZ4Qbjag2=+P6S6x71nirmeKoKGu4vByxoaQpqA@mail.gmail.com>
  • References: <mailman.4.1568714413.3736.frama-c-discuss@lists.gforge.inria.fr> <CADR7Ut1qYQyVZ4Qbjag2=+P6S6x71nirmeKoKGu4vByxoaQpqA@mail.gmail.com>
Hello, and thanks for your interest in Frama-Clang,

Le mar. 17 sept. 2019 à 15:48, Richard Ford <richardlford at gmail.com> a
écrit :

> Good job! I've been looking forward to an updated Frama-Clang.
> The Frama-Clang user manual refers to an ACSL++ manual which I've not been
> able to find. Has it been completed?
>

A first draft is available (against thanks mainly to David Cok), we have
indeed to release yet publically. However, as far as the implementation is
concerned, a good approximation is that it handles basic ACSL annotations
with C++ symbols.


>
> I'm wondering what support there is for exception handling. It seems like
> that would require extensions to
> the basic frama-c framework.
>
> What kind of support do the proving plugins, e.g. Jessie and Wp, have for
> it?
>
>
Indeed, there is support in the kernel for that: the AST contains specific
nodes for throwing and catching exceptions, and a specific AST
transformation is dedicated to remove these nodes (via some kind of global
variable). The result is a plain C program, but some support will be needed
at the annotation level as well (basically the introduction of the planned
`throws` clauses, in the same spirit as ACSL "abrupt clauses").


> I'm part of a group studying formal methods and we would like to
> contribute to a formal methods project.
> Do you have some suggested tasks that we could do to help Frama-Clang?
> We particularly would like to make the verification of C++ code more
> practical.
>
>
Again, thanks for your interest in Frama-Clang. There's a lot to be done in
terms of debugging, completing STL support, and annotating the STL itself,
even with very basic specifications. We can of course answer to questions
on this mailing list, but for more involved collaborations, we'll need to
find a more formal setup, e.g. some kind of collaborative project.


> Have you considered moving development of Frama-C and related plugins to
> an open platform like
> github, and using its issues and pull-request features for collaboration?
>
>
Yes, this is on our todo list. There are a few non-technical roadblocks,
though, and devising the best strategy is not trivial.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190917/bcd6811f/attachment-0001.html>