The Mthread plug-in

The Mthread plug-in automatically analyzes concurrent C programs, using the techniques used by the Value analysis. At the end of its execution, the concurrent behavior of each thread is over-approximated. Thus, the information delivered by the plug-in take into account all the possible concurrent behaviors of the program.

The results of Mthread are many-fold:


The plug-in is currently available under a proprietary licence. You can contact to obtain such a licence.

Evaluation versions, in the form of pre-compiled binaries compatible with Frama-C Oxygen, are also available for some platforms. Do not hesitate to contact us if you are interested.


The plug-in is activated with the following command line:

frama-c -mthread file1.c file2.c ... concurrent_library.c

Notice that you must explicitely pass a stubbed version of your concurrency library on the command-line. Support for the often used pthread primitives is included in the plug-in. Preliminary support for the VxWorks and Win32 libraries also exist.

The main options are:

Gives some additional information during computation.
-mt-shared-zones n
Show the values written in all shared zones at level 1, and with the calling contexts in which they are written at level 2.
Print the calling context at which the concurrent operations occur.
-mt-extract html
Generate an html summary of the results, as well as the concurrent (sliced) graphs of each thread.
Gives the whole list of options


Known Restrictions


For any questions, remarks or suggestions, please contact .