diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 145f78d752fa39329c42bdfb48d90bccfe9f76ef..c9c6d57ad0c73ec729c54283b2ee229358132cca 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -207,7 +207,7 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
   Annotations.register_funspec new_kf;
   dup_spec_status old_prj kf new_kf spec new_spec;
   Options.feedback ~dkey ~level:2 "function %s" name;
-  GFun(fundec, loc)
+  GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
 
 (* ********************************************************************** *)
 (* Visitor *)
@@ -220,27 +220,25 @@ class dup_functions_visitor prj = object (self)
 
   val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
   val mutable before_memory_model = Before_gmp
-  val mutable libc_decls = []
+  val mutable new_definitions: global list = []
+  (* new definitions of the annotated functions which will contain the
+     translation of the E-ACSL constract *)
 
   method private before_memory_model = match before_memory_model with
   | Before_gmp | Gmp | After_gmp -> true
   | Memory_model | Code -> false
 
   method private insert_libc l =
-    match libc_decls with
+    match new_definitions with
     | [] -> l
     | _ :: _ ->
-      let res = List.fold_left (fun acc g -> g :: acc) l libc_decls in
-      libc_decls <- [];
+      (* add the generated definitions of libc at the end of [l]. This way,
+         we are sure that they have access to all of it (in particular, the
+         memory model and GMP) *)
+      let res = l @ new_definitions in
+      new_definitions <- [];
       res
 
-  method private dup_libc g new_g =
-    if self#before_memory_model then begin
-      libc_decls <- new_g :: libc_decls;
-      [ g ]
-    end else
-      self#insert_libc [ g; new_g ]
-
   method private next () =
     match before_memory_model with
     | Before_gmp -> ()
@@ -328,12 +326,17 @@ if there are memory-related annotations.@]"
 	in
 	let spec = Annotations.funspec ~populate:false kf in
 	let vi_bhv = Cil.get_varinfo self#behavior vi in
-	let new_g = 
-	  Project.on prj
-	    (dup_global loc (Project.current ()) spec self#behavior kf vi_bhv) 
-	    new_vi 
-	in
-	self#dup_libc g new_g
+        let new_g, new_decl =
+          Project.on prj
+            (dup_global loc (Project.current ()) spec self#behavior kf vi_bhv)
+            new_vi
+        in
+        (* postpone the introduction of the new function definition to the
+           end *)
+        new_definitions <- new_g :: new_definitions;
+        (* put the declaration before the original function in order to solve
+           issue with recursive functions *)
+        [ new_decl; g ]
       | _ -> assert false)
   | GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
       when Misc.is_library_loc loc ->
@@ -348,20 +351,20 @@ if there are memory-related annotations.@]"
       when Cil.is_builtin vi ->
     self#next ();
     Cil.JustCopy
-  | _ -> 
+  | _ ->
     self#next ();
-    Cil.DoChildrenPost self#insert_libc
+    Cil.DoChildren
 
   method !vfile _ =
     Cil.DoChildrenPost
       (fun f ->
-	match libc_decls with
-	| [] -> f
-	| _ :: _ -> 
-	  (* required by the few cases where there is no global tagged as
-	     [Code] in the file. *)
-	  f.globals <- self#insert_libc f.globals; 
-	  f)
+        match new_definitions with
+        | [] -> f
+        | _ :: _ ->
+          (* required by the few cases where there is no global tagged as
+             [Code] in the file. *)
+          f.globals <- self#insert_libc f.globals;
+          f)
 
   initializer
     Project.copy ~selection:(Parameter_state.get_selection ()) prj;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index cfcb4eb5edca2d8028b8d71336c50404b0f41d90..7785f52bb951c487c08d98e17514e3260f8c193a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -1,8 +1,8 @@
 tests/bts/bts1307.i:14:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
 tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
 [value] user error: type long double not implemented. Using double instead
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 0e3d475024a06484351ed9101b95eb6d0b3183a1..156fd24a1dd5319903f4652e0972c4cb1a0e33f4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -1,11 +1,16 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/bts/bts1399.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/bts/bts1399.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -13,13 +18,6 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index a17813f8eec7a7244564446b9c5a777584caedbb..de1b634bd4ac537229113252e9ffc1247c74ddc8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -31,63 +31,7 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
       ensures
         *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
  */
