From 3476e2d763eb9638f79c9e995c0ab4d105a0b7ae Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 23 Aug 2011 13:45:27 +0000
Subject: [PATCH] Update according to kernel changes. Some oracles still broken
 (see comment in Env.add_assert)

---
 src/plugins/e-acsl/env.ml                                | 9 ++++++++-
 src/plugins/e-acsl/options.mli                           | 8 ++++----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c      | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_array.c       | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c        | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c  | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_false.c       | 2 +-
 .../tests/e-acsl-runtime/oracle/gen_function_contract.c  | 2 +-
 .../tests/e-acsl-runtime/oracle/gen_integer_constant.c   | 2 +-
 .../tests/e-acsl-runtime/oracle/gen_nested_code_annot.c  | 2 +-
 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_null.c        | 2 +-
 .../tests/e-acsl-runtime/oracle/gen_other_constants.c    | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c      | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_true.c        | 2 +-
 15 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 0e7ee7c1983..e2d8c8d1003 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 bb1d8ec29f3..c141632bb58 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 7361611b9f4..8da06b547cf 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 43c3797902f..544404c6a2c 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 395856a53c8..f9fcaa6fba4 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 4b7df2a3eac..9a49a5b9bac 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 05dd2926413..896e8e07c9c 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 4c9805123aa..905f2505d5d 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 f3a115e07bf..ff9270e09b6 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 2a00e9922ce..c1cf5dd3276 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 9f9ad7bc51a..6bc72d79e79 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 5601a500404..3d53d3b5582 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 f3570d72c0e..dc09d603692 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 95d44f6fc78..247ab01e0ab 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 a2a819c9663..dcdb30984f2 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;
 }
-- 
GitLab