Dear all,
On behalf of all its developers, I am glad to announce the release of Mopsa v1.1! You can just opam install mopsa
.
What is Mopsa? Mopsa stands for Modular and Open Platform for Static Analysis. It aims at easing the development and use of static analyzers. More specifically, Mopsa is a generic framework for building sound static analyzer based on the theory of abstract interpretation. Mopsa is independent of language and abstraction choices. Developers are free to add arbitrary abstractions (numeric, pointer, memory, etc.) and syntax iterators for new languages. Mopsa encourages the development of independent abstractions which can cooperate or be combined to improve precision.
v1.1 changes. This new version brings several expressivity, precision and interface improvements, notably:
- Trace and state partitioning.
introduces breaking changes in the API of domains.
- Suggestions to trigger automatic testcase reduction whenever Mopsa crashes
- As a side-effect, Mopsa is able to generate preprocessed files from make targets using option
-c-preprocess-and-exit=file.i
, which might be useful for other users too! This has been experimented on our coreutils benchmarks, and can also be used to generate the preprocessed files used in the Software-Verification Benchmarks.
- As a side-effect, Mopsa is able to generate preprocessed files from make targets using option
- Bash completion support, thanks to arg-complete developped by Simmo Saan.