[Tests] Added new non-regression tests for \initialized and \offset

predicates

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

+/* run.config
+   COMMENT: Behaviours of the \initialized E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int A = 0;
+int B;
+
+int main(void) {
+  /* All globals are initialized, even if the initializer is not given */
+  int *p = &A;
+  int *q = &B;
+  /*@assert \initialized(&A) ; */
+  /*@assert \initialized(&B) ; */
+  /*@assert \initialized(p) ;  */
+  /*@assert \initialized(q) ;  */
+
+  /* A local variable without an initializer is uninitialized */
+  int a = 0;
+  int b;
+  long c[2] = { 1, 1 };
+  long d[2];
+  p = &a;
+  q = &b;
+
+  /*@assert \initialized(&a) ; */
+  /*@assert ! \initialized(&b) ; */
+  /*@assert \initialized(p) ; */
+  /*@assert ! \initialized(q) ; */
+  /*@assert \initialized(&c) ; */
+  /*@assert ! \initialized(&d) ; */
+
+  /* Local variables also initialized by assignments */
+  b = 0;
+  d[0] = 1;
+  /*@assert \initialized(&b) ; */
+  /*@assert \initialized(q) ;  */
+  /*@assert ! \initialized(&d) ;  */
+  d[1] = 1;
+  /*@assert \initialized(&d) ;  */
+
+  /* Malloc allocates un-initialized memory */
+  p = (int*)malloc(sizeof(int*));
+  /*@assert ! \initialized(p) ; */
+
+  /* Calloc allocates initialized memory */
+  q = (int*)calloc(1, sizeof(int));
+  /*@ 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) ; */
+  q++;
+  /*@assert ! \initialized(q) ; */
+  q--;
+
+  /* Initialized on un-allocated regions is always false. This does not lead
+   * to undefined bevaviours in production mode or assertion failures in debug
+   * mode. */
+  free(p);
+  free(q);
+  /*@assert ! \initialized(p) ; */
+  /*@assert ! \initialized(q) ; */
+}

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

+/* run.config
+   COMMENT: Behaviours of the \offset E-ACSL predicate
+*/
+
+#include <stdlib.h>
+
+int main() {
+  /* Stack offsets */
+  char c;
+  /*@assert \offset(&c) == 0; */
+
+  short slist[3];
+  short *ps = slist;
+  /*@assert \offset(ps) == 0; */
+  /*@assert \offset(ps + 1) == 2; */
+  /*@assert \offset(ps + 2) == 4; */
+
+  int ilist [3];
+  int *pi = ilist;
+  /*@assert \offset(pi) == 0; */
+  /*@assert \offset(pi + 1) == 4; */
+  /*@assert \offset(pi + 2) == 8; */
+
+  /* Heap offsets */
+  long *p = (long*)malloc(sizeof(long)*12);
+  /*@assert \offset(p) == 0; */
+  /*@assert \offset(p+1) == 8; */
+  /*@assert \offset(p+2) == 16; */
+  return 0;
+}

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

