diff --git a/TD1/.DS_Store b/TD1/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..d01b1532d58335ad9f4ee22eda1f8f91b7e85519 Binary files /dev/null and b/TD1/.DS_Store differ diff --git a/TD1/Rapport.md b/TD1/Rapport.md new file mode 100644 index 0000000000000000000000000000000000000000..bc0ba37084ebb33bc28ecc6c331df5c3cd7f9905 --- /dev/null +++ b/TD1/Rapport.md @@ -0,0 +1,84 @@ +# Rapport + +## CERT C EXP33-C. Do not read uninitialized memory + +### Question 1 + +Les messages émis sont 'normaux', sachant que sign vaut -1, 1 ou UNINITIALIZED et que la valeur de retour de la fonction est 0 ou 1 (booléen). +Le problème du CERT est identifiable grâce à la possibilité d'avoir un sign UNINITIALIZED. + +### Question 2 + +Il n'y a pas de Red Alarm. +Pour le second 'if' de 'set_flag', la valeur de number est dans l'intervalle [-INT_MIN..0], ce qui correspond bien au faite qu'il est dans le 'else' de la condition de 'number > 0'. + +### Question 3 + +Le Frama_C_show_each_set_flag affiche '[-INT_MIN..INT_MAX], {-1;1}' +Le Frama_C_show_each_is_negative affiche '[-INT_MIN..INT_MAX], {-1;1}' +On voit que le UNINITIALIZED n'est plus pris en compte dans les lignes suivantes, Eva considère que sign vaut 1 ou -1. + +### Question 4 + + +Avec '-eva-partition-history 2', Frama_C_show_each_set_flag affiche maintenant trois cas différents : +Frama_C_show_each_set_flag : {0}, Bottom +Frama_C_show_each_set_flag : [-INT_MIN..-1], {-1} +Frama_C_show_each_set_flag : [1..INT_MAX], {1} + +On voit que Eva garde en mémoire plusieurs chemins d'exécution et 'relit' les valeurs de number et de sign en fonction des cas. + +### Question 5 + +On voit avec l'option '-eva-interprocedural-history' que l'analyse lève une erreur : '1 access to uninitialized left-values'. +En effet, dans le scope de la fonction 'set_flag', la valeur de sign peut être non initialisé et si on garde cette information en revenant de la fonction, on accède à cette variable non initialisé dans le return, ce qui déclance l'alarme rouge. + +### Question 6 + +En mettant 'number >= 0' dans la première condition de 'set_flag', on va initialiser la valeur de 'sign' dans tous les cas. +En effet, l'exécution d'Eva ne déclenche plus d'alarme après cette modification. + +## CERT C EXP33-C bis + +### Question 7 + +Dans l'exécution du ficher 'cert_exp_33_realloc.c', Eva déclenche 2 erreur : + +- 1 access to uninitialized left-values +- 1 escaping address + +Celle qui correspond à la lecture d'une location mémoire non-initialisée est la première : access to uninitialized left-values. + +### Question 8 + +Avec une option de '-eva-slevel 3', nous n'avons plus qu'une erreur : 1 access to uninitialized left-values. En effet, les problèmes où resize_array rate et renvoie 0 sont attrapé apr le handle error. +Eva se 'souvient' que l'array est alloué si et seulement si resize_array retourne quelque chose de non nul. +Maintenant qu'Eva est sûr que les print du tableau tapent dans un emplacement alloué, la seule erreur qu'il reste est que cette emplacement n'est pas initialisé. + +### Question 9 + +Avec la correction, il n'y a plus d'erreur détecté par Eva (le nouveau tableau a bien été initialisé) + +## CWE 20 + +### Question 10 + +Frama-C/Eva est plutôt critique du code... 8 alarmes sont déclenchées : + +- 5 integer overflows +- 2 invalid memory accesses +- 1 access to uninitialized left-values + +### Question 11 + +Les modifications proposées ne permettent pas de supprimer toutes les erreurs. Elles suppriment les 5 erreurs integer overflows mais pas les accès invalid et la non-initialisation. + +### Question 12 + +Grâce à la directive de split, on a plus les accès invalides à la mémoire + +## libstring + +### Question 13 + +Il n'y a bien aucune erreur dans l'exécution avec la librairie libstring. diff --git a/config/cert_exp_33.c b/TD1/config/cert_exp_33.c similarity index 100% rename from config/cert_exp_33.c rename to TD1/config/cert_exp_33.c diff --git a/config/cert_exp_33_realloc.c b/TD1/config/cert_exp_33_realloc.c similarity index 100% rename from config/cert_exp_33_realloc.c rename to TD1/config/cert_exp_33_realloc.c diff --git a/config/cwe20.c b/TD1/config/cwe20.c similarity index 100% rename from config/cwe20.c rename to TD1/config/cwe20.c diff --git a/config/example1.c b/TD1/config/example1.c similarity index 100% rename from config/example1.c rename to TD1/config/example1.c diff --git a/config/libstring.c b/TD1/config/libstring.c similarity index 100% rename from config/libstring.c rename to TD1/config/libstring.c diff --git a/config/libstring.h b/TD1/config/libstring.h similarity index 100% rename from config/libstring.h rename to TD1/config/libstring.h diff --git a/config/miniz.c b/TD1/config/miniz.c similarity index 100% rename from config/miniz.c rename to TD1/config/miniz.c diff --git a/config/miniz.h b/TD1/config/miniz.h similarity index 100% rename from config/miniz.h rename to TD1/config/miniz.h diff --git a/frama-c-gui.png b/TD1/frama-c-gui.png similarity index 100% rename from frama-c-gui.png rename to TD1/frama-c-gui.png diff --git a/studia.png b/TD1/studia.png similarity index 100% rename from studia.png rename to TD1/studia.png diff --git a/tp.md b/TD1/tp.md similarity index 100% rename from tp.md rename to TD1/tp.md