Blog

Using Mopsa-Build to help preprocessing and parsing sources for Frama-C
André Maroneze (reviewed by Virgile Prevosto) on 19 September 2025

MOPSA is a research-oriented static analyzer which includes a tool called mopsa-build, a wrapper for build commands (esp. make) that helps the analysis. Frama-C can now use the same tool to help automate some parsing steps! JSON Compilation Databases (JCDBs, a.k.a. compile-commands.json) A JSON Compilation Database (referred from now on as...

Read More

On Dedicated Specification Languages Beyond ACSL contracts
Virgile Prevosto on 13 June 2025

La critique du langage ne peut éluder ce fait que nos paroles nous engagent et que nous devons leur être fidèles. — Albert Camus This post was originally written for the SecOPERA project’s blog. A crucial, but often neglected aspect of formal software evaluation process, is how we specify the...

Read More

General tips for debugging preprocessing and parsing issues
André Maroneze on 18 September 2024

Motivated by some recent discussions concerning a hard-to-parse code base, this post presents a few techniques used by Frama-C developers to quickly understand and debug parsing-related errors. We are constantly improving parsing and error messages, so hopefully some of these tips will become unnecessary in the future. Origin of parsing...

Read More