CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Consignes pour l'installation de Frama-C/WP

Ces consignes concernent les deux séances sur Frama-C encadrées par Nikolai Kosmatov.

Il est fortement recommandé d’installer Frama-C au préalable sur votre machine personnelle avant la séance pour ne pas perdre de temps pendant le TP. Il sera possible d'utiliser l'une des solutions d'installation suivantes :

1. Docker

Installer une image docker avec Frama-C v.22.0 et MetAcsl v.0.1. Il y a deux possibilités, la première étant la plus simple à mettre en œuvre.

Affichage dans le navigateur web

Cette solution fonctionne avec tous les systèmes d'exploitation.

Téléchargez ce script sous Linux ou celui-ci sous Windows, et placez le dans le dossier où vous souhaitez travailler. Exécutez ensuite ce script (dans PowerShell sous Windows), il téléchargera l'image Docker lors de la première utilisation. Votre navigateur web devrait s'ouvrir sur l'adresse http://localhost:6080 et afficher le bureau Ubuntu. Vous pouvez lancer un terminal depuis la barre d'outils en bas de l'écran. Vos fichiers se trouvent dans /workspace. Vous pouvez tester l'installation en exécutant la commande frama-c-gui, vous devriez voir l'interface graphique de Frama-C s'afficher.

Les fichiers sources et la documentation sont disponibles sur GitHub.

Affichage avec un server X11

Cette solution ne fonctionne pour l'instant pas sous Linux.

Sous MacOS, elle fonctionne avec le serveur XQuartz, et sous Windows avec le serveur VcXsrv.

Téléchargez ce script sous Linux ou celui-ci sous Windows, et placez le dans le dossier où vous souhaitez travailler. Exécutez ensuite ce script (dans PowerShell sous Windows), il téléchargera l'image Docker lors de la première utilisation. Une fois connecté dans le conteneur Docker, utilisez la commande frama-c-gui pour lancer Frama-C.

Les fichiers sources et la documentation sont disponibles sur GitHub.

Pour l'utilisation d'images Docker avec une interface graphique sous X11, vous pouvez également consulter cette page.

2. VirtualBox

Installer VirtualBox sur votre machine personnelle, puis télécharger et importer la VM (sous Linux Ubuntu) avec Frama-C v.22.0 et MetAcsl 0.1, provisoirement disponible à partir de VM_Frama-C_22.ova. Le login et le mot de passe sont user. Cette VM a été testée avec la version VirtualBox 6.1 (normalement, le format OVA devrait être compatible avec d’autres versions.)

3. Installation native

Installer une version récente de Frama-C (la dernière est Frama-C 22.0 (Titanium), de novembre 2020) sur votre machine personnelle. On l'utilisera de préférence sous Linux. L'installation est possible via opam (recommandé), ou à partir des sources, ou à partir des packages Linux. Sous Linux Ubuntu, on peut procéder comme suit :

  • installer opam (version ≥ 2.0.0), voir https://opam.ocaml.org/doc/Install.html
  • vérifier la version d’opam installée (opam --version)
  • installer Frama-C, Alt-Ergo, Why3, MetAcsl et leurs dépendances, par exemple, avec les commandes suivantes :
  opam init
  opam update
  opam switch create 4.08.1_fc22 ocaml-base-compiler.4.08.1
  eval `opam env`
  opam install depext 
  opam depext frama-c.22.0
  opam install alt-ergo.2.3.0 why3.1.3.3 frama-c.22.0 frama-c-metacsl.0.1
  why3 config --detect

Pour plus de détail, voir https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md

Pour tester l’installation, lancer frama-c-gui dans un terminal, vous devez voir s’ouvrir l’interface graphique de Frama-C.