diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 90a70b081ad5d1f6cfe4b9528a9c50647ef4c3f7..63265847a27f0bd79dc3af7c784c4d61f69777b9 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -220,7 +220,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
       end;
       apply_call_results_hooks call init_state (`Reuse i);
       (* call can be cached since it was cached once *)
-      Transfer.{states; cacheable = Cacheable; builtin=false}
+      Transfer.{ states; cacheable = Cacheable; }
 
   (* ----- Body or specification analysis ----------------------------------- *)
 
@@ -273,7 +273,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     if Parameters.ValShowProgress.get () then
       Self.feedback
         "Done for function %a" Kernel_function.pretty call.kf;
-    Transfer.{ states = resulting_states; cacheable; builtin=false }
+    Transfer.{ states = resulting_states; cacheable; }
 
   (* ----- Use of cvalue builtins ------------------------------------------- *)
 
@@ -310,8 +310,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     match final_state with
     | `Bottom ->
       apply_call_results_hooks call state (`Builtin ([], None));
-      let cacheable = Eval.Cacheable in
-      Transfer.{states; cacheable; builtin=true}
+      Transfer.{ states; cacheable = Eval.Cacheable; }
     | `Value final_state ->
       let cvalue_call = get_cvalue_call call in
       let post = get_cvalue_or_top final_state in
@@ -324,7 +323,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
         Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
       in
       let states = List.map insert cvalue_states in
-      Transfer.{states; cacheable; builtin=true}
+      Transfer.{ states; cacheable; }
 
   (* Uses cvalue builtin only if the cvalue domain is available. Otherwise, only
      use the called function specification. *)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 2579ca24f8ae0dd9644b455e45ec8a18232cdb4b..bc4fc022505ea84a9461d0507229715fd5c467fa 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -41,7 +41,6 @@ module type S = sig
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: Eval.cacheable;
-    builtin: bool;
   }
   val compute_call_ref:
     (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
@@ -295,7 +294,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: cacheable;
-    builtin: bool;
   }
 
   (* Forward reference to [Eval_funs.compute_call] *)
@@ -304,8 +302,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
      call_result) ref
     = ref (fun _ -> assert false)
 
-  (* Returns the result of a call, and a boolean that indicates whether a
-     builtin has been used to interpret the call. *)
+  (* Returns the result of a call. *)
   let process_call stmt call recursion valuation state =
     Eva_utils.push_call_stack call.kf stmt;
     let cleanup () =
@@ -323,7 +320,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
           Domain.Store.register_initial_state callstack call.kf state;
           !compute_call_ref stmt call recursion state
         | `Bottom ->
-          { states = []; cacheable = Cacheable; builtin=false }
+          { states = []; cacheable = Cacheable; }
       in
       cleanup ();
       res
@@ -460,12 +457,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     (* Process the call according to the domain decision. *)
     let call_result = process_call stmt call recursion valuation state in
     let leaving_vars = leaving_vars kf_callee in
-    (* Do not try to reduce concrete arguments if a builtin was used. *)
-    let gather_reduced_arguments =
-      if call_result.builtin
-      then fun _ _ _ -> `Value []
-      else gather_reduced_arguments
-    in
     (* Treat each result one by one. *)
     let process state =
       (* Gathers the possible reductions on the value of the concrete arguments
diff --git a/src/plugins/eva/engine/transfer_stmt.mli b/src/plugins/eva/engine/transfer_stmt.mli
index 7da3e2be794787a059471923e14b7d7bdacf7260..8f5c2527e0cc2fce3e143a4bc011bb38df745c80 100644
--- a/src/plugins/eva/engine/transfer_stmt.mli
+++ b/src/plugins/eva/engine/transfer_stmt.mli
@@ -51,7 +51,6 @@ module type S = sig
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: Eval.cacheable;
-    builtin: bool;
   }
 
   val compute_call_ref:
diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml
index aa9227c45553d7d538902228d7a64968d56395e2..2aff52c9bf29e0e89220b727bcada149633d33eb 100644
--- a/src/plugins/eva/legacy/eval_op.ml
+++ b/src/plugins/eva/legacy/eval_op.ml
@@ -128,22 +128,28 @@ let reduce_by_initialized_defined f loc state =
     state
 
 let reduce_by_valid_loc ~positive access loc typ state =
-  let value = Cvalue.Model.find state loc in
-  let loc_bits = Locations.loc_bytes_to_loc_bits value in
+  let value = Cvalue.Model.find_indeterminate state loc in
+  let loc_bytes = Cvalue.V_Or_Uninitialized.get_v value in
+  let loc_bits = Locations.loc_bytes_to_loc_bits loc_bytes in
   let size = Bit_utils.sizeof_pointed typ in
-  let value_as_loc = Locations.make_loc loc_bits size in
+  let location = Locations.make_loc loc_bits size in
+  let reduced_location =
+    if positive
+    then Locations.valid_part access location
+    else Locations.invalid_part location
+  in
+  let reduced_loc_bytes = Locations.loc_to_loc_without_size reduced_location in
   let reduced_value =
-    Locations.loc_to_loc_without_size
-      (if positive
-       then Locations.valid_part access value_as_loc
-       else Locations.invalid_part value_as_loc )
+    if positive
+    then Cvalue.V_Or_Uninitialized.initialized reduced_loc_bytes
+    else Cvalue.V_Or_Uninitialized.map (fun _ -> reduced_loc_bytes) value
   in
-  if V.equal value reduced_value
+  if Cvalue.V_Or_Uninitialized.equal value reduced_value
   then state
   else
-  if V.equal V.bottom reduced_value
+  if Cvalue.V_Or_Uninitialized.(equal bottom reduced_value)
   then Cvalue.Model.bottom
-  else Cvalue.Model.reduce_previous_binding state loc reduced_value
+  else Cvalue.Model.reduce_indeterminate_binding state loc reduced_value
 
 let make_loc_contiguous loc =
   try
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 709c0be21386ffd30db98ada627b86de4ffa5828..ab2f98468fb829b093a001c480cbc0803effebb4 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -534,6 +534,15 @@ let same_etype t1 t2 =
   | TPtr (p1, _), TPtr (p2, _) -> Cil_datatype.Typ.equal p1 p2
   | _, _ -> Cil_datatype.Typ.equal t1 t2
 
+(* Returns the kind of floating-point represented by a logic type, or None. *)
+let logic_type_fkind = function
+  | Ctype typ -> begin
+      match Cil.unrollType typ with
+      | TFloat (fkind, _) -> Some fkind
+      | _ -> None
+    end
+  | _ -> None
+
 let infer_binop_res_type op targ =
   match op with
   | PlusA | MinusA | Mult | Div -> targ
