Installer frama-c sur un système Guix

Frama-c

Frama-c est une plate-forme open-source pour l'analyse de code C. Il permet de prouver des propriété d'un programme à partir du code source et de spécification intégrer au code source. Il est donc possible de vérifier les spécifications pour un code donné. Pour cela frama-c utilise le langage ACSL.

Installation

À ce jour frama-c n'est pas présent dans les dépôts Guix, il nous faux donc l'installer par un autre moyen. La procédure d'installation recommander sur la page de frama-c utilise Opam, qui est le gestionnaire de paquet OCaml. Nous allons l'utiliser, en attendant de faire un vrai paquet Guix.

Environnement

Je considère ici que les outils de développement de base (gcc, make, pkg-config) sont déjà installer sur votre système.

Pour les dépendanceq je vous propose un script qui permettra d'entrer dans un environnent contenant les dépendances, sans pour autant les installer dans l'environnement courant. Cela va permettre de rentrer et de sortir de l'environnement à notre guise.

#!/bin/sh

guix environment --ad-hoc                       \
    opam                                        \
    unzip                                       \
    make                                        \
    gmp                                         \
    libgnomecanvas                              \
    gtk+@2                                      \
    gtksourceview@2                             \
    zlib

Pour rentrer dans l'environnement il suffit de lancer le script en mode terminal:

chmod u+x ./env.sh
./env.sh

Configuration d'Opam

Avant d'installer frama-c il est nécessaire de configuré opam, cette étape va nécessiter de rajouter un nouveau fichier envrc.

export PKG_CONFIG_PATH=$GUIX_ENVIRONMENT/share/pkgconfig/:$PKG_CONFIG_PATH
export PKG_CONFIG_PATH=$GUIX_ENVIRONMENT/lib/pkgconfig/:$PKG_CONFIG_PATH
export LD_LIBRARY_PATH=$GUIX_ENVIRONMENT/lib:$LD_LIBRARY_PATH

Ce fichier va nous permettre exporter dans notre environnement les bons chemins. On commence par ajouter explicitement les chemins ajouter par notre environnement courant pour pkgconfig. Ainsi que les chemins pour nos bibliothèques dynamique.

Pour appliquer les changements, on utilise cette commande.

source envrc

Puis on initialise opam, quand il demande si l'on veut qu'il modifie votre ~/.bash_profile, nous allons répondre non.

opam init

Finalement, nous allons ajouter une ligne à notre fichier envrc, ce qui nous donne le fichier suivant.

export PKG_CONFIG_PATH=$GUIX_ENVIRONMENT/share/pkgconfig/:$PKG_CONFIG_PATH
export PKG_CONFIG_PATH=$GUIX_ENVIRONMENT/lib/pkgconfig/:$PKG_CONFIG_PATH
export LD_LIBRARY_PATH=$GUIX_ENVIRONMENT/lib:$LD_LIBRARY_PATH

eval $(opam env)

Frama-c

Maintenant on peut installer frama-c avec la commande suivante.

opam install frama-c

Opam va maintenant télécharger et installer environ 37 paquets.

J'ai eu des problèmes avec la version 22, je vous conseille donc d'installer la version 21.1 en utilisant frama-c.21.1 au lieu de frama-c.

Dernière étape, configuré why3:

why3 config --detect

Lancement

On doit maintenant pourvoir lancer frama-c.

Mode Emacs ACSL

Frama-c est fournie avec un mode Emacs pour éditer les spécifications ACSL dans les sources C avec de la coloration syntaxique. Pour utiliser ce mode, vous pouvez rajouter les lignes suivante à votre configuration Emacs, ~/.emacs.

(load-file "~/.opam/default/share/emacs/site-lisp/acsl.el")
(load-file "~/.opam/default/share/emacs/site-lisp/frama-c-init.el")