Page du cours de Conception Formelle -- Partie Frama-C
Polycopié
Sa version open-dyslexic est ici
Sujets de TD machine
- TP1 :
- TP2 :
- TP3 :
- TP4 :
- TP5 :
Sujets d’exercices
- TD1 :
- TD2 :
- TD3 :
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
- Le site de Frama-C
- Documentation pour ACSL (notamment pour la syntaxe)
- Manuel du module WP
- Manuel du module RTE
- ACSL by Example. Un livre donnant des exemples (par difficulté croissante) d’algorithmes spécifiés et vérifiés avec Frama-c.