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.