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] Announce: simple concurrency analysis plugin

  • Subject: [Frama-c-discuss] Announce: simple concurrency analysis plugin
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Sun, 26 May 2013 13:55:36 +0200
  • In-reply-to: <CAO7_hEtZSNyKq+QVdDf7xG=6jVjZa_GTUvW9M8XG8QR+UdTjsA@mail.gmail.com>
  • References: <CAO7_hEtZSNyKq+QVdDf7xG=6jVjZa_GTUvW9M8XG8QR+UdTjsA@mail.gmail.com>
Hi Dan and Damien,

Sorry for not having answered earlier, but the beginning of may is
often a slow time in France :-)

We would like to thank you for this remarkable contribution. I've
tried your plugin on own of our concurrent examples, and the detection
of shared variables that were not accessed through pointers worked
flawlessly. Together with the great GUI workflow, studying shared
accesses was extremely convenient.

This plugin is a great addition to the Frama-C ecosystem, and we
appreciate that you decided to open-source it. Do not hesitate to
add-it to the list of external plugins at
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:external_plugins
for better reference.

Cheers,


On Tue, May 7, 2013 at 7:26 PM, Daniel Sheridan <djs at adelard.com> wrote:
> Dear all,
>
> We are pleased to announce the "simple concurrency analysis" plugin
> for Frama-C. This has been the subject of research at Adelard
> sponsored by the UK nuclear industry, and is the first of several
> plugins that we hope to release under LGPL licenses.
>
> This plugin is aimed at helping to identify possible sources of
> variable corruption where variables are shared between main program
> code and interrupt service routines. It doesn't use the value analysis
> plugin, so it is simple and fast, but doesn't analyse pointers.
>
> Source code and instructions are available from
> https://bitbucket.org/adelard/simple-concurrency
>
>     Dan and Damien.
>
> --
> Adelard LLP, Exmouth House, 3-11 Pine Street, London, EC1R 0JH, UK
> Tel: +44 (0)20 7832 5850 Fax: +44 (0)20 7832 5870,
> Web: http://www.adelard.com
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



-- 
Boris