Une démo de CompCert

Dans le cadre de la présentation de CompCert et Coq (pour le cours ACSS en Ensimag 2A), voilà une petite démo de CompCert.

• Commencez par télécharger et visualiser la vidéo.
• Vous pouvez rejouer la démo en téléchargeant l'archive demo.tgz, puis avec les commandes:

         tar zxvf demo.tgz
         ./demo.sh mini_example.c 1 replay
       

  Alternativement, vous pouvez regarder la liste des passes disponibles avec:

         ./demo.sh mini_example.c
       

  ... puis relancer l'étape 10 (oracle d'allocation de registres) avec:

         ./demo.sh mini_example.c 10 replay
       

  L'argument replay indique qu'il ne faut pas chercher à recompiler mini_example.c avec CompCert.