-void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
-{
-  float *__gen_e_acsl_at_3;
-  float *__gen_e_acsl_at_2;
-  float *__gen_e_acsl_at;
-  {
-    int __gen_e_acsl_valid;
-    int __gen_e_acsl_valid_2;
-    int __gen_e_acsl_valid_3;
-    __e_acsl_store_block((void *)(& Mtmax_in),8UL);
-    __e_acsl_store_block((void *)(& Mwmax),8UL);
-    __e_acsl_store_block((void *)(& Mtmax_out),8UL);
-    __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
-                    (char *)"\\valid(Mtmax_in)",5);
-    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
-                    (char *)"foo",(char *)"\\valid(Mwmax)",6);
-    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
-                    (char *)"foo",(char *)"\\valid(Mtmax_out)",7);
-    __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
-    __gen_e_acsl_at_3 = Mwmax;
-    __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
-    __gen_e_acsl_at_2 = Mtmax_in;
-    __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
-    __gen_e_acsl_at = Mtmax_out;
-    foo(Mtmax_in,Mwmax,Mtmax_out);
-  }
-  {
-    int __gen_e_acsl_valid_read;
-    int __gen_e_acsl_valid_read_2;
-    int __gen_e_acsl_valid_read_3;
-    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
-                                                  sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"foo",
-                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",11);
-    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
-                                                    sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
-                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",11);
-    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
-                                                    sizeof(float));
-    __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
-                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
-    __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (long double)(
-                                        (long double)5 - ((long double)(
-                                                          5 / 80) * *__gen_e_acsl_at_3) * 0.4),
-                    (char *)"Postcondition",(char *)"foo",
-                    (char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
-                    11);
-    __e_acsl_delete_block((void *)(& Mtmax_in));
-    __e_acsl_delete_block((void *)(& Mwmax));
-    __e_acsl_delete_block((void *)(& Mtmax_out));
-    return;
-  }
-}
+void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);
 
 /*@ requires \valid(Mtmin_in);
     requires \valid(Mwmin);
@@ -113,6 +57,43 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
   return;
 }
 
+/*@ requires \valid(Mtmin_in);
+    requires \valid(Mwmin);
+    requires \valid(Mtmin_out);
+    
+    behavior UnderEstimate_Motoring:
+      assumes \true;
+      ensures
+        *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
+          *\old(Mtmin_in) ≢ 0.:
+          0.85**\old(Mwmin) ≢ 0.;
+ */
+void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);
+
+int main(void)
+{
+  int __retres;
+  float f;
+  float g;
+  float h;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __e_acsl_store_block((void *)(& h),4UL);
+  __e_acsl_store_block((void *)(& g),4UL);
+  __e_acsl_store_block((void *)(& f),4UL);
+  __e_acsl_full_init((void *)(& f));
+  f = (float)1.0;
+  __e_acsl_full_init((void *)(& g));
+  g = (float)1.0;
+  __gen_e_acsl_foo(& f,& g,& h);
+  __gen_e_acsl_bar(& f,& g,& h);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& h));
+  __e_acsl_delete_block((void *)(& g));
+  __e_acsl_delete_block((void *)(& f));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
 /*@ requires \valid(Mtmin_in);
     requires \valid(Mwmin);
     requires \valid(Mtmin_out);
@@ -219,28 +200,71 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
   }
 }
 
-int main(void)
+/*@ requires \valid(Mtmax_in);
+    requires \valid(Mwmax);
+    requires \valid(Mtmax_out);
+    
+    behavior OverEstimate_Motoring:
+      assumes \true;
+      ensures
+        *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
+ */
+void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
 {
-  int __retres;
-  float f;
-  float g;
-  float h;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(& h),4UL);
-  __e_acsl_store_block((void *)(& g),4UL);
-  __e_acsl_store_block((void *)(& f),4UL);
-  __e_acsl_full_init((void *)(& f));
-  f = (float)1.0;
-  __e_acsl_full_init((void *)(& g));
-  g = (float)1.0;
-  __gen_e_acsl_foo(& f,& g,& h);
-  __gen_e_acsl_bar(& f,& g,& h);
-  __retres = 0;
-  __e_acsl_delete_block((void *)(& h));
-  __e_acsl_delete_block((void *)(& g));
-  __e_acsl_delete_block((void *)(& f));
-  __e_acsl_memory_clean();
-  return __retres;
+  float *__gen_e_acsl_at_3;
+  float *__gen_e_acsl_at_2;
+  float *__gen_e_acsl_at;
+  {
+    int __gen_e_acsl_valid;
+    int __gen_e_acsl_valid_2;
+    int __gen_e_acsl_valid_3;
+    __e_acsl_store_block((void *)(& Mtmax_in),8UL);
+    __e_acsl_store_block((void *)(& Mwmax),8UL);
+    __e_acsl_store_block((void *)(& Mtmax_out),8UL);
+    __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
+                    (char *)"\\valid(Mtmax_in)",5);
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
+                    (char *)"foo",(char *)"\\valid(Mwmax)",6);
+    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
+                    (char *)"foo",(char *)"\\valid(Mtmax_out)",7);
+    __e_acsl_store_block((void *)(& __gen_e_acsl_at_3),8UL);
+    __gen_e_acsl_at_3 = Mwmax;
+    __e_acsl_store_block((void *)(& __gen_e_acsl_at_2),8UL);
+    __gen_e_acsl_at_2 = Mtmax_in;
+    __e_acsl_store_block((void *)(& __gen_e_acsl_at),8UL);
+    __gen_e_acsl_at = Mtmax_out;
+    foo(Mtmax_in,Mwmax,Mtmax_out);
+  }
+  {
+    int __gen_e_acsl_valid_read;
+    int __gen_e_acsl_valid_read_2;
+    int __gen_e_acsl_valid_read_3;
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
+                                                  sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"foo",
+                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",11);
+    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+                                                    sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
+                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",11);
+    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+                                                    sizeof(float));
+    __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
+                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
+    __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (long double)(
+                                        (long double)5 - ((long double)(
+                                                          5 / 80) * *__gen_e_acsl_at_3) * 0.4),
+                    (char *)"Postcondition",(char *)"foo",
+                    (char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
+                    11);
+    __e_acsl_delete_block((void *)(& Mtmax_in));
+    __e_acsl_delete_block((void *)(& Mwmax));
+    __e_acsl_delete_block((void *)(& Mtmax_out));
+    return;
+  }
 }
 
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 500ffb75a67fa4fe785a42292ac8775640bf2a32..6af28302ec36306fdee867b47c1b484cbe21a209 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -24,6 +24,43 @@ int sorted(int *t, int n)
   return_label: return __retres;
 }
 
+/*@ behavior yes:
+      assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+      ensures \result ≡ 1;
+ */
+int __gen_e_acsl_sorted(int *t, int n);
+
+int main(void)
+{
+  int __retres;
+  int t[7];
+  int n;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __e_acsl_store_block((void *)(t),28UL);
+  __e_acsl_initialize((void *)(t),sizeof(int));
+  t[0] = 1;
+  __e_acsl_initialize((void *)(& t[1]),sizeof(int));
+  t[1] = 4;
+  __e_acsl_initialize((void *)(& t[2]),sizeof(int));
+  t[2] = 4;
+  __e_acsl_initialize((void *)(& t[3]),sizeof(int));
+  t[3] = 5;
+  __e_acsl_initialize((void *)(& t[4]),sizeof(int));
+  t[4] = 5;
+  __e_acsl_initialize((void *)(& t[5]),sizeof(int));
+  t[5] = 5;
+  __e_acsl_initialize((void *)(& t[6]),sizeof(int));
+  t[6] = 7;
+  n = __gen_e_acsl_sorted(t,7);
+  /*@ assert n ≡ 1; */
+  __e_acsl_assert(n == 1,(char *)"Assertion",(char *)"main",(char *)"n == 1",
+                  23);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(t));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
 /*@ behavior yes:
       assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
       ensures \result ≡ 1;
@@ -82,35 +119,4 @@ int __gen_e_acsl_sorted(int *t, int n)
   }
 }
 
-int main(void)
-{
-  int __retres;
-  int t[7];
-  int n;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(t),28UL);
-  __e_acsl_initialize((void *)(t),sizeof(int));
-  t[0] = 1;
-  __e_acsl_initialize((void *)(& t[1]),sizeof(int));
-  t[1] = 4;
-  __e_acsl_initialize((void *)(& t[2]),sizeof(int));
-  t[2] = 4;
-  __e_acsl_initialize((void *)(& t[3]),sizeof(int));
-  t[3] = 5;
-  __e_acsl_initialize((void *)(& t[4]),sizeof(int));
-  t[4] = 5;
-  __e_acsl_initialize((void *)(& t[5]),sizeof(int));
-  t[5] = 5;
-  __e_acsl_initialize((void *)(& t[6]),sizeof(int));
-  t[6] = 7;
-  n = __gen_e_acsl_sorted(t,7);
-  /*@ assert n ≡ 1; */
-  __e_acsl_assert(n == 1,(char *)"Assertion",(char *)"main",(char *)"n == 1",
-                  23);
-  __retres = 0;
-  __e_acsl_delete_block((void *)(t));
-  __e_acsl_memory_clean();
-  return __retres;
-}
-
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index d39a561886aa2dcf275fc5099184ecb140b5d754..0f982ae2c8480b47dbd087f158fdb5caef766af3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -17,6 +17,41 @@ void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
   return;
 }
 