+/* Generated by Frama-C */
+int A = 0;
+int B;
+void __e_acsl_globals_init(void)
+{
+  __store_block((void *)(& B),4UL);
+  __full_init((void *)(& B));
+  __store_block((void *)(& A),4UL);
+  __full_init((void *)(& A));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int *p;
+  int *q;
+  int a;
+  int b;
+  long c[2];
+  long d[2];
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __e_acsl_globals_init();
+  __store_block((void *)(d),16UL);
+  __store_block((void *)(c),16UL);
+  __store_block((void *)(& b),4UL);
+  __store_block((void *)(& a),4UL);
+  __store_block((void *)(& q),8UL);
+  __store_block((void *)(& p),8UL);
+  __full_init((void *)(& p));
+  p = & A;
+  __full_init((void *)(& q));
+  q = & B;
+  /*@ assert \initialized(&A); */
+  __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(&A)",14);
+  /*@ assert \initialized(&B); */
+  __e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(&B)",15);
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)p,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+                    (char *)"\\initialized(p)",16);
+  }
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized_2;
+    __e_acsl_initialized_2 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(q)",17);
+  }
+  __full_init((void *)(& a));
+  a = 0;
+  __initialize((void *)(c),sizeof(long));
+  c[0] = (long)1;
+  __initialize((void *)(& c[1]),sizeof(long));
+  c[1] = (long)1;
+  __full_init((void *)(& p));
+  p = & a;
+  __full_init((void *)(& q));
+  q = & b;
+  /*@ assert \initialized(&a); */
+  {
+    int __e_acsl_initialized_3;
+    __e_acsl_initialized_3 = __initialized((void *)(& a),sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(&a)",27);
+  }
+  /*@ assert ¬\initialized(&b); */
+  {
+    int __e_acsl_initialized_4;
+    __e_acsl_initialized_4 = __initialized((void *)(& b),sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_4,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(&b)",28);
+  }
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized_5;
+    __e_acsl_initialized_5 = __initialized((void *)p,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_5,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(p)",29);
+  }
+  /*@ assert ¬\initialized(q); */
+  {
+    int __e_acsl_initialized_6;
+    __e_acsl_initialized_6 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_6,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(q)",30);
+  }
+  /*@ assert \initialized(&c); */
+  {
+    int __e_acsl_initialized_7;
+    __e_acsl_initialized_7 = __initialized((void *)(& c),sizeof(long [2]));
+    __e_acsl_assert(__e_acsl_initialized_7,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(&c)",31);
+  }
+  /*@ assert ¬\initialized(&d); */
+  {
+    int __e_acsl_initialized_8;
+    __e_acsl_initialized_8 = __initialized((void *)(& d),sizeof(long [2]));
+    __e_acsl_assert(! __e_acsl_initialized_8,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(&d)",32);
+  }
+  __full_init((void *)(& b));
+  b = 0;
+  __initialize((void *)(d),sizeof(long));
+  d[0] = (long)1;
+  /*@ assert \initialized(&b); */
+  {
+    int __e_acsl_initialized_9;
+    __e_acsl_initialized_9 = __initialized((void *)(& b),sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_9,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(&b)",37);
+  }
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized_10;
+    __e_acsl_initialized_10 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_10,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(q)",38);
+  }
+  /*@ assert ¬\initialized(&d); */
+  {
+    int __e_acsl_initialized_11;
+    __e_acsl_initialized_11 = __initialized((void *)(& d),sizeof(long [2]));
+    __e_acsl_assert(! __e_acsl_initialized_11,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(&d)",39);
+  }
+  __initialize((void *)(& d[1]),sizeof(long));
+  d[1] = (long)1;
+  /*@ assert \initialized(&d); */
+  {
+    int __e_acsl_initialized_12;
+    __e_acsl_initialized_12 = __initialized((void *)(& d),sizeof(long [2]));
+    __e_acsl_assert(__e_acsl_initialized_12,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(&d)",41);
+  }
+  __full_init((void *)(& p));
+  p = (int *)__e_acsl_malloc(sizeof(int *));
+  /*@ assert ¬\initialized(p); */
+  {
+    int __e_acsl_initialized_13;
+    __e_acsl_initialized_13 = __initialized((void *)p,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_13,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(p)",45);
+  }
+  __full_init((void *)(& q));
+  q = (int *)__calloc((unsigned long)1,sizeof(int));
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized_14;
+    __e_acsl_initialized_14 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_14,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(q)",49);
+  }
+  __full_init((void *)(& q));
+  q = (int *)__e_acsl_realloc((void *)q,(unsigned long)2 * sizeof(int));
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized_15;
+    __e_acsl_initialized_15 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(__e_acsl_initialized_15,(char *)"Assertion",
+                    (char *)"main",(char *)"\\initialized(q)",54);
+  }
+  __full_init((void *)(& q));
+  q ++;
+  /*@ assert ¬\initialized(q); */
+  {
+    int __e_acsl_initialized_16;
+    __e_acsl_initialized_16 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_16,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(q)",56);
+  }
+  __full_init((void *)(& q));
+  q --;
+  __e_acsl_free((void *)p);
+  __e_acsl_free((void *)q);
+  /*@ assert ¬\initialized(p); */
+  {
+    int __e_acsl_initialized_17;
+    __e_acsl_initialized_17 = __initialized((void *)p,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_17,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(p)",64);
+  }
+  /*@ assert ¬\initialized(q); */
+  {
+    int __e_acsl_initialized_18;
+    __e_acsl_initialized_18 = __initialized((void *)q,sizeof(int));
+    __e_acsl_assert(! __e_acsl_initialized_18,(char *)"Assertion",
+                    (char *)"main",(char *)"!\\initialized(q)",65);
+  }
+  __retres = 0;
+  __delete_block((void *)(& B));
+  __delete_block((void *)(& A));
+  __delete_block((void *)(d));
+  __delete_block((void *)(c));
+  __delete_block((void *)(& b));
+  __delete_block((void *)(& a));
+  __delete_block((void *)(& q));
+  __delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

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

+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  char c;
+  short slist[3];
+  short *ps;
+  int ilist[3];
+  int *pi;
+  long *p;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __store_block((void *)(& p),8UL);
+  __store_block((void *)(& pi),8UL);
+  __store_block((void *)(ilist),12UL);
+  __store_block((void *)(& ps),8UL);
+  __store_block((void *)(slist),6UL);
+  __store_block((void *)(& c),1UL);
+  /*@ assert \offset(&c) ≡ 0; */
+  {
+    int __e_acsl_offset;
+    __e_acsl_offset = __offset((void *)(& c));
+    __e_acsl_assert((unsigned long)__e_acsl_offset == (unsigned long)0,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(&c) == 0",10);
+  }
+  __full_init((void *)(& ps));
+  ps = slist;
+  /*@ assert \offset(ps) ≡ 0; */
+  {
+    int __e_acsl_offset_2;
+    __e_acsl_offset_2 = __offset((void *)ps);
+    __e_acsl_assert((unsigned long)__e_acsl_offset_2 == (unsigned long)0,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(ps) == 0",14);
+  }
+  /*@ assert \offset(ps+1) ≡ 2; */
+  {
+    int __e_acsl_offset_3;
+    __e_acsl_offset_3 = __offset((void *)(ps + 1));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_3 == (unsigned long)2,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(ps+1) == 2",15);
+  }
+  /*@ assert \offset(ps+2) ≡ 4; */
+  {
+    int __e_acsl_offset_4;
+    __e_acsl_offset_4 = __offset((void *)(ps + 2));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_4 == (unsigned long)4,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(ps+2) == 4",16);
+  }
+  __full_init((void *)(& pi));
+  pi = ilist;
+  /*@ assert \offset(pi) ≡ 0; */
+  {
+    int __e_acsl_offset_5;
+    __e_acsl_offset_5 = __offset((void *)pi);
+    __e_acsl_assert((unsigned long)__e_acsl_offset_5 == (unsigned long)0,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(pi) == 0",20);
+  }
+  /*@ assert \offset(pi+1) ≡ 4; */
+  {
+    int __e_acsl_offset_6;
+    __e_acsl_offset_6 = __offset((void *)(pi + 1));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_6 == (unsigned long)4,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(pi+1) == 4",21);
+  }
+  /*@ assert \offset(pi+2) ≡ 8; */
+  {
+    int __e_acsl_offset_7;
+    __e_acsl_offset_7 = __offset((void *)(pi + 2));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_7 == (unsigned long)8,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(pi+2) == 8",22);
+  }
+  __full_init((void *)(& p));
+  p = (long *)__e_acsl_malloc(sizeof(long) * (unsigned long)12);
+  /*@ assert \offset(p) ≡ 0; */
+  {
+    int __e_acsl_offset_8;
+    __e_acsl_offset_8 = __offset((void *)p);
+    __e_acsl_assert((unsigned long)__e_acsl_offset_8 == (unsigned long)0,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(p) == 0",26);
+  }
+  /*@ assert \offset(p+1) ≡ 8; */
+  {
+    int __e_acsl_offset_9;
+    __e_acsl_offset_9 = __offset((void *)(p + 1));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_9 == (unsigned long)8,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(p+1) == 8",27);
+  }
+  /*@ assert \offset(p+2) ≡ 16; */
+  {
+    int __e_acsl_offset_10;
+    __e_acsl_offset_10 = __offset((void *)(p + 2));
+    __e_acsl_assert((unsigned long)__e_acsl_offset_10 == (unsigned long)16,
+                    (char *)"Assertion",(char *)"main",
+                    (char *)"\\offset(p+2) == 16",28);
+  }
+  __retres = 0;
+  __delete_block((void *)(& p));
+  __delete_block((void *)(& pi));
+  __delete_block((void *)(ilist));
+  __delete_block((void *)(& ps));
+  __delete_block((void *)(slist));
+  __delete_block((void *)(& c));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

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

+[e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `realloc':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:200:[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/initialized.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+tests/e-acsl-runtime/initialized.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+tests/e-acsl-runtime/initialized.c:10:[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.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:215:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:208:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:222:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/initialized.c:45:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:49:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:201:[value] warning: function __e_acsl_realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:216:[value] warning: function __e_acsl_realloc, behavior dealloc: precondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:211:[value] warning: function __e_acsl_realloc, behavior alloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:218:[value] warning: function __e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:219:[value] warning: function __e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:226:[value] warning: function __e_acsl_realloc, behavior fail: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/initialized.c:54:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/initialized.c:56:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
+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.

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

+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+tests/e-acsl-runtime/offset.c:7:[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.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/offset.c:26:[value] warning: assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/offset.c:27:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/offset.c:28:[value] warning: assertion got status unknown.