Page du cours de Conception Formelle -- Partie Frama-C

Polycopié

Le cours est là

Sa version open-dyslexic est ici

Sujets de TD machine

Sujets d’exercices

Devoir maison

Annales d’examens

Quelques sujets d’années passées. Le format devrait être globalement similaire.

Comment mettre en place son environnement de travail

Au CREMI

Avant chaque session, tapez les commandes suivantes :

  • export OPAMROOT=/opt/local/opam
  • eval $(opam env)

La première fois uniquement (après les 2 précédentes) :

  • why3 config detect

Une fois cela fait, vous pourrez travailler sur les TPs, en lançant frama-c-gui (cf TP1).

Chez vous

Il faut d’abord installer Frama-c. Vous pouvez vous reporter aux instructions du site web de Frama-c, mais cela devrait correspondre, si vous êtes sur linux, à :

  • installer opam via votre gestionnaire de paquet
  • l’initialiser avec opam init
  • installer les paquets nécessaires avec opam install alt-ergo z3 why3 frama-c

Ensuite, avant chaque session, tapez :

  • eval $(opam env)

La première fois :

  • why3 config detect

Ressources utiles