# Mode d'emploi TP WP de Frama-C

## Initialiser Frama-C sur sa session Ensimag:

    source /matieres/4MMACSS/init-frama-c.sh

Vérifier avec

    frama-c --version

qui doit répondre

    25.0 (Manganese)

## Télécharger les fichiers du TP:

   tp_wp.zip

## Prendre en main l'archive fournie:

L'archive  contient:
- un ensemble de fichiers *.c
- un Makefile

Pour chaque fichier -- excepté `any.c`, qui est un fichier auxiliaire
définissant une fonction retournant un entier lu sur l'entrée standard
-- vous devez prouver avec Frama-C que le programme n'a pas de RTE et
que toutes les assertions sont valides (quelques indications sont
données dans les commentaires commençant par `// TODO`). En
particulier, vous aurez à trouver les invariants de boucles
nécessaires pour faire ces preuves.

Avant d'analyser vos fichiers avec Frama-C, compilez les avec l'option
`-Wall` de `gcc`, afin de vérifier leur correction syntaxique (lancez
juste `make all`). Vous pouvez exécutez chacun de ces programmes et
observer la valeur de retour de leur fonction `main`, en vous
inspirant de la ligne de commande donnée ici pour le programme `mult17`

    ./mult17; echo $?

(attention, dans le shell, la valeur de retour est donnée comme un
entier non-signé sur un octet, avec une sémantique "modulo").

Alors, pour lancer la vérification du programme `mult17.c` en Frama-C,
lancer la commande suivante. Ici, l'option `-wp-split` indique de casser
les obligations de preuve autant que possible, ce qui aide à
identifier où le prouveur échoue éventuellement:

    frama-c-gui -wp -wp-rte -wp-split mult17.c &

Vous pouvez éventuellement commencer par faire la vérification sans
les conditions RTE (sans l'option `-wp-rte`) et l'insérer
ultérieurement.

## Utiliser Frama-C

L'interface de Frama-C ne permet pas d'éditer les fichiers. Afin de modifier un fichier:

- modifier et sauver le fichier dans votre éditeur favori;
- afin de réessayer la preuve d'une seule annotation: d'abord, charger votre modification avec le menu ``File/Reparse'';
 ensuite, lancer le prouveur par un clic-droit  sur la ligne de l'annotation;
- afin de réessayer la preuve de toutes les annotations, c'est plus rapide d'utiliser Frama-C en mode console:

        frama-c -wp -wp-rte -wp-split myfile.c

Ne relancer l'interface graphique que pour voir les obligations de preuve non prouvées:

    frama-c-gui -wp -wp-rte -wp-split myfile.c &


## Comprendre les couleurs des "boulettes" sur les annotations
- blue: waiting for the proof
- green: proved
- orange: the proof attempt has failed
- green/orange: proved by assuming an other orange goal


## Voir les buts donnés au SMT-Solveur

- cliquer sur le menu "WP Goals"
- cliquer sur un but:
  * surligne en bleu l'assertion ACSL correspondant à ce but
  * surligne en jaune la sequence d'instructions impliquées dans ce but
  * surligne en rose les assertions ACSL utilisées (dépendances)
- réciproquement, cliquer sur une assertion ACSL fait apparaître la
  liste des buts associés à cette assertion (il y en a plusieurs à
  cause du -wp-split)
- double-cliquer sur un but affiche celui-ci (un onglet permet de
  choisir différents mode d'affichage)
- on quitte cette fenêtre d'affichage en cliquant sur le bouton
  "list of goals" (un bouton avec un doigt au-dessus d'un texte).


## Ordre des exercices

### Exercice 1

- mult17.c: un premier exemple pour prendre un main et comprendre l'outil
  + lancer `frama-c-gui mult17.c &`
  + faire insérer les assertions rte (absence de débordements) sur la fonction "mult" (via clic-droit sur la fonction mult dans la fenêtre centrale) 
  + puis essayer de faire prouver les assertions de la fonction "mult" par WP.
- mult17.c: débogguer le programme pour les assertions soient prouvées.


### Exercice 2 

- div0.c: invariants + precondition + postcondition + function calls.
- linear_search.c: linear search in an array.


### Exercice 3 au choix selon le temps

- div1.c: proche de  "div0.c" mais avec une introduction aux pointeurs aux aliases
- copie de tableau: comprendre `disjoint_array_copy.c` et prouver `array_copy.c` (copie de tableau avec recouvrement possible)

### Exercices avancés optionnels

- binary_search.c: une version non signée de `binary_search` pour faire la recherche dans de très gros tableaux!
- min_sort.c: tri par sélection avec manipulation de pointeur (suivre les TODO)


## Installer Frama-C sur son PC

1. Installer OPAM: http://opam.ocaml.org/doc/Install.html.

2. Si la version OPAM >= 2.1  (cf. `opam --version`)

        opam pin frama-c 25.0

3. Si la version OPAM < 2.1

        opam install depext
        opam depext frama-c
        opam pin frama-c 25.0

4. Finaliser l'installation:

        opam pin alt-ergo 2.4.0
        rm -f ~/.why3.conf ; why3 config detect