diff --git a/_posts/2020-06-17-analysis-scripts-user-manual.md b/_posts/2020-06-17-analysis-scripts-user-manual.md new file mode 100644 index 0000000000000000000000000000000000000000..78db8b4f7f13f1f847c1759c5dce1f67bfdc4f4c --- /dev/null +++ b/_posts/2020-06-17-analysis-scripts-user-manual.md @@ -0,0 +1,51 @@ +--- +layout: post +author: André Maroneze +date: 2020-06-17 12:00 +0100 +categories: scripts usability +title: "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](http://frama-c.com/download/frama-c-user-manual.pdf). +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](https://git.frama-c.com/pub/frama-c), 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*](https://sparta.eu). +Stay tuned! + +<small>*This project has received funding from the European Union's Horizon 2020 +research and innovation programme under grant agreement No 830892.</small>