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: richardlford at gmail.com (Richard Ford)
  • Date: Tue, 17 Sep 2019 09:48:03 -0400
  • In-reply-to: <mailman.4.1568714413.3736.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.4.1568714413.3736.frama-c-discuss@lists.gforge.inria.fr>

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?

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?

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.

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?

Richard L Ford


On Tue, Sep 17, 2019 at 6:00 AM <
frama-c-discuss-request at lists.gforge.inria.fr> wrote:

> Send Frama-c-discuss mailing list submissions to
>         frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
>         frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
>         frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
> Today's Topics:
>
>    1. An upcoming tutorial on Frama-C - October 10,     2019 at FM 2019
>       in Porto (Nikolay Kosmatov)
>    2. Installation procedure of Frama-C Potassium in the Windows
>       Subsystem for Linux (Max Veen)
>    3. Frama-Clang 0.0.7 (Virgile Prevosto)
>
>
>
> ---------- Forwarded message ----------
> From: Nikolay Kosmatov <nikolaikosmatov at gmail.com>
> To: frama-c-discuss at lists.gforge.inria.fr, gdr.gpl at imag.fr,
> gdr-im at gdr-im.fr, alp-diffusion at univ-lille1.fr
> Cc:
> Bcc:
> Date: Mon, 16 Sep 2019 16:16:19 +0200
> Subject: [Frama-c-discuss] An upcoming tutorial on Frama-C - October 10,
> 2019 at FM 2019 in Porto
> Dear Frama-C users and future users,
>
> We are happy to announce an upcoming tutorial on Frama-C
>
>   "*Formal Verification of IoT Software with Frama-C*"
>
> that will take place
>
>   on October 10, 2019
>   at FM 2019: the 3rd World Congress on Formal Methods
>   in Porto, Portugal
>   http://formalmethods2019.inesctec.pt/?page_id=84
>
> A description of the tutorial is available here.
> <https://allanblanchard.github.io/tutorials/Tutorial-FM-19-Formal-Verification-of-IoT-Software-with-Frama-C.html>
> We plan to post in a few days a link to a virtual machine (that we
> recommend to download before the tutorial) containing tools and exercices.
>
> Best regards,
> Nikolai
>
> For the tutorial presenters,
> Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue
>
>
>
> ---------- Forwarded message ----------
> From: Max Veen <mveen at intecma.nl>
> To: frama-c-discuss at lists.gforge.inria.fr
> Cc:
> Bcc:
> Date: Tue, 17 Sep 2019 09:20:26 +0200
> Subject: [Frama-c-discuss] Installation procedure of Frama-C Potassium in
> the Windows Subsystem for Linux
> Hi all,
>
> I want to use Frama-C on Windows 10 professional for analyzing and
> instrumenting our code.
>
> I have tried to install Frama-C with Cygwin and MingW on windows, but
> this installation has many
>
> library version dependencies and is cumbersome.
>
> So I have tried to find a more convenient and better way to accomplish
> this.
>
> On the web I encoutered a blog from June this year of Frama-C news and
> ideas by André Maroneze.
>
> In this blog he tells in a nutshell the installation procedure to get
> Frama-C running on the WSL.
>
> What I like to know is the full installation procedure details to get
> Frama-C up and running on WIndows 10
>
> with the WSL and the X-server for the Frama GUI.
>
> Can anyone of you guys (André) help me with the installation details?
>
> I will be very grateful!
>
> Thanks for help in advance.
>
> Regards,
>
> Max
>
>
>
>
>
> ---------- Forwarded message ----------
> From: Virgile Prevosto <virgile.prevosto at m4x.org>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Cc:
> Bcc:
> Date: Tue, 17 Sep 2019 11:34:49 +0200
> Subject: [Frama-c-discuss] Frama-Clang 0.0.7
> Dear list,
>
> it is a pleasure for us to celebrate the 230th anniversary of the
> discovery of Mimas by William Herschel with the release of Frama-Clang
> v0.0.7. Feel free to download it at https://frama-c.com/frama-clang.html
>
> Frama-Clang is a Frama-C plug-in acting as a C++ front-end of the
> platform. Among the main changes in this release are:
>
> - A user manual
> - totally rewritten ACSL++ parser, with a much simpler and more
> maintainable implementation
> - more headers in the Frama-Clang implementation of the STL
> - preliminary support for lambdas
> - compatibility with Frama-C 19.0 Potassium
> - compatibility with clang/llvm 6 to 8
>
> Finally, I'd like to thank David Cok, who just spent 18 months on
> sabbatical with us and has been the main force behind, among other things,
> the user manual and the new ACSL++ parser.
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190917/87cce599/attachment.html>