diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 441dadd082b596b5059a305cb6267f5b8af6d54b..2e3e91305da4f48e33281e7d1dc0e01a3ca700ba 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -681,7 +681,8 @@ end
 = struct
 
   let process_quantif ~loc p =
-    Current_loc.set loc;
+    let open Current_loc.Operators in
+    let<> UpdatedCurrentLoc = loc in
     match p.pred_content with
     | Pforall(bound_vars, ({ pred_content = Pimplies(_, _) } as goal)) ->
       compute_guards loc ~is_forall:true p bound_vars goal
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index c9dafda541ae474b21073ae00cb76149f677be75..8c0478348ff40a11be1f1b57d865818f56d47980 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -782,7 +782,8 @@ let consolidated_must_monitor_vi vi =
 let concurrent_function_ref = ref None
 
 let abort_because_of_concurrent ~loc vi =
-  Current_loc.set loc;
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = loc in
   Options.abort
     ~current:true
     "Found concurrent function %a and monitored memory properties.\n\
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 4d660be4b00bc720ce11e1207c50203195dca545..df3fa3c6b4b174cf5ed97640890c39c9cfc0260f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -340,6 +340,8 @@ let rec type_term
     ~profile
     t =
   Options.feedback ~dkey ~level:5 "typing (sub-)term %a" Printer.pp_term t;
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = t.term_loc in
   let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
   let compute_ctx ?ctx i =
     (* in order to get a minimal amount of generated casts for operators, the
@@ -355,7 +357,6 @@ let rec type_term
       mk_ctx ~use_gmp_opt:true (ty_of_interv i)
   in
   let infer t =
-    Current_loc.set t.term_loc;
     (* this pattern matching implements the formal rules of the JFLA's paper
        (and of course also covers the missing cases). Also enforce the invariant
        that every subterm is typed, even if it is not an integer. *)
@@ -771,7 +772,8 @@ and type_predicate ~profile p =
     do_both f g = (try f() with e -> try g(); raise e with | _ -> raise e); g()
   in
   let p = Logic_normalizer.get_pred p in
-  Current_loc.set p.pred_loc;
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = p.pred_loc in
   (* this pattern matching also follows the formal rules of the JFLA's paper *)
   match p.pred_content with
   | Pfalse | Ptrue -> ()
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 8ad48d0909a36ec4a3712a8fd27b60e1a5b029e4..e3e881fbe292e96713d6e6673cd49c2862d073df 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -22,6 +22,7 @@
 
 open Cil_types
 open Contract_types
+open Current_loc.Operators
 module Error = Translation_error
 
 (**************************************************************************)
@@ -243,7 +244,7 @@ let setup_assumes kf env contract =
           else
             let assumes = assumes_predicate env b.b_assumes in
             let loc = assumes.pred_loc in
-            Current_loc.set loc;
+            let<> UpdatedCurrentLoc = loc in
             let idx = get_bhvr_idx contract b.b_name in
             Rtl_call.set_assumes ~loc env kf contract_e idx assumes
         with exn ->
@@ -320,8 +321,7 @@ let check_default_requires kf env contract =
          if Translate_utils.must_translate
              (Property.ip_of_requires kf kinstr b ip_requires) then
            let tp_requires = ip_requires.ip_content in
-           let loc = tp_requires.tp_statement.pred_loc in
-           Current_loc.set loc;
+           let<> UpdatedCurrentLoc = tp_requires.tp_statement.pred_loc in
            Translate_predicates.do_it kf env tp_requires
          else
            env)
@@ -355,7 +355,7 @@ let check_other_requires kf env contract =
                | Assert | Check ->
                  let requires = tp_requires.tp_statement in
                  let loc = requires.pred_loc in
-                 Current_loc.set loc;
+                 let<> UpdatedCurrentLoc = loc in
                  (* Prepend the name of the behavior *)
                  let requires =
                    { requires with pred_name = b.b_name :: requires.pred_name }
@@ -406,7 +406,7 @@ let check_other_requires kf env contract =
         (* Generate a predicate that will retrieve and test the
            already computed assumes value for the behavior *)
         let loc = assumes.pred_loc in
-        Current_loc.set loc;
+        let<> UpdatedCurrentLoc = loc in
         let assumes_vi, assumes_e, env =
           get_or_create_assumes_var ~loc env
         in
@@ -439,7 +439,7 @@ type translate_ppt =
 let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract clauses =
   let kinstr = Env.get_kinstr env in
   let loc = contract.location in
-  Current_loc.set loc;
+  let<> UpdatedCurrentLoc = loc in
   let do_clause env bhvrs =
     let bhvrs_list = Datatype.String.Set.elements bhvrs in
     let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
@@ -612,7 +612,7 @@ let check_complete_and_disjoint kf env contract =
     let env = check_bhvrs env Disjoint disjoints in
     env
   else begin
-    Current_loc.set contract.location;
+    let<> UpdatedCurrentLoc = contract.location in
     Options.warning
       ~current:true
       "@[Some assumes clauses could not be translated.@ Ignoring complete and \
@@ -622,6 +622,7 @@ let check_complete_and_disjoint kf env contract =
 
 (** Insert ensures check for the given contract in the environement *)
 let check_post_conds kf env contract =
+  let<> UpdatedCurrentLoc = contract.location in
   let get_or_create_assumes_var =
     mk_get_or_create_var kf Cil_const.intType "assumes_value"
   in
@@ -644,8 +645,7 @@ let check_post_conds kf env contract =
            if Translate_utils.must_translate
                (Property.ip_of_ensures kf kinstr b tp) then
              let tp_post_cond = ip_post_cond.ip_content in
-             let loc = tp_post_cond.tp_statement.pred_loc in
-             Current_loc.set loc;
+             let<> UpdatedCurrentLoc = tp_post_cond.tp_statement.pred_loc in
              match termination with
              | Normal ->
                (* If translating the default behavior, directly translate the
@@ -674,7 +674,7 @@ let check_post_conds kf env contract =
                | Assert | Check -> begin
                    let post_cond = tp_post_cond.tp_statement in
                    let loc = post_cond.pred_loc in
-                   Current_loc.set loc;
+                   let<> UpdatedCurrentLoc = loc in
                    match termination with
                    | Normal ->
                      (* Prepend the name of the behavior *)
@@ -778,6 +778,7 @@ let translate_preconditions kf env contract =
 let translate_postconditions kf env =
   let env = Env.set_annotation_kind env Postcondition in
   let contract, env = Env.pop_and_get_contract env in
+  let<> UpdatedCurrentLoc = contract.location in
   let do_it env =
     let env = check_post_conds kf env contract in
     env
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index eea4fb644ad18ce5aaeb3ce448e7e3d047a2aa0d..16b66960d7cbe3832a6a3619b5996663c4f5d63f 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -592,6 +592,9 @@ let add_malloc_and_free_stmts kf fundec =
 let inject_in_fundec main fundec =
   let vi = fundec.svar in
   let kf = try Globals.Functions.get vi with Not_found -> assert false in
+  let loc = Kernel_function.get_location kf in
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = loc in
   (* convert ghost variables *)
   vi.vghost <- false;
   let unghost_local vi =
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 10fc89d05129a85acca95f666c4571485442c3dc..0300bc5e6ee74528ccc33d4e30d47b10f7e0b4a7 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -69,6 +69,8 @@ let handle_annotations env kf stmt =
              let logic_env = Env.Logic_env.get env in
              Typing.preprocess_term ~use_gmp_opt:true ~logic_env t;
              let ty = Typing.get_typ ~logic_env t in
+             let open Current_loc.Operators in
+             let<> UpdatedCurrentLoc = t.term_loc in
              if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
              let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
              let vi_old, e_old, env =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index 3f484c98307adf09c9b9432267a43fbe7166b3d6..6be71b9118f61923d3d0984f01c7cbad0ddc6f91 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -48,7 +48,6 @@ let pre_funspec kf env funspec =
     env
   in
   let loc = Kernel_function.get_location kf in
-  Current_loc.set loc;
   let env = convert_unsupported_clauses env in
   let contract = Contract.create ~loc funspec in
   Env.with_params
@@ -91,6 +90,8 @@ let pre_code_annotation kf stmt env annot =
         ~f:(fun env -> Contract.translate_preconditions kf env contract)
         env
     | AInvariant(l, loop_invariant, p) ->
+      let open Current_loc.Operators in
+      let<> UpdatedCurrentLoc = p.tp_statement.pred_loc in
       if Translate_utils.must_translate
           (Property.ip_of_code_annot_single kf stmt annot) then
         let env = Env.set_annotation_kind env Invariant in
@@ -109,6 +110,8 @@ let pre_code_annotation kf stmt env annot =
       else
         env
     | AVariant (t, measure) ->
+      let open Current_loc.Operators in
+      let<> UpdatedCurrentLoc = t.term_loc in
       if Translate_utils.must_translate
           (Property.ip_of_code_annot_single kf stmt annot)
       then Env.set_loop_variant env ?measure t
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index f7bfcc06715baad3b6fdba56a872043391ba7f00..58c424efd6d6a3b5344bade03cf8978db2faec40 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -486,6 +486,11 @@ let for_stmt env kf stmt =
   let stmt_translations = Pred_or_term.Hashtbl.create 7 in
   At_data.Set.fold
     (fun ({ lscope; pot; error } as at_data) env ->
+       let open Current_loc.Operators in
+       let<> UpdatedCurrentLoc = match pot with
+         | PoT_pred p -> p.pred_loc
+         | PoT_term t -> t.term_loc
+       in
        let vi_or_err, env =
          let vi_or_err = Pred_or_term.Hashtbl.find_opt stmt_translations pot in
          match error, vi_or_err with
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index 584028365c4948abc71e5acf193394a1a487ec34..41fb13f9bef6d9b223a3276ce9cf17d9a0d43e48 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -73,7 +73,8 @@ let relation_to_binop = function
 let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
   let loc = p.pred_loc in
   let logic_env = Env.Logic_env.get env in
-  Current_loc.set loc;
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = loc in
   let of_bool = function true -> Cil.one ~loc | false -> Cil.zero ~loc in
   match p.pred_content with
   | Pfalse -> Cil.zero ~loc, adata, env
@@ -332,6 +333,8 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
     - [env]: the current environment.
     - [p]: the predicate to translate. *)
 and to_exp ~adata ?inplace ?name kf ?rte env p =
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = p.pred_loc in
   Assert.push_pending_register_data();
   let p = Logic_normalizer.get_pred p in
   let rte = match rte with None -> Env.generate_rte env | Some b -> b in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index e898f1dca194d56a6739d4c4c149bffc153b5688..b1abe02964f2dd81c1325fcbb930961cd1cec70b 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -261,6 +261,8 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
 
 and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
   let loc = t.term_loc in
+  let open Current_loc.Operators in
+  let<> UpdatedCurrentLoc = loc in
   let logic_env = Env.Logic_env.get env in
   match t.term_node with
   | TConst c ->
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 5cd7569f230a7abdffdba25a4517f09d83fecac7..10e7833ca2a69339d60278f4f969dc7c13c3dbcc 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -20,26 +20,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type location = Cil_datatype.Location.t
+
 (** Internal module holding the exception of [Error].
 
     The module is included into [Make_with_opt] later and should not be used
     directly. However we need to have a separate module for the exception so
     that every exception built by [Make] is the exact same type. *)
 module Exn = struct
-  exception Typing_error of Options.category option * string
-  exception Not_yet of Options.category option * string
-  exception Not_memoized of Options.category option
+  exception Typing_error of location * Options.category option * string
+  exception Not_yet of location * Options.category option * string
+  exception Not_memoized of location * Options.category option
 end
 
 module type S = sig
   type 'a result = ('a, exn) Result.t
   include module type of Exn
-  val make_untypable: string -> exn
-  val make_not_yet: string -> exn
-  val make_not_memoized: unit -> exn
-  val untypable: string -> 'a
-  val not_yet: string -> 'a
-  val not_memoized: unit -> 'a
+  val make_untypable: ?loc:Cil_datatype.Location.t -> string -> exn
+  val make_not_yet: ?loc:Cil_datatype.Location.t -> string -> exn
+  val make_not_memoized: ?loc:Cil_datatype.Location.t -> unit -> exn
+  val untypable: ?loc:Cil_datatype.Location.t -> string -> 'a
+  val not_yet: ?loc:Cil_datatype.Location.t -> string -> 'a
+  val not_memoized: ?loc:Cil_datatype.Location.t -> unit -> 'a
   val print_not_yet: string -> unit
   val handle: ('a -> 'a) -> 'a -> 'a
   val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
@@ -63,13 +65,16 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
   type 'a result = ('a, exn) Result.t
   include Exn
 
