diff --git a/share/libc/__fc_string_axiomatic.h b/share/libc/__fc_string_axiomatic.h
index efd4b09bc698630ed51de4c0ae6bdece653e5e11..249460be20a7dc8219ee5147bac8c80566ff5348 100644
--- a/share/libc/__fc_string_axiomatic.h
+++ b/share/libc/__fc_string_axiomatic.h
@@ -44,7 +44,6 @@ __BEGIN_DECLS
   @ }
   @*/
 
-
 /*@ axiomatic MemChr {
   @ logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n)
   @   reads s[0..n - 1];
@@ -52,7 +51,8 @@ __BEGIN_DECLS
   @
   @ logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n)
   @   reads s[0..n - 1];
-  @ // Returns the offset at which [c] appears in [s]. // TODO: is n useful?
+  @ // Returns the offset at which [c] appears in [s], or [n-1] otherwise.
+  @ // It represents the largest searched index when looking for [c] in [s].
   @
   @ axiom memchr_def{L}:
   @   \forall char *s; \forall ℤ c; \forall ℤ n;
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 2c39d88a1ba0dec4b714b367d2135072004533d3..8aa7d62c36c76a1fbc8f628a6bbc24ec5819e295 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -435,6 +435,10 @@ let _frama_c_strnlen_wrapper =
   register_builtin "strnlen"
     ~search:Ival.zero ~stop_at_0:false ~typ:Char ~length:true ~limit:1
 
+let frama_c_memchr_off_wrapper =
+  do_search
+    ~search:Ival.bottom ~stop_at_0:false ~typ:Char ~length:true ~limit:2
+
 let _frama_c_memchr_wrapper =
   register_builtin "memchr"
     ~search:Ival.bottom ~stop_at_0:false ~typ:Char ~length:false ~limit:2
@@ -451,6 +455,10 @@ let frama_c_wcslen_wrapper =
   register_builtin "wcslen"
     ~search:Ival.zero ~stop_at_0:false ~typ:Wide ~length:true ?limit:None
 
+let frama_c_wmemchr_off_wrapper =
+  do_search
+    ~search:Ival.bottom ~stop_at_0:false ~typ:Wide ~length:true ~limit:2
+
 let frama_c_wcschr_wrapper =
   register_builtin "wcschr"
     ~search:Ival.bottom ~stop_at_0:true ~typ:Wide ~length:false ?limit:None
diff --git a/src/plugins/value/domains/cvalue/builtins_string.mli b/src/plugins/value/domains/cvalue/builtins_string.mli
index a19e4d7b09194af36918c3be2c7a7146782d9c47..b5e79dfd512c10bf57c9b776e20f696072011e23 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.mli
+++ b/src/plugins/value/domains/cvalue/builtins_string.mli
@@ -30,3 +30,5 @@ val frama_c_strlen_wrapper: str_builtin_sig
 val frama_c_wcslen_wrapper: str_builtin_sig
 val frama_c_strchr_wrapper: str_builtin_sig
 val frama_c_wcschr_wrapper: str_builtin_sig
+val frama_c_memchr_off_wrapper: str_builtin_sig
+val frama_c_wmemchr_off_wrapper: str_builtin_sig
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 13ffb2300d361dc1c7c9e14434997e9e78116197..83e32e3c30e54a678d4356bc472fcc3d8bc74e77 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -557,29 +557,30 @@ let constraint_trange idx size_arr =
 
 (* Note: "charlen" stands for either strlen or wcslen *)
 
-(* Evaluates the logical predicates [strlen/wcslen] using str* builtins.
-   Returns [res, alarms], where [res] is the return value of [strlen]
-   ([None] the evaluation results in [bottom]). *)
-let logic_charlen_builtin wrapper state v =
+(* Applies a cvalue [builtin] to the list of arguments [args_list] in the
+   current state of [env]. Returns [v, alarms], where [v] is the resulting
+   cvalue, or [None] if the builtin leads to [bottom]. *)
+let apply_logic_builtin builtin env args_list =
   (* the call below could in theory return Builtins.Invalid_nb_of_args,
      but logic typing constraints prevent that. *)
-  let res, alarms = wrapper state [v] in
+  let res, alarms = builtin (env_current_state env) args_list in
   match res with
   | None -> None
-  | Some offsm -> Some (offsm, alarms)
+  | Some offsm ->
+    let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
+    let v = Cvalue.V_Or_Uninitialized.get_v v in
+    Some (v, alarms)
 
 (* Never raises exceptions; instead, returns [-1,+oo] in case of alarms
    (most imprecise result possible for the logic strlen/wcslen predicates). *)
 let eval_logic_charlen wrapper env v ldeps =
   let eover =
-    match logic_charlen_builtin wrapper (env_current_state env) v with
+    match apply_logic_builtin wrapper env [v] with
     | None -> Cvalue.V.bottom
-    | Some (offsm, alarms) ->
+    | Some (v, alarms) ->
       if alarms
       then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
-      else
-        let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
-        Cvalue.V_Or_Uninitialized.get_v v
+      else v
   in
   let eunder = under_from_over eover in
   (* the C strlen function has type size_t, but the logic strlen function has
@@ -590,14 +591,12 @@ let eval_logic_charlen wrapper env v ldeps =
 (* Evaluates the logical predicates strchr/wcschr. *)
 let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
   let eover =
-    match builtin (env_current_state env) [s; c] with
-    | None, _ -> Cvalue.V.bottom
-    | Some offsm, alarms ->
+    match apply_logic_builtin builtin env [s; c] with
+    | None -> Cvalue.V.bottom
+    | Some (r, alarms) ->
       if alarms
       then Cvalue.V.zero_or_one
       else
-        let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
-        let r = Cvalue.V_Or_Uninitialized.get_v v in
         let ctrue = Cvalue.V.contains_non_zero r
         and cfalse = Cvalue.V.contains_zero r in
         match ctrue, cfalse with
@@ -613,6 +612,23 @@ let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
   let ldeps = join_logic_deps ldeps_s ldeps_c in
   { etype; ldeps; eover; empty = false; eunder }
 
+(* Evaluates the logical functions memchr_off/wmemchr_off. *)
+let eval_logic_memchr_off builtin env s c n =
+  let minus_one = Cvalue.V.inject_int Integer.minus_one in
+  let positive = Cvalue.V.inject_ival Ival.positive_integers in
+  let pred_n = Cvalue.V.add_untyped Int_Base.one n.eover minus_one in
+  let n_pos = Cvalue.V.narrow positive pred_n in
+  let eover =
+    if Cvalue.V.is_bottom n_pos then minus_one else
+      match apply_logic_builtin builtin env [s.eover; c.eover; n_pos] with
+      | None -> pred_n
+      | Some (v, alarms) ->
+        if alarms then Cvalue.V.join pred_n v else
+        if Cvalue.V.equal n_pos pred_n then v else Cvalue.V.join minus_one v
+  in
+  let ldeps = join_logic_deps s.ldeps (join_logic_deps c.ldeps n.ldeps) in
+  { (einteger eover) with ldeps }
+
 (* Evaluates the logical predicate is_allocable, according to the following
    logic:
    - if the size to allocate is always too large (> SIZE_MAX), allocation fails;
@@ -682,6 +698,8 @@ let known_logic_funs = [
   "wcslen", Libc;
   "strchr", Libc;
   "wcschr", Libc;
+  "memchr_off", Libc;
+  "wmemchr_off", Libc;
   "atan2", ACSL;
   "atan2f", ACSL;
   "pow", ACSL;
@@ -1304,6 +1322,17 @@ and eval_known_logic_function ~alarm_mode env li labels args =
     in
     eval_logic_charlen builtin { env with e_cur = lbl } r.eover r.ldeps
 
+  | ("memchr_off" | "wmemchr_off") as b,  _, [lbl], [arg_s; arg_c; arg_n] ->
+    let s = eval_term ~alarm_mode env arg_s in
+    let c = eval_term ~alarm_mode env arg_c in
+    let n = eval_term ~alarm_mode env arg_n in
+    let builtin =
+      if b = "memchr_off"
+      then Builtins_string.frama_c_memchr_off_wrapper
+      else Builtins_string.frama_c_wmemchr_off_wrapper
+    in
+    eval_logic_memchr_off builtin { env with e_cur = lbl } s c n
+
   | ("strchr" | "wcschr") as b,  _, [lbl], [arg_s; arg_c] ->
     let s = eval_term ~alarm_mode env arg_s in
     let c = eval_term ~alarm_mode env arg_c in
@@ -1526,7 +1555,7 @@ let eval_valid_read_str ~wide env v =
     if wide then Builtins_string.frama_c_wcslen_wrapper
     else Builtins_string.frama_c_strlen_wrapper
   in
-  match logic_charlen_builtin wrapper (env_current_state env) v with
+  match apply_logic_builtin wrapper env [v] with
   | None -> (* bottom state => string always invalid *) False
   | Some (_res, alarms) ->
     if alarms
diff --git a/tests/builtins/memchr.c b/tests/builtins/memchr.c
index 7b39c55a84529e8cdd1e28b6fe2637e7f4fad4eb..f6563da4796ccaafff22d63fcac92ddcb8f684e6 100644
--- a/tests/builtins/memchr.c
+++ b/tests/builtins/memchr.c
@@ -202,17 +202,17 @@ void memchr_large() {
   a[20] = 0;
   a[75] = 0;
   Ival offset = RANGE(3, 30);
-  MEMCHR(RES, z1, a, offset, c, 100); // alarm from precondition
+  MEMCHR(RES, z1, a, offset, c, 100);
   //@ assert (z1 >= -1 && z1 <= 75);
   //@ assert refined: (z1 == 20 || z1 == 75);
 
   offset = RANGE(5, 17);
-  MEMCHR(RES, z2, a, offset, c, 100); // alarm from precondition
+  MEMCHR(RES, z2, a, offset, c, 100);
   //@ assert (z2 >= -1 && z2 <= 20);
   //@ assert refined: (z2 == 20);
 
   offset = RANGE(60, 74);
-  MEMCHR(RES, z3, a, offset, c, 100); // alarm from precondition
+  MEMCHR(RES, z3, a, offset, c, 100);
   //@ assert (z3 >= -1 && z3 <= 75);
   //@ assert refined: (z3 == 75);
 
@@ -313,14 +313,14 @@ void memchr_misc() {
   MEMCHR2(RES, sz2, str, 0, 3, c, 12); // alarm in precondition
   //@ assert (sz2 == 0); // alarm
   loc_char_array[3] = '\0';
-  MEMCHR_bottom(loc_char_array, 0, c, 5); // alarm in precondition
-  MEMCHR(RES, sz4a, zero_str, 0, c, 9); // no alarm
+  MEMCHR_bottom(loc_char_array, 0, c, 5); // red alarm in precondition
+  MEMCHR(RES, sz4a, zero_str, 0, c, 9);
   //@ assert (sz4a == 3);
-  MEMCHR(RES, sz4b, zero_str, 4, c, 9); // alarm in precondition
+  MEMCHR(RES, sz4b, zero_str, 4, c, 9);
   //@ assert (sz4b == 4);
-  MEMCHR(RES, sz4c, zero_str, 5, c, 9); // alarm in precondition
+  MEMCHR(RES, sz4c, zero_str, 5, c, 9);
   //@ assert (sz4c == 5);
-  MEMCHR(RES, sz4d, zero_str, 6, c, 9); // alarm in precondition
+  MEMCHR(RES, sz4d, zero_str, 6, c, 9);
   //@ assert (sz4d == 9);
 }
 
@@ -498,13 +498,13 @@ void memchr_unbounded_n() {
   if (n < 0) n = 0;
   CHAR_PTR(s);
   STRING(s,"abc");
-  MEMCHR(RES, zu1, s, 0, c, n); // warning from precondition
+  MEMCHR(RES, zu1, s, 0, c, n);
   //@ assert (zu1 == -1 || zu1 == 3);
   Ival o = NONDET(0,1);
   MEMCHR(RES, zu2, s, o, c, n); // warning from precondition
   //@ assert (zu2 == -1 || zu2 == 2 || zu2 == 3);
   STRING(s,"bcd\0eg");
-  MEMCHR(RES, zu3, s, 0, c, n); // warning from precondition
+  MEMCHR(RES, zu3, s, 0, c, n);
   //@ assert (zu3 == -1 || zu3 == 3);
 }
 
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index d77c490f0c7d086f6a2150c57f9c6585a7e3c1f2..228d7406ba2bb1a8b76ab084431e8a9005743923 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -21,14 +21,8 @@
 [eva] computing for function memchr_small_sets <- main.
   Called from tests/builtins/memchr.c:652.
 [eva] tests/builtins/memchr.c:90: Call to builtin memchr
-[eva] share/libc/string.h:69: 
-  Cannot evaluate range bound memchr_off((char *)s, c, n)
-  (unsupported ACSL construct: logic function memchr_off). Approximating
 [eva:alarm] tests/builtins/memchr.c:90: Warning: 
   function memchr: precondition 'valid' got status unknown.
-[eva] share/libc/string.h:72: 
-  Cannot evaluate range bound memchr_off((char *)s, c, n)
-  (unsupported ACSL construct: logic function memchr_off). Approximating
 [eva:alarm] tests/builtins/memchr.c:90: Warning: 
   function memchr: precondition 'initialization' got status unknown.
 [eva:alarm] tests/builtins/memchr.c:90: Warning: 
@@ -99,11 +93,11 @@
 [eva] tests/builtins/memchr.c:121: assertion got status valid.
 [eva] tests/builtins/memchr.c:122: Call to builtin memchr
 [eva:alarm] tests/builtins/memchr.c:122: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:122: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:122: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+  function memchr: precondition 'valid' got status invalid.
+[eva] tests/builtins/memchr.c:122: 
+  function memchr: no state left, precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:122: 
+  function memchr: no state left, precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:128: Call to builtin memchr
 [eva:alarm] tests/builtins/memchr.c:128: Warning: 
   function memchr: precondition 'valid' got status unknown.
@@ -128,9 +122,9 @@
 [eva] tests/builtins/memchr.c:140: 
   function memchr: precondition 'valid' got status valid.
 [eva:alarm] tests/builtins/memchr.c:140: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
+  function memchr: precondition 'initialization' got status invalid.
 [eva] tests/builtins/memchr.c:140: 
-  function memchr: precondition 'danglingness' got status valid.
+  function memchr: no state left, precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:145: Call to builtin memchr
 [eva] tests/builtins/memchr.c:145: 
   function memchr: precondition 'valid' got status valid.
@@ -169,12 +163,12 @@
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] tests/builtins/memchr.c:205: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:205: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:205: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:205: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:205: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:205: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:205: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:205: Frama_C_show_each_mymemchr: {20; 75}
 [eva] tests/builtins/memchr.c:206: assertion got status valid.
 [eva] tests/builtins/memchr.c:207: assertion 'refined' got status valid.
@@ -184,12 +178,12 @@
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] tests/builtins/memchr.c:210: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:210: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:210: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:210: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:210: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:210: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:210: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:210: Frama_C_show_each_mymemchr: {20}
 [eva] tests/builtins/memchr.c:211: assertion got status valid.
 [eva] tests/builtins/memchr.c:212: assertion 'refined' got status valid.
@@ -199,12 +193,12 @@
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] tests/builtins/memchr.c:215: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:215: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:215: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:215: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:215: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:215: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:215: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:215: Frama_C_show_each_mymemchr: {75}
 [eva] tests/builtins/memchr.c:216: assertion got status valid.
 [eva] tests/builtins/memchr.c:217: assertion 'refined' got status valid.
@@ -328,11 +322,11 @@
   Called from tests/builtins/memchr.c:658.
 [eva] tests/builtins/memchr.c:307: Call to builtin memchr
 [eva:alarm] tests/builtins/memchr.c:307: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:307: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:307: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+  function memchr: precondition 'valid' got status invalid.
+[eva] tests/builtins/memchr.c:307: 
+  function memchr: no state left, precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:307: 
+  function memchr: no state left, precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:310: Call to builtin memchr
 [eva:alarm] tests/builtins/memchr.c:310: Warning: 
   function memchr: precondition 'valid' got status unknown.
@@ -357,9 +351,9 @@
 [eva] tests/builtins/memchr.c:316: 
   function memchr: precondition 'valid' got status valid.
 [eva:alarm] tests/builtins/memchr.c:316: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
+  function memchr: precondition 'initialization' got status invalid.
 [eva] tests/builtins/memchr.c:316: 
-  function memchr: precondition 'danglingness' got status valid.
+  function memchr: no state left, precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:317: Call to builtin memchr
 [eva] tests/builtins/memchr.c:317: 
   function memchr: precondition 'valid' got status valid.
@@ -370,30 +364,30 @@
 [eva] tests/builtins/memchr.c:317: Frama_C_show_each_mymemchr: {3}
 [eva] tests/builtins/memchr.c:318: assertion got status valid.
 [eva] tests/builtins/memchr.c:319: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:319: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:319: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:319: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:319: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:319: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:319: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:319: Frama_C_show_each_mymemchr: {4}
 [eva] tests/builtins/memchr.c:320: assertion got status valid.
 [eva] tests/builtins/memchr.c:321: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:321: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:321: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:321: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:321: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:321: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:321: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:321: Frama_C_show_each_mymemchr: {5}
 [eva] tests/builtins/memchr.c:322: assertion got status valid.
 [eva] tests/builtins/memchr.c:323: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:323: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:323: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:323: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:323: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:323: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:323: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:323: Frama_C_show_each_mymemchr: {9}
 [eva] tests/builtins/memchr.c:324: assertion got status valid.
 [eva] Recording results for memchr_misc
@@ -423,12 +417,12 @@
 [eva] tests/builtins/memchr.c:336: Frama_C_show_each_mymemchr2: {3; 4}
 [eva] tests/builtins/memchr.c:337: assertion got status valid.
 [eva] tests/builtins/memchr.c:341: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:341: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:341: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:341: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:341: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:341: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:341: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva:alarm] tests/builtins/memchr.c:341: Warning: 
   pointer subtraction. assert \base_addr(_ss_1) ≡ \base_addr(s1);
 [eva] tests/builtins/memchr.c:341: Frama_C_show_each_mymemchr: {3; 4}
@@ -439,6 +433,12 @@
 [eva] tests/builtins/memchr.c:341: Call to builtin memchr
 [eva] tests/builtins/memchr.c:341: Frama_C_show_each_mymemchr: {3; 4}
 [eva] tests/builtins/memchr.c:341: Call to builtin memchr
+[eva:alarm] tests/builtins/memchr.c:341: Warning: 
+  function memchr: precondition 'valid' got status unknown.
+[eva:alarm] tests/builtins/memchr.c:341: Warning: 
+  function memchr: precondition 'initialization' got status unknown.
+[eva:alarm] tests/builtins/memchr.c:341: Warning: 
+  function memchr: precondition 'danglingness' got status unknown.
 [eva] tests/builtins/memchr.c:341: Frama_C_show_each_mymemchr: {3; 4; 7; 8}
 [eva] tests/builtins/memchr.c:348: Call to builtin memchr
 [eva] tests/builtins/memchr.c:348: 
@@ -457,9 +457,9 @@
 [eva] tests/builtins/memchr.c:170: 
   function memchr: precondition 'valid' got status valid.
 [eva:alarm] tests/builtins/memchr.c:170: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
+  function memchr: precondition 'initialization' got status invalid.
 [eva] tests/builtins/memchr.c:170: 
-  function memchr: precondition 'danglingness' got status valid.
+  function memchr: no state left, precondition 'danglingness' got status valid.
 [eva] Recording results for memchr_bitfields
 [eva] Done for function memchr_bitfields
 [eva] computing for function memchr_bitfields2 <- main.
@@ -493,8 +493,8 @@
   function memchr: precondition 'valid' got status valid.
 [eva] tests/builtins/memchr.c:270: 
   function memchr: precondition 'initialization' got status valid.
-[eva:alarm] tests/builtins/memchr.c:270: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:270: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:270: Frama_C_show_each_mymemchr: {0}
 [eva] tests/builtins/memchr.c:271: assertion got status valid.
 [eva] Recording results for memchr_escaping
@@ -662,12 +662,12 @@
 [eva] tests/builtins/memchr.c:431: Frama_C_show_each_mymemchr2: {-1; 3}
 [eva] tests/builtins/memchr.c:432: assertion got status valid.
 [eva] tests/builtins/memchr.c:435: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:435: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:435: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:435: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:435: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:435: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:435: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:435: Frama_C_show_each_mymemchr2: {-1; 3; 7}
 [eva] tests/builtins/memchr.c:436: assertion got status valid.
 [eva] Recording results for memchr_small_sets_n
@@ -821,12 +821,12 @@
 [eva] computing for function memchr_unbounded_n <- main.
   Called from tests/builtins/memchr.c:667.
 [eva] tests/builtins/memchr.c:501: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:501: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:501: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:501: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:501: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:501: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:501: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:501: Frama_C_show_each_mymemchr: {-1; 3}
 [eva] tests/builtins/memchr.c:502: assertion got status valid.
 [eva] tests/builtins/memchr.c:504: Call to builtin memchr
@@ -839,12 +839,12 @@
 [eva] tests/builtins/memchr.c:504: Frama_C_show_each_mymemchr: {-1; 3}
 [eva] tests/builtins/memchr.c:505: assertion got status valid.
 [eva] tests/builtins/memchr.c:507: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:507: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:507: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:507: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:507: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:507: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:507: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:507: Frama_C_show_each_mymemchr: {-1; 3}
 [eva] tests/builtins/memchr.c:508: assertion got status valid.
 [eva] Recording results for memchr_unbounded_n
@@ -1103,12 +1103,12 @@
 [eva] tests/builtins/memchr.c:603: assertion got status valid.
 [eva] tests/builtins/memchr.c:606: Frama_C_show_each_c: {98}
 [eva] tests/builtins/memchr.c:607: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:607: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:607: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:607: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:607: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:607: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:607: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:607: Frama_C_show_each_mymemchr: {1}
 [eva] tests/builtins/memchr.c:607: Call to builtin memchr
 [eva] tests/builtins/memchr.c:607: 
@@ -1200,12 +1200,12 @@
 [eva] tests/builtins/memchr.c:624: assertion got status valid.
 [eva] tests/builtins/memchr.c:627: Frama_C_show_each_c: {98; 99}
 [eva] tests/builtins/memchr.c:628: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:628: Warning: 
-  function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:628: Warning: 
-  function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:628: Warning: 
-  function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:628: 
+  function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:628: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:628: 
+  function memchr: precondition 'danglingness' got status valid.
 [eva] tests/builtins/memchr.c:628: Frama_C_show_each_mymemchr: {1; 2}
 [eva] tests/builtins/memchr.c:628: Call to builtin memchr
 [eva] tests/builtins/memchr.c:628: 
diff --git a/tests/builtins/oracle/str_allocated.res.oracle b/tests/builtins/oracle/str_allocated.res.oracle
index c9803d3d5b662a6663f342a57f79b74c71bd7856..2faad16056db552a1304d5cc5d2c02be6b900c8c 100644
--- a/tests/builtins/oracle/str_allocated.res.oracle
+++ b/tests/builtins/oracle/str_allocated.res.oracle
@@ -19,14 +19,8 @@
 [eva:alarm] tests/builtins/str_allocated.c:14: Warning: 
   accessing uninitialized left-value. assert \initialized(&b);
 [eva] tests/builtins/str_allocated.c:14: Call to builtin memchr
-[eva] share/libc/string.h:69: 
-  Cannot evaluate range bound memchr_off((char *)s, c, n)
-  (unsupported ACSL construct: logic function memchr_off). Approximating
 [eva:alarm] tests/builtins/str_allocated.c:14: Warning: 
   function memchr: precondition 'valid' got status unknown.
-[eva] share/libc/string.h:72: 
-  Cannot evaluate range bound memchr_off((char *)s, c, n)
-  (unsupported ACSL construct: logic function memchr_off). Approximating
 [eva:alarm] tests/builtins/str_allocated.c:14: Warning: 
   function memchr: precondition 'initialization' got status unknown.
 [eva:alarm] tests/builtins/str_allocated.c:14: Warning: 
diff --git a/tests/libc/memchr_off.c b/tests/libc/memchr_off.c
new file mode 100644
index 0000000000000000000000000000000000000000..e29e5d9a9570f082b70d168a55e54885fa921c14
--- /dev/null
+++ b/tests/libc/memchr_off.c
@@ -0,0 +1,21 @@
+#include <string.h>
+#include <wchar.h>
+
+void main() {
+  char *s = "abc";
+  //@ check valid: memchr_off(s, 'a', 3) == 0;
+  //@ check valid: memchr_off(s, 'b', 3) == 1;
+  //@ check not_found: memchr_off(s, 'b', 1) == 0;
+  //@ check valid: memchr_off(s, 'b', 2) == 1;
+  //@ check not_found: memchr_off(s, 'd', 2) == 1;
+  //@ check not_found: memchr_off(s, 'd', 5) == 4;
+  //@ check valid: memchr_off(s+1, 'b', 5) == 0;
+  //@ check zero_length: memchr_off(s, 'a', 0) == -1;
+  char *t = s+1;
+  //@ check valid: memchr_off(&t[-1], 'b', 3) == 1;
+  //@ check not_found: memchr_off(&s[-1], 'a', 3) == 2;
+
+  wchar_t *ws = L"abc";
+  //@ check valid: wmemchr_off(ws, (wchar_t)L'a', 3) == 0;
+  //@ check valid: wmemchr_off(ws, (wchar_t)L'b', 3) == 1;
+}
diff --git a/tests/libc/oracle/memchr_off.res.oracle b/tests/libc/oracle/memchr_off.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4e1fe052835d21ac2820e9168e24eed03eac8586
--- /dev/null
+++ b/tests/libc/oracle/memchr_off.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/libc/memchr_off.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] tests/libc/memchr_off.c:6: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:7: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:8: check 'not_found' got status valid.
+[eva] tests/libc/memchr_off.c:9: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:10: check 'not_found' got status valid.
+[eva] tests/libc/memchr_off.c:11: check 'not_found' got status valid.
+[eva] tests/libc/memchr_off.c:12: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:13: check 'zero_length' got status valid.
+[eva] tests/libc/memchr_off.c:15: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:16: check 'not_found' got status valid.
+[eva] tests/libc/memchr_off.c:19: check 'valid' got status valid.
+[eva] tests/libc/memchr_off.c:20: check 'valid' got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  s ∈ {{ "abc" }}
+  t ∈ {{ "abc" + {1} }}
+  ws ∈ {{ L"abc" }}
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index 8e6c444ee9de224d23eb1b8e1040a87196b79489..bf7be7856c70d4995356619b9b5d331ff8a39e68 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.0.res.oracle
@@ -10,9 +10,6 @@
 [eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
 [eva] tests/libc/wchar_c_h.c:31: 
   function wmemchr: precondition 'valid' got status valid.
-[eva] share/libc/wchar.h:58: 
-  Cannot evaluate range bound wmemchr_off(s, c, n)
-  (unsupported ACSL construct: logic function wmemchr_off). Approximating
 [eva] tests/libc/wchar_c_h.c:31: 
   function wmemchr: precondition 'initialization' got status valid.
 [eva] tests/libc/wchar_c_h.c:31: 
diff --git a/tests/libc/oracle/wchar_c_h.1.res.oracle b/tests/libc/oracle/wchar_c_h.1.res.oracle
index 8a8b446879fbfa8b923ba6416bbab050564219f2..e2ce9fb620744d289469c26659eb948bb6118ae2 100644
--- a/tests/libc/oracle/wchar_c_h.1.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.1.res.oracle
@@ -10,9 +10,6 @@
 [eva] tests/libc/wchar_c_h.c:31: Call to builtin wmemchr
 [eva] tests/libc/wchar_c_h.c:31: 
   function wmemchr: precondition 'valid' got status valid.
-[eva] share/libc/wchar.h:58: 
-  Cannot evaluate range bound wmemchr_off(s, c, n)
-  (unsupported ACSL construct: logic function wmemchr_off). Approximating
 [eva] tests/libc/wchar_c_h.c:31: 
   function wmemchr: precondition 'initialization' got status valid.
 [eva] tests/libc/wchar_c_h.c:31: 
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index 2ffbd071fc836e2895f3dcf5ae60d6a8f06b29ec..bf863d20cc98ba05b724a972dbc48a76447e3120 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -24,20 +24,14 @@
 [eva] tests/libc/wchar_h.c:13: Call to builtin wmemchr
 [eva] tests/libc/wchar_h.c:13: 
   function wmemchr: precondition 'valid' got status valid.
-[eva] share/libc/wchar.h:58: 
-  Cannot evaluate range bound wmemchr_off(s, c, n)
-  (unsupported ACSL construct: logic function wmemchr_off). Approximating
-[eva:alarm] tests/libc/wchar_h.c:13: Warning: 
-  function wmemchr: precondition 'initialization' got status unknown.
+[eva] tests/libc/wchar_h.c:13: 
+  function wmemchr: precondition 'initialization' got status valid.
 [eva] tests/libc/wchar_h.c:13: 
   function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:14: check 'ok' got status valid.
 [eva] tests/libc/wchar_h.c:15: Call to builtin wmemchr
-[eva] share/libc/wchar.h:55: 
-  Cannot evaluate range bound wmemchr_off(s, c, n)
-  (unsupported ACSL construct: logic function wmemchr_off). Approximating
-[eva:alarm] tests/libc/wchar_h.c:15: Warning: 
-  function wmemchr: precondition 'valid' got status unknown.
+[eva] tests/libc/wchar_h.c:15: 
+  function wmemchr: precondition 'valid' got status valid.
 [eva] tests/libc/wchar_h.c:15: 
   function wmemchr: precondition 'initialization' got status valid.
 [eva] tests/libc/wchar_h.c:15: 
@@ -47,40 +41,40 @@
 [eva] tests/libc/wchar_h.c:18: 
   function wmemchr: precondition 'valid' got status valid.
 [eva:alarm] tests/libc/wchar_h.c:18: Warning: 
-  function wmemchr: precondition 'initialization' got status unknown.
+  function wmemchr: precondition 'initialization' got status invalid.
 [eva] tests/libc/wchar_h.c:18: 
-  function wmemchr: precondition 'danglingness' got status valid.
+  function wmemchr: no state left, precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:21: Call to builtin wmemchr
-[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
-  function wmemchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
-  function wmemchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:21: Warning: 
-  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:21: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_h.c:21: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_h.c:21: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:22: check 'ok' got status valid.
 [eva] tests/libc/wchar_h.c:24: Call to builtin wmemchr
-[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
-  function wmemchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
-  function wmemchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:24: Warning: 
-  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:24: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_h.c:24: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_h.c:24: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:25: check 'ok' got status valid.
 [eva] tests/libc/wchar_h.c:26: Call to builtin wmemchr
-[eva:alarm] tests/libc/wchar_h.c:26: Warning: 
-  function wmemchr: precondition 'valid' got status unknown.
+[eva] tests/libc/wchar_h.c:26: 
+  function wmemchr: precondition 'valid' got status valid.
 [eva:alarm] tests/libc/wchar_h.c:26: Warning: 
   function wmemchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:26: Warning: 
-  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:26: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:27: check 'ok' got status valid.
 [eva] tests/libc/wchar_h.c:29: Call to builtin wmemchr
-[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
-  function wmemchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
-  function wmemchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/libc/wchar_h.c:29: Warning: 
-  function wmemchr: precondition 'danglingness' got status unknown.
+[eva] tests/libc/wchar_h.c:29: 
+  function wmemchr: precondition 'valid' got status valid.
+[eva] tests/libc/wchar_h.c:29: 
+  function wmemchr: precondition 'initialization' got status valid.
+[eva] tests/libc/wchar_h.c:29: 
+  function wmemchr: precondition 'danglingness' got status valid.
 [eva] tests/libc/wchar_h.c:30: check 'ok' got status valid.
 [eva] computing for function wcsncpy <- main.
   Called from tests/libc/wchar_h.c:33.