+/*@ ensures
+      *\old(AverageAccel) ≡
+      (((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
+                                                                    Accel))[1])+(*
+        \old(Accel))[0])/5;
+ */
+void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
+                                                 int *AverageAccel);
+
+int main(void)
+{
+  int __retres;
+  ArrayInt Accel;
+  int av;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __e_acsl_store_block((void *)(& av),4UL);
+  __e_acsl_store_block((void *)(Accel),20UL);
+  __e_acsl_initialize((void *)(Accel),sizeof(int));
+  Accel[0] = 1;
+  __e_acsl_initialize((void *)(& Accel[1]),sizeof(int));
+  Accel[1] = 2;
+  __e_acsl_initialize((void *)(& Accel[2]),sizeof(int));
+  Accel[2] = 3;
+  __e_acsl_initialize((void *)(& Accel[3]),sizeof(int));
+  Accel[3] = 4;
+  __e_acsl_initialize((void *)(& Accel[4]),sizeof(int));
+  Accel[4] = 5;
+  __gen_e_acsl_atp_NORMAL_computeAverageAccel(& Accel,& av);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& av));
+  __e_acsl_delete_block((void *)(Accel));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
 /*@ ensures
       *\old(AverageAccel) ≡
       (((((*\old(Accel))[4]+(*\old(Accel))[3])+(*\old(Accel))[2])+(*\old(
@@ -100,30 +135,4 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
   }
 }
 
-int main(void)
-{
-  int __retres;
-  ArrayInt Accel;
-  int av;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __e_acsl_store_block((void *)(& av),4UL);
-  __e_acsl_store_block((void *)(Accel),20UL);
-  __e_acsl_initialize((void *)(Accel),sizeof(int));
-  Accel[0] = 1;
-  __e_acsl_initialize((void *)(& Accel[1]),sizeof(int));
-  Accel[1] = 2;
-  __e_acsl_initialize((void *)(& Accel[2]),sizeof(int));
-  Accel[2] = 3;
-  __e_acsl_initialize((void *)(& Accel[3]),sizeof(int));
-  Accel[3] = 4;
-  __e_acsl_initialize((void *)(& Accel[4]),sizeof(int));
-  Accel[4] = 5;
-  __gen_e_acsl_atp_NORMAL_computeAverageAccel(& Accel,& av);
-  __retres = 0;
-  __e_acsl_delete_block((void *)(& av));
-  __e_acsl_delete_block((void *)(Accel));
-  __e_acsl_memory_clean();
-  return __retres;
-}
-
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 7224b8101cb0651f8750c4b80369ef62a508451c..db30db6d1bfde9f6c878611e38d273294a174172 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -43,6 +43,19 @@ void *memchr(void const *buf, int c, size_t n)
     return __retres;
 }
 
+/*@ behavior exists:
+      assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+      ensures
+        ∀ int j;
+          0 ≤ j < \offset((char *)\result) ⇒
+          (int)*((char *)\old(buf)+j) ≢ \old(c);
+    
+    behavior not_exists:
+      assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+      ensures \result ≡ (void *)0;
+ */
+void *__gen_e_acsl_memchr(void const *buf, int c, size_t n);
+
 /*@ behavior exists:
       assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
       ensures
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 2f59e51e4e11af6a3b41d530ce459f400702d5b2..018bdb83c5c87129869332175ad44b14345e29b6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -12,6 +12,12 @@ void loop(void)
   return;
 }
 
+/*@ requires global_i ≡ 0;
+    requires \valid(global_i_ptr);
+    requires global_i_ptr ≡ &global_i;
+ */
+void __gen_e_acsl_loop(void);
+
 /*@ requires global_i ≡ 0;
     requires \valid(global_i_ptr);
     requires global_i_ptr ≡ &global_i;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
index fd2388c68c596dfd7f411085ec3dedf6d99a0f63..13f06d38575453150c363be957494b2b3f1b5072 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/base_addr.c:61:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/base_addr.c:61:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/base_addr.c:61:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
index 312ef0ea478cb3851b2f206ec5a485ee0ca3769c..33f7f62f1588be39761cb3bb8fef6f58da254ede 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/block_length.c:61:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/block_length.c:61:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/block_length.c:61:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
index 0eeb4d5756e633eb0940802c3e8a54490f7b3000..84ba859eabbf753a27919d7f839807d5aafdb120 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/call.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/call.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/call.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
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 2b6d552e8233b649fadf488f6cc825499b2644f5..90fbfd1130c2b5e048471e38a4bce05c37bc5e0a 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,16 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/freeable.c:25:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/freeable.c:25:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -13,13 +18,6 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[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: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_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index c93d124df956e8ace69689cab6a599dc68dd8e78..8bc83fa220cd48d8c7e83ad3497432975fd0df4d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -12,24 +12,7 @@ int *f(int *x, int *y)
 }
 
 /*@ ensures \valid(\result); */
-int *__gen_e_acsl_f(int *x, int *y)
-{
-  int *__retres;
-  __e_acsl_store_block((void *)(& __retres),8UL);
-  __e_acsl_store_block((void *)(& x),8UL);
-  __e_acsl_store_block((void *)(& y),8UL);
-  __retres = f(x,y);
-  {
-    int __gen_e_acsl_valid;
-    __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(int));
-    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Postcondition",(char *)"f",
-                    (char *)"\\valid(\\result)",10);
-    __e_acsl_delete_block((void *)(& x));
-    __e_acsl_delete_block((void *)(& y));
-    __e_acsl_delete_block((void *)(& __retres));
-    return __retres;
-  }
-}
+int *__gen_e_acsl_f(int *x, int *y);
 
 int main(void)
 {
@@ -59,4 +42,24 @@ int main(void)
   return __retres;
 }
 
+/*@ ensures \valid(\result); */
+int *__gen_e_acsl_f(int *x, int *y)
+{
+  int *__retres;
+  __e_acsl_store_block((void *)(& __retres),8UL);
+  __e_acsl_store_block((void *)(& x),8UL);
+  __e_acsl_store_block((void *)(& y),8UL);
+  __retres = f(x,y);
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(int));
+    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Postcondition",(char *)"f",
+                    (char *)"\\valid(\\result)",10);
+    __e_acsl_delete_block((void *)(& x));
+    __e_acsl_delete_block((void *)(& y));
+    __e_acsl_delete_block((void *)(& __retres));
+    return __retres;
+  }
+}
+
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index eef5c27e687b43a0ba7be444ba78276a01481d91..4078c1fd83e93e035ef6d837313f3735ae673600 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -9,13 +9,7 @@ void f(void)
 }
 
 /*@ ensures X ≡ 1; */
-void __gen_e_acsl_f(void)
-{
-  f();
-  __e_acsl_assert(X == 1,(char *)"Postcondition",(char *)"f",
-                  (char *)"X == 1",8);
-  return;
-}
+void __gen_e_acsl_f(void);
 
 /*@ ensures X ≡ 2;
     ensures Y ≡ 2; */