-  let make_untypable msg = Typing_error (P.phase, msg)
-  let make_not_yet msg = Not_yet (P.phase, msg)
-  let make_not_memoized () = Not_memoized P.phase
+  let make_untypable ?(loc = Current_loc.get ()) msg =
+    Typing_error (loc, P.phase, msg)
+  let make_not_yet ?(loc = Current_loc.get ()) msg =
+    Not_yet (loc, P.phase, msg)
+  let make_not_memoized ?(loc = Current_loc.get ()) () =
+    Not_memoized (loc, P.phase)
 
-  let untypable msg = raise (make_untypable msg)
-  let not_yet msg = raise (make_not_yet msg)
-  let not_memoized () = raise (make_not_memoized ())
+  let untypable ?loc msg = raise (make_untypable ?loc msg)
+  let not_yet ?loc msg = raise (make_not_yet ?loc msg)
+  let not_memoized ?loc () = raise (make_not_memoized ?loc ())
 
   let pp_phase fmt phase =
     match phase with
@@ -92,11 +97,14 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
   let print_not_yet msg =
     do_print_not_yet P.phase msg
 
+  let with_loc loc f = Current_loc.with_loc loc f ()
+
   let generic_handle f res x =
     try
       f x
     with
-    | Typing_error (phase, s) ->
+    | Typing_error (loc, phase, s) ->
+      with_loc loc @@ fun () ->
       let msg =
         Format.asprintf "@[invalid E-ACSL construct@ `%s'%a.@]"
           s
