diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 0e7ee7c1983a3ef5939232c262473793d1b68727..e2d8c8d10031e1f2762a5aef1149971d4482c6e2 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -72,7 +72,14 @@ let add_stmt env s =
   { env with beginning_of_block = s :: env.beginning_of_block }
 
 let add_assert s p = 
-  Queue.add (fun () -> Annotations.add_assert s [ !self ] p) !queue
+  Queue.add
+    (fun () -> 
+      (* Don't work since the kernel_function does not yet exist in the new
+	 project. Virgile said he was implementing the missing stuff in the
+	 visitor. Wait and see... *)
+      let kf = Kernel_function.find_englobing_kf s in
+      Annotations.add_assert kf s [ !self ] p) 
+    !queue
 
 let new_var env ty mk_stmts = 
   let is_t = Mpz.is_t ty in
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index bb1d8ec29f3c4c2f98e42dfc53cac5b969803a38..c141632bb58b31ade5aa917e5370ce9954e6b26f 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -23,11 +23,11 @@ open Plugin
 
 include S (** implementation of Log.S for E-ACSL *)
 
-module Check: BOOL
-module Project_name: STRING
+module Check: Bool
+module Project_name: String
 
-module Include_headers: BOOL
-module Use_assert: BOOL
+module Include_headers: Bool
+module Use_assert: Bool
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 7361611b9f4810860b6d21c172ead295a3ad5058..8da06b547cf775f97491132f1f6f7eaa36e4cf9b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index 43c3797902fd55a2090f3b548949d14907638228..544404c6a2c87c4e3cd7579be7f235aea1c216d8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 395856a53c8ceffce36e5abb3126ba6751e8d2c6..f9fcaa6fba4ff2631003bebba137d2c52183d2c4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -558,7 +558,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 4b7df2a3eac3185dfa7de5366d8dedcf3d6be29a..9a49a5b9bac388ac1fa391fbce07fb8b200c641d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -562,7 +562,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index 05dd29264133a87c54b4ef5d3dc805902d49a0a0..896e8e07c9cd556d9b1eeddbec4cbd7a51e80cb0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
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 4c9805123aa6cf32a5613c46e5ef4e2cc3a53c34..905f2505d5d5ec5111f9a0f22457d7fb447a67ed 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
@@ -570,7 +570,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index f3a115e07bfc91429d95983eb189337a7e3d516b..ff9270e09b6653e34b578f8b6f7b6128fc5fbbb3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -560,7 +560,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index 2a00e9922cec25e01289734cbbd48b6ce0dd9528..c1cf5dd3276c8dc8056421aa8668ec2570e2e227 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -559,7 +559,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 9f9ad7bc51a750d85b4aa8fb53af8ea570949a8c..6bc72d79e79492a9df4b9b9f51859c0d9c7ef948 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index 5601a5004045a1085ed0eb511f7119150f60f90e..3d53d3b5582991895b6c52270c8efbdb5497680e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index f3570d72c0e55f6674ab5ac4970ce93dad76df40..dc09d6036924a1c54314a1200f46637c02cb8713 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -563,7 +563,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 95d44f6fc78879650b612322f4287143e006cedc..247ab01e0ab116318e18729ec57bdc25c701377f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -559,7 +559,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index a2a819c96637c423ace06d84261a822e8441f30a..dcdb30984f20058d8d8a8a1602de2f4082ce2d3d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -546,7 +546,7 @@ __inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
 extern void exit(int status);
 void e_acsl_fail(char *msg)
 {
-  printf((char const *)"%s\n",msg);
+  printf("%s\n",msg);
   exit(1);
   return;
 }