From 8ae74828bd0cd08e613134dcaafadd8875283828 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 20 Feb 2024 19:17:43 +0100
Subject: [PATCH] [ir2cabs] use wchar_t also in ACSL++ translation

---
 convert.ml                                    | 24 ++++++++--------
 tests/basic/oracle/placement_new.res.oracle   | 28 +++++++++++--------
 .../oracle/stl_shared_ptr_mistake6.res.oracle |  4 +--
 3 files changed, 30 insertions(+), 26 deletions(-)

diff --git a/convert.ml b/convert.ml
index 02055430..50c629a2 100644
--- a/convert.ml
+++ b/convert.ml
@@ -2146,21 +2146,21 @@ and convert_init_statement env init does_remove_virtual =
           let env = Convert_env.add_local_var env id_name typ.plain_type in
           match init_val with
           | None ->
-      let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
-      (env, aux, init::l, def, base)
+	    let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
+	    (env, aux, init::l, def, base)
           | Some init ->
             let var = Local { prequalification = []; decl_name = id_name } in
             let env,aux',init, def' =
               convert_initializer env typ var init does_remove_virtual
             in
-      let def = match def' with
-        | None -> def
-        | Some stmt -> stmt::def
-      in
-      let init = (id_name, decl JUSTBASE,attrs,loc),init in
-      env, merge_aux aux' aux, init::l, def, base)
-  init_declarator_list
-  (env, empty_aux, [], [], None)
+	    let def = match def' with
+	      | None -> def
+	      | Some stmt -> stmt::def
+	    in
+	    let init = (id_name, decl JUSTBASE,attrs,loc),init in
+	    env, merge_aux aux' aux, init::l, def, base)
+	init_declarator_list
+	(env, empty_aux, [], [], None)
     in
     let l = List.rev l in
     if l = [] then
@@ -2776,8 +2776,8 @@ let iter_on_array ?(incr=true) env idx length mk_body =
   let init =
     if incr then const_int 0
     else BINARY(SUB, length,
-    {expr_loc=loc;
-    expr_node=const_int 1})
+		{expr_loc=loc;
+		 expr_node=const_int 1})
   in
   let last = if incr then length.expr_node else const_int 0 in
   let last_test = if incr then LT else GE in
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 8b784187..8a0d1fdb 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -295,30 +295,33 @@ axiomatic WcsLen {
   axiom wcslen_pos_or_null{L}:
     ∀ wchar_t *s;
     ∀ ℤ i;
-      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
-      *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
+      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (long)0) ∧
+      *(s + i) ≡ (long)0 ⇒ wcslen(s) ≡ i;
   
   axiom wcslen_neg{L}:
-    ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
+    ∀ long *s;
+      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (long)0) ⇒ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
     ∀ wchar_t *s;
-    ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
+    ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (long)0;
   
   axiom wcslen_at_null{L}:
-    ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
+    ∀ long *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (long)0;
   
   axiom wcslen_not_zero{L}:
     ∀ wchar_t *s;
-    ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
+    ∀ int i;
+      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (long)0 ⇒ i < wcslen(s);
   
   axiom wcslen_zero{L}:
     ∀ wchar_t *s;
-    ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
+    ∀ int i;
+      0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (long)0 ⇒ i ≡ wcslen(s);
   
   axiom wcslen_sup{L}:
     ∀ wchar_t *s;
-    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
+    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (long)0 ⇒ 0 ≤ wcslen(s) ≤ i;
   
   axiom wcslen_shift{L}:
     ∀ wchar_t *s;
@@ -326,13 +329,14 @@ axiomatic WcsLen {
   
   axiom wcslen_create{L}:
     ∀ wchar_t *s;
-    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
+    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ (long)0 ⇒ 0 ≤ wcslen(s) ≤ i;
   
   axiom wcslen_create_shift{L}:
     ∀ wchar_t *s;
     ∀ int i;
     ∀ int k;
-      0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
+      0 ≤ k ≤ i ∧ *(s + i) ≡ (long)0 ⇒
+      0 ≤ wcslen(s + k) ≤ i - k;
   
   }
  */
@@ -371,8 +375,8 @@ axiomatic WcsChr {
   axiom wcschr_def{L}:
     ∀ wchar_t *wcs;
     ∀ ℤ wc;
-      wcschr(wcs, wc) ≡ \true ⇔
-      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)wc);
+      wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (long)((int)wc));
   
   }
  */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 25559b64..ee5379d5 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -542,8 +542,8 @@ axiomatic WcsChr {
   axiom wcschr_def{L}:
     ∀ wchar_t *wcs;
     ∀ ℤ wc;
-      wcschr(wcs, wc) ≡ \true ⇔
-      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (wchar_t)wc);
+(??)      wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
+(??)      (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (long)((int)wc));
   
   }
  */
-- 
GitLab