diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
index e4d9ad5a610240c9847a396520430409cbbdc4f1..3eeb429e6f0fd2e83b2b4287d0f570bcd2630408 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/freeable.c
+++ b/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])); */
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
index abe9c3312b1e7e0ddcf423b9bc5fcdf52edcd843..43d2f9e6c3572c8981173ec8aa4ac396950dac61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
@@ -1,11 +1,11 @@
[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);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
index 533330efbb6a685ed53daaf312216e1bc5e7ccd7..e648aba7240f9e4e6947fc90e9ea2c08a09011c0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -1,9 +1,18 @@
/* Generated by Frama-C */
+char array[1024];
+void __e_acsl_globals_init(void)
+{
+ __store_block((void *)(array),1024UL);
+ __full_init((void *)(& array));
+ return;
+}
+
int main(void)
{
int __retres;
int *p;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
__store_block((void *)(& p),8UL);
/*@ assert ¬\freeable(p); */
{
@@ -11,14 +20,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));
@@ -27,14 +36,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); */
@@ -42,9 +51,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;