diff --git a/Makefile.generating b/Makefile.generating
index 12dd18b3f0afb4cb03bfaf8a9e8a9e682730a238..31a445a75ca111f32afc84a2b6a6748409d9436f 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -133,11 +133,23 @@ ifeq ($(HAS_OCAML408),yes)
         Format.String_tag str -> str \
       | _ -> raise (Invalid_argument "unsupported tag extension")
   FORMAT_STAG_OF_STRING=Format.String_tag s
+  HAS_OCAML407_OR_408=yes
 else
   DYNLINK_INIT=Dynlink.init
   FORMAT_STAG=tag
   FORMAT_STRING_OF_STAG=s
   FORMAT_STAG_OF_STRING=s
+  ifeq ($(HAS_OCAML407),yes)
+    HAS_OCAML407_OR_408=yes
+  else
+    HAS_OCAML407_OR_408=no
+  endif
+endif
+
+ifeq ($(HAS_OCAML407_OR_408),yes)
+  FLOAT_MAX_FLOAT=Float.max_float
+else
+  FLOAT_MAX_FLOAT=Pervasives.max_float
 endif
 
 src/libraries/stdlib/transitioning.ml: \
@@ -153,6 +165,7 @@ src/libraries/stdlib/transitioning.ml: \
          -e 's/@ASSOC_OPT@/$(ASSOC_OPT)/g' \
          -e 's/@ASSQ_OPT@/$(ASSQ_OPT)/g' \
          -e 's/@DYNLINK_INIT@/$(DYNLINK_INIT)/g' \
