Le projet Csur

Introduction

Le projet Csur est un analyseur assez simple de code C. Il est présenté ici sous forme d'un projet servant d'évaluation aux étudiants du cours d'analyses statique de Jean Goubault-Larrecq. Le but de Csur est de détecter des erreurs communes à l'exécution dans des programmes C: code mort, débordements arithmétiques, accés illégaux à des zones mémoires.

Le projet Csur est soumis à un copyright, dont le but est de permettre sa libre distribution à des fins non commerciales. La version de ce répertoire est une version destinée au projet étudiant susmentionné: certains sources ont été tronqués afin que les étudiants puissent les compléter; cependant tous les fichiers .cmo ainsi que l'exécutable csur sont fournis. Il existe une autre version de ce répertoire dont les sources sont complets, soumis à un copyright similaire, mais dont l'accès est interdit aux étudiants: contacter Jean Goubault-Larrecq.

Le projet se trouve dans le répertoire courant, ou bien sous forme d'une archive tar compressée par gzip. Consultez le makefile pour plus d'informations. Csur est prévu pour fonctionner sur machines Linux disposant d'Ocaml. Csur est écrit en Ocaml, et a été testé avec Ocaml 2.04. Pour fonctionner, Csur a besoin que le préprocesseur C cpp et le compilateur gcc soient tous les deux accessibles dans le PATH. Le premier est utilisé pour effectuer tous les traitements dévolus au préprocesseur C, le second est utilisé comme un moyen facile et sûr (quoiqu'un peu lent) de calculer des tailles de types de données et des offsets dans des structures.

Csur traite pratiquement de tout le C ANSI: il ne lui manque en gros que les types énumérés, les bitfields et les initialiseurs. De plus, il ne reconnaît pas certaines bizarreries comme la syntaxe L'a' pour les caractères Unicode, '\xa0' pour les caractères hexa. Les mots-clés auto et register sont ignorés. Il n'y a pas de notion de portée pour les struct et les union (elles sont toutes globales). A part ca, les plus grosses limitations de Csur sont qu'il ne sait pas faire d'analyse séparée: il ne sait analyser que des programmes qui tiennent en un seul fichier; et qu'il n'a aucune idée de la sémantique de la plupart des fonctions des bibliothèques C standard (pour l'instant).

Comment effectuer votre travail de projet

1. Intervalles d'entiers - opérations arithmétiques: itv_int.ml, cf. itv_int.mli;
2. Intervalles d'entiers - opérations logiques: itv_int_log.ml, cf. itv_int_log.mli;
3. Intervalles flottants: itv_float.ml, cf. itv_float.mli;
4. Zones mémoire et pointeurs: zones.ml, cf. zones.mli;
5. Glu - calculs sur environnements abstraits, généralités et pointeurs: glue.ml, cf. glue.mli;
6. Glu - calculs sur environnements abstraits, opérations arithmétiques et logiques: glue_log.ml, cf. glue_log.mli;
7. Fonctions de bibliothèque: api.ml, cf. api.mli;
8. Affichage des résultats: report.ml, cf. report.mli.

Foire aux questions

Comment je vérifie que ca compile?
Sous Unix, tapez ./configure. Si vous tapez 0, vous n'aurez plus qu'à taper make et vérifier que ca fonctionne. Pour commencer à coder, tapez le numéro de votre projet. Dans les deux cas, cela vous fabrique le bon makefile.
Sous Windows... utilisez Cygwin.

Ca ne compile pas!
Vous avez peut-être une version ancienne (d'avant vendredi 7 février 2003, 14h15); re-récupérez la nouvelle version. N'oubliez pas de taper ./configure puis make.

Quelles versions de OCaml sont supportées?
Les versions 2.04 et 3.06, à l'heure actuelle. Si vous avez une autre version, plusieurs possibilités: la meilleure est d'installer OCaml v3.06; si vous ne le voulez pas, mais que vous avez une version proche, disons 2.07, alors tentez votre chance en faisant ln -s Ref-2.04 Ref-2.07; dans tous les autres cas, envoyez-moi un mail.

csur compile, mais j'ai un message d'erreur étrange à l'exécution
par exemple

./csur: error while loading shared librairies: libncurses.so.4: cannot open shared objet file: No such file or directory

Vous avez un problème dans l'installation de OCaml. Réinstallez OCaml.

Comment vous serez jugés