Frama-C The Ltest “meta-plugin” (composed of three parts: LUncov, LAnnotate and LReplay) has been (re-)released on Frama-C’s public Gitlab, and as 3 opam packages: frama-c-luncov, frama-c-lannotate, and lreplay. These plugins help measure test coverage based on hyperlabels. Details about them are published here and here (you can also see the LTest...
Read MoreIn 2016, a few blog posts (part 1, part 2, part 3) presented a short tutorial on writing ACSL clauses for Eva (back then, the Value Analysis plug-in). A few things changed since then, but posting them again in this blog would lead to the same issue in the future....
Read MoreThere are several reasons one might want to run an old version of Frama-C: to test some outdated plugin which is only compatible with a previous version; to re-run analyses mentioned in an old tutorial or blog post; to compare results between Frama-C versions; for nostalgia’s sake. Whatever the reason,...
Read MoreIn Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement assert: the admit and check annotations. In a nutshell, assert P is equivalent to check P; admit P. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external...
Read MoreNew Frama-C Docker images, with a graphical interface, are available in the Docker Hub. They allow running Frama-C via a browser, on Windows, macOS and Linux. Frama-C + Docker + noVNC = Frama-C GUI on a browser The “traditional” Frama-C Docker images available on Docker Hub lack the graphical interface,...
Read More