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 MoreThe analysis scripts provided with Frama-C, which have been mentioned in this blog several times, are now documented in the Frama-C User Manual. This should provide a more complete and up-to-date experience concerning these scripts. Faster iterations with daily Frama-C snapshots Deploying analysis scripts usually required very long iteration times:...
Read MoreFrama-C has a somewhat obscure plug-in called Obfuscator, whose original purpose was to help industrial users give the Frama-C developers enough information about confidential use cases, for debugging and optimizations. However, sharing proprietary code is never easy: is the obfuscation good enough? Are there legal issues involved? Is it worth...
Read MoreOne of the new features in Frama-C 18 (Argon) is the annotation @loop unroll, used by the Eva plug-in to replace and improve upon the usage of slevel for semantically unrolling loops. This new annotation is more stable, predictable, and overall more efficient. In this post we present the annotation...
Read MoreA recurring subject when using Frama-C, especially intriguing for newcomers, is how to reach the stage where parsing of a realistic code base (as in, one that uses external libraries and compiles to different architectures) succeeds. This post will show a bit of the depth involved in the subject, presenting...
Read More