Frama-C: analyse statique de programmes C

Anne Frama-C analyse_statique

Pour vérifier les dépendances nécessaires à Frama-C, on fait l’installation dans une machine virtuelle vide.

Installation

Comme je l’ai expliqué, j’utilise VirtualBox, et les étapes suivantes ont été faite à partir d’une installation propre d’une Debian (debian-testing-amd64-netinst.iso) sans logiciel optionnel (construire la machine prend environ 15 minutes).

  • démarrer la machine et se connecter comme user (ou tout autre nom que l’on a donné à l’utilisateur)

  • installer sudo, ajouter user aux sudoers, et se déconnecter :

$ su
# apt-get install sudo
# adduser user sudo
# ^D
# ^D
  • se reconnecter en tant que user et installer certains paquets :
$ sudo apt-get install gcc make vim
$ sudo apt-get install ocaml ocaml-findlib
$ sudo apt-get install xfce4
  • démarrer le serveur X pour avoir un environnement graphique :
$ startx
  • ouvrir un terminal, et installer d’autres paquets :
$ sudo apt-get install liblablgtksourceview2-ocaml-dev
$ sudo apt-get install liblablgtk2-gnome-ocaml-dev
$ sudo apt-get install graphviz
  • récupérer Frama-C et le décompresser :
$ wget http://frama-c.com/download/frama-c-Fluorine-20130601.tar.gz
$ tar zxvf frama-c-Fluorine-20130601.tar.gz
  • configurer, compiler et installer :
$ cd frama-c-Fluorine-20130601
$ ./configure
$ make
$ sudo make install
  • essayer en faisant :
$ frama-c --help
$ frama-c --verision
$ frama-c-gui

Et ça doit marcher !

Cette installation ne conitient pas le greffon jessie (ni why, etc) et pour utiliser le greffon WP, d’autres outils sont probablement nécessaires (comme alt-ergo, coq, et autres).

Preprocessing C applications

S’il y a des problèmes au sujet du pré-processing des sources C, voir pluôt mes notes au sujet de gcc.

Documentation

Voir aussi :

Table des matières
Tags
Dernières notes