diff --git a/config/cert_exp_33_realloc.c b/config/cert_exp_33_realloc.c index 30cbd3e28a454416cdb24c1baf5210d603e59c87..4933f33d3dd936ac882ed51e558d06b3e84e4f63 100644 --- a/config/cert_exp_33_realloc.c +++ b/config/cert_exp_33_realloc.c @@ -1,5 +1,7 @@ #include <stdlib.h> #include <stdio.h> + + enum { OLD_SIZE = 10, NEW_SIZE = 20 }; int *resize_array(int *array, size_t count) { @@ -7,7 +9,7 @@ int *resize_array(int *array, size_t count) { return 0; } - int *ret = (int *)realloc(array, count * sizeof(int)); + int *ret = (int *)realloc(array, count * sizeof(int)); //@ split ret==0; if (!ret) { free(array); return 0; @@ -26,6 +28,7 @@ void func(void) { for (size_t i = 0; i < OLD_SIZE; ++i) { array[i] = i; + Frama_C_show_each_init_array(array[i]); } array = resize_array(array, NEW_SIZE);