Frama-C Github Action

André Maroneze - 19th Nov 2020

In 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 from the cloud

With the Docker images mentioned in the previous post, we created a Frama-C/Eva Github Action, which has been published to the Github Marketplace in the Code quality category (since sound static analysis is not (yet!) a category).

This action reuses the analysis scripts architecture to provide a standardized way to run Eva from any C project. It still requires a non-trivial setup, so it is currently recommended for users already having experience with Frama-C.

If you already have a code base configured to use Frama-C’s analysis scripts (as indicated in chapter Analysis Scripts, in the Frama-C user manual), you can simply follow the instructions present in the Github Action README to add a CI pipeline that will, after each commit, re-run Eva and produce some text logs and a SARIF report. Other developers in the same project, even if they have never installed Frama-C, will still be able to see the results (e.g. with a VS Code extension for SARIF) and benefit from the analysis.

If you have never setup Frama-C in your code base, it is still possible to do so via the Github Action, but it is not recommended: trying to blindly setup Frama-C to parse and analyze a new code base, having only the feedback from the CI pipeline, is likely to be slow and error-prone. We expect that, in the future, this task will be easier; for now, however, we recommend users to locally use Frama-C for the initial setup.

Note that this is but one of several possible Frama-C actions; other plug-ins and analyses can be partially automated and thus benefit from CI integration. In particular, we intend to release some heuristics-based scripts which should be able to estimate the difficulty of running Frama-C on a new code base, even before trying to parse it. Running such a script via a Github Action would allow prospective users to have a rough idea of whether Eva might give interesting results. All of this is in the pipeline, and we expect it to be available soon!

Gitlab CI with Frama-C

If you have some C code hosted on Gitlab, you can use a Docker-based Gitlab Runner to integrate Frama-C in your CI pipeline. You will need a Docker executor and a Frama-C Docker image, such as the ones in our Docker Hub.

An example of its usage can be found in Frama-C’s Open Source Case Studies repository. It contains several directories, each of them a use case, with one or more “whole program” analyses; in some cases, a single .c file; in others, the full test suite of a complete application.

Each use case follows the same convention: a .frama-c directory containing a GNUmakefile which lists the targets and analysis parameters (preprocessing flags, Eva fine-tuning). The main directory contains a global Makefile with a target all which allows running all test cases. Then, a Makefile.common file included by each test case allows the easy addition of a sarif rule which produces a SARIF report via the Markdown Report plug-in. Then, the following .gitlab-ci.yml file creates the CI integration:

default:
  image: framac/frama-c:dev

build:
  tags:
    - docker
  script:
    - make -B all >/dev/null
    - git diff --exit-code
    - make sarif
  artifacts:
    paths:
    - "*/.frama-c/*.sarif"

We use the development version of the Frama-C Docker file (note: prefer using a fixed, stable Frama-C release, unless you want to closely track the Frama-C development). The docker tag is specific to our Gitlab instance, used by a Gitlab Runner.

The script part itself is very short: basically, run make all, compare oracles (via git diff), and produce SARIF reports. These are all bundled up as artifacts after the run, and can be downloaded and displayed in an IDE or SARIF viewer.

Practical examples

For a practical usage example of the Frama-C/Eva Github action, see our (periodically up-to-date) fork of Monocypher with a working .github/workflows/main.yml and a CI badge in the README.md.

For an example with Gitlab, as mentioned before, our open-source-case-studies repository contains a .gitlab-ci.yml file and a CI badge showing if the CI build passed, that is, if the SARIF artifact was produced.

Conclusion

Thanks to the Frama-C Docker images, and to the structure provided by analysis scripts, integrating Frama-C in the CI pipeline of a code base is relatively easy. For new users, the hardest part is the setup of the code base itself to run with Frama-C: finding sources, parsing flags, fine-tuning Eva, etc. Once these are done, the CI integration is straightforward.

Acknowledgements

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 830892 (a.k.a. SPARTA). One of the goals of SPARTA is to promote better integration between tools, so support for CI pipelines and standardized formats (SARIF) is a way to foster collaboration.

André Maroneze
19th Nov 2020