Frama-C 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 MoreLa 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 MoreMotivated 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 MoreThis page redirects to the Frama-C Days 2024 Slides Gallery
Read MoreAfter 5 years of absence, the Frama-C Days are back! On June 13 and 14, will be held the Frama-C Days at Maison de la Radio et de la Musique in Paris. What to expect? Many exciting interventions from both academic and industrial users of the Frama-C environment, for sharing...
Read More