@@ -106,7 +114,8 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
         ~once:true ~current:true
         "@[%s@ Ignoring annotation.@]" msg;
       res
-    | Not_yet (phase, s) ->
+    | Not_yet (loc, phase, s) ->
+      with_loc loc @@ fun () ->
       do_print_not_yet phase s;
       res
 
@@ -117,7 +126,8 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
       match getter parameter with
       | Result.Ok res -> res
       | Result.Error exn -> raise exn
-    with Not_memoized phase ->
+    with Not_memoized (loc, phase) ->
+      with_loc loc @@ fun () ->
       Options.fatal
         "@[%s was not performed on construct %a%a@]"
         analyse_name
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 6eb07dc42c8c6cd86009de8961192ee57d096486..547508cb2bfbe996f1385b038e91f9a0f96ec3b9 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -26,33 +26,33 @@ module type S = sig
   type 'a result = ('a, exn) Result.t
   (** Represent either a result of type ['a] or an error with an exception. *)
 
-  exception Typing_error of Options.category option * string
+  exception Typing_error of Cil_datatype.Location.t * Options.category option * string
   (** Typing error where the first element is the phase where the error occured
       and the second element is the error message. *)
 
-  exception Not_yet of Options.category option * string
+  exception Not_yet of Cil_datatype.Location.t * Options.category option * string
   (** "Not yet supported" error where the first element is the phase where the
       error occured and the second element is the error message. *)
 
-  exception Not_memoized of Options.category option
+  exception Not_memoized of Cil_datatype.Location.t * Options.category option
   (** "Not memoized" error with the phase where the error occured. *)
 
-  val make_untypable: string -> exn
+  val make_untypable: ?loc:Cil_datatype.Location.t -> string -> exn
   (** Make a [Typing_error] exception with the given message. *)
 
-  val make_not_yet: string -> exn
+  val make_not_yet: ?loc:Cil_datatype.Location.t -> string -> exn
   (** Make a [Not_yet] exception with the given message. *)
 
-  val make_not_memoized: unit -> exn
+  val make_not_memoized: ?loc:Cil_datatype.Location.t -> unit -> exn
   (** Make a [Not_memoized] exception with the given message. *)
 
-  val untypable: string -> 'a
+  val untypable: ?loc:Cil_datatype.Location.t -> string -> 'a
   (** @raise Typing_error with the given message for the current phase. *)
 
-  val not_yet: string -> 'a
+  val not_yet: ?loc:Cil_datatype.Location.t -> string -> 'a
   (** @raise Not_yet with the given message for the current phase. *)
 
-  val not_memoized: unit -> 'a
+  val not_memoized: ?loc:Cil_datatype.Location.t -> unit -> 'a
   (** @raise Not_memoized for the current phase. *)
 
   val print_not_yet: string -> unit
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
index 96e87b4281599a62d57423f7c2349dfd86234f62..6fce00762a06077f6d3592d9c6c993e734a762ef 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
@@ -14,10 +14,6 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index 88f5b05f952d084127490c66dc534b3a3bedef73..ece498629b55657c3e1e34cacec38d03c11ad122 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -14,9 +14,6 @@
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index fe418e3cb585043c4c0f16efed9d2bd819add417..18154f6f6213dc02aab6be50903541c27e974e6d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -46,18 +46,12 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 38f864e7d0f3e5a5bd1e88848b719c497a519162..f52c455c798a32059e20c3db712ff28a4b0f2f54 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -41,18 +41,12 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 7a5615f923dd9a607416e4d21a551c4d8f1d8726..23c21e99648907caf63b24de3f1bd6097b518efb 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -44,18 +44,12 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 24ff5e96514076d264ec4ba323ece9b43c87b4c1..3d60921bd1791ef1f90e040c6364adb15e56f391 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -75,12 +75,6 @@
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning: 
   E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning: 
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
index 496843958f3e470bd647ac27b72a7c93444c0616..4250f5f5259de104cd1710e22443b501f2a41d08 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/sequential_threads.res.oracle
@@ -11,12 +11,6 @@
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning: 
   E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning: 
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 24ff5e96514076d264ec4ba323ece9b43c87b4c1..3d60921bd1791ef1f90e040c6364adb15e56f391 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -75,12 +75,6 @@
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning: 
   E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning: 
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
index 03caab5991344f201a680280a4b7c6b4e3d4e864..ebd235a065b6a7f449d37e0526bfb25773f0e0d1 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_safe_locations.res.oracle
@@ -11,12 +11,6 @@
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:405: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:410: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/pthread.h:413: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:357: Warning: 
   E-ACSL construct `\valid_function' is not yet supported. Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/pthread.h:355: Warning: 
diff --git a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
index a8484b26730007e01de0fa06eb22f74791da90d0..c0831f879b2fe26614435cb031e6abfa7f6bd23f 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
+++ b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
@@ -1,7 +1,7 @@
 [e-acsl] beginning translation.
 [e-acsl] functions_contiki.c:29: Warning: 
   no assigns clause generated for function length because pointers as arguments is not yet supported
-[e-acsl] functions_contiki.c:29: Warning: 
+[e-acsl] functions_contiki.c:20: Warning: 
   no assigns clause generated for function length_aux because pointers as arguments is not yet supported
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] functions_contiki.c:29: Warning: 
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 313b4259076ce75daa42b8cb0d0f5c6ec98fad3d..0373a3bc7c8eae47067b3e0a4b33d9c6b18b7bdc 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -20,9 +20,6 @@
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 23cc72521061a7f3f56a33ca1677fad652bc072f..6ea6f74635e3967de6c3b6d100e358da724b2b46 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -34,6 +34,10 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:422: Warning: 
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:419: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
@@ -41,10 +45,6 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:193: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:196: Warning: 
   E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:204: Warning: 
@@ -55,10 +55,6 @@
 [e-acsl] FRAMAC_SHARE/libc/string.h:192: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:197: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:200: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
@@ -70,10 +66,6 @@
     \forall char *p; \old(s) <= p < \result ==> *p != (char)\old(c)'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:158: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:158: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
@@ -87,9 +79,6 @@
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning: 
   E-ACSL construct `terminates clause' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index 37368c20591586b5389598157a929a0270e414d4..91d25a8396e8008dbdac92dcf06e46d17966dd48 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -14,10 +14,6 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
index d35a4002aa1ad8679db90991595af70652d7e4b4..63e75d6abc4ca699b6b0fe2711814762a029e356 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -17,19 +17,9 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:500: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:501: Warning: 
   no assigns clause generated for function strnlen because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/string.h:500: Warning: 
-  E-ACSL construct
-  `logic functions or predicates with no definition nor reads clause'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:506: Warning: 
-  E-ACSL construct
-  `logic functions or predicates with no definition nor reads clause'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:513: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:300: Warning: 
   E-ACSL construct
   `logic functions or predicates with no definition nor reads clause'
   is not yet supported.
@@ -48,29 +38,19 @@
 [e-acsl] FRAMAC_SHARE/libc/string.h:496: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:504: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:511: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:511: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:518: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:476: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:477: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:478: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:478: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:480: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
@@ -93,10 +73,6 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:431: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
@@ -119,11 +95,11 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:419: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:420: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:420: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:422: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index e1c36e05ce0dca81dca0c381114fd01928601a54..e018ddbb511c5f3e51f450276b03d83c22e8781d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -10,48 +10,20 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:859: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:866: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:874: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:886: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning: 
   Some assumes clauses could not be translated.
   Ignoring complete and disjoint behaviors annotations.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:857: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning: 
   E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:872: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning: 
   no assigns clause generated for function valid_string because pointers as arguments is not yet supported
 [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:884: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:892: Warning: 
   E-ACSL construct
   `logic functions or predicates with no definition nor reads clause'
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index b9cee10fd6fe2a9ed6d7989a5439d1a1b379b7e1..e572e7941c40c525c7d153bd76b2f07313853389 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -20,7 +20,4 @@
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:802: Warning: 
   E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:803: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle
index 9c2f89c255754a11262b466c9b9cc683ec979a2d..e19fe1f52be199c567aaf49df127be91ba1074d2 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vdso.res.oracle
@@ -5,7 +5,4 @@
 [e-acsl] FRAMAC_SHARE/libc/time.h:113: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/time.h:116: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index 1fe29a8e3921f62c6782fd95d4e97f5975f7edaa..ffd8eb30897eec1e7dadfbd2c7d6f6a737dedf4e 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -10,48 +10,20 @@
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:859: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:866: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:874: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:886: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning: 
   Some assumes clauses could not be translated.
   Ignoring complete and disjoint behaviors annotations.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:857: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning: 
   E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:872: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning: 
   no assigns clause generated for function valid_string because pointers as arguments is not yet supported
 [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning: 
   E-ACSL construct `logic functions or predicates performing read accesses'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:884: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:892: Warning: 
   E-ACSL construct
   `logic functions or predicates with no definition nor reads clause'
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 1c517990dc7efad810a5cd1421690c7b1cf5cd42..0eab9debfc3c2305181a3b6883f60762b748cc79 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -11,10 +11,6 @@
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:556: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:561: Warning: 
-  E-ACSL construct `logic functions or predicates performing read accesses'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:561: Warning: 
   function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.