@@ -27,15 +21,7 @@ void g(void)
 
 /*@ ensures X ≡ 2;
     ensures Y ≡ 2; */
-void __gen_e_acsl_g(void)
-{
-  g();
-  __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"g",
-                  (char *)"X == 2",12);
-  __e_acsl_assert(Y == 2,(char *)"Postcondition",(char *)"g",
-                  (char *)"Y == 2",13);
-  return;
-}
+void __gen_e_acsl_g(void);
 
 /*@ requires X ≡ 2; */
 void h(void)
@@ -45,13 +31,7 @@ void h(void)
 }
 
 /*@ requires X ≡ 2; */
-void __gen_e_acsl_h(void)
-{
-  __e_acsl_assert(X == 2,(char *)"Precondition",(char *)"h",(char *)"X == 2",
-                  17);
-  h();
-  return;
-}
+void __gen_e_acsl_h(void);
 
 /*@ requires X ≡ 3;
     requires Y ≡ 2; */
@@ -63,15 +43,7 @@ void i(void)
 
 /*@ requires X ≡ 3;
     requires Y ≡ 2; */
-void __gen_e_acsl_i(void)
-{
-  __e_acsl_assert(X == 3,(char *)"Precondition",(char *)"i",(char *)"X == 3",
-                  21);
-  __e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"i",(char *)"Y == 2",
-                  22);
-  i();
-  return;
-}
+void __gen_e_acsl_i(void);
 
 /*@ behavior b1:
       requires X ≡ 5;
@@ -97,21 +69,7 @@ void j(void)
       requires Y ≡ 2;
       ensures X ≡ Y+1;
  */
-void __gen_e_acsl_j(void)
-{
-  __e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
-                  27);
-  __e_acsl_assert((long)X == (long)3 + (long)Y,(char *)"Precondition",
-                  (char *)"j",(char *)"X == 3+Y",30);
-  __e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"j",(char *)"Y == 2",
-                  31);
-  j();
-  __e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"j",
-                  (char *)"X == 3",28);
-  __e_acsl_assert((long)X == (long)Y + (long)1,(char *)"Postcondition",
-                  (char *)"j",(char *)"X == Y+1",32);
-  return;
-}
+void __gen_e_acsl_j(void);
 
 /*@ behavior b1:
       assumes X ≡ 1;
@@ -139,32 +97,7 @@ void k(void)
       requires X ≡ 3;
       requires X+Y ≡ 5;
  */
-void __gen_e_acsl_k(void)
-{
-  {
-    int __gen_e_acsl_implies;
-    int __gen_e_acsl_and;
-    int __gen_e_acsl_implies_2;
-    int __gen_e_acsl_and_2;
-    int __gen_e_acsl_implies_3;
-    if (! (X == 1)) __gen_e_acsl_implies = 1;
-    else __gen_e_acsl_implies = X == 0;
-    __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",(char *)"k",
-                    (char *)"X == 1 ==> X == 0",38);
-    if (X == 3) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0;
-    if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
-    else __gen_e_acsl_implies_2 = X == 3;
-    __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
-                    (char *)"k",(char *)"X == 3 && Y == 2 ==> X == 3",42);
-    if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
-    if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
-    else __gen_e_acsl_implies_3 = (long)X + (long)Y == (long)5;
-    __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
-                    (char *)"k",(char *)"X == 3 && Y == 2 ==> X+Y == 5",43);
-    k();
-  }
-  return;
-}
+void __gen_e_acsl_k(void);
 
 /*@ ensures X ≡ 5; */
 int l(void)
@@ -175,14 +108,7 @@ int l(void)
 }
 
 /*@ ensures X ≡ 5; */
-int __gen_e_acsl_l(void)
-{
-  int __retres;
-  __retres = l();
-  __e_acsl_assert(X == 5,(char *)"Postcondition",(char *)"l",
-                  (char *)"X == 5",47);
-  return __retres;
-}
+int __gen_e_acsl_l(void);
 
 /*@ behavior b1:
       assumes X ≡ 7;
@@ -210,46 +136,7 @@ void m(void)
       ensures X ≡ 7;
       ensures X ≡ \old(X)+Y;
  */
-void __gen_e_acsl_m(void)
-{
-  int __gen_e_acsl_at_4;
-  int __gen_e_acsl_at_3;
-  int __gen_e_acsl_at_2;
-  int __gen_e_acsl_at;
-  __gen_e_acsl_at_4 = X;
-  {
-    int __gen_e_acsl_and_2;
-    if (X == 5) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
-    __gen_e_acsl_at_3 = __gen_e_acsl_and_2;
-  }
-  {
-    int __gen_e_acsl_and;
-    if (X == 5) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0;
-    __gen_e_acsl_at_2 = __gen_e_acsl_and;
-  }
-  __gen_e_acsl_at = X == 7;
-  m();
-  {
-    int __gen_e_acsl_implies;
-    int __gen_e_acsl_implies_2;
-    int __gen_e_acsl_implies_3;
-    if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
-    else __gen_e_acsl_implies = X == 95;
-    __e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"m",
-                    (char *)"\\old(X == 7) ==> X == 95",56);
-    if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1;
-    else __gen_e_acsl_implies_2 = X == 7;
-    __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
-                    (char *)"m",(char *)"\\old(X == 5 && Y == 2) ==> X == 7",
-                    60);
-    if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_3 = 1;
-    else __gen_e_acsl_implies_3 = (long)X == (long)__gen_e_acsl_at_4 + (long)Y;
-    __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Postcondition",
-                    (char *)"m",
-                    (char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",61);
-    return;
-  }
-}
+void __gen_e_acsl_m(void);
 
 /*@ requires X > 0;
     requires X < 10;
@@ -268,6 +155,35 @@ void n(void)
   return;
 }
 
+/*@ requires X > 0;
+    requires X < 10;
+    
+    behavior b1:
+      assumes X ≡ 7;
+      ensures X ≡ 8;
+    
+    behavior b2:
+      assumes X ≡ 5;
+      ensures X ≡ 98;
+ */
+void __gen_e_acsl_n(void);
+
+int main(void)
+{
+  int __retres;
+  __gen_e_acsl_f();
+  __gen_e_acsl_g();
+  __gen_e_acsl_h();
+  __gen_e_acsl_i();
+  __gen_e_acsl_j();
+  __gen_e_acsl_k();
+  __gen_e_acsl_l();
+  __gen_e_acsl_m();
+  __gen_e_acsl_n();
+  __retres = 0;
+  return __retres;
+}
+
 /*@ requires X > 0;
     requires X < 10;
     
@@ -305,20 +221,169 @@ void __gen_e_acsl_n(void)
   }
 }
 
-int main(void)
+/*@ behavior b1:
+      assumes X ≡ 7;
+      ensures X ≡ 95;
+    
+    behavior b2:
+      assumes X ≡ 5;
+      assumes Y ≡ 2;
+      ensures X ≡ 7;
+      ensures X ≡ \old(X)+Y;
+ */
+void __gen_e_acsl_m(void)
+{
+  int __gen_e_acsl_at_4;
+  int __gen_e_acsl_at_3;
+  int __gen_e_acsl_at_2;
+  int __gen_e_acsl_at;
+  __gen_e_acsl_at_4 = X;
+  {
+    int __gen_e_acsl_and_2;
+    if (X == 5) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
+    __gen_e_acsl_at_3 = __gen_e_acsl_and_2;
+  }
+  {
+    int __gen_e_acsl_and;
+    if (X == 5) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0;
+    __gen_e_acsl_at_2 = __gen_e_acsl_and;
+  }
+  __gen_e_acsl_at = X == 7;
+  m();
+  {
+    int __gen_e_acsl_implies;
+    int __gen_e_acsl_implies_2;
+    int __gen_e_acsl_implies_3;
+    if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
+    else __gen_e_acsl_implies = X == 95;
+    __e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"m",
+                    (char *)"\\old(X == 7) ==> X == 95",56);
+    if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1;
+    else __gen_e_acsl_implies_2 = X == 7;
+    __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
+                    (char *)"m",(char *)"\\old(X == 5 && Y == 2) ==> X == 7",
+                    60);
+    if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_3 = 1;
+    else __gen_e_acsl_implies_3 = (long)X == (long)__gen_e_acsl_at_4 + (long)Y;
+    __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Postcondition",
+                    (char *)"m",
+                    (char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",61);
+    return;
+  }
+}
+
+/*@ ensures X ≡ 5; */
+int __gen_e_acsl_l(void)
 {
   int __retres;
-  __gen_e_acsl_f();
-  __gen_e_acsl_g();
-  __gen_e_acsl_h();
-  __gen_e_acsl_i();
-  __gen_e_acsl_j();
-  __gen_e_acsl_k();
-  __gen_e_acsl_l();
-  __gen_e_acsl_m();
-  __gen_e_acsl_n();
-  __retres = 0;
+  __retres = l();
+  __e_acsl_assert(X == 5,(char *)"Postcondition",(char *)"l",
+                  (char *)"X == 5",47);
   return __retres;
 }
 
