Frama-C In 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 MoreWhen using Frama-C in a series of benchmarks or test suites, especially when they consist of several small programs, consider using -no-autoload-plugins for better performance. This post explains why it is useful, as well as its downsides. Minimize startup time with -no-autoload-plugins By default, running frama-c makes it load all...
Read MoreIn the previous post, we mentioned the official Frama-C Docker images. In this post, we present two examples where these images allow us to incorporate Frama-C in a continuous integration process: a Frama-C Github Action, as well as integration of Frama-C in a Gitlab CI pipeline. Github Action: run Frama-C/Eva...
Read MoreFrama-C now has official Docker images in the Docker Hub! In this post we describe what they contain and how we intend to evolve them. If you have other uses for Docker images, don’t hesitate to contact us! Official Frama-C Docker Images in Docker Hub Official Frama-C Docker images are...
Read More