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: djs at (Daniel Sheridan)
  • Date: Tue, 7 May 2013 18:26:40 +0100

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

    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,