+/*@ behavior b1:
+      assumes X ≡ 1;
+      requires X ≡ 0;
+    
+    behavior b2:
+      assumes X ≡ 3;
+      assumes Y ≡ 2;
+      requires X ≡ 3;
+      requires X+Y ≡ 5;
+ */
+void __gen_e_acsl_k(void)
+{
+  {
+    int __gen_e_acsl_implies;
+    int __gen_e_acsl_and;
+    int __gen_e_acsl_implies_2;
+    int __gen_e_acsl_and_2;
+    int __gen_e_acsl_implies_3;
+    if (! (X == 1)) __gen_e_acsl_implies = 1;
+    else __gen_e_acsl_implies = X == 0;
+    __e_acsl_assert(__gen_e_acsl_implies,(char *)"Precondition",(char *)"k",
+                    (char *)"X == 1 ==> X == 0",38);
+    if (X == 3) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0;
+    if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+    else __gen_e_acsl_implies_2 = X == 3;
+    __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Precondition",
+                    (char *)"k",(char *)"X == 3 && Y == 2 ==> X == 3",42);
+    if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
+    if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
+    else __gen_e_acsl_implies_3 = (long)X + (long)Y == (long)5;
+    __e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
+                    (char *)"k",(char *)"X == 3 && Y == 2 ==> X+Y == 5",43);
+    k();
+  }
+  return;
+}
+
+/*@ behavior b1:
+      requires X ≡ 5;
+      ensures X ≡ 3;
+    
+    behavior b2:
+      requires X ≡ 3+Y;
+      requires Y ≡ 2;
+      ensures X ≡ Y+1;
+ */
+void __gen_e_acsl_j(void)
+{
+  __e_acsl_assert(X == 5,(char *)"Precondition",(char *)"j",(char *)"X == 5",
+                  27);
+  __e_acsl_assert((long)X == (long)3 + (long)Y,(char *)"Precondition",
+                  (char *)"j",(char *)"X == 3+Y",30);
+  __e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"j",(char *)"Y == 2",
+                  31);
+  j();
+  __e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"j",
+                  (char *)"X == 3",28);
+  __e_acsl_assert((long)X == (long)Y + (long)1,(char *)"Postcondition",
+                  (char *)"j",(char *)"X == Y+1",32);
+  return;
+}
+
+/*@ requires X ≡ 3;
+    requires Y ≡ 2; */
+void __gen_e_acsl_i(void)
+{
+  __e_acsl_assert(X == 3,(char *)"Precondition",(char *)"i",(char *)"X == 3",
+                  21);
+  __e_acsl_assert(Y == 2,(char *)"Precondition",(char *)"i",(char *)"Y == 2",
+                  22);
+  i();
+  return;
+}
+
+/*@ requires X ≡ 2; */
+void __gen_e_acsl_h(void)
+{
+  __e_acsl_assert(X == 2,(char *)"Precondition",(char *)"h",(char *)"X == 2",
+                  17);
+  h();
+  return;
+}
+
+/*@ ensures X ≡ 2;
+    ensures Y ≡ 2; */
+void __gen_e_acsl_g(void)
+{
+  g();
+  __e_acsl_assert(X == 2,(char *)"Postcondition",(char *)"g",
+                  (char *)"X == 2",12);
+  __e_acsl_assert(Y == 2,(char *)"Postcondition",(char *)"g",
+                  (char *)"Y == 2",13);
+  return;
+}
+
+/*@ ensures X ≡ 1; */
+void __gen_e_acsl_f(void)
+{
+  f();
+  __e_acsl_assert(X == 1,(char *)"Postcondition",(char *)"f",
+                  (char *)"X == 1",8);
+  return;
+}
+
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
index bece9f7196a10089d1f9bced2783be1bc86160a5..a59138963615961ea62b70f52e42df4439a69922 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
@@ -266,7 +266,7 @@ int main(void)
                     (char *)"main",(char *)"!\\initialized(p)",65);
   }
   __e_acsl_full_init((void *)(& q));
-  q = (int *)__e_acsl_calloc((unsigned long)1,sizeof(int));
+  q = (int *)__gen_e_acsl_calloc((unsigned long)1,sizeof(int));
   /*@ assert \initialized(q); */
   {
     int __gen_e_acsl_initialized_27;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index 016a37366bb8950ea4faaa9a997b00797ae0c573..e6cbbeeddcae98b2f29a3d6f1905ee04ba7a3e9d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -30,6 +30,9 @@ int __gen_e_acsl_main(void)
   return_label: return __retres;
 }
 
