diff --git a/config/cert_exp_33.c b/config/cert_exp_33.c
index c4fe87dcaaa750ddb5fe19c8053b12b3a334c10f..69882ef2e5321cb7737cd9743fc7d7fa4795353b 100644
--- a/config/cert_exp_33.c
+++ b/config/cert_exp_33.c
@@ -1,3 +1,5 @@
+#include <stddef.h>
+
void set_flag(int number, int *sign_flag) {
if (NULL == sign_flag) {
return;
@@ -8,10 +10,12 @@ void set_flag(int number, int *sign_flag) {
} else if (number < 0) {
*sign_flag = -1;
}
+ Frama_C_show_each_set_flag(number, *sign_flag);
}
int is_negative(int number) {
int sign;
set_flag(number, &sign);
+ Frama_C_show_each_is_negative(number, sign);
return sign < 0;
}
diff --git a/config/cert_exp_33_realloc.c b/config/cert_exp_33_realloc.c
index 30cbd3e28a454416cdb24c1baf5210d603e59c87..49534c04bd93dca74198a4336a3d22602eb96dc3 100644
--- a/config/cert_exp_33_realloc.c
+++ b/config/cert_exp_33_realloc.c
@@ -8,6 +8,7 @@ int *resize_array(int *array, size_t count) {
}
int *ret = (int *)realloc(array, count * sizeof(int));
+ //@ split ret==0;
if (!ret) {
free(array);
return 0;
diff --git a/config/cwe20.c b/config/cwe20.c
index 9a723653eb1eb7474248a502ab6c75b6e3b0d4e4..1960e1d34548f9d69a1ec528dc8871bbe8f09fd9 100644
--- a/config/cwe20.c
+++ b/config/cwe20.c
@@ -24,10 +24,16 @@ int main () {
if ( EOF == error ){
die("No integer passed: Die evil hacker!\n");
}
+ if (m <= 0 || n <= 0) {
+ die("Dimensions must be positive: Die evil hacker!\n");
+ }
if ( m > MAX_DIM || n > MAX_DIM ) {
die("Value too large: Die evil hacker!\n");
}
board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+ if (board == NULL) {
+ return 2;
+ }
for (int i = 0; i < m; i++) {
for (int j = 0; j < n; j++) {
board[n*i+j] = 0;
diff --git a/config/libstring.c b/config/libstring.c
index c8a87c267e122d100bf1d92c06567448fa796fe0..d074eaa3d3dc1d2da19a1acae0c678499c115ea6 100644
--- a/config/libstring.c
+++ b/config/libstring.c
@@ -9,6 +9,7 @@
#define unlikely(x) __builtin_expect(!!(x), 0)
#include "libstring.h"
+#include "__fc_builtin.h"
#define BUF_LEN 65536
#define CAP_DEFAULT 10
@@ -437,3 +438,39 @@ string_t *string_vector_reduce(reducefunc_t func,
const char *libstring_version() {
return LIBSTRING_VERSION;
}
+
+
+int main(void) {
+ char cstr1[256];
+ char cstr2[256];
+
+ for (int i = 0; i < 255; i++) {
+ cstr1[i] = (char) Frama_C_interval(1, 127);
+ cstr2[i] = (char) Frama_C_interval(1, 127);
+ }
+ cstr1[255] = '\0';
+ cstr2[255] = '\0';
+
+ string_t *s1 = string_new(cstr1);
+ string_t *s2 = string_new(cstr2);
+ if (s1 == NULL || s2 == NULL) {
+ printf("Allocation error in string_new\n");
+ return 1;
+ }
+
+ string_t *s_concat = string_concat(s1, s2);
+ if (s_concat == NULL) {
+ printf("Concatenation error\n");
+ free(s1);
+ free(s2);
+ return 1;
+ }
+
+ string_println(s_concat);
+
+ free(s1);
+ free(s2);
+ free(s_concat);
+
+ return 0;
+}
\ No newline at end of file
diff --git a/rapport.md b/rapport.md
new file mode 100644
index 0000000000000000000000000000000000000000..0aab125bba47ba629b9818f36fd13a9fc9cc8b74
--- /dev/null
+++ b/rapport.md
@@ -0,0 +1,281 @@
+# Rapport
+
+## CERT C EXP33-C. Do not read uninitialized memory
+
+### Première exécution de Frama-C
+
+Lorsque je lance la commande `frama-c -eva -main is_negative cert_exp_33.c`, j'obtiens la réponse suivante :
+
+```
+[kernel] Parsing cert_exp_33.c (with preprocessing)
+[eva] Analyzing a complete application starting at is_negative
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] cert_exp_33.c:18: Warning:
+ accessing uninitialized left-value. assert \initialized(&sign);
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function set_flag:
+ sign ∈ {-1; 1} or UNINITIALIZED
+[eva:final-states] Values at end of function is_negative:
+ sign ∈ {-1; 1}
+ __retres ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 9 statements reached (out of 11): 81% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+```
+
+L'analyseur identifie que la variable `sign` est potentiellement non-initialisée (`sign ∈ {-1; 1} or UNINITIALIZED`), ce qui génère une alarme (`1 alarm generated by the analysis: 1 access to uninitialized left-values`)
+
+Après avoir ajouté les lignes de la forme `Frama_C_show_each_*`, j'obtiens la réponse suivante :
+
+```
+[kernel] Parsing cert_exp_33.c (with preprocessing)
+[eva] Analyzing a complete application starting at is_negative
+[eva:initial-state] Values of globals at initialization
+
+[eva] cert_exp_33.c:13:
+ Frama_C_show_each_set_flag: [-2147483648..2147483647], {-1; 1}
+[eva] cert_exp_33.c:19:
+ Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+[eva:alarm] cert_exp_33.c:20: Warning:
+ accessing uninitialized left-value. assert \initialized(&sign);
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function set_flag:
+ sign ∈ {-1; 1} or UNINITIALIZED
+[eva:final-states] Values at end of function is_negative:
+ sign ∈ {-1; 1}
+ __retres ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 11 statements reached (out of 13): 84% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+```
+
+### Partitionner les traces
+
+J'ajoute l'option -eva-partition-traces.
+
+Pour n = 1, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..0], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19:
+ Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+```
+
+Pour n = 2, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: {0}, ⊥
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19:
+ Frama_C_show_each_is_negative: [-2147483648..2147483647], {-1; 1}
+```
+
+Pour n = 3, j'obtiens le même résultat que pour n = 2.
+
+### Partitionnement inter-procédural
+
+Quand j'ajoute l'option `-eva-interprocedural-history`, j'obtiens les résultats suivants :
+
+```
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: {0}, ⊥
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:13: Frama_C_show_each_set_flag: [1..2147483647], {1}
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: {0}, ⊥
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: [-2147483648..-1], {-1}
+[eva] cert_exp_33.c:19: Frama_C_show_each_is_negative: [1..2147483647], {1}
+[eva:alarm] cert_exp_33.c:20: Warning:
+ accessing uninitialized left-value. assert \initialized(&sign);
+```
+
+On voit apparaître une alarme qui n'était pas présente dans les résultats précédents. Cette alarme apparaît également dans l'interface graphique.
+
+## CERT C EXP33-C bis
+
+### Première analyse
+
+Je choisis de lancer la commande suivante :
+
+```
+frama-c -eva -eva-partition-history 3 -eva-interprocedural-history -main func cert_exp_33_realloc.c
+```
+
+Voici les résultats obtenus :
+
+```
+
+[kernel] Parsing cert_exp_33_realloc.c (with preprocessing)
+[eva] Analyzing a complete application starting at func
+[eva:initial-state] Values of globals at initialization
+
+[eva] cert_exp_33_realloc.c:21: allocating variable **malloc_func_l21
+[eva] cert_exp_33_realloc.c:27: starting to merge loop iterations
+[eva] cert_exp_33_realloc.c:10: allocating variable **realloc_resize_array_l10
+[eva:alarm] cert_exp_33_realloc.c:12: Warning:
+accessing left-value that contains escaping addresses.
+assert ¬\dangling(&array);
+[eva] using specification for function printf_va_1
+[eva:alarm] cert_exp_33_realloc.c:38: Warning:
+accessing uninitialized left-value. assert \initialized(array + i_0);
+[eva] cert_exp_33_realloc.c:37: starting to merge loop iterations
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function resize_array:
+array ∈ {{ &__malloc_func_l21[0] }} or ESCAPINGADDR
+ret ∈ {{ NULL ; &__realloc_resize_array_l10[0] }}
+array ∈ {{ &__malloc_func_l21[0] }} or ESCAPINGADDR
+**retres ∈ {{ NULL ; &**realloc_resize_array_l10[0] }}
+[eva:final-states] Values at end of function func:
+**fc_heap_status ∈ [--..--]
+array ∈ {{ NULL ; &**realloc_resize_array_l10[0] }}
+S**\_fc_stdout[0..1] ∈ [--..--]
+**malloc_func_l21[0] ∈ {0} or UNINITIALIZED
+[1] ∈ {1} or UNINITIALIZED
+[2] ∈ {2} or UNINITIALIZED
+[3..9] ∈ {3; 4; 5; 6; 7; 8; 9} or UNINITIALIZED
+[eva:summary] ====== ANALYSIS SUMMARY ======
+
+---
+
+2 functions analyzed (out of 2): 100% coverage.
+In these functions, 34 statements reached (out of 37): 91% coverage.
+
+---
+
+No errors or warnings raised during the analysis.
+
+---
+
+2 alarms generated by the analysis:
+1 access to uninitialized left-values
+1 escaping address
+
+---
+
+Evaluation of the logical properties reached by the analysis:
+Assertions 0 valid 0 unknown 0 invalid 0 total
+Preconditions 3 valid 0 unknown 0 invalid 3 total
+100% of the logical properties reached have been proven.
+
+---
+
+```
+
+On remarque que deux alarmes ont été générées par l'analyse : une alarme pour un accès à une valeur non-initialisée et une alarme pour un accès à une adresse qui s'échappe.
+
+Je choisis d'exécuter la commande suivante :
+
+```
+frama-c-gui -eva -eva-min-loop-unroll 10 -main func cert_exp_33_realloc.c
+```
+
+Je vois bien apparaître une nouvelle alarme rouge dans l'interface graphique.
+
+### Analyse précise de `realloc`
+
+J'ajoute la ligne `//@ split ret==0;` dans le code : l'alarme disparaît, comme attendu.
+
+## CWE 20
+
+### Première analyse
+
+Les alarmes portent sur deux types de problèmes :
+
+- Débordements entiers sur les expressions m*n et (m-1)*n qui pourraient dépasser la plage des entiers si les valeurs de m et n ne sont pas correctement bornées.
+- Accès mémoire invalides, dont un accès à une case non initialisée lors de la lecture de board[(m-1)*n].
+
+En pratique, si on impose que 0 < m, n ≤ MAX_DIM, ces alarmes sont de faux positifs et le programme se comporte correctement.
+
+### Patch 1
+
+J'ajoute le code suivant :
+
+```
+ if (m <= 0 || n <= 0) {
+ die("Dimensions must be positive: Die evil hacker!\n");
+ }
+```
+
+Les cinq erreurs liées aux débordements entiers disparaissent.
+
+### Patch 2
+
+J'ajoute le code suivant :
+
+```
+if (board == NULL) {
+ return 2;
+ }
+
+```
+
+Mais je ne parviens pas à éliminer les erreurs restantes.
+
+## libstring
+
+### concat
+
+J'ajoute la fonction main suivante à la fin de `libstring.c` :
+
+```
+int main(void) {
+ char cstr1[256];
+ char cstr2[256];
+
+ for (int i = 0; i < 255; i++) {
+ cstr1[i] = (char) Frama_C_interval(1, 127);
+ cstr2[i] = (char) Frama_C_interval(1, 127);
+ }
+ cstr1[255] = '\0';
+ cstr2[255] = '\0';
+
+ string_t *s1 = string_new(cstr1);
+ string_t *s2 = string_new(cstr2);
+ if (s1 == NULL || s2 == NULL) {
+ printf("Allocation error in string_new\n");
+ return 1;
+ }
+
+ string_t *s_concat = string_concat(s1, s2);
+ if (s_concat == NULL) {
+ printf("Concatenation error\n");
+ free(s1);
+ free(s2);
+ return 1;
+ }
+
+ string_println(s_concat);
+
+ free(s1);
+ free(s2);
+ free(s_concat);
+
+ return 0;
+}
+```
+
+J'obtiens pourtant les erreurs suivantes :
+
+```
+3 alarms generated by the analysis:
+ 3 accesses to uninitialized left-values
+```