[tests] Improved tests for \initialized predicate to include test cases

that explore behaviours of initialized using un-allocated memory blocks

src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c

@@ -34,26 +34,26 @@ int main(void) {
   /* Local variables also initialized by assignments */
   b = 0;
   d[0] = 1;
-  /*@assert \initialized(&b) ; */
-  /*@assert \initialized(q) ;  */
-  /*@assert ! \initialized(&d) ;  */
+  /*@assert \initialized(&b); */
+  /*@assert \initialized(q);  */
+  /*@assert ! \initialized(&d);  */
   d[1] = 1;
-  /*@assert \initialized(&d) ;  */
+  /*@assert \initialized(&d);  */
 
   /* Malloc allocates un-initialized memory */
   p = (int*)malloc(sizeof(int*));
-  /*@assert ! \initialized(p) ; */
+  /*@assert ! \initialized(p); */
 
   /* Calloc allocates initialized memory */
   q = (int*)calloc(1, sizeof(int));
-  /*@ assert \initialized(q) ; */
+  /*@ assert \initialized(q); */
 
   /* Block reallocared using `realloc' carries initialization of the of the
    * existing fragment but does not initialize the newly allocated one */
   q = (int*)realloc(q, 2*sizeof(int));
-  /*@assert \initialized(q) ; */
+  /*@assert \initialized(q); */
   q++;
-  /*@assert ! \initialized(q) ; */
+  /*@assert ! \initialized(q); */
   q--;
 
   /* Initialized on un-allocated regions is always false. This does not lead
@@ -61,6 +61,17 @@ int main(void) {
    * mode. */
   free(p);
   free(q);
-  /*@assert ! \initialized(p) ; */
-  /*@assert ! \initialized(q) ; */
-}
+  /*@assert ! \initialized(p); */
+  /*@assert ! \initialized(q); */
+
+  /* Spoofing access to  non-existing stack address */
+  q = (int*)(&q - 1024*5);
+  /*assert ! \initialized(q); */
+
+  /* Spoofing access to  non-existing global address */
+  q = (int*)128;
+  /*@assert ! \initialized(q); */
+
+  p = NULL;
+  /*@assert ! \initialized(p); */
+}
\ No newline at end of file

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c

@@ -191,6 +191,26 @@ int main(void)
     __e_acsl_assert(! __e_acsl_initialized_18,(char *)"Assertion",
                     (char *)"main",(char *)"!\\initialized(q)",65);
   }
+  __full_init((void *)(& q));
+  q = (int *)(& q - 1024 * 5);
+  __full_init((void *)(& q));
+  q = (int *)128;
+  /*@ assert ¬\initialized(q); */
+  {
+    int __e_acsl_initialized_19;
+    __e_acsl_initialized_19 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_19,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(q)",73);
+  }
+  __full_init((void *)(& p));
+  p = (int *)0;
+  /*@ assert ¬\initialized(p); */
+  {
+    int __e_acsl_initialized_20;
+    __e_acsl_initialized_20 = __initialized((void *)p,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_20,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(p)",76);
+  }
   __retres = 0;
   __delete_block((void *)(& B));
   __delete_block((void *)(& A));

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle

@@ -58,3 +58,5 @@ FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \poi
 FRAMAC_SHARE/libc/stdlib.h:177:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
 tests/e-acsl-runtime/initialized.c:64:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/initialized.c:65:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:73:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:76:[value] warning: assertion got status unknown.