+/*@ ensures X ≡ 3; */
+int main(void);
+
 /*@ ensures X ≡ 3; */
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index b182b73dce562c7f2f7180704f94782e51dd4c9c..9b5601428d5433ef9e50942410bfc3a5679b3781 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -92,6 +92,42 @@ int search(int elt)
   return_label: return __retres;
 }
 
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
+    
+    behavior exists:
+      assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
+      ensures \result ≡ 1;
+    
+    behavior not_exists:
+      assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
+      ensures \result ≡ 0;
+ */
+int __gen_e_acsl_search(int elt);
+
+int main(void)
+{
+  int __retres;
+  int found;
+  {
+    int i;
+    i = 0;
+    while (i < 10) {
+      A[i] = i * i;
+      i ++;
+    }
+  }
+  found = __gen_e_acsl_search(36);
+  /*@ assert found ≡ 1; */
+  __e_acsl_assert(found == 1,(char *)"Assertion",(char *)"main",
+                  (char *)"found == 1",31);
+  found = __gen_e_acsl_search(5);
+  /*@ assert found ≡ 0; */
+  __e_acsl_assert(found == 0,(char *)"Assertion",(char *)"main",
+                  (char *)"found == 0",34);
+  __retres = 0;
+  return __retres;
+}
+
 /*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
     
     behavior exists:
@@ -197,28 +233,4 @@ int __gen_e_acsl_search(int elt)
   }
 }
 
-int main(void)
-{
-  int __retres;
-  int found;
-  {
-    int i;
-    i = 0;
-    while (i < 10) {
-      A[i] = i * i;
-      i ++;
-    }
-  }
-  found = __gen_e_acsl_search(36);
-  /*@ assert found ≡ 1; */
-  __e_acsl_assert(found == 1,(char *)"Assertion",(char *)"main",
-                  (char *)"found == 1",31);
-  found = __gen_e_acsl_search(5);
-  /*@ assert found ≡ 0; */
-  __e_acsl_assert(found == 0,(char *)"Assertion",(char *)"main",
-                  (char *)"found == 0",34);
-  __retres = 0;
-  return __retres;
-}
-
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
index b36c7fd023642732f35f85bdcbbb737adaed7f07..630a6bcaab125656a8eae6b8a9076bf812608fcf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
@@ -69,7 +69,8 @@ int main(int argc, char **argv)
   __e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
                   (char *)"b == (char *)((void *)0)",59);
   __e_acsl_full_init((void *)(& b));
-  b = (char *)__e_acsl_calloc(18446744073709551615UL,18446744073709551615UL);
+  b = (char *)__gen_e_acsl_calloc(18446744073709551615UL,
+                                  18446744073709551615UL);
   /*@ assert __e_acsl_heap_size ≡ 16; */
   __e_acsl_assert(__e_acsl_heap_size == (unsigned long)16,
                   (char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index 6c1e496f75c15df488769235e860cef434f170cf..117b941eb90c449a6582b061a6726093521ebf8a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -7,19 +7,7 @@ int f(int x)
 }
 
 /*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
-int __gen_e_acsl_f(int x)
-{
-  int __gen_e_acsl_at_2;
-  int __gen_e_acsl_at;
-  int __retres;
-  __gen_e_acsl_at_2 = x;
-  __gen_e_acsl_at = x;
-  __retres = f(x);
-  __e_acsl_assert(__retres == (int)((long)__gen_e_acsl_at - (long)__gen_e_acsl_at_2),
-                  (char *)"Postcondition",(char *)"f",
-                  (char *)"\\result == (int)(\\old(x)-\\old(x))",5);
-  return __retres;
-}
+int __gen_e_acsl_f(int x);
 
 int Y = 1;
 /*@ ensures \result ≡ Y; */
@@ -29,19 +17,25 @@ int g(int x)
 }
 
 /*@ ensures \result ≡ Y; */
-int __gen_e_acsl_g(int x)
+int __gen_e_acsl_g(int x);
+
+/*@ ensures \result ≡ 0; */
+int h(void)
 {
   int __retres;
-  __retres = g(x);
-  __e_acsl_assert(__retres == Y,(char *)"Postcondition",(char *)"g",
-                  (char *)"\\result == Y",16);
+  __retres = 0;
   return __retres;
 }
 
 /*@ ensures \result ≡ 0; */
-int h(void)
+int __gen_e_acsl_h(void);
+
+int main(void)
 {
   int __retres;
+  __gen_e_acsl_f(1);
+  __gen_e_acsl_g(Y);
+  __gen_e_acsl_h();
   __retres = 0;
   return __retres;
 }
@@ -56,13 +50,28 @@ int __gen_e_acsl_h(void)
   return __retres;
 }
 
-int main(void)
+/*@ ensures \result ≡ Y; */
+int __gen_e_acsl_g(int x)
 {
   int __retres;
-  __gen_e_acsl_f(1);
-  __gen_e_acsl_g(Y);
-  __gen_e_acsl_h();
-  __retres = 0;
+  __retres = g(x);
+  __e_acsl_assert(__retres == Y,(char *)"Postcondition",(char *)"g",
+                  (char *)"\\result == Y",16);
+  return __retres;
+}
+
+/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
+int __gen_e_acsl_f(int x)
+{
+  int __gen_e_acsl_at_2;
+  int __gen_e_acsl_at;
+  int __retres;
+  __gen_e_acsl_at_2 = x;
+  __gen_e_acsl_at = x;
+  __retres = f(x);
+  __e_acsl_assert(__retres == (int)((long)__gen_e_acsl_at - (long)__gen_e_acsl_at_2),
+                  (char *)"Postcondition",(char *)"f",
+                  (char *)"\\result == (int)(\\old(x)-\\old(x))",5);
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 02a945dca83c592e6948a11f49ab156948621f1b..f95bcfe3f1506f6e2db66a46ee64e902906d46a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -39,28 +39,7 @@ int *f(int *x)
 
 /*@ requires \valid(x);
     ensures \valid(\result); */
-int *__gen_e_acsl_f(int *x)
-{
-  int *__retres;
-  __e_acsl_store_block((void *)(& __retres),8UL);
-  {
-    int __gen_e_acsl_valid;
-    __e_acsl_store_block((void *)(& x),8UL);
-    __gen_e_acsl_valid = __e_acsl_valid((void *)x,sizeof(int));
-    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
-                    (char *)"\\valid(x)",13);
-    __retres = f(x);
-  }
-  {
-    int __gen_e_acsl_valid_2;
-    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)__retres,sizeof(int));
-    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
-                    (char *)"\\valid(\\result)",14);
-    __e_acsl_delete_block((void *)(& x));
-    __e_acsl_delete_block((void *)(& __retres));
-    return __retres;
-  }
-}
+int *__gen_e_acsl_f(int *x);
 
 void g(void)
 {
@@ -109,6 +88,31 @@ void g(void)
   return;
 }
 
