From 83ad6e59b561cb67da7355cb6fe984439c316b32 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 7 Mar 2016 17:31:27 +0100
Subject: [PATCH] [tests] Improved tests  for \initialized predicate to include
 test cases that explore behaviours of initialized using un-allocated memory
 blocks

---
 .../e-acsl/tests/e-acsl-runtime/initialized.c | 33 ++++++++++++-------
 .../e-acsl-runtime/oracle/gen_initialized.c   | 20 +++++++++++
 .../oracle/initialized.res.oracle             |  2 ++
 3 files changed, 44 insertions(+), 11 deletions(-)

diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
index 886159e1d67..143514ebbcd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
+++ b/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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
index dd211269b42..c5cd0f5e667 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
+++ b/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));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
index 843ddc6ecd9..9384d673883 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
+++ b/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.
-- 
GitLab