Analysis scripts: up-to-date information in the Frama-C User Manual

The 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: with one Frama-C release each 6 months, users needed to wait before fixes and new features, which meant less feedback from users.

With the availability of public daily snapshots, it is now much easier to provide users with new features and test different approaches.

Not only for Eva

The analysis scripts were initially developed for usage with the Eva plug-in, but they were always intended for a more widespread Frama-C usage. A small section on the Eva user manual mentioned their usage, but without many details, due to their constant evolution.

As their usage matures, we expect some convergence from other plug-ins, to provide a more unified approach and to maximize their utility. Dedicating an entire chapter of the User Manual to them should help achieve this objective.

Towards continuous integration with Frama-C

The usage of analysis scripts is shifting from a formal methods-centric view – in which the code is considered as “finished” and the main task is the verification with Frama-C – towards an agile development-centric view, in which Frama-C is a tool to be used throughout the development process. By inserting Frama-C in a continuous integration pipeline, the user should obtain helpful feedback after each commit.

Current developments in the platform should allow this to become true in the nearby future, thanks to the support of EU project SPARTA*. Stay tuned!

*This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 830892.