+/*@ requires \valid(x);
+    ensures \valid(\result); */
+int *__gen_e_acsl_f(int *x)
+{
+  int *__retres;
+  __e_acsl_store_block((void *)(& __retres),8UL);
+  {
+    int __gen_e_acsl_valid;
+    __e_acsl_store_block((void *)(& x),8UL);
+    __gen_e_acsl_valid = __e_acsl_valid((void *)x,sizeof(int));
+    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
+                    (char *)"\\valid(x)",13);
+    __retres = f(x);
+  }
+  {
+    int __gen_e_acsl_valid_2;
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)__retres,sizeof(int));
+    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
+                    (char *)"\\valid(\\result)",14);
+    __e_acsl_delete_block((void *)(& x));
+    __e_acsl_delete_block((void *)(& __retres));
+    return __retres;
+  }
+}
+
 void __e_acsl_globals_init(void)
 {
   __e_acsl_store_block((void *)(& Z),4UL);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 73deb1a555c541ab18c921baffedb2068d607f07..0a335bdaffe7fe7cc507e69eeb5f636f3c50bcf0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -35,6 +35,27 @@ struct list *f(struct list *l)
     return __retres;
 }
 
+/*@ behavior B1:
+      assumes l ≡ \null;
+      ensures \result ≡ \old(l);
+    
+    behavior B2:
+      assumes ¬\valid(l);
+      assumes ¬\valid(l->next);
+      ensures \result ≡ \old(l);
+ */
+struct list *__gen_e_acsl_f(struct list *l);
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __gen_e_acsl_f((struct list *)0);
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
 /*@ behavior B1:
       assumes l ≡ \null;
       ensures \result ≡ \old(l);
@@ -106,14 +127,4 @@ struct list *__gen_e_acsl_f(struct list *l)
   }
 }
 
-int main(void)
-{
-  int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
-  __gen_e_acsl_f((struct list *)0);
-  __retres = 0;
-  __e_acsl_memory_clean();
-  return __retres;
-}
-
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle
index 236134c85761fdfdb7e3c60de8caa7dc44c5b628..6a5e63eae5f20b0419ee2c9a1457b71c53f1ce75 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
index dd5c54109fb3cfb93fef610edc03ddcd5c71b5d2..8a6001896bd90475ee5d2d619ff1b4c66f8b1e07 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle
@@ -1,61 +1,62 @@
 [e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `calloc':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
 [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:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-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.
-tests/e-acsl-runtime/initialized.c:12:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-tests/e-acsl-runtime/initialized.c:12:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:191:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:191:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/e-acsl-runtime/initialized.c:96:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/initialized.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/initialized.c:96:[e-acsl] warning: E-ACSL construct `disjoint behaviors' 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.
+FRAMAC_SHARE/libc/stdlib.h:206:[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.
+FRAMAC_SHARE/libc/stdlib.h:206:[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.
+FRAMAC_SHARE/libc/stdlib.h:199:[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.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `\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.
+FRAMAC_SHARE/libc/stdlib.h:178:[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 `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete 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.
+FRAMAC_SHARE/libc/stdlib.h:178:[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 `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' 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.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' 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.
+FRAMAC_SHARE/libc/stdlib.h:166:[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:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_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 __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/initialized.c:65:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/initialized.c:69:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:201:[value] warning: function __gen_e_acsl_realloc: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:216:[value] warning: function __gen_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 __gen_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 __gen_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 __gen_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 __gen_e_acsl_realloc, behavior fail: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:192:[value] warning: function __gen_e_acsl_realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:207:[value] warning: function __gen_e_acsl_realloc, behavior dealloc: precondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:202:[value] warning: function __gen_e_acsl_realloc, behavior alloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:209:[value] warning: function __gen_e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:210:[value] warning: function __gen_e_acsl_realloc, behavior dealloc: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:217:[value] warning: function __gen_e_acsl_realloc, behavior fail: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/initialized.c:74:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/initialized.c:76:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __gen_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 __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:179:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0);
 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:84:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/initialized.c:85:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/initialized.c:93:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index bf21eb3a7263fbf394668798147ec5a8e746bf37..7af93084ecafd1cfb9bfba435770be22979d762f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/localvar.c:18:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/localvar.c:18:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/localvar.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
index dead02674d0d3c1874a5da4b54dd8a0a94af0a0e..636c9e84d45762d6b2b13d6b9e8975b938884e84 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
@@ -1,45 +1,46 @@
 [e-acsl] beginning translation.
+[e-acsl] warning: annotating undefined function `calloc':
+                  the generated program may miss memory instrumentation
+                  if there are memory-related annotations.
 [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:156:[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 `\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:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/memsize.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-tests/e-acsl-runtime/memsize.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:191:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:191:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/e-acsl-runtime/memsize.c:69:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/memsize.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/memsize.c:69:[e-acsl] warning: E-ACSL construct `disjoint behaviors' 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.
+FRAMAC_SHARE/libc/stdlib.h:206:[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.
+FRAMAC_SHARE/libc/stdlib.h:206:[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.
+FRAMAC_SHARE/libc/stdlib.h:199:[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.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:213:[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 `\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.
+FRAMAC_SHARE/libc/stdlib.h:178:[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 `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete 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.
+FRAMAC_SHARE/libc/stdlib.h:178:[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 `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' 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.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' 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.
+FRAMAC_SHARE/libc/stdlib.h:166:[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/libc/stdlib.h:163:[value] warning: function __gen_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 __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/memsize.c:22:[value] warning: assertion got status unknown.
 tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
index ee672ce0bab9df6f283f9b7db443b4e8fed45319..c21c041bd00762e3f1103eb9c22916bf52052b16 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/offset.c:55:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/offset.c:55:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/offset.c:55:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index f0ad15098a8312f6ceb601edcc226f7b8d9ef46c..74fa2a87aa44d9a16ac6e2b055545f9a0bd0de5a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -1,10 +1,10 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/ptr_init.c:26:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/ptr_init.c:26:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/ptr_init.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
index 45750468b0fbdc3d9ec514eac5934eec968cfbb9..1c33113def7fdc97420d2d95e93c8692942824f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -2,7 +2,7 @@
 [e-acsl] warning: annotating undefined function `fopen':
                   the generated program may miss memory instrumentation
                   if there are memory-related annotations.
-tests/e-acsl-runtime/stdout.c:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/e-acsl-runtime/stdout.c:11:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index a74480a2be56851d17b1ab3f8d42434724eabea0..006ce91f496a1b9116396f5cd1587c07f0de0c2a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -1,11 +1,16 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -13,13 +18,6 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index ed12c3b0d9dc9b0f3640049dad0ed3f2aeb0454b..22951efd584ac785e47d460a5ddbd3430db4f264 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -1,11 +1,16 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/valid_alias.c:17:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/valid_alias.c:17:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -13,13 +18,6 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 45d1159e99b0f5a1d2a3c5968f7b47724ce6bbd7..c27dbd9bb0282333fd49e5ee52cc39dc4e0152ca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -1,11 +1,16 @@
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/e-acsl-runtime/vector.c:28:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -13,13 +18,6 @@ FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns claus
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
-                  Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 79cc76ee82b8020d2521410da4baff6c054e406a..970ee1078a16323c82780ead62de626f0e762906 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -30,15 +30,7 @@ void f(void)
 }
 
 /*@ ensures \at(A,Post) ≡ 3; */
