partie realloc

config/cert_exp_33.c

@@ -16,9 +16,6 @@ void set_flag(int number, int *sign_flag)
   {
     *sign_flag = -1;
   }
-  else{
-    *sign_flag = 0;
-  }
   Frama_C_show_each_set_flag(number, *sign_flag);
 }
 

config/cert_exp_33_realloc.c

 #include <stdlib.h>
 #include <stdio.h>
+#include <string.h>
+ 
 enum { OLD_SIZE = 10, NEW_SIZE = 20 };
-
-int *resize_array(int *array, size_t count) {
-  if (0 == count) {
+  
+int *resize_array(int *array, size_t old_count, size_t new_count) {
+  if (0 == new_count) {
     return 0;
   }
-
-  int *ret = (int *)realloc(array, count * sizeof(int));
+  
+  int *ret = (int *)realloc(array, new_count * sizeof(int)); //@ split ret==0; 
   if (!ret) {
     free(array);
     return 0;
   }
-
+  
+  if (new_count > old_count) {
+    memset(ret + old_count, 0, (new_count - old_count) * sizeof(int));
+  }
+  
   return ret;
 }
-
+  
 void func(void) {
-
+  
   int *array = (int *)malloc(OLD_SIZE * sizeof(int));
   if (0 == array) {
     /* Handle error */
     return;
   }
-
+  
   for (size_t i = 0; i < OLD_SIZE; ++i) {
     array[i] = i;
   }
-
-  array = resize_array(array, NEW_SIZE);
+  
+  array = resize_array(array, OLD_SIZE, NEW_SIZE);
   if (0 == array) {
     /* Handle error */
     return;
   }
-
+  
   for (size_t i = 0; i < NEW_SIZE; ++i) {
     printf("%d ", array[i]);
   }
-}
+}
\ No newline at end of file

rapport.docx

+J'ai eu quelques soucis liés à l'absence du include en début de code
+
+sign peut être non-initialisé si number = 0
+avec partition history, eva sépare les cas de number en positif, nul et négatif
+red alarm quand partiion-history > 2
+avec interprocedural history, la console spammme, attention à bien avoir le include time
+
+correction de set_flag : remplacer > par >=
+
+**Realloc**
+Point d'entrée choisi : func
+Red Alarm quand -eva-slevel = 10
+
+
+Problème : le code corrigé fait apparaitre de nouvelles erreurs et mêmes de nouvelles alarmes rouges
+Corrigé en ajoutant les return dans la version corrigée du code
+