Merge branch 'master' of git.frama-c.com:frama-c/e-acsl

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)

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;
 }

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

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);
 }

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);
 }

src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i

+/* 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;
+}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle

+[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 ======

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

+[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 ======

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

+/* 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;
+}
+
+