[tests] improve the testcase for \freeable to take into account BTS entry #1830

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

@@ -3,11 +3,13 @@
    STDOPT: +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
 */
 
-#include "stdlib.h"
+#include <stdlib.h>
 
 extern void *malloc(size_t p);
 extern void free(void* p);
 
+char array[1024];
+
 int main(void) {
   int *p;
   /*@ assert ! \freeable(p); */
@@ -17,4 +19,8 @@ int main(void) {
   /*@ assert \freeable(p); */
   free(p);
   /*@ assert ! \freeable(p); */
+
+  // test cases for BTS #1830
+  /*@ assert ! \freeable(array); */
+  /*@ assert ! \freeable(&(array[5])); */
 }

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

 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:11:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:11:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:11:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -21,5 +21,5 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-tests/e-acsl-runtime/freeable.c:13:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/freeable.c:13:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
+tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);

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

 /* Generated by Frama-C */
+char array[1024];
+void __e_acsl_memory_init(void)
+{
+  __store_block((void *)(array),1024UL);
+  __full_init((void *)(& array));
+  return;
+}
+
 int main(void)
 {
   int __retres;
   int *p;
+  __e_acsl_memory_init();
   __store_block((void *)(& p),8UL);
   /*@ assert ¬\freeable(p); */
   {
@@ -10,14 +19,14 @@ int main(void)
     /*@ assert Value: initialisation: \initialized(&p); */
     __e_acsl_freeable = __freeable((void *)p);
     e_acsl_assert(! __e_acsl_freeable,(char *)"Assertion",(char *)"main",
-                  (char *)"!\\freeable(p)",13);
+                  (char *)"!\\freeable(p)",15);
   }
   /*@ assert ¬\freeable((void *)0); */
   {
     int __e_acsl_freeable_2;
     __e_acsl_freeable_2 = __freeable((void *)0);
     e_acsl_assert(! __e_acsl_freeable_2,(char *)"Assertion",(char *)"main",
-                  (char *)"!\\freeable((void *)0)",14);
+                  (char *)"!\\freeable((void *)0)",16);
   }
   __full_init((void *)(& p));
   p = (int *)__e_acsl_malloc((unsigned long)4 * sizeof(int));
@@ -26,14 +35,14 @@ int main(void)
     int __e_acsl_freeable_3;
     __e_acsl_freeable_3 = __freeable((void *)(p + 1));
     e_acsl_assert(! __e_acsl_freeable_3,(char *)"Assertion",(char *)"main",
-                  (char *)"!\\freeable(p+1)",16);
+                  (char *)"!\\freeable(p+1)",18);
   }
   /*@ assert \freeable(p); */
   {
     int __e_acsl_freeable_4;
     __e_acsl_freeable_4 = __freeable((void *)p);
     e_acsl_assert(__e_acsl_freeable_4,(char *)"Assertion",(char *)"main",
-                  (char *)"\\freeable(p)",17);
+                  (char *)"\\freeable(p)",19);
   }
   __e_acsl_free((void *)p);
   /*@ assert ¬\freeable(p); */
@@ -41,9 +50,24 @@ int main(void)
     int __e_acsl_freeable_5;
     __e_acsl_freeable_5 = __freeable((void *)p);
     e_acsl_assert(! __e_acsl_freeable_5,(char *)"Assertion",(char *)"main",
-                  (char *)"!\\freeable(p)",19);
+                  (char *)"!\\freeable(p)",21);
+  }
+  /*@ assert ¬\freeable((char *)array); */
+  {
+    int __e_acsl_freeable_6;
+    __e_acsl_freeable_6 = __freeable((void *)(array));
+    e_acsl_assert(! __e_acsl_freeable_6,(char *)"Assertion",(char *)"main",
+                  (char *)"!\\freeable((char *)array)",24);
+  }
+  /*@ assert ¬\freeable(&array[5]); */
+  {
+    int __e_acsl_freeable_7;
+    __e_acsl_freeable_7 = __freeable((void *)(& array[5]));
+    e_acsl_assert(! __e_acsl_freeable_7,(char *)"Assertion",(char *)"main",
+                  (char *)"!\\freeable(&array[5])",25);
   }
   __retres = 0;
+  __delete_block((void *)(array));
   __delete_block((void *)(& p));
   __e_acsl_memory_clean();
   return __retres;