-void __gen_e_acsl_f(void)
-{
-  int __gen_e_acsl_at;
-  f();
-  __gen_e_acsl_at = A;
-  __e_acsl_assert(__gen_e_acsl_at == 3,(char *)"Postcondition",(char *)"f",
-                  (char *)"\\at(A,Post) == 3",7);
-  return;
-}
+void __gen_e_acsl_f(void);
 
 void g(int *p, int *q)
 {
@@ -118,21 +110,7 @@ int h(int x)
 }
 
 /*@ ensures \result ≡ \old(x); */
-int __gen_e_acsl_h(int x)
-{
-  int __gen_e_acsl_at;
-  int __retres;
-  __e_acsl_store_block((void *)(& __retres),4UL);
-  __e_acsl_store_block((void *)(& x),4UL);
-  __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
-  __gen_e_acsl_at = x;
-  __retres = h(x);
-  __e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
-                  (char *)"h",(char *)"\\result == \\old(x)",38);
-  __e_acsl_delete_block((void *)(& x));
-  __e_acsl_delete_block((void *)(& __retres));
-  return __retres;
-}
+int __gen_e_acsl_h(int x);
 
 int main(void)
 {
@@ -180,4 +158,32 @@ int main(void)
   return __retres;
 }
 
+/*@ ensures \result ≡ \old(x); */
+int __gen_e_acsl_h(int x)
+{
+  int __gen_e_acsl_at;
+  int __retres;
+  __e_acsl_store_block((void *)(& __retres),4UL);
+  __e_acsl_store_block((void *)(& x),4UL);
+  __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
+  __gen_e_acsl_at = x;
+  __retres = h(x);
+  __e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
+                  (char *)"h",(char *)"\\result == \\old(x)",38);
+  __e_acsl_delete_block((void *)(& x));
+  __e_acsl_delete_block((void *)(& __retres));
+  return __retres;
+}
+
+/*@ ensures \at(A,Post) ≡ 3; */
+void __gen_e_acsl_f(void)
+{
+  int __gen_e_acsl_at;
+  f();
+  __gen_e_acsl_at = A;
+  __e_acsl_assert(__gen_e_acsl_at == 3,(char *)"Postcondition",(char *)"f",
+                  (char *)"\\at(A,Post) == 3",7);
+  return;
+}
+
 
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 1f55d180a68b8c69dfc58ae4f75f64434eb2bf03..2ecfd6cb4622e09915cfb8b8ddbb07dac4abbc1e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -74,26 +74,7 @@ void f(void)
 }
 
 /*@ ensures \at(A,Post) ≡ 3; */
-void __gen_e_acsl_f(void)
-{
-  int __gen_e_acsl_at;
-  f();
-  {
-    mpz_t __gen_e_acsl_;
-    mpz_t __gen_e_acsl__2;
-    int __gen_e_acsl_eq;
-    __gen_e_acsl_at = A;
-    __gmpz_init_set_si(__gen_e_acsl_,(long)__gen_e_acsl_at);
-    __gmpz_init_set_si(__gen_e_acsl__2,(long)3);
-    __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
-                                 (__mpz_struct const *)(__gen_e_acsl__2));
-    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
-                    (char *)"\\at(A,Post) == 3",7);
-    __gmpz_clear(__gen_e_acsl_);
-    __gmpz_clear(__gen_e_acsl__2);
-    return;
-  }
-}
+void __gen_e_acsl_f(void);
 
 void g(int *p, int *q)
 {
@@ -187,32 +168,7 @@ int h(int x)
 }
 
 /*@ ensures \result ≡ \old(x); */
-int __gen_e_acsl_h(int x)
-{
-  int __gen_e_acsl_at;
-  int __retres;
-  __e_acsl_store_block((void *)(& __retres),4UL);
-  __e_acsl_store_block((void *)(& x),4UL);
-  __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
-  __gen_e_acsl_at = x;
-  __retres = h(x);
-  {
-    mpz_t __gen_e_acsl_result;
-    mpz_t __gen_e_acsl_;
-    int __gen_e_acsl_eq;
-    __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
-    __gmpz_init_set_si(__gen_e_acsl_,(long)__gen_e_acsl_at);
-    __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_result),
-                                 (__mpz_struct const *)(__gen_e_acsl_));
-    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"h",
-                    (char *)"\\result == \\old(x)",38);
-    __e_acsl_delete_block((void *)(& x));
-    __gmpz_clear(__gen_e_acsl_result);
-    __gmpz_clear(__gen_e_acsl_);
-    __e_acsl_delete_block((void *)(& __retres));
-    return __retres;
-  }
-}
+int __gen_e_acsl_h(int x);
 
 int main(void)
 {
@@ -319,4 +275,54 @@ int main(void)
   return __retres;
 }
 
+/*@ ensures \result ≡ \old(x); */
+int __gen_e_acsl_h(int x)
+{
+  int __gen_e_acsl_at;
+  int __retres;
+  __e_acsl_store_block((void *)(& __retres),4UL);
+  __e_acsl_store_block((void *)(& x),4UL);
+  __e_acsl_store_block((void *)(& __gen_e_acsl_at),4UL);
+  __gen_e_acsl_at = x;
+  __retres = h(x);
+  {
+    mpz_t __gen_e_acsl_result;
+    mpz_t __gen_e_acsl_;
+    int __gen_e_acsl_eq;
+    __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
+    __gmpz_init_set_si(__gen_e_acsl_,(long)__gen_e_acsl_at);
+    __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_result),
+                                 (__mpz_struct const *)(__gen_e_acsl_));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"h",
+                    (char *)"\\result == \\old(x)",38);
+    __e_acsl_delete_block((void *)(& x));
+    __gmpz_clear(__gen_e_acsl_result);
+    __gmpz_clear(__gen_e_acsl_);
+    __e_acsl_delete_block((void *)(& __retres));
+    return __retres;
+  }
+}
+
+/*@ ensures \at(A,Post) ≡ 3; */
+void __gen_e_acsl_f(void)
+{
+  int __gen_e_acsl_at;
+  f();
+  {
+    mpz_t __gen_e_acsl_;
+    mpz_t __gen_e_acsl__2;
+    int __gen_e_acsl_eq;
+    __gen_e_acsl_at = A;
+    __gmpz_init_set_si(__gen_e_acsl_,(long)__gen_e_acsl_at);
+    __gmpz_init_set_si(__gen_e_acsl__2,(long)3);
+    __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_),
+                                 (__mpz_struct const *)(__gen_e_acsl__2));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
+                    (char *)"\\at(A,Post) == 3",7);
+    __gmpz_clear(__gen_e_acsl_);
+    __gmpz_clear(__gen_e_acsl__2);
+    return;
+  }
+}
+