diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index f79b919df168f6740f8721c301a4e7a73a86d7b3..dd90b193a0e3bf612ae301a6b99ddac97a631073 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -371,7 +371,7 @@ struct _block * __get_cont (void * ptr) {
}
/* tmp->addr <= ptr, tmp may contain ptr
ptr is contained if tmp is large enough (begin addr + size) */
- else if((size_t)ptr < tmp->leaf->size + tmp->addr)
+ else if((size_t)ptr <= tmp->leaf->size + tmp->addr)
return tmp->leaf;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
else if (ind == -1)
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
index 39f1e48cfe3c7fb7b64ec0bb6029edc36be5343b..062c11623d9cc656434d50f810b2302adff0c98b 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
@@ -99,11 +99,12 @@ struct _block* __get_exact(void* ptr) {
struct _block* __get_cont(void* ptr) {
struct _node * tmp = __list;
for(; tmp != NULL; tmp = tmp->next) {
- if(tmp->value->ptr <= (size_t)ptr
- && (size_t)ptr < tmp->value->ptr + tmp->value->size)
- return tmp->value;
- else if(tmp->value->ptr > (size_t)ptr)
+ if(tmp->value->ptr > (size_t)ptr)
break;
+ if(tmp->value->size == 0 && (size_t)ptr == tmp->value->ptr)
+ return tmp->value;
+ if((size_t)ptr < tmp->value->ptr + tmp->value->size)
+ return tmp->value;
}
return NULL;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index 9ad56794b9ff0043d9f8b3ea3a935417532fbf72..8db9c737e840388279e08131c6a3c854d8dc2ff9 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -332,7 +332,7 @@ int __valid(void* ptr, size_t size) {
struct _block * tmp;
if(ptr == NULL)
return false;
- assert(size > 0);
+ //assert(size > 0);
tmp = __get_cont(ptr);
return (tmp == NULL) ?
false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
@@ -344,7 +344,7 @@ int __valid_read(void* ptr, size_t size) {
struct _block * tmp;
if(ptr == NULL)
return false;
- assert(size > 0);
+ //assert(size > 0);
tmp = __get_cont(ptr);
return (tmp == NULL) ?
false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
index c55c28bf603657b172b6eaac0acc1bbdcefb05a8..7a6b990915436f842b0d6e6ebd2ca4226bdab8e7 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
@@ -156,6 +156,8 @@ struct _block* __get_exact(void* ptr) {
struct _block* _get_cont_rec(struct _node * node, void* ptr) {
if(node == NULL) return NULL;
else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr);
+ else if(node->value->size == 0 && node->value->ptr == (size_t)ptr)
+ return node->value;
else if(node->value->ptr+node->value->size > (size_t)ptr) return node->value;
else return _get_cont_rec(node->right, ptr);
}
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
index 1a98fd6e2e01379664c3b1b0212e6aa645bfd5f2..253a8bc3ef11e4c7baae3fdee214c5c3b5079e86 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
@@ -111,6 +111,8 @@ struct _block* __get_exact(void* ptr) {
struct _block* _get_cont_rec(struct _node * node, void* ptr) {
if(node == NULL) return NULL;
else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr);
+ else if(node->value->size == 0 && node->value->ptr == (size_t)ptr)
+ return node->value;
else if(node->value->ptr+node->value->size > (size_t)ptr) return node->value;
else return _get_cont_rec(node->right, ptr);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
new file mode 100644
index 0000000000000000000000000000000000000000..bcf7a9e9f42fdc2681324d8f9b3676feceb4c4d9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
@@ -0,0 +1,15 @@
+/* run.config
+ COMMENT: pointer to an empty struct
+ EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
+*/
+
+struct toto {};
+
+int main() {
+ struct toto s;
+ //@ assert \valid(&s);
+ struct toto *p;
+ p = &s;
+ //@ assert \valid(p);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74bbf857adb7b54faca5fa445c26eaf4a1ec3fbe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
@@ -0,0 +1,30 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __full_init
+tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74bbf857adb7b54faca5fa445c26eaf4a1ec3fbe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
@@ -0,0 +1,30 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __full_init
+tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+[value] using specification for function __initialized
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
new file mode 100644
index 0000000000000000000000000000000000000000..678a82b6e694e6fcd652dcc99f1c04476ef6021b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -0,0 +1,115 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+struct toto {
+
+};
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int main(void)
+{
+ int __retres;
+ struct toto s;
+ struct toto *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& s),0U);
+ /*@ assert \valid(&s); */
+ {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)(& s),sizeof(struct toto));
+ e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&s)",10);
+ }
+ __full_init((void *)(& p));
+ p = & s;
+ /*@ assert \valid(p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(struct toto *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_2;
+ __e_acsl_valid_2 = __valid((void *)p,sizeof(struct toto));
+ __e_acsl_and = __e_acsl_valid_2;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& s));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+