+         -e 's/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/g' \
          -e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
          -e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
          -e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 82a079e98bd4fab78b03020d910170aaa3b64b1e..226cab728c71b687a44893152ae307cd1af3e012 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -51,11 +51,7 @@ extern int pselect(int nfds, fd_set * readfds,
   requires errorfds: errorfds == \null || \valid(errorfds);
   requires timeout: timeout == \null || \valid(timeout);
   assigns __fc_fds_state \from __fc_fds_state;
-  assigns readfds  == \null ? \empty : *readfds,
-          writefds == \null ? \empty : *writefds,
-          errorfds == \null ? \empty : *errorfds,
-          timeout == \null ? \empty : *timeout,
-          \result
+  assigns *readfds, *writefds, *errorfds, *timeout, \result
     \from indirect:nfds,
           indirect:readfds, indirect:*readfds,
           indirect:writefds, indirect:*writefds,
diff --git a/share/libc/signal.h b/share/libc/signal.h
index f42d35711ab12190c0f7e2900f36ce4a2b922333..27ae78965980e8df8e4473bf131b5c445da1faa8 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -205,8 +205,8 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
   requires valid_oldact_or_null: oldact == \null || \valid(oldact);
   requires valid_read_act_or_null: act == \null || \valid_read(act);
   requires separation:separated_acts: \separated(act, oldact);
-  assigns oldact == \null ? \empty : *oldact \from __fc_p_sigaction;
-  assigns act == \null ? \empty : __fc_p_sigaction[signum] \from *act;
+  assigns *oldact \from __fc_p_sigaction;
+  assigns __fc_p_sigaction[signum] \from *act;
   assigns \result \from indirect:signum, indirect:act, indirect:*act,
                         indirect:oldact, indirect:*oldact;
   ensures act_changed: act == \null || \subset(__fc_p_sigaction[signum], *act);
@@ -225,8 +225,7 @@ extern int sigaction(int signum, const struct sigaction *restrict act,
   requires separation: (set == oldset == \null) ||
                        \separated(set, oldset);
   assigns \result \from indirect:how, indirect:set, indirect:oldset;
-  assigns oldset == \null ? \empty : *oldset
-          \from indirect:how, indirect:oldset;
+  assigns *oldset \from indirect:how, indirect:oldset;
   ensures result_ok_or_error: \result == 0 || \result == -1;
   ensures initialization:oldset_initialized:
     oldset != \null && \result == 0 ==> \initialized(oldset);
diff --git a/share/libc/stropts.h b/share/libc/stropts.h
index 48351585e7e3537806592d6ac9d2d6cf81d9f2af..3b0ee82968b303fbf98723c0d45d05198c11e4ea 100644
--- a/share/libc/stropts.h
+++ b/share/libc/stropts.h
@@ -172,7 +172,7 @@ extern int    __va_ioctl_int(int fd, int request, int arg);
 
 /*@ assigns \result \from indirect:fd, indirect:request,
       indirect:((char*)argp)[0..];
-    assigns argp != \null ? ((char*)argp)[0..] : \empty \from
+    assigns ((char*)argp)[0..] \from
       indirect:fd, indirect:request, ((char*)argp)[0..]; */
 extern int    __va_ioctl_ptr(int fd, int request, void* argp);
 
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 73fed482445f4c6a663ae88e8535b45fc5c704a8..b860763f4d3909a5c198a66af5701417801f78c9 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -151,16 +151,16 @@ extern int getitimer(int which, struct itimerval *curr_value);
 /*@
   requires valid_new_value: \valid_read(new_value);
   requires old_value_null_or_valid: old_value == \null || \valid(old_value);
-  assigns old_value != \null ? *old_value : \empty \from
-    indirect:which, indirect:old_value, indirect:new_value,
-    __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+  assigns *old_value \from indirect:which, indirect:old_value,
+                           indirect:new_value, __fc_itimer_real,
+                           __fc_itimer_virtual, __fc_itimer_prof;
   assigns \result \from indirect:which, indirect:new_value, indirect:*new_value;
   ensures result_ok_or_error: \result == 0 || \result == -1;
   behavior real:
     assumes itimer_real_and_valid:
       which == ITIMER_REAL && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty \from __fc_itimer_real;
+    assigns *old_value \from __fc_itimer_real;
     assigns __fc_itimer_real \from *new_value;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
@@ -168,14 +168,14 @@ extern int getitimer(int which, struct itimerval *curr_value);
     assumes itimer_virtual_and_valid:
       which == ITIMER_VIRTUAL && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty  \from __fc_itimer_virtual;
+    assigns *old_value \from __fc_itimer_virtual;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
   behavior prof:
     assumes itimer_prof_and_valid:
       which == ITIMER_PROF && __VALID_ITIMERVAL(new_value);
     assigns \result \from \nothing;
-    assigns old_value != \null ? *old_value : \empty  \from __fc_itimer_prof;
+    assigns *old_value \from __fc_itimer_prof;
     ensures result_ok: \result == 0;
     ensures initialization:old_value: \initialized(old_value);
   behavior invalid:
diff --git a/share/libc/time.h b/share/libc/time.h
index 60e5031571f9ef5e2d527e9b5e8a81907ae66a36..52c66700cc80c3df73b708b8f6a302a30b2d6877 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -216,9 +216,8 @@ extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
     assumes no_einval: valid_clock_id(clock_id);
     assigns \result \from indirect:__fc_time, indirect:clock_id, indirect:rqtp,
                           indirect:*rqtp;
-    assigns rmtp == \null ? \empty : *rmtp \from __fc_time, indirect:clock_id,
-                                                 indirect:rqtp, indirect:*rqtp,
-                                                 indirect:rmtp;
+    assigns *rmtp \from __fc_time, indirect:clock_id, indirect:rqtp,
+                        indirect:*rqtp, indirect:rmtp;
     ensures result_interrupted: \result == EINTR;
     ensures initialization:interrupted_remaining:
       rmtp != \null ==> \initialized(&rmtp->tv_sec) && \initialized(&rmtp->tv_nsec);
@@ -263,9 +262,8 @@ extern struct tm *localtime_r(const time_t *restrict timep,
   requires valid_nanosecs: 0 <= rqtp->tv_nsec < 1000000000;
   requires valid_remaining_or_null: rmtp == \null || \valid(rmtp);
   assigns \result \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp;
-  assigns rmtp == \null ? \empty : *rmtp \from indirect:__fc_time,
-                                               indirect:rqtp, indirect:*rqtp,
-                                               indirect:rmtp;
+  assigns *rmtp \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp,
+                      indirect:rmtp;
   ensures result_elapsed_or_interrupted: \result == 0 || \result == -1;
   ensures initialization:interrupted_remaining:
     rmtp != \null && \result == -1 ==>
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 9aecb292da713a7214e26574f10a62229de8f029..7448601a76488d7a93c75987b7b33f8a9e6d434e 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -138,8 +138,9 @@ let () =
 
 (* Load Frama-c from disk if required *)
 let load_binary () =
-  let filename = Kernel.LoadState.get () in
-  if filename <> "" then begin
+  let filepath = Kernel.LoadState.get () in
+  if filepath <> Filepath.Normalized.unknown then begin
+    let filename = Filepath.Normalized.to_pretty_string filepath in
     try
       Project.load_all filename
     with Project.IOError s ->
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index d74de525bfa58a548f5990215ab66750e7423ef6..d20cc20285af3175eabfb4202058616734e426ae 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -442,6 +442,91 @@ struct
   module Empty_string(X: Parameter_sig.Input_with_arg) =
     String(struct include X let default = empty_string end)
 
+  (* ************************************************************************ *)
+  (** {3 Filepath} *)
+  (* ************************************************************************ *)
+
+  module Fc_Filepath = Filepath
+
+  module Filepath
+      (X: sig
+         include Parameter_sig.Input_with_arg
+         val existence : Parameter_sig.existence
+       end) =
+  struct
+
+    exception No_file
+    exception File_exists
+
+    include Build
+        (struct
+          include Datatype.Filepath
+          include X
+          let default () = Filepath.Normalized.unknown
+          let functor_name = "Filepath"
+        end)
+
+    let check_existence existence fp =
+      match existence with
+      | Parameter_sig.Indifferent -> ()
+      | Parameter_sig.Must_exist ->
+        if not (Sys.file_exists (Filepath.Normalized.to_pretty_string fp)) then
+          raise No_file
+      | Parameter_sig.Must_not_exist ->
+        if Sys.file_exists (Filepath.Normalized.to_pretty_string fp) then
+          raise File_exists
+
+    let existence = X.existence
+
+    let convert f oldstr newstr =
+      let oldfp = Filepath.Normalized.to_pretty_string oldstr in
+      let newfp = Filepath.Normalized.to_pretty_string newstr in
+      f oldfp newfp
+
+    let set fp = check_existence existence fp ; set fp
+
+    let set_str s = set (Filepath.Normalized.of_string s)
+
+    let add_option name =
+      Cmdline.add_option
+        name
+        ~argname:X.arg_name
+        ~help:X.help
+        ~visible:is_visible
+        ~ext_help:!Parameter_customize.optional_help_ref
+        ~plugin:P.shortname
+        ~group
+        stage
+        (Cmdline.String set_str)
+
+    let parameter_get fp = Filepath.Normalized.to_pretty_string (get fp)
+    let parameter_add_set_hook f = add_set_hook (convert f)
+    let parameter_add_update_hook f = add_update_hook (convert f)
+
+    let parameter =
+      let accessor =
+        Typed_parameter.String
+          ({ Typed_parameter.get = parameter_get;
+             set = set_str;
+             add_set_hook = parameter_add_set_hook;
+             add_update_hook = parameter_add_update_hook },
+           fun () -> [])
+      in
+      let p =
+	Typed_parameter.create ~name ~help:X.help ~accessor ~is_set
+      in
+      add_parameter !Parameter_customize.group_ref stage p;
+      add_option X.option_name;
+      Parameter_customize.reset ();
+      if is_dynamic then
+	let plugin = empty_string in
+	Dynamic.register
+          ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+      else
+	p
+
+  end
+
   (* ************************************************************************ *)
   (** {3 Collections} *)
   (* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index bb827691793567e0bbe804f712a2fb7293d5a96b..a36076d68471974e040e4d0cebef792d3d185d74 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -321,6 +321,24 @@ module type Specific_dir = sig
 
 end
 
+type existence = Must_exist | Must_not_exist | Indifferent
+
+(** signature for normalized pathnames. *)
+module type Filepath = sig
+
+  exception No_file
+  (** raised by {!set} if no file exists and [existence] is [Must_exist]. *)
+
+  exception File_exists
+  (** raised by {!set} if some file exists and [existence] is
+      [Must_nos_exist]. *)
+
+  val existence: existence
+
+  include S with type t = Filepath.Normalized.t
+
+end
+
 (* ************************************************************************** *)
 (** {3 Collections} *)
 (* ************************************************************************** *)
@@ -515,6 +533,13 @@ module type Builder = sig
   (** @plugin development guide *)
   module Empty_string(X: Input_with_arg): String
 
+  module Fc_Filepath = Filepath
+
+  module Filepath(X: sig
+      include Input_with_arg
+      val existence: existence
+    end): Filepath
+
   exception Cannot_build of string
   module Make_set
     (E:
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 10241320736c4495275430db1a8a6ac2bbecc563..f686cd7684e27896afc96eae7409215a3f6d11be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -445,6 +445,14 @@ module Parameter = struct
         let modname = "String"
       end)
 
+  module Filepath =
+    Common
+      (struct
+        type t = Datatype.Filepath.t
+        let ty = Datatype.Filepath.ty
+        let modname = "Filepath"
+      end)
+
   module StringSet = struct
     include Common
         (struct include Datatype.String.Set let modname = "StringSet" end)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index c837a15601e045eb08dfe2a936ba8c4960687689..3650174dc2a424590dc3ba3473e6db44c1abc3be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -118,6 +118,9 @@ module Parameter : sig
   (** String parameters. *)
   module String : Common with type t = string
 
+  (** Filepath parameters. *)
+  module Filepath : Common with type t = Datatype.Filepath.t
+
   (** Set of string parameters. *)
   module StringSet : sig
     include Common with type t = Datatype.String.Set.t
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 41dcb5d8d089e8d56b26ceba6a29e28d14e31de2..3bcff739e6a5064f21a7fd18923c3992c43c6ce3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -716,10 +716,11 @@ let () = Parameter_customize.set_cmdline_stage Cmdline.Loading
    reset *) 
 (*let () = Parameter_customize.do_not_projectify ()*)
 module LoadState =
-  P.Empty_string
+  P.Filepath
     (struct
        let option_name = "-load"
        let arg_name = "filename"
+       let existence = Parameter_sig.Must_exist
        let help = "load a previously-saved session from file <filename>"
      end)
 
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 7976e6c86673f65f73788c64e6a77b384b0a0fed..0b43666bb0891fda4c20fae462daa956571e9dec 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -299,7 +299,7 @@ module BigIntsHex: Parameter_sig.Int
 module SaveState: Parameter_sig.String
   (** Behavior of option "-save" *)
 
-module LoadState: Parameter_sig.String
+module LoadState: Parameter_sig.Filepath
   (** Behavior of option "-load" *)
 
 module LoadModule: Parameter_sig.String_list
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index f24bdbcfb2680fd819c456b99b0c6d7ca87c8dd9..01d5831cbe50b7cc0048d60f594a888d4a58ad32 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -534,7 +534,7 @@ struct
 
     let pp_source fmt = function
       | None -> ()
-      | Some src -> Format.fprintf fmt "%a:" Filepath.pp_pos src
+      | Some src -> Format.fprintf fmt "%a:" Fc_Filepath.pp_pos src
   end
 
   (* Output must be synchronized with functions [prefix_*] in module Log. *)
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index de6215991de78ead186f5deb8cca34095989fb99..cf09ddd667ed096ced79582ad7905f8ddc82ed19 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -37,6 +37,10 @@ module Dynlink = struct
   let init = @DYNLINK_INIT@
 end
 
+module Float = struct
+  let max_float = @FLOAT_MAX_FLOAT@
+end
+
 module Format = struct
   type stag = Format.@FORMAT_STAG@
   let string_of_stag s = @FORMAT_STRING_OF_STAG@
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 521cf30c013bf939d5bbecc4444a682620267319..94ae54311a9ca97d31b0eab45927b7d4454c96c8 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -49,6 +49,11 @@ module Dynlink: sig
   val init: unit -> unit
 end
 
+(** 4.07 *)
+module Float: sig
+  val max_float: float
+end
+
 (** 4.08 *)
 module Format: sig
   type stag
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 0e774657a818b0b5f91cafba14f4b21197480427..eb86c85f6945e397d7e3b1af0e3959c71faa5500 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -224,6 +224,7 @@ module Normalized = struct
   let pretty fmt p = Format.fprintf fmt "%s" (pretty p)
   let pp_abs fmt p = Format.fprintf fmt "%s" p
   let unknown = normalize ""
+  let is_unknown fp = equal fp unknown
 end
 
 type position =
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 6ea46d821541a1de524e1baad38bbadcf6339b54..74eef31bbdbb8d6f2ff340258beffeef3539cd65 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -120,6 +120,9 @@ module Normalized: sig
 
   (** Unknown filepath, used as 'dummy' for [Datatype.Filepath]. *)
   val unknown: t
+
+  (** @since Frama-C+dev *)
+  val is_unknown: t -> bool
 end
 
 (** Describes a position in a source file.
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 5515e44a3b884a7281f00342677c689c8333baa1..d5438b227de994181748fcdadfd7c43f3a49b05b 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -138,6 +138,7 @@ let reduce_to_valid_location out loc =
       begin
         if is_assigns out && not (Locations.is_bottom_loc loc) then
           Value_parameters.warning ~current:true ~once:true
+            ~wkey:Value_parameters.wkey_invalid_assigns
             "@[Completely invalid destination@ for %a.@ \
              Ignoring.@]" pp_assign_free_alloc out;
         None
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 5471f4b343ffdf7d312a50bdf3420e27ebf77731..5eb874d2566e44e9e243f6d50027377060d47373 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -98,6 +98,8 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
 let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll:for"
 let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
 let wkey_signed_overflow = register_warn_category "signed-overflow"
+let wkey_invalid_assigns = register_warn_category "invalid-assigns"
+let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
 
 module ForceValues =
   WithOutput
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index fe24f33b22e81e956807ffba17fae01f421217a2..a5f62e9cff6d10c4d4ebaef1a4dae9da8b8294f2 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -204,6 +204,9 @@ val wkey_missing_loop_unroll_for : warn_category
 (** Warning category for signed overflows *)
 val wkey_signed_overflow : warn_category
 
+(** Warning category for 'completely invalid' assigns clause *)
+val wkey_invalid_assigns : warn_category
+
 (** Debug category used to print information about invalid pointer comparisons*)
 val dkey_pointer_comparison: category
 
diff --git a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
index 834a0dde5f6db9f527a604df92cba0f2fa2a7226..195847c4a798c48e04d7613f0a9ff77e106c4001 100644
--- a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
@@ -13,6 +13,9 @@
 [eva] Initial state computed
 [eva] using specification for function __va_ioctl_void
 [eva] using specification for function __va_ioctl_ptr
+[eva:invalid-assigns] tests/known/ioctl.c:17: 
+  Completely invalid destination for assigns clause *((char *)argp + (0 ..)).
+  Ignoring.
 [eva] using specification for function __va_ioctl_int
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index eaeda7b458b0f7f0faafe7ea4bc32524c11a8f0d..7b6ba044a297053255417158844f6f6f361a1c78 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -976,7 +976,7 @@ let base_output () =
               | dir ->
                   make_output_dir dir ; dir in
       base_output := Some output;
-      Filepath.add_symbolic_dir "WPOUT" output ;
+      Fc_Filepath.add_symbolic_dir "WPOUT" output ;
       output
   | Some output -> output
 
@@ -1018,7 +1018,7 @@ let has_print_generated () = has_dkey cat_print_generated
 
 let print_generated ?header file =
   let header = match header with
-    | None -> Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
+    | None -> Fc_Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
     | Some head -> head in
   debug ~dkey:cat_print_generated "%S@\n%t@." header
     begin fun fmt ->
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index e27e83c8af3557509f71e9dee55793438f58b39d..35235461d13ed2ecd8659d12fcde6992bb47ce76 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -39,7 +39,7 @@
 [eva] computing for function f <- invalid_assigns_imprecise <- main.
   Called from tests/builtins/imprecise.c:11.
 [eva] using specification for function f
-[eva] tests/builtins/imprecise.c:11: Warning: 
+[eva:invalid-assigns] tests/builtins/imprecise.c:11: 
   Completely invalid destination for assigns clause *p. Ignoring.
 [eva] Done for function f
 [eva] Recording results for invalid_assigns_imprecise
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 107f92c67f3f62604ce53ca25bf5a5672e0c65be..417ea214e24ff7f7103182badf324309869ad81f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3145,10 +3145,9 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
         \old(oldact) ≡ \null ∨
         *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
-    assigns oldact ≡ \null? \empty: *oldact,
-            act ≡ \null? \empty: *(__fc_p_sigaction + signum), \result;
-    assigns oldact ≡ \null? \empty: *oldact \from __fc_p_sigaction;
-    assigns act ≡ \null? \empty: *(__fc_p_sigaction + signum) \from *act;
+    assigns *oldact, *(__fc_p_sigaction + signum), \result;
+    assigns *oldact \from __fc_p_sigaction;
+    assigns *(__fc_p_sigaction + signum) \from *act;
     assigns \result
       \from (indirect: signum), (indirect: act), (indirect: *act),
             (indirect: oldact), (indirect: *oldact);
@@ -3166,11 +3165,10 @@ extern int sigaction(int signum, struct sigaction const * __restrict act,
       initialization: oldset_initialized:
         \old(oldset) ≢ \null ∧ \result ≡ 0 ⇒
         \initialized(\old(oldset));
-    assigns \result, oldset ≡ \null? \empty: *oldset;
+    assigns \result, *oldset;
     assigns \result
       \from (indirect: how), (indirect: set), (indirect: oldset);
-    assigns oldset ≡ \null? \empty: *oldset
-      \from (indirect: how), (indirect: oldset);
+    assigns *oldset \from (indirect: how), (indirect: oldset);
  */
 extern int sigprocmask(int how, sigset_t const * __restrict set,
                        sigset_t * __restrict oldset);
@@ -5840,11 +5838,11 @@ axiomatic nanosleep_predicates {
       ensures
         remaining_valid:
           \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
-      assigns \result, rmtp ≡ \null? \empty: *rmtp;
+      assigns \result, *rmtp;
       assigns \result
         \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
               (indirect: *rqtp);
-      assigns rmtp ≡ \null? \empty: *rmtp
+      assigns *rmtp
         \from __fc_time, (indirect: clock_id), (indirect: rqtp),
               (indirect: *rqtp), (indirect: rmtp);
     
@@ -5901,10 +5899,10 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
       interrupted_remaining_valid:
         \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
         0 ≤ \old(rmtp)->tv_nsec < 1000000000;
-    assigns \result, rmtp ≡ \null? \empty: *rmtp;
+    assigns \result, *rmtp;
     assigns \result
       \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
-    assigns rmtp ≡ \null? \empty: *rmtp
+    assigns *rmtp
       \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
             (indirect: rmtp);
  */
@@ -6753,8 +6751,8 @@ extern int getitimer(int which, struct itimerval *curr_value);
     requires
       old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
-    assigns old_value ≢ \null? *old_value: \empty, \result;
-    assigns old_value ≢ \null? *old_value: \empty
+    assigns *old_value, \result;
+    assigns *old_value
       \from (indirect: which), (indirect: old_value), (indirect: new_value),
             __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
     assigns \result
@@ -6767,10 +6765,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty,
-              __fc_itimer_real;
+      assigns \result, *old_value, __fc_itimer_real;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_real;
+      assigns *old_value \from __fc_itimer_real;
       assigns __fc_itimer_real \from *new_value;
     
     behavior virtual:
@@ -6780,10 +6777,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty;
+      assigns \result, *old_value;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty
-        \from __fc_itimer_virtual;
+      assigns *old_value \from __fc_itimer_virtual;
     
     behavior prof:
       assumes
@@ -6792,9 +6788,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
           0 ≤ new_value->it_interval.tv_usec ≤ 999999;
       ensures result_ok: \result ≡ 0;
       ensures initialization: old_value: \initialized(\old(old_value));
-      assigns \result, old_value ≢ \null? *old_value: \empty;
+      assigns \result, *old_value;
       assigns \result \from \nothing;
-      assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_prof;
+      assigns *old_value \from __fc_itimer_prof;
     
     behavior invalid:
       assumes
@@ -6818,27 +6814,25 @@ extern int setitimer(int which,
     requires writefds: writefds ≡ \null ∨ \valid(writefds);
     requires errorfds: errorfds ≡ \null ∨ \valid(errorfds);
     requires timeout: timeout ≡ \null ∨ \valid(timeout);
-    assigns __fc_fds_state, readfds ≡ \null? \empty: *readfds,
-            writefds ≡ \null? \empty: *writefds,
-            errorfds ≡ \null? \empty: *errorfds,
-            timeout ≡ \null? \empty: *timeout, \result;
+    assigns __fc_fds_state, *readfds, *writefds, *errorfds, *timeout,
+            \result;
     assigns __fc_fds_state \from __fc_fds_state;
-    assigns readfds ≡ \null? \empty: *readfds
+    assigns *readfds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns writefds ≡ \null? \empty: *writefds
+    assigns *writefds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns errorfds ≡ \null? \empty: *errorfds
+    assigns *errorfds
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
             (indirect: *timeout), __fc_fds_state;
-    assigns timeout ≡ \null? \empty: *timeout
+    assigns *timeout
       \from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
             (indirect: writefds), (indirect: *writefds),
             (indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
@@ -7129,11 +7123,11 @@ extern int __va_ioctl_void(int fd, int request);
  */
 extern int __va_ioctl_int(int fd, int request, int arg);
 
-/*@ assigns \result, argp ≢ \null? *((char *)argp + (0 ..)): \empty;
+/*@ assigns \result, *((char *)argp + (0 ..));
     assigns \result
       \from (indirect: fd), (indirect: request),
             (indirect: *((char *)argp + (0 ..)));
-    assigns argp ≢ \null? *((char *)argp + (0 ..)): \empty
+    assigns *((char *)argp + (0 ..))
       \from (indirect: fd), (indirect: request), *((char *)argp + (0 ..));
  */
 extern int __va_ioctl_ptr(int fd, int request, void *argp);
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
index ca158666adf08acb2890a53b2ae8fecfddb3e132..a5ac900a0e19e23678ca830eeef10d3ef012d55b 100644
--- a/tests/libc/oracle/libgen_h.res.oracle
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -15,7 +15,7 @@
   Called from tests/libc/libgen_h.c:11.
 [eva] tests/libc/libgen_h.c:11: 
   function basename: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:11: Warning: 
+[eva:invalid-assigns] tests/libc/libgen_h.c:11: 
   Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
 [eva] Done for function basename
 [eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown.
@@ -30,7 +30,7 @@
   Called from tests/libc/libgen_h.c:16.
 [eva] tests/libc/libgen_h.c:16: 
   function dirname: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:16: Warning: 
+[eva:invalid-assigns] tests/libc/libgen_h.c:16: 
   Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
 [eva] Done for function dirname
 [eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown.
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 42c80f2642d6fdde9b66d2ab9487b73f4ff7b8a8..9d071e5884c3e373da23a02893036f0d8bbbaee3 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -83,6 +83,8 @@
   function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
 [eva] tests/libc/signal_h.c:35: 
   function sigprocmask: precondition 'separation' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:35: 
+  Completely invalid destination for assigns clause *oldset. Ignoring.
 [eva] Done for function sigprocmask
 [eva] computing for function sigprocmask <- main.
   Called from tests/libc/signal_h.c:38.
@@ -137,6 +139,8 @@
   function sigaction: precondition 'valid_read_act_or_null' got status valid.
 [eva] tests/libc/signal_h.c:51: 
   function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:51: 
+  Completely invalid destination for assigns clause *oldact. Ignoring.
 [eva] Done for function sigaction
 [eva] Recording results for main
 [eva] done for function main
@@ -176,9 +180,7 @@
                 [15]{.sa_handler; .sa_sigaction} ∈ {0}
                 [15]{.sa_mask; .sa_flags} ∈ [--..--]
                 [16]{.sa_handler; .sa_sigaction} ∈ {0}
-                [16]{.sa_mask; .sa_flags} ∈ [--..--]
-                [17]{.sa_handler; .sa_sigaction} ∈ {0}
-                [17]{.sa_mask; .sa_flags} ∈ [--..--]
+                {[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
                 [18] ∈
                 {{ garbled mix of &{__fc_sigaction}
                  (origin: Library function) }}
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 75780c1ba4a10561b67f6deb39440fddbcfbf8cb..55c5afe6dad117fc0beb325fa0f45052db727460 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -134,7 +134,7 @@
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva] tests/libc/string_h.c:72: 
   function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:72: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:72: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok
 [eva:alarm] tests/libc/string_h.c:73: Warning: assertion got status unknown.
@@ -144,7 +144,7 @@
   function strtok: precondition 'valid_string_delim' got status valid.
 [eva:alarm] tests/libc/string_h.c:75: Warning: 
   function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:75: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:75: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok
 [eva:alarm] tests/libc/string_h.c:76: Warning: 
@@ -221,7 +221,7 @@
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva] tests/libc/string_h.c:102: 
   function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:102: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:102: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok_r
 [eva:alarm] tests/libc/string_h.c:103: Warning: assertion got status unknown.
@@ -233,7 +233,7 @@
   function strtok_r: precondition 'valid_saveptr' got status valid.
 [eva:alarm] tests/libc/string_h.c:105: Warning: 
   function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:105: Warning: 
+[eva:invalid-assigns] tests/libc/string_h.c:105: 
   Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
 [eva] Done for function strtok_r
 [eva:alarm] tests/libc/string_h.c:106: Warning: 
diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle
index 41fa7f4bc4969060e4bf3300451702b172018a50..453a3465161df7694e3616278d3db5120e82a673 100644
--- a/tests/libc/oracle/sys_select.res.oracle
+++ b/tests/libc/oracle/sys_select.res.oracle
@@ -72,6 +72,10 @@
   function select: precondition 'errorfds' got status valid.
 [eva] tests/libc/sys_select.c:31: 
   function select: precondition 'timeout' got status valid.
+[eva:invalid-assigns] tests/libc/sys_select.c:31: 
+  Completely invalid destination for assigns clause *writefds. Ignoring.
+[eva:invalid-assigns] tests/libc/sys_select.c:31: 
+  Completely invalid destination for assigns clause *errorfds. Ignoring.
 [eva] Done for function select
 [eva] computing for function FD_ISSET <- main.
   Called from tests/libc/sys_select.c:32.
diff --git a/tests/libc/oracle/sys_time.res.oracle b/tests/libc/oracle/sys_time.res.oracle
index 3c7c79cab30db005eb3c7f1d6087a189d033aa56..18c18fa9f8cf4ac0e2cd2252f3a3baf3d7dcd62c 100644
--- a/tests/libc/oracle/sys_time.res.oracle
+++ b/tests/libc/oracle/sys_time.res.oracle
@@ -11,6 +11,8 @@
   function setitimer: precondition 'valid_new_value' got status valid.
 [eva] tests/libc/sys_time.c:6: 
   function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva:invalid-assigns] tests/libc/sys_time.c:6: 
+  Completely invalid destination for assigns clause *old_value. Ignoring.
 [eva] Done for function setitimer
 [eva] tests/libc/sys_time.c:7: assertion got status valid.
 [eva] computing for function setitimer <- main.
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index 5fcd6c6d027bc01e634adfc623934e6e724e7607..7e8f729d1beae0a1300355d51b3f1c84f7826b6c 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -37,9 +37,13 @@
   function nanosleep: precondition 'valid_nanosecs' got status valid.
 [eva] tests/libc/time_h.c:22: 
   function nanosleep: precondition 'valid_remaining_or_null' got status valid.
+[eva:invalid-assigns] tests/libc/time_h.c:22: 
+  Completely invalid destination for assigns clause *rmtp. Ignoring.
 [eva] Done for function nanosleep
 [eva] computing for function nanosleep <- main.
   Called from tests/libc/time_h.c:22.
+[eva:invalid-assigns] tests/libc/time_h.c:22: 
+  Completely invalid destination for assigns clause *rmtp. Ignoring.
 [eva] Done for function nanosleep
 [eva] computing for function clock_nanosleep <- main.
   Called from tests/libc/time_h.c:28.
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 761d38bcf9e226c2597073376f838576ca755dd9..4dda7f7cf8b0609d64b17c78ec40d983449de12b 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -27,7 +27,7 @@
 [kernel:annot:missing-spec] tests/value/leaf_spec.i:22: Warning: 
   Neither code nor specification for function k, generating default assigns from the prototype
 [eva] using specification for function k
-[eva] tests/value/leaf_spec.i:22: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:22: 
   Completely invalid destination for assigns clause *l. Ignoring.
 [eva] Done for function k
 [eva] computing for function k0 <- main.
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index 666a0ee653ea406fd618ea0f479ba41d7741adf0..aa1978e94dfdb9044fb6881d77a2a219b2701da0 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -9,9 +9,9 @@
 [kernel:annot:missing-spec] tests/value/leaf_spec.i:27: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
-[eva] tests/value/leaf_spec.i:27: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:27: 
   Completely invalid destination for assigns clause *x. Ignoring.
-[eva] tests/value/leaf_spec.i:27: Warning: 
+[eva:invalid-assigns] tests/value/leaf_spec.i:27: 
   Completely invalid destination for assigns clause *y. Ignoring.
 [eva] Done for function f
 [eva] Recording results for main1