Vincent Penelle

Comment installer frama-c :

Méthode à préférer

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.

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).
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. 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). 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.
tom(); ?>