Overview
Mopsa is an open-source multi-language static analyzer. It aims at preventing software bugs at compile time before actually running the program. Mopsa is a sound static analyzer that ensures that (1) all possible executions are covered and that (2) the analysis will terminate in finite time. It is developed using the theory of abstract interpretation that guarantees this soundness by construction.
This User Manual describes how to get started with the Mopsa analyzer. It explains the primary options and tools provided by the analyzer that help in analyzing real-world programs.
Note
This software is a product of the Mopsa research project.
If you use Mopsa and find it useful, we’d love to hear about it! You can for instance post a support request on the GitLab project to tell us about your experience. In case of issue, you can also file a bug report.
Scope
Mopsa currently supports the analysis of a large subset of C and a subset of Python 3. It reports safety errors:
On C: run-time errors (overflows, invalid arithmetic or pointer operations, invalid memory accesses, double frees), assertion failures, failed preconditions for calls to the C library (invalid arguments, invalid formats, …).
On Python: uncaught exceptions, including types errors and assertion failures.
The precise list is given in the reports section.
Limitations
Warning
Mopsa is still an academic tool, under heavy development, and may contain limitations and bugs.
Features, options, and output format are subject to change and may not be in sync with this documentation.
Please report issues on the issue tracker on the GitLab project page.
On C: no support for recursive functions, concurrency, signals, bit-fields, long jumps, inline assembly, complex numbers, nor multidimensional variable length arrays; incomplete support for the C library; support for only a low-level, cell-based memory model.
On Python: no support for
eval
,async
, meta-classes, nor recursive functions; limited support for the standard library.
Mopsa aims at being sound, but it is not complete. Soundness implies that (on a theoretical level) it reports all possible errors within the classes of safety errors it handles. Incompleteness implies that it can also report spurious errors not occurring in any actual execution. This is due to a loss of precision when computing program behaviors at an abstract level, and can sometimes be corrected by choosing more precise analysis options (as exemplified in this manual).
Mopsa is a whole-program analysis. It requires the full source code of the analyzed program to be available, and an entry-point. Alternatively, for library functions that are called by with no provided source, it is possible to provide instead stubs modeling their effect. Stubs are already provided for a significant part of the standard C library and a part of the Python standard library.
Additional resources
the source code of Mopsa is available on GitLab
the GitLab group has additional projects using Mopsa, notably analysis benchmarks
the page for the research project has links to the scientific publications underlying the design of Mopsa