@@ -1864,6 +1873,29 @@ and eval_term_as_exact_locs ~alarm_mode env t =
 (* --- Reduction by predicates                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
+(* Apply [reduce] to the value of location [arg] if it is an exact location. *)
+and reduce_exact_location ~alarm_mode env reduce loc =
+  match eval_term_as_exact_locs ~alarm_mode env loc with
+  | Logic_var logic_var ->
+    let cvalue = LogicVarEnv.find logic_var env.logic_vars in
+    let cvalue = reduce logic_var.lv_type cvalue in
+    if V.is_bottom cvalue then raise Reduce_to_bottom;
+    add_logic_var env logic_var cvalue
+  | Location (typ_loc, locs) ->
+    let aux loc env =
+      let state = env_current_state env in
+      let v = find_or_alarm ~alarm_mode state loc in
+      let v = Cvalue_forward.reinterpret typ_loc v in
+      let v' = reduce (Ctype typ_loc) v in
+      if V.is_bottom v' then raise Reduce_to_bottom;
+      if V.equal v' v then env else
+        let state' = Cvalue.Model.reduce_previous_binding state loc v' in
+        overwrite_current_state env state'
+    in
+    Eval_op.apply_on_all_locs aux locs env
+  | exception Not_an_exact_loc
+  | exception LogicEvalError _ -> env
+
 and reduce_by_valid env positive access (tset: term) =
   let exception DoNotReduce in
   (* Auxiliary function that reduces \valid(lv+offs), where lv is atomic
@@ -1990,49 +2022,49 @@ and reduce_by_valid env positive access (tset: term) =
   in
   do_one env tset
 
+(* Reduces the possible value of [arg] by assuming it points to a valid string
+   (or not if [positive] is false), for reading or writing according to [access].
+   This reduces the possible value of [arg] to a valid pointer (thus only
+   considering the first character of the string), and filters out bases that
+   cannot be a valid string because strlen returns bottom.
+   This reduction could be improved by also reducing offsets according to the
+   position of \0 in the pointed strings. *)
+and reduce_by_valid_string ~alarm_mode env positive ~wide ~access arg =
+  (* First, reduces [arg] assuming it is a valid pointer. *)
+  let env = reduce_by_valid env positive access arg in
+  (* Reduce the cvalue [v]:
+     - if [positive] holds, remove bases which cannot be a valid string
+       as the proper strlen builtin returns bottom;
+     - if [positive] is false, remove bases which are a valid string,
+       as the proper strlen builtin returns no alarm. *)
+  let reduce _typ v =
+    let wrapper =
+      if wide
+      then Builtins_string.frama_c_wcslen_wrapper
+      else Builtins_string.frama_c_strlen_wrapper
+    in
+    let aux base offset acc =
+      let value = Cvalue.V.inject base offset in
+      let v, alarms = apply_logic_builtin wrapper env [value] in
+      (* Beware of not removing const strings on the negation of \valid_string. *)
+      let alarms = alarms || (access = Write && Base.is_read_only base) in
+      if (positive && Cvalue.V.is_bottom v)
+      || (not positive && not alarms)
+      then acc
+      else Cvalue.V.add base offset acc
+    in
+    Cvalue.V.fold_i aux v Cvalue.V.bottom
+  in
+  reduce_exact_location ~alarm_mode env reduce arg
+
 (* reduce [tl] so that [rl rel tr] holds *)
 and reduce_by_left_relation ~alarm_mode env positive tl rel tr =
-  try
-    let debug = false in
-    if debug then Format.printf "#Left term %a@." Printer.pp_term tl;
-    let exact_location = eval_term_as_exact_locs ~alarm_mode env tl in
-    let rtl = eval_term ~alarm_mode env tr in
-    let cond_v = rtl.eover in
-    let comp = Eva_utils.conv_relation rel in
-    match exact_location with
-    | Logic_var logic_var ->
-      let cvalue = LogicVarEnv.find logic_var env.logic_vars in
-      let reduce = Eval_op.backward_comp_left_from_type logic_var.lv_type in
-      let cvalue = reduce positive comp cvalue cond_v in
-      if V.is_bottom cvalue then raise Reduce_to_bottom;
-      add_logic_var env logic_var cvalue
-    | Location (typ_loc, locs) ->
-      let reduce = Eval_op.backward_comp_left_from_type (Ctype typ_loc) in
-      if debug then Format.printf "#Val right term %a@." V.pretty cond_v;
-      let aux loc env =
-        let state = env_current_state env in
-        if debug then Format.printf "#Left term as lv loc %a, typ %a@."
-            Locations.pretty loc Printer.pp_typ typ_loc;
-        let v = find_or_alarm ~alarm_mode state loc in
-        if debug then Format.printf "#Val left lval %a@." V.pretty v;
-        let v = Cvalue_forward.reinterpret typ_loc v in
-        if debug then Format.printf "#Cast left lval %a@." V.pretty v;
-        let v' = reduce positive comp v cond_v in
-        if debug then Format.printf "#Val reduced %a@." V.pretty v';
-        (* TODOBY: if loc is an int that has been silently cast to real, we end
-           up reducing an int according to a float. Instead, we should convert v
-           to  real, then cast back v_asym to the good range *)
-        if V.is_bottom v' then raise Reduce_to_bottom;
-        if V.equal v' v then
-          env
-        else
-          let state' =
-            Cvalue.Model.reduce_previous_binding state loc v'
-          in
-          overwrite_current_state env state'
-      in
-      Eval_op.apply_on_all_locs aux locs env
-  with Not_an_exact_loc | LogicEvalError _ -> env
+  let rtl = eval_term ~alarm_mode env tr in
+  let comp = Eva_utils.conv_relation rel in
+  let reduce typ cvalue =
+    Eval_op.backward_comp_left_from_type typ positive comp cvalue rtl.eover
+  in
+  reduce_exact_location ~alarm_mode env reduce tl
 
 and reduce_by_relation ~alarm_mode env positive t1 rel t2 =
   (* special case: t1 is a term of the form "a rel' b",
@@ -2061,31 +2093,21 @@ and reduce_by_known_papp ~alarm_mode env positive li _labels args =
      reduces its value in [env] by using the backward propagator on fval
      [fval_reduce]. *)
   let reduce_float fval_reduce arg =
-    try
-      match eval_term_as_exact_locs ~alarm_mode env arg with
-      | Logic_var _ -> env
-      | Location (typ_loc, locs) ->
-        let aux loc env =
-          let state = env_current_state env in
-          let v = find_or_alarm ~alarm_mode state loc in
-          let v =  Cvalue_forward.reinterpret typ_loc v in
-          let v = match Cil.unrollType typ_loc with
-            | TFloat (fkind,_) -> begin
-                let v = Cvalue.V.project_float v in
-                let kind = Fval.kind fkind in
-                match fval_reduce kind v with
-                | `Value f -> V.inject_float f
-                | `Bottom -> V.bottom
-              end
-            | _ -> (* Better safe than sorry, we may have e.g. an int location
-                      here *)
-              raise Not_an_exact_loc
-          in
-          let state' = Cvalue.Model.reduce_previous_binding state loc v in
-          overwrite_current_state env state'
-        in
-        Eval_op.apply_on_all_locs aux locs env
-    with Cvalue.V.Not_based_on_null -> env
+    let reduce typ cvalue =
+      match logic_type_fkind typ with
+      | Some fkind -> begin
+          try
+            let v = Cvalue.V.project_float cvalue in
+            let kind = Fval.kind fkind in
+            match fval_reduce kind v with
+            | `Value f -> V.inject_float f
+            | `Bottom -> V.bottom
+          with Cvalue.V.Not_based_on_null -> cvalue
+        end
+      | None -> cvalue (* Better safe than sorry, we may have e.g. an int
+                          location here *)
+    in
+    reduce_exact_location ~alarm_mode env reduce arg
   in
   (* Reduces [f] to positive or negative infinity (according to [pos]),
      or to the complement if [positive] is false. *)
@@ -2121,28 +2143,18 @@ and reduce_by_known_papp ~alarm_mode env positive li _labels args =
     reduce_by_relation ~alarm_mode env positive t1 Rgt t2
   | ("\\ge_float" | "\\ge_double"), [t1;t2] ->
     reduce_by_relation ~alarm_mode env positive t1 Rge t2
-  | "\\subset", [argl;argr] when positive -> begin
-      let alarm_mode = alarm_reduce_mode () in
-      let vr = (eval_term ~alarm_mode env argr).eover in
-      match eval_term_as_exact_locs ~alarm_mode env argl with
-      | Logic_var logic_var ->
-        let vl = LogicVarEnv.find logic_var env.logic_vars in
-        let reduced = Cvalue.V.narrow vl vr in
-        if V.equal V.bottom reduced then raise Reduce_to_bottom;
-        add_logic_var env logic_var reduced
-      | Location (_typ, locsl) ->
-        let aux locl env =
-          let state = env_current_state env in
-          let vl = find_or_alarm ~alarm_mode state locl in
-          let reduced = V.narrow vl vr in
-          if V.equal V.bottom reduced then raise Reduce_to_bottom;
-          let state' =
-            Cvalue.Model.reduce_previous_binding state locl reduced
-          in
-          overwrite_current_state env state'
-        in
-        Eval_op.apply_on_all_locs aux locsl env
-    end
+  | "\\subset", [argl;argr] when positive ->
+    let vr = (eval_term ~alarm_mode env argr).eover in
+    let reduce _typ vl = Cvalue.V.narrow vl vr in
+    reduce_exact_location ~alarm_mode env reduce argl
+  | "valid_read_string", [arg] ->
+    reduce_by_valid_string ~alarm_mode env positive ~wide:false ~access:Read arg
+  | "valid_string", [arg] ->
+    reduce_by_valid_string ~alarm_mode env positive ~wide:false ~access:Write arg
+  | "valid_read_wstring", [arg] ->
+    reduce_by_valid_string ~alarm_mode env positive ~wide:true ~access:Read arg
+  | "valid_wstring", [arg] ->
+    reduce_by_valid_string ~alarm_mode env positive ~wide:true ~access:Write arg
 
   | _ -> (* Do not fail here. We can be asked to reduce on predicates that we
             can evaluate, but on which we are not able to reduce on (yet ?).*)
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 249e874dac1c5ca3971640c3baf12d3db698de8b..28d8bac402b60642a6f46a399abd794616a4f0f9 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -19,7 +19,7 @@
   strchr_misc_static_str ∈ {0}
   strchr_misc_zero_str ∈ {0}
 [eva] computing for function strchr_small_sets <- main.
-  Called from strchr.c:546.
+  Called from strchr.c:548.
 [eva] strchr.c:88: Call to builtin strchr
 [eva] strchr.c:88: 
   function strchr: precondition 'valid_string_s' got status valid.
@@ -50,7 +50,7 @@
 [eva] Recording results for strchr_small_sets
 [eva] Done for function strchr_small_sets
 [eva] computing for function strchr_zero_termination <- main.
-  Called from strchr.c:547.
+  Called from strchr.c:549.
 [eva] strchr.c:113: Call to builtin strchr
 [eva:alarm] strchr.c:113: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
@@ -65,7 +65,7 @@
 [eva] Recording results for strchr_zero_termination
 [eva] Done for function strchr_zero_termination
 [eva] computing for function strchr_initialization <- main.
-  Called from strchr.c:548.
+  Called from strchr.c:550.
 [eva] strchr.c:132: Call to builtin strchr
 [eva:alarm] strchr.c:132: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
@@ -87,7 +87,7 @@
 [eva] Recording results for strchr_initialization
 [eva] Done for function strchr_initialization
 [eva] computing for function strchr_large <- main.
-  Called from strchr.c:549.
+  Called from strchr.c:551.
 [eva] computing for function init_array_nondet <- strchr_large <- main.
   Called from strchr.c:197.
 [eva] strchr.c:189: Call to builtin memset
@@ -158,7 +158,7 @@
 [eva] Recording results for strchr_large
 [eva] Done for function strchr_large
 [eva] computing for function strchr_large_uninit <- main.
-  Called from strchr.c:550.
+  Called from strchr.c:552.
 [eva] computing for function init_array_nondet <- strchr_large_uninit <- main.
   Called from strchr.c:229.
 [eva] strchr.c:189: Call to builtin memset
@@ -205,7 +205,7 @@
 [eva] Recording results for strchr_large_uninit
 [eva] Done for function strchr_large_uninit
 [eva] computing for function strchr_misc_array <- main.
-  Called from strchr.c:551.
+  Called from strchr.c:553.
 [eva] computing for function Frama_C_interval <- strchr_misc_array <- main.
   Called from strchr.c:270.
 [eva] strchr.c:270: 
@@ -221,7 +221,7 @@
 [eva] Recording results for strchr_misc_array
 [eva] Done for function strchr_misc_array
 [eva] computing for function strchr_misc <- main.
-  Called from strchr.c:552.
+  Called from strchr.c:554.
 [eva] strchr.c:301: Call to builtin strchr
 [eva:alarm] strchr.c:301: Warning: 
   function strchr: precondition 'valid_string_s' got status invalid.
@@ -263,7 +263,7 @@
 [eva] Recording results for strchr_misc
 [eva] Done for function strchr_misc
 [eva] computing for function strchr_misc2 <- main.
-  Called from strchr.c:553.
+  Called from strchr.c:555.
 [eva] strchr.c:326: Call to builtin strchr
 [eva] strchr.c:326: 
   function strchr: precondition 'valid_string_s' got status valid.
@@ -300,14 +300,14 @@
 [eva] Recording results for strchr_misc2
 [eva] Done for function strchr_misc2
 [eva] computing for function strchr_bitfields <- main.
-  Called from strchr.c:554.
+  Called from strchr.c:556.
 [eva] strchr.c:166: Call to builtin strchr
 [eva:alarm] strchr.c:166: Warning: 
   function strchr: precondition 'valid_string_s' got status invalid.
 [eva] Recording results for strchr_bitfields
 [eva] Done for function strchr_bitfields
 [eva] computing for function strchr_bitfields2 <- main.
-  Called from strchr.c:555.
+  Called from strchr.c:557.
 [eva] strchr.c:183: Call to builtin strchr
 [eva] strchr.c:183: 
   function strchr: precondition 'valid_string_s' got status valid.
@@ -316,7 +316,7 @@
 [eva] Recording results for strchr_bitfields2
 [eva] Done for function strchr_bitfields2
 [eva] computing for function strchr_escaping <- main.
-  Called from strchr.c:556.
+  Called from strchr.c:558.
 [eva:alarm] strchr.c:258: Warning: 
   pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
 [eva:locals-escaping] strchr.c:258: Warning: 
@@ -334,7 +334,7 @@
 [eva] Recording results for strchr_escaping
 [eva] Done for function strchr_escaping
 [eva] computing for function strchr_big_array <- main.
-  Called from strchr.c:557.
+  Called from strchr.c:559.
 [eva:alarm] strchr.c:353: Warning: out of bounds write. assert \valid(p);
 [eva:alarm] strchr.c:355: Warning: out of bounds write. assert \valid(p);
 [eva:alarm] strchr.c:357: Warning: out of bounds write. assert \valid(p);
@@ -430,7 +430,7 @@
 [eva] Recording results for strchr_big_array
 [eva] Done for function strchr_big_array
 [eva] computing for function strchr_no_zero_but_ok <- main.
-  Called from strchr.c:558.
+  Called from strchr.c:560.
 [eva] strchr.c:422: Call to builtin strchr
 [eva] strchr.c:422: 
   function strchr: precondition 'valid_string_s' got status valid.
@@ -459,7 +459,7 @@
 [eva] Recording results for strchr_no_zero_but_ok
 [eva] Done for function strchr_no_zero_but_ok
 [eva] computing for function strchr_small_sets_chars <- main.
-  Called from strchr.c:559.
+  Called from strchr.c:561.
 [eva] strchr.c:463: Frama_C_show_each_c: {97}
 [eva] strchr.c:464: Call to builtin strchr
 [eva] strchr.c:464: 
@@ -604,7 +604,7 @@
 [eva] Recording results for strchr_small_sets_chars
 [eva] Done for function strchr_small_sets_chars
 [eva] computing for function strchr_unbounded <- main.
-  Called from strchr.c:560.
+  Called from strchr.c:562.
 [eva] strchr.c:519: Call to builtin strchr
 [eva] strchr.c:519: 
   function strchr: precondition 'valid_string_s' got status valid.
@@ -613,60 +613,58 @@
 [eva] strchr.c:524: Call to builtin strchr
 [eva:alarm] strchr.c:524: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
-[eva:alarm] strchr.c:524: Warning: 
-  pointer subtraction. assert \base_addr(_ss_0) ≡ \base_addr(s);
 [eva] strchr.c:524: Frama_C_show_each_mystrchr: [-1..26]
 [eva] strchr.c:525: assertion got status valid.
 [eva] computing for function init_array_nondet <- strchr_unbounded <- main.
-  Called from strchr.c:526.
+  Called from strchr.c:527.
 [eva] strchr.c:189: Call to builtin memset
 [eva] Recording results for init_array_nondet
 [eva] Done for function init_array_nondet
-[eva] strchr.c:527: Call to builtin strchr
-[eva:alarm] strchr.c:527: Warning: 
+[eva] strchr.c:528: Call to builtin strchr
+[eva:alarm] strchr.c:528: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
-[eva:alarm] strchr.c:527: Warning: 
+[eva:alarm] strchr.c:528: Warning: 
   pointer subtraction. assert \base_addr(_ss_1) ≡ \base_addr(s);
-[eva] strchr.c:527: Frama_C_show_each_mystrchr: [-1..29]
-[eva] strchr.c:528: assertion got status valid.
-[eva] strchr.c:529: Call to builtin strchr
-[eva:alarm] strchr.c:529: Warning: 
+[eva] strchr.c:528: Frama_C_show_each_mystrchr: [-1..29]
+[eva] strchr.c:529: assertion got status valid.
+[eva] strchr.c:530: Call to builtin strchr
+[eva:alarm] strchr.c:530: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
-[eva:alarm] strchr.c:529: Warning: 
+[eva:alarm] strchr.c:530: Warning: 
   pointer subtraction. assert \base_addr(_ss_2) ≡ \base_addr(s);
-[eva] strchr.c:529: Frama_C_show_each_mystrchr: [-1..29]
-[eva] strchr.c:530: assertion got status valid.
+[eva] strchr.c:530: Frama_C_show_each_mystrchr: [-1..29]
+[eva] strchr.c:531: assertion got status valid.
 [eva] Recording results for strchr_unbounded
 [eva] Done for function strchr_unbounded
 [eva] computing for function strchr_invalid <- main.
-  Called from strchr.c:561.
-[eva:garbled-mix:write] strchr.c:536: 
+  Called from strchr.c:563.
+[eva:garbled-mix:write] strchr.c:537: 
   Assigning imprecise value to s because of arithmetic operation on addresses.
-[eva] strchr.c:536: Call to builtin strchr
-[eva:alarm] strchr.c:536: Warning: 
+[eva] strchr.c:538: Call to builtin strchr
+[eva:alarm] strchr.c:538: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
-[eva:alarm] strchr.c:536: Warning: 
+[eva:alarm] strchr.c:538: Warning: 
   pointer comparison. assert \pointer_comparable((void *)_ss, (void *)0);
-[eva:alarm] strchr.c:536: Warning: 
+[eva:alarm] strchr.c:538: Warning: 
   pointer subtraction. assert \base_addr(_ss) ≡ \base_addr(s);
-[eva:alarm] strchr.c:536: Warning: 
+[eva:alarm] strchr.c:538: Warning: 
   signed overflow. assert -2147483648 ≤ _ss - s;
-[eva:alarm] strchr.c:536: Warning: 
+[eva:alarm] strchr.c:538: Warning: 
   signed overflow. assert _ss - s ≤ 2147483647;
-[eva] strchr.c:536: Frama_C_show_each_mystrchr: [-2147483648..2147483647]
+[eva] strchr.c:538: Frama_C_show_each_mystrchr: [-2147483648..2147483647]
 [eva] Recording results for strchr_invalid
 [eva] Done for function strchr_invalid
 [eva] computing for function strchr_garbled_mix_in_char <- main.
-  Called from strchr.c:562.
-[eva:alarm] strchr.c:541: Warning: 
+  Called from strchr.c:564.
+[eva:alarm] strchr.c:543: Warning: 
   pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
-[eva:garbled-mix:write] strchr.c:541: 
+[eva:garbled-mix:write] strchr.c:543: 
   Assigning imprecise value to garbled
   because of arithmetic operation on addresses.
-[eva:alarm] strchr.c:542: Warning: 
+[eva:alarm] strchr.c:544: Warning: 
   pointer downcast. assert (unsigned int)garbled ≤ 2147483647;
-[eva] strchr.c:542: Call to builtin strchr
-[eva:alarm] strchr.c:542: Warning: 
+[eva] strchr.c:544: Call to builtin strchr
+[eva:alarm] strchr.c:544: Warning: 
   function strchr: precondition 'valid_string_s' got status invalid.
 [eva] Recording results for strchr_garbled_mix_in_char
 [eva] Done for function strchr_garbled_mix_in_char
@@ -674,7 +672,10 @@
 [eva] Done for function main
 [eva:garbled-mix:summary] 
   Origins of garbled mix generated during analysis:
-    strchr.c:541: arithmetic operation on addresses
+    strchr.c:537: arithmetic operation on addresses
+      (read in 1 statement, propagated through 2 statements)
+      garbled mix of &{s; "hello"}
+    strchr.c:543: arithmetic operation on addresses
       (read in 1 statement, propagated through 2 statements)
       garbled mix of &{x}
 [eva] ====== VALUES COMPUTED ======
@@ -725,7 +726,7 @@
   z1 ∈ {0}
   z2 ∈ {0}
 [eva:final-states] Values at end of function strchr_garbled_mix_in_char:
-  garbled ∈ {{ garbled mix of &{x} (origin: Arithmetic {strchr.c:541}) }}
+  garbled ∈ {{ garbled mix of &{x} (origin: Arithmetic {strchr.c:543}) }}
 [eva:final-states] Values at end of function strchr_initialization:
   c ∈ {0}
   empty_or_uninitialized[0] ∈ {0} or UNINITIALIZED
@@ -738,7 +739,7 @@
    [3] ∈ {0}
   z3 ∈ {3}
 [eva:final-states] Values at end of function strchr_invalid:
-  s ∈ {{ "hello" }}
+  s ∈ {{ &s + {0; 1; 2; 3} ; "hello" + {0; 1; 2; 3; 4; 5} }}
   unused ∈ [--..--]
 [eva:final-states] Values at end of function strchr_large:
   Frama_C_entropy_source ∈ [--..--]
diff --git a/tests/builtins/oracle/strlen.res.oracle b/tests/builtins/oracle/strlen.res.oracle
index f49d683946a6cf103a2072184addcef1a23c12ac..1998d07eb2c5d4eb738d3b6dcb21612791eb8072 100644
--- a/tests/builtins/oracle/strlen.res.oracle
+++ b/tests/builtins/oracle/strlen.res.oracle
@@ -448,7 +448,7 @@
   offset4 ∈ {-1; 0; 1; 2}
   offset5 ∈ [-4..7]
   offset6 ∈ [-10..0]
-  p ∈ {{ &buf + [-10..0] }}
+  p ∈ {{ &buf[0] }}
 [eva:final-states] Values at end of function small_sets:
   s ∈ {{ "b\000c" }}
   p ∈ {{ "b\000c" + {0; 2} }}
diff --git a/tests/builtins/oracle/strnlen2.res.oracle b/tests/builtins/oracle/strnlen2.res.oracle
index d1ba49e93a3362c939bade35aabd93d5bba47741..f554968beef79c411e521f9b290838822ce89bd9 100644
--- a/tests/builtins/oracle/strnlen2.res.oracle
+++ b/tests/builtins/oracle/strnlen2.res.oracle
@@ -877,7 +877,7 @@
   offset4 ∈ {-1; 0; 1; 2}
   offset5 ∈ [-4..7]
   offset6 ∈ [-10..0]
-  p ∈ {{ &buf + [-10..0] }}
+  p ∈ {{ &buf[0] }}
 [eva:final-states] Values at end of function no_zero_but_ok:
   s[0..9] ∈ {1}
    [10] ∈ {0}
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index 5130d9010d0b11eb4e84fba4d4577525b1b1f8d9..a5de0cd779733ac1419fd06657318b8832524640 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -478,8 +478,7 @@
             [1] ∈ {0}
 [eva:final-states] Values at end of function negative_offsets:
   Frama_C_entropy_source ∈ [--..--]
-  buf[0..88] ∈ {65} or UNINITIALIZED
-     [89..98] ∈ {0; 65} or UNINITIALIZED
+  buf[0..98] ∈ {65} or UNINITIALIZED
      [99] ∈ {0}
   len1 ∈ UNINITIALIZED
   len2 ∈ UNINITIALIZED
@@ -491,7 +490,7 @@
   offset4 ∈ {-1; 0; 1; 2}
   offset5 ∈ [-4..7]
   offset6 ∈ [-10..0]
-  p ∈ {{ &buf + [-40..0],0%4 }}
+  p ∈ {{ &buf[0] }}
 [eva:final-states] Values at end of function small_sets:
   s ∈ {{ L"b\000c" }}
   p ∈ {{ L"b\000c" + {0; 8} }}
diff --git a/tests/builtins/strchr.c b/tests/builtins/strchr.c
index e3678b241247fc7dbf44ea6e501954fd6267c6fe..7ec4541e850070efd2827d198103ff66c4ec2a30 100644
--- a/tests/builtins/strchr.c
+++ b/tests/builtins/strchr.c
@@ -29,7 +29,7 @@ typedef int RES;
 #define STRING(var,str) var = str;
 
 #define TSZ 12
-const char* tab_str[TSZ] = 
+const char* tab_str[TSZ] =
   {
     "" , // 0
     "a", // 1
@@ -523,6 +523,7 @@ void strchr_unbounded() {
   IF_NONDET(s, t);
   STRCHR(RES, u2, s, 0, c); // alarm
   //@ assert (u2 >= -1 && u2 <= 26); // alarm
+  IF_NONDET(s, t);
   init_array_nondet(t, 0, 29, 0, 1);
   STRCHR(RES, u3, s, 0, c); // alarm
   //@ assert (u3 >= -1 && u3 <= 29); // alarm
@@ -533,7 +534,8 @@ void strchr_unbounded() {
 void strchr_invalid() {
   CHAR_PTR(s);
   STRING(s,"hello");
-  STRCHR(RES, unused, s, (unsigned int)&s, 1); // alarm
+  s = (char *)(s + (unsigned int)(&s));
+  STRCHR(RES, unused, s, 0, 1); // alarm
 }
 
 void strchr_garbled_mix_in_char() {
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
index a5a008b319c574be7132f331a72745112c3825e5..9e5405c1b5985d48f0095eaa36feacc6be89081d 100644
--- a/tests/libc/oracle/libgen_h.res.oracle
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -42,7 +42,7 @@
   __fc_dirname[0..4095] ∈ [--..--]
   path[0..127] ∈ [--..--]
   base ∈ {{ &__fc_basename[0] ; &path[0] }}
-  base2 ∈ {{ NULL ; &__fc_basename[0] }}
+  base2 ∈ {{ &__fc_basename[0] }}
   dir ∈ {{ &__fc_dirname[0] ; &path[0] }}
-  dir2 ∈ {{ NULL ; &__fc_dirname[0] }}
+  dir2 ∈ {{ &__fc_dirname[0] }}
   __retres ∈ {0}
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index d22196b6d84b637203ec7233e78108ac2cca333b..1f2d4bb2994253ac4ad94e7074c908d114de2f4a 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -163,8 +163,6 @@
 [eva:alarm] FRAMAC_SHARE/libc/stdlib.c:137: Warning: 
   function strchr: precondition 'valid_string_s' got status unknown.
 [eva] FRAMAC_SHARE/libc/stdlib.c:141: Call to builtin strlen
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.c:141: Warning: 
-  function strlen: precondition 'valid_string_s' got status unknown.
 [eva] FRAMAC_SHARE/libc/stdlib.c:147: 
   Reusing old results for call to __fc_initenv
 [eva] computing for function Frama_C_nondet <- setenv <- main.
@@ -237,11 +235,7 @@
 [eva] computing for function unsetenv <- main.
   Called from stdlib_c_env.c:24.
 [eva] FRAMAC_SHARE/libc/stdlib.c:167: Call to builtin strchr
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.c:167: Warning: 
-  function strchr: precondition 'valid_string_s' got status unknown.
 [eva] FRAMAC_SHARE/libc/stdlib.c:171: Call to builtin strlen
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.c:171: Warning: 
-  function strlen: precondition 'valid_string_s' got status unknown.
 [eva] FRAMAC_SHARE/libc/stdlib.c:177: 
   Reusing old results for call to __fc_initenv
 [eva] computing for function Frama_C_nondet <- unsetenv <- main.
@@ -311,7 +305,7 @@
    [8..9] ∈ {0}
   i2 ∈ [--..--]
   r1 ∈ {{ NULL ; &s[0] ; &__fc_env_strings + [0..63] ; "BLA=1" }}
-  r2 ∈ {{ NULL ; &s[0] ; &__fc_env_strings + [0..63] ; "BLA=1" }}
+  r2 ∈ {{ &s[0] ; &__fc_env_strings + [0..63] ; "BLA=1" }}
   i3 ∈ {-1; 0}
   i4 ∈ {-1; 0}
   i5 ∈ {-1; 0}
diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle
index 1779ee8c716488fdc0f783559066655c68cc23c9..a4bafca7fceaafd44e41fd0fcfcc599a2f6c42ec 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -230,7 +230,7 @@
 [eva:final-states] Values at end of function main5:
   q ∈ {{ &y }}
   p ∈ {0}
-  r ∈ {{ &y }} or UNINITIALIZED
+  r ∈ {{ &y }}
 [eva:final-states] Values at end of function main6:
   S_f1_0_S_vs[0] ∈ {1}
              [1] ∈ [--..--]
diff --git a/tests/value/oracle/strings_logic.res.oracle b/tests/value/oracle/strings_logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..08a758fed244f805e53df4fe7897c68e1b5686bc
--- /dev/null
+++ b/tests/value/oracle/strings_logic.res.oracle
@@ -0,0 +1,282 @@
+[kernel] Parsing strings_logic.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
+  nondet ∈ [--..--]
+[eva] computing for function reduce_by_valid_string <- main.
+  Called from strings_logic.c:209.
+[eva:loop-unroll:auto] strings_logic.c:30: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:36: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:41: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:48: Automatic loop unrolling.
+[eva:loop-unroll:auto] strings_logic.c:53: Automatic loop unrolling.
+[eva:alarm] strings_logic.c:84: Warning: assertion got status unknown.
+[eva] strings_logic.c:85: 
+  Frama_C_show_each_valid_string_zero_offset:
+  {{ &s1 ; &s2 ; &s_zero ; &s_partially_valid ; &s_imprecise ; &s_unknown ;
+     &anything }}
+[eva:alarm] strings_logic.c:89: Warning: assertion got status unknown.
+[eva] strings_logic.c:90: 
+  Frama_C_show_each_valid_read_string_zero_offset:
+  {{ &s1 ; &s2 ; &s_const ; &s_zero ; &s_partially_valid ; &s_imprecise ;
+     &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:94: Warning: assertion got status unknown.
+[eva] strings_logic.c:95: 
+  Frama_C_show_each_invalid_string_zero_offset:
+  {{ NULL ; &s_const ; &s_uninit ; &s_partially_initialized ; &s_imprecise ;
+     &s_unknown ; &anything ; "hello\000 world" ; "hello world" }}
+[eva:alarm] strings_logic.c:99: Warning: assertion got status unknown.
+[eva] strings_logic.c:100: 
+  Frama_C_show_each_invalid_read_string_zero_offset:
+  {{ NULL ; &s_uninit ; &s_partially_initialized ; &s_imprecise ; &s_unknown ;
+     &anything }}
+[eva:alarm] strings_logic.c:108: Warning: assertion got status unknown.
+[eva] strings_logic.c:109: 
+  Frama_C_show_each_valid_string_precise_offset:
+  {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_zero + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10} }}
+[eva:alarm] strings_logic.c:113: Warning: assertion got status unknown.
+[eva] strings_logic.c:114: 
+  Frama_C_show_each_valid_read_string_precise_offset:
+  {{ &s1 + {5; 10} ; &s2 + {5; 10} ; &s_const + {5; 10} ;
+     &s_zero + {5; 10; 20} ; &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10} ;
+     "hello\000 world" + {5; 10} ; "hello world" + {5; 10} }}
+[eva:alarm] strings_logic.c:118: Warning: assertion got status unknown.
+[eva] strings_logic.c:119: 
+  Frama_C_show_each_invalid_string_precise_offset:
+  {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+     &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+     "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:123: Warning: assertion got status unknown.
+[eva] strings_logic.c:124: 
+  Frama_C_show_each_invalid_read_string_precise_offset:
+  {{ NULL + {5; 10; 20} ; &s1 + {5; 10; 20} ; &s2 + {5; 10; 20} ;
+     &s_const + {5; 10; 20} ; &s_uninit + {5; 10; 20} ;
+     &s_partially_initialized + {5; 10; 20} ;
+     &s_partially_valid + {5; 10; 20} ; &s_imprecise + {5; 10; 20} ;
+     &s_unknown + {5; 10; 20} ; &anything + {5; 10; 20} ;
+     "hello\000 world" + {5; 10; 20} ; "hello world" + {5; 10; 20} }}
+[eva:alarm] strings_logic.c:131: Warning: assertion got status unknown.
+[eva] strings_logic.c:132: 
+  Frama_C_show_each_valid_string_imprecise_offset:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:136: Warning: assertion got status unknown.
+[eva] strings_logic.c:137: 
+  Frama_C_show_each_valid_read_string_imprecise_offset:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+     "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:141: Warning: assertion got status unknown.
+[eva] strings_logic.c:142: 
+  Frama_C_show_each_invalid_string_imprecise_offset:
+  {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+     &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+     &s_partially_initialized + [-123..147] ;
+     &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+     &s_unknown + [-123..147] ; &anything + [-123..147] ;
+     "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva:alarm] strings_logic.c:146: Warning: assertion got status unknown.
+[eva] strings_logic.c:147: 
+  Frama_C_show_each_invalid_read_string_imprecise_offset:
+  {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+     &s_const + [-123..147] ; &s_zero + [-123..147] ; &s_uninit + [-123..147] ;
+     &s_partially_initialized + [-123..147] ;
+     &s_partially_valid + [-123..147] ; &s_imprecise + [-123..147] ;
+     &s_unknown + [-123..147] ; &anything + [-123..147] ;
+     "hello\000 world" + [-123..147] ; "hello world" + [-123..147] }}
+[eva] computing for function garbled_mix <- reduce_by_valid_string <- main.
+  Called from strings_logic.c:151.
+[eva] using specification for function garbled_mix
+[eva:garbled-mix:assigns] strings_logic.c:151: 
+  The specification of function garbled_mix
+  has generated a garbled mix of addresses for assigns clause \result.
+[eva] Done for function garbled_mix
+[eva:alarm] strings_logic.c:154: Warning: assertion got status unknown.
+[eva] strings_logic.c:155: 
+  Frama_C_show_each_valid_string_garbled_mix:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] }}
+[eva:alarm] strings_logic.c:159: Warning: assertion got status unknown.
+[eva] strings_logic.c:160: 
+  Frama_C_show_each_valid_read_string_garbled_mix:
+  {{ &s1 + [0..13] ; &s2 + [0..12] ; &s_const + [0..16] ; &s_zero + [0..31] ;
+     &s_partially_initialized + [0..31] ; &s_partially_valid + [0..31] ;
+     &s_imprecise + [0..31] ; &s_unknown + [0..31] ; &anything + [0..15] ;
+     "hello\000 world" + [0..12] ; "hello world" + [0..11] }}
+[eva:alarm] strings_logic.c:164: Warning: assertion got status unknown.
+[eva] strings_logic.c:165: 
+  Frama_C_show_each_invalid_string_garbled_mix:
+  {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                      s_partially_initialized; s_partially_valid; s_imprecise;
+                      s_unknown; anything; "hello\000 world"; "hello world"}
+  (origin: Library function {strings_logic.c:151}) }}
+[eva:alarm] strings_logic.c:169: Warning: assertion got status unknown.
+[eva] strings_logic.c:170: 
+  Frama_C_show_each_invalid_read_string_garbled_mix:
+  {{ garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                      s_partially_initialized; s_partially_valid; s_imprecise;
+                      s_unknown; anything; "hello\000 world"; "hello world"}
+  (origin: Library function {strings_logic.c:151}) }}
+[eva] Recording results for reduce_by_valid_string
+[eva] Done for function reduce_by_valid_string
+[eva] computing for function reduce_by_valid_wstring <- main.
+  Called from strings_logic.c:210.
+[eva:alarm] strings_logic.c:193: Warning: assertion got status unknown.
+[eva] strings_logic.c:194: 
+  Frama_C_show_each_wide_string_valid_wstring: {{ &ws1 ; &ws_zero }}
+[eva:alarm] strings_logic.c:198: Warning: assertion got status unknown.
+[eva] strings_logic.c:199: 
+  Frama_C_show_each_wide_string_valid_read_wstring:
+  {{ &ws1 ; &ws_zero ; L"Wide literal" }}
+[eva:alarm] strings_logic.c:203: Warning: assertion got status unknown.
+[eva] strings_logic.c:204: 
+  Frama_C_show_each_wide_string_invalid_read_wstring:
+  {{ &ws1 ; &ws_zero ; &wchar ; &ws_with_hole ; L"Wide literal" }}
+[eva] Recording results for reduce_by_valid_wstring
+[eva] Done for function reduce_by_valid_wstring
+[eva] Recording results for main
+[eva] Done for function main
+[eva:garbled-mix:summary] 
+  Origins of garbled mix generated during analysis:
+    strings_logic.c:151: assigns clause on addresses
+      (read in 2 statements, propagated through 1 statement)
+      garbled mix of &{s1; s2; s_const; s_zero; s_uninit;
+                       s_partially_initialized; s_partially_valid; s_imprecise;
+                       s_unknown; anything; "hello\000 world"; "hello world"}
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function reduce_by_valid_string:
+  s1[0] ∈ {104}
+    [1] ∈ {101}
+    [2..3] ∈ {108}
+    [4] ∈ {111}
+    [5] ∈ {0}
+    [6] ∈ {32}
+    [7] ∈ {119}
+    [8] ∈ {111}
+    [9] ∈ {114}
+    [10] ∈ {108}
+    [11] ∈ {100}
+    [12] ∈ {33}
+    [13] ∈ {0}
+  s2[0] ∈ {104}
+    [1] ∈ {101}
+    [2..3] ∈ {108}
+    [4] ∈ {111}
+    [5] ∈ {32}
+    [6] ∈ {119}
+    [7] ∈ {111}
+    [8] ∈ {114}
+    [9] ∈ {108}
+    [10] ∈ {100}
+    [11] ∈ {33}
+    [12] ∈ {0}
+  s_const[0] ∈ {99}
+         [1] ∈ {111}
+         [2] ∈ {110}
+         [3] ∈ {115}
+         [4] ∈ {116}
+         [5] ∈ {32}
+         [6] ∈ {99}
+         [7] ∈ {104}
+         [8] ∈ {97}
+         [9] ∈ {114}
+         [10] ∈ {32}
+         [11] ∈ {97}
+         [12..13] ∈ {114}
+         [14] ∈ {97}
+         [15] ∈ {121}
+         [16] ∈ {0}
+  s_zero[0..31] ∈ {0}
+  s_partially_initialized[0..9] ∈ UNINITIALIZED
+                         [10..24] ∈ {105}
+                         [25] ∈ {0}
+                         [26..31] ∈ UNINITIALIZED
+  s_invalid[0..31] ∈ {97}
+  s_partially_valid[0..7] ∈ {111}
+                   [8] ∈ {0}
+                   [9..15] ∈ {111}
+                   [16] ∈ {0}
+                   [17..31] ∈ {111}
+  s_imprecise[0..31] ∈ [--..--]
+  s_unknown[0..31] ∈ [--..--] or UNINITIALIZED
+  anything.ptr ∈ {{ &x }}
+          .d ∈ [-128. .. 127.]
+          .c ∈ [--..--]
+          .[bits 104 to 127] ∈ UNINITIALIZED
+  p ∈ {0}
+  offset ∈ {5; 10; 20}
+[eva:final-states] Values at end of function reduce_by_valid_wstring:
+  ws1[0] ∈ {104}
+     [1] ∈ {101}
+     [2..3] ∈ {108}
+     [4] ∈ {111}
+     [5] ∈ {0}
+     [6] ∈ {32}
+     [7] ∈ {119}
+     [8] ∈ {105}
+     [9] ∈ {100}
+     [10] ∈ {101}
+     [11] ∈ {32}
+     [12] ∈ {119}
+     [13] ∈ {111}
+     [14] ∈ {114}
+     [15] ∈ {108}
+     [16] ∈ {100}
+     [17] ∈ {33}
+     [18] ∈ {0}
+  ws_zero[0..31] ∈ {0}
+  wchar ∈ {90}
+  ws_with_hole[0][bits 0 to 7]# ∈ {104}%32, bits 0 to 7 
+              [0][bits 8 to 15] ∈ {0}
+              [0][bits 16 to 31]# ∈ {104}%32, bits 16 to 31 
+              [1] ∈ {105}
+  wp ∈
+    {{ &ws1[0] ; &ws_zero[0] ; &wchar ; &ws_with_hole[0] ; L"Wide literal" }} or UNINITIALIZED
+[eva:final-states] Values at end of function main:
+  
+[from] Computing for function reduce_by_valid_string
+[from] Computing for function garbled_mix <-reduce_by_valid_string
+[from] Done for function garbled_mix
+[from] Done for function reduce_by_valid_string
+[from] Computing for function reduce_by_valid_wstring
+[from] Done for function reduce_by_valid_wstring
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function garbled_mix:
+  \result FROM p
+[from] Function reduce_by_valid_string:
+  NO EFFECTS
+[from] Function reduce_by_valid_wstring:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function reduce_by_valid_string:
+    s1[0..13]; s2[0..12]; s_const[0..16]; s_zero[0..31];
+    s_partially_initialized[10..25]; i; s_invalid[0..31]; i_0;
+    s_partially_valid[0..31]; i_1; s_imprecise[0..31]; i_2; s_unknown[0..31];
+    i_3; anything{.ptr; .d; .c}; p; offset; tmp; tmp_0
+[inout] Inputs for function reduce_by_valid_string:
+    nondet
+[inout] Out (internal) for function reduce_by_valid_wstring:
+    ws1[0..18]; ws_zero[0..31]; wchar; ws_with_hole[0..1]; wp
+[inout] Inputs for function reduce_by_valid_wstring:
+    nondet
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    nondet
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 78f84b5adc28a23ea09391128d089ce0c39e5da7..022406b2a822fbd89d2cb53235062f9a3296e260 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -61,9 +61,6 @@
   locals {z} escaping the scope of a block of alarms through p
 [eva:alarm] summary.i:45: Warning: 
   assertion 'rte,mem_access' got status unknown.
-[eva:alarm] summary.i:45: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&p);
 [eva] Recording results for alarms
 [eva] Done for function alarms
 [eva] computing for function logic <- main.
@@ -111,7 +108,7 @@
     by the Eva analyzer:      0 errors    1 warning
     by the Frama-C kernel:    0 errors    3 warnings
   ----------------------------------------------------------------------------
-  18 alarms generated by the analysis:
+  17 alarms generated by the analysis:
        3 invalid memory accesses
        3 integer overflows
        2 accesses out of bounds index
@@ -119,7 +116,6 @@
        2 nan or infinite floating-point values
        2 illegal conversions from floating-point to integer
        1 division by zero
-       1 escaping address
        2 others
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis:
diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ed8b014f3c938746a7a7790d93d56af817eedd62
--- /dev/null
+++ b/tests/value/oracle_multidim/strings_logic.res.oracle
@@ -0,0 +1,8 @@
+83c83
+<   {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+>   {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+92c92
+<   {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
+---
+>   {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
diff --git a/tests/value/strings_logic.c b/tests/value/strings_logic.c
new file mode 100644
index 0000000000000000000000000000000000000000..d0f2e58ffffcd1b7d5070f22c273565c7d0fe1ad
--- /dev/null
+++ b/tests/value/strings_logic.c
@@ -0,0 +1,211 @@
+/* run.config*
+   STDOPT: +"-eva-auto-loop-unroll 32"
+*/
+
+/* Tests the evaluation and reduction by ACSL predicate on strings. */
+
+#include "__fc_string_axiomatic.h"
+#include "wchar.h"
+volatile char nondet;
+
+struct anything {
+  int *ptr;
+  double d;
+  char c;
+};
+
+/*@ assigns \result \from p; */
+char* garbled_mix(char *p);
+
+/* Tests the reduction by ACSL predicate "valid_string" and "valid_read_string"
+   from the Frama-C libc. */
+void reduce_by_valid_string (void) {
+  char s1[] = "hello\000 world!";
+  char s2[] = "hello world!";
+  const char s_const[] = "const char array";
+  char s_zero[32] = {0};
+  char s_uninit[32];
+
+  char s_partially_initialized[32]; // valid only between 10 and 25.
+  for (int i = 10; i < 25; i++) {
+    s_partially_initialized[i] = 'i';
+  }
+  s_partially_initialized[25] = '\0';
+
+  char s_invalid[32]; // Invalid as no terminating \0
+  for (int i = 0; i < 32; i++){
+    s_invalid[i] = 'a';
+  }
+
+  char s_partially_valid[32]; // valid up to offset 16.
+  for (int i = 0; i < 32; i++){
+    s_partially_valid[i] = 'o';
+  }
+  s_partially_valid[8] = '\0';
+  s_partially_valid[16] = '\0';
+
+  char s_imprecise[32]; // char array of imprecise values
+  for (int i = 0; i < 32; i++){
+    s_imprecise[i] = nondet;
+  }
+
+  char s_unknown[32]; // char array of imprecise values that may be uninitialized
+  for (int i = 0; i < 32; i++) {
+    if (nondet) s_unknown[i] = nondet;
+  }
+
+  int x;
+  struct anything anything;
+  anything.ptr = &x;
+  anything.d = (double)nondet;
+  anything.c = nondet;
+
+  // Pointer p that can point to any of the strings above.
+  char *p;
+  switch (nondet) {
+    case 0: p = "hello\000 world"; break;
+    case 1: p = "hello world"; break;
+    case 2: p = s1; break;
+    case 3: p = s2; break;
+    case 4: p = s_const; break;
+    case 5: p = s_zero; break;
+    case 6: p = s_uninit; break;
+    case 7: p = s_partially_initialized; break;
+    case 8: p = s_partially_valid; break;
+    case 9: p = s_imprecise; break;
+    case 10: p = s_unknown; break;
+    case 11: p = (char *)&anything; break;
+    default: p = NULL;
+  }
+
+  // Test with a zero offset for all bases.
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_zero_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_zero_offset(p);
+  }
+
+  // Test with a precise non-zero non-singleton offset.
+  int offset = nondet ? 5 : (nondet ? 10 : 20);
+  p = p + offset;
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_precise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_precise_offset(p);
+  }
+
+  // Test with a very imprecise offset.
+  p = p + nondet;
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_imprecise_offset(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_imprecise_offset(p);
+  }
+
+  // Test with a garbled mix.
+  p = garbled_mix(p);
+
+  if (nondet) {
+    //@ assert valid_string(p);
+    Frama_C_show_each_valid_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_string(p);
+    Frama_C_show_each_valid_read_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_string(p);
+    Frama_C_show_each_invalid_string_garbled_mix(p);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_string(p);
+    Frama_C_show_each_invalid_read_string_garbled_mix(p);
+  }
+
+  p = NULL;
+}
+
+void reduce_by_valid_wstring (void) {
+  wchar_t ws1[] = L"hello\000 wide world!";
+  wchar_t ws_zero[32] = {0};
+  wchar_t wchar = L'Z';
+  wchar_t ws_with_hole[2] = L"hi"; // no space for L'\0'!
+  ((char*)ws_with_hole)[1] = '\0'; // valid string but not valid wide string
+
+  wchar_t *wp;
+  switch (nondet) {
+    case 0: wp = ws1; break;
+    case 1: wp = L"Wide literal"; break;
+    case 2: wp = ws_zero; break;
+    case 3: wp = &wchar; break;
+    case 4: wp = ws_with_hole; break;
+  }
+
+  if (nondet) {
+    //@ assert valid_wstring(wp);
+    Frama_C_show_each_wide_string_valid_wstring(wp);
+  }
+
+  if (nondet) {
+    //@ assert valid_read_wstring(wp);
+    Frama_C_show_each_wide_string_valid_read_wstring(wp);
+  }
+
+  if (nondet) {
+    //@ assert !valid_read_wstring(wp);
+    Frama_C_show_each_wide_string_invalid_read_wstring(wp);
+  }
+}
+
+void main (void) {
+  reduce_by_valid_string();
+  reduce_by_valid_wstring();
+}