From 3239324141c4cab1de3c6bdd32900df7fb200af5 Mon Sep 17 00:00:00 2001
From: Moi <you@example.com>
Date: Fri, 21 Mar 2025 08:11:44 +0100
Subject: [PATCH] rename sous TD1
---
TD1/.DS_Store | Bin 0 -> 6148 bytes
TD1/Rapport.md | 84 +++++++++++++++++++
{config => TD1/config}/cert_exp_33.c | 0
{config => TD1/config}/cert_exp_33_realloc.c | 0
{config => TD1/config}/cwe20.c | 0
{config => TD1/config}/example1.c | 0
{config => TD1/config}/libstring.c | 0
{config => TD1/config}/libstring.h | 0
{config => TD1/config}/miniz.c | 0
{config => TD1/config}/miniz.h | 0
frama-c-gui.png => TD1/frama-c-gui.png | Bin
studia.png => TD1/studia.png | Bin
tp.md => TD1/tp.md | 0
13 files changed, 84 insertions(+)
create mode 100644 TD1/.DS_Store
create mode 100644 TD1/Rapport.md
rename {config => TD1/config}/cert_exp_33.c (100%)
rename {config => TD1/config}/cert_exp_33_realloc.c (100%)
rename {config => TD1/config}/cwe20.c (100%)
rename {config => TD1/config}/example1.c (100%)
rename {config => TD1/config}/libstring.c (100%)
rename {config => TD1/config}/libstring.h (100%)
rename {config => TD1/config}/miniz.c (100%)
rename {config => TD1/config}/miniz.h (100%)
rename frama-c-gui.png => TD1/frama-c-gui.png (100%)
rename studia.png => TD1/studia.png (100%)
rename tp.md => TD1/tp.md (100%)
diff --git a/TD1/.DS_Store b/TD1/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..d01b1532d58335ad9f4ee22eda1f8f91b7e85519
GIT binary patch
literal 6148
zcmZQzU|@7AO)+F(5MW?n;9!8zj35RBCIAV8Fop~hR0Kpbg3ZWeNKYy+E=bDBPlCz~
zb_(QnHil$|e1<%RGzL`n??@`h$t*50Fu2CZ#LU9V#?H>k&dnYhoRME1T#{H)TI`fq
z6b<5q<mcxk!PtpOVVSAr@d6^w`FSOYnR%&2ASJ<>DXB?`MKR%-c`5njPWh#IDaByD
zPzg>>4$gQ1iRx-2GgBP}BMZw~9ffL3BLf`;6JxX5T22m8Wqs?Q`0SkAy!<XmpfWN-
zXa-&=4Wqgl7#L9eR2E#6my@5D4vKe}qEUJ@1V%$(Gz3ONV8n(1wEp1W9<d=X>haMK
z7!3hjApj~L6rgQJ2PoYDp+Qm%j0_B*<}-+9ftdm62QYxdKw3dGNGpg2X=PvpvA|}4
zwK6a=K(sP~yCEQbpe_lB25V<vWB_YtU}OMmXMi<&86nyk7$MpjV4W96h;{}>h;{}>
zh<2FsM(NQI7!3hv2rxrv0Z{$#$^g$o5YbU`Gz3ONU_^ufBa2J0ixap~#_nHGT??vD
z6QI(d+8<IKgDPs&MgS9JKv4p!6ja@Vw1Q}GRm{i$smVth0<aJorAI@6{viMW>yAtg
literal 0
HcmV?d00001
diff --git a/TD1/Rapport.md b/TD1/Rapport.md
new file mode 100644
index 0000000..bc0ba37
--- /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
--
GitLab