Comment installer frama-c :
Méthode à préférer
- Suivez les instructions données là.
- Une fois cela fait, il faut dire au système d’utiliser les paquets opam. Cela se fait à l’aide de la commande `eval $(opam env)` (que vous pouvez parfaitement ajouter dans votre bashrc).
- Avant de lancer frama-c pour la première fois, il faut dire à why3 de détecter les prouveurs (sinon il ne saura rien prouver), cela se fait à l’aide de la commande `why3 config --full-config`.
- Une fois cela fait, vous pouvez lancez frama-c grâce à la commande `frama-c-gui FICHIERS` (où on remplace FICHIERS par les fichiers à analyser), en ajoutant d’éventuelles options. Mais on verra cela en TP.
Ancien tutoriel que je laisse pour l’histoire, mais il est sans doute moins utile.
Attention : Ceci est une tentative de tutoriel, que j’ai pu tester avec certains d’entre vous et chez moi. Je ne garantis pas que ça marchera chez tout le monde. En cas de problème, si vous n’êtes pas sous linux, j’aurai sans doute du mal à vous aider directement, mais vous pouvez consulter la documentation de frama-c sur leur site ou demander de l’aide sur stackoverflow (les développeurs y sont assez actifs. Toutefois, avant de recourir à cela, lisez bien tout ce que je mets ici, et les messages d’erreurs que vous aurez. Certaines erreurs peuvent être peu lisible, mais normalement, la plupart seront réglées par ce que je vais dire ici.
Méthode simple mais pas forcément à jour ni complète.
Votre gestionnaire de paquet dispose peut-être d’un paquet frama-c (c’est le cas sous Debian). Faites attention à s’il installe la version graphique ou pas. Sous Debian, il y a deux paquets : frama-c-base qui n’installe pas la version graphique, et frama-c qui l’installe, donc installez évidemment la seconde (on peut faire tout le cours en version en ligne de commande, mais c’est moins pratique et lisible). Ça ne sera pas la dernière version, mais on s’en fout. Sous archlinux, il existe un paquet dans AUR qui a l’air d’être à jour (j’ai pas testé cela dit).
Dans tous les cas, vérifiez que vous avez bien un prouveur d’installé avec. Dans ce cours, un seul est suffisant (alt-ergo, qui normalement sera installé avec), mais attention, depuis la version 20, il faut obligatoirement installer également why3 (idem, il y a probablement des paquets pour ces derniers).
Méthode plus avancée qui donne un truc à jour.
Cette méthode utilise opam qui est un gestionnaire de paquet pour Ocaml (un peu comme pip). Ce n’est pas le plus simple à mettre en place, mais une fois que ça l’est, ça marche bien.
1: Installer opam
Cela va dépendre de votre sytème d’exploitation. Plus d’info
ici.
- Pour linux, vous avez très probablement un paquet nommé 'opam' dans votre gestionnaire de paquet. Installez-le.
- Pour mac, le paquet 'opam' est normalement disponible via homebrew.
- Pour windows, je ne sais pas trop, mais cette page explique comment faire. Je n’ai pas testé, je ne sais pas si c’est facile ou compliqué. Dans la mesure du possible, je vous conseille de ne pas utiliser windows pour ce cours (mais si vous n’avez pas d’autre moyen, ça doit rester possible).
2: Initialiser opam
Lancez la commande 'opam init' et acceptez les options par défaut. C’est fait.
Attention, cela met en place opam, mais n’ajoute PAS les paquets installés via opam dans votre PATH (pour que votre terminal trouve les programmes installés).
- Pour que cela soit le cas, il faut taper 'eval $(opam env)' dans votre terminal, et vous aurez alors accès aux programmes installés via opam.
Attention, cette commande n’est valide QUE pour la session en cours. Je vous conseille d’ajouter cette commande dans votre .bash_rc, comme ça elle sera exécutée à chaque fois que vous lancez un terminal.
3: Installer frama-c.
D’abord, on va installer les dépendances demandées par frama-c.
- Tapez 'opam install depext'.
- Tapez 'opam depext frama-c'.
Opam va alors installer, via votre gestionnaire de paquet, tous les paquets de votre distribution dont frama-c a besoin (essentiellement, les paquets gtk requis).
- Installons maintenant frama-c avec 'opam install frama-c'.
Frama-c est maintenant normalement installé, avec la version 22.0, et tous les modules externes dont nous aurons besoin.
Attention ! En cas d’erreur
Il est possible que cela ne marche pas (je viens de le faire chez moi, sous manjaro, et depext n’avait visiblement pas installé les paquets nécessaires). Dans ce cas, il manque probablement des paquets qui vous seront mentionnés dans les erreurs. Regardez-les bien. Sous manjaro, j’ai du installer manuellement les paquets 'gtksourceview2' et 'libgnomecanvas' (dans AUR). A priori, sous ubuntu/debian, ce problème n’arrive pas.
4: Forcer why3 à utiliser alt-ergo.
Un dernier point important, avec les versions actuelles des paquets (14/03/2020), il y a un léger problème : why3 (qui dans la version 20 rassemble tous les prouveurs pour que frama-c les utilise) ne reconnait pas par défaut la dernière version d’alt-ergo (le prouveur qu’on utilise). Pour régler cela, il suffit de taper la commande suivante :
Frama-c devrait maintenant pouvoir utiliser alt-ergo, et vous avez normalement une installation fonctionnelle de frama-c permettant de réaliser les TP. Ouf.
Il vous faudra peut-être activer alt-ergo dans frama-c, en cliquant sur le bouton 'Provers' dans l’onglet WP, et en passant l’interrupteur à ON.