gfletcher03/frama-concur repository overview

Introduction: This project is an extension to the Frama-C software analyser for C, to provide a simple way to discover potential concurrency problems in interrupt-driven C code. Command-line and GUI versions are available.

This plugin was developed by Adelard LLP as part of the FEAST research project, conducted on behalf of CINIF (the Control and Instrumentation Nuclear Industry Forum).

Goals: The Simple Concurrency Analysis Plugin is aimed at small, embedded systems, typically without an operating system. These systems commonly use interrupts to manage hardware and other interactions, and use shared variables to communicate between the main thread and the interrupt service routines. As interrupts can occur at any time, these shared variables can be corrupted.

To help discover potential sources of problems, this plugin does three things:

Help identify interrupt service routines. These may not be obvious from the C source. The plugin identifies all functions which are not called from elsewhere in code as possible interrupt service routines. Identify shared variables. For every combination of the main thread and an interrupt service routine, the plugin identifies variables which may be accessed by both. These are the global variables and other variables with static storage duration (e.g., function local variables declared static). Identify where the variables are accessed. For a given variable, the plugin lists all reads and writes to that variable, reachable from the main and chosen interrupt threads.

Caveats: To keep the plugin simple and fast, it does not attempt to process pointers. This means that variable accesses via pointers are not identified by this plugin, and calls to function pointers are not followed. See issue #1.

For programs where this is critical, the Mthread plugin provides a much more advanced analysis.

The size information reported by -accesses-for (see below) is dependent on Frama-C's -machdep option being set correctly.