diff --git a/configurator.ml b/configurator.ml
index 5e4c11ec982fdb654024e607b565b737a77097e0..87bb3e182bb859d7587594362268c4949d44fd28 100644
--- a/configurator.ml
+++ b/configurator.ml
@@ -234,6 +234,27 @@ module Fc_version = struct
       "s|@MINOR_VERSION@|%s|" version.minor
 end
 
+module OS = struct
+  type t = Windows | MacOS | OtherUnix
+
+  let get configurator =
+    match C.ocaml_config_var_exn configurator "os_type" with
+    | "Win32" -> Windows
+    | _ ->
+      match C.ocaml_config_var_exn configurator "system" with
+      | "macosx" -> MacOS
+      | _ -> OtherUnix
+
+  let pp_sed fmt t =
+    let module_dirs = match t with
+      | Windows   -> "Win_dirs"
+      | MacOS     -> "Macos_dirs"
+      | OtherUnix -> "Unix_dirs"
+    in
+    Format.fprintf fmt
+      "s|@FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@|%s|" module_dirs
+end
+
 let python_available configurator =
   let result = C.Process.run configurator "python3" ["--version"] in
   if result.exit_code <> 0 then false
@@ -256,9 +277,11 @@ let python_available configurator =
 let configure configurator =
   let version = Fc_version.get configurator in
   let cpp = Cpp.get configurator in
+  let os = OS.get configurator in
   let config_sed = open_out "config.sed" in
   let fmt = Format.formatter_of_out_channel config_sed in
-  Format.fprintf fmt "%a\n%a\n" Fc_version.pp_sed version Cpp.pp_sed cpp ;
+  Format.fprintf fmt "%a\n%a\n%a\n"
+    Fc_version.pp_sed version Cpp.pp_sed cpp OS.pp_sed os ;
   close_out config_sed ;
   let python = open_out "python-3.7-available" in
   Printf.fprintf python "%b" (python_available configurator) ;
diff --git a/src/kernel_internals/runtime/macos_dirs.ml b/src/kernel_internals/runtime/macos_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..042dc2beb9298b39951c13842f540f4fef730320
--- /dev/null
+++ b/src/kernel_internals/runtime/macos_dirs.ml
@@ -0,0 +1,17 @@
+let home () =
+  match Sys.getenv "HOME" with
+  | "" -> raise Not_found
+  | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+  let open Filepath.Normalized in
+  match Sys.getenv_opt env with
+  | Some s when s <> "" -> concat (of_string s) "frama-c"
+  | _ -> concats (home ()) default
+
+let cache () =
+  env_or_default "XDG_CACHE_HOME" [ "Library" ; "Caches" ; "frama-c"]
+let config () =
+  env_or_default "XDG_CONFIG_HOME" [ "Application Support" ; "frama-c" ; "config" ]
+let state () =
+  env_or_default "XDG_STATE_HOME" [ "Application Support" ; "frama-c" ; "state" ]
diff --git a/src/kernel_internals/runtime/system_config.ml.in b/src/kernel_internals/runtime/system_config.ml.in
index fbf4944d65994bb6ad2ae0632c5f838e6065e456..028fd90f61dc36f31d07c00a11b2203cc1f9dedb 100644
--- a/src/kernel_internals/runtime/system_config.ml.in
+++ b/src/kernel_internals/runtime/system_config.ml.in
@@ -91,3 +91,7 @@ module Preprocessor = struct
 
   let supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
 end
+
+module User_dirs = struct
+  include @FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@
+end
diff --git a/src/kernel_internals/runtime/system_config.mli b/src/kernel_internals/runtime/system_config.mli
index ccceae3922695ec7df56cf3a875981beec763237..b0eb095867a359264564f43ea6c4bb5cd8e3d856 100644
--- a/src/kernel_internals/runtime/system_config.mli
+++ b/src/kernel_internals/runtime/system_config.mli
@@ -112,6 +112,18 @@ module Preprocessor : sig
   *)
 end
 
+(** Default user directories *)
+module User_dirs : sig
+  val cache: unit -> Filepath.Normalized.t
+  (** Where Frama-C should read/write cached files. *)
+
+  val config: unit -> Filepath.Normalized.t
+  (** Where Frama-C should read/write config files. *)
+
+  val state: unit -> Filepath.Normalized.t
+  (** Where Frama-C should read/write state files *)
+end
+
 val is_gui: bool
 (** Is the Frama-C GUI running? *)
 
diff --git a/src/kernel_internals/runtime/unix_dirs.ml b/src/kernel_internals/runtime/unix_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3ac63d6ef4f98328f9d5d7e4e6ca666b5b90eef2
--- /dev/null
+++ b/src/kernel_internals/runtime/unix_dirs.ml
@@ -0,0 +1,20 @@
+let home () =
+  match Sys.getenv "HOME" with
+  | "" -> raise Not_found
+  | s -> Filepath.Normalized.of_string s
+
+let env_or_default env default =
+  let open Filepath.Normalized in
+  let location =
+    match Sys.getenv_opt env with
+    | Some env when env <> "" -> of_string env
+    | _ -> concats (home ()) default
+  in
+  concat location "frama-c"
+
+let cache () =
+  env_or_default "XDG_CACHE_HOME" [ ".cache" ]
+let config () =
+  env_or_default "XDG_CONFIG_HOME" [ ".config" ]
+let state () =
+  env_or_default "XDG_STATE_HOME" [ ".local" ; "state" ]
diff --git a/src/kernel_internals/runtime/win_dirs.ml b/src/kernel_internals/runtime/win_dirs.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a8bf5c510e5f9c90957fd9ec8994f1cae74fc34c
--- /dev/null
+++ b/src/kernel_internals/runtime/win_dirs.ml
@@ -0,0 +1,13 @@
+let env_or_default env default sub =
+  let open Filepath.Normalized in
+  match Sys.getenv_opt env, sub with
+  | Some s, _ (* ignored *) when s <> "" -> concat (of_string s) "frama-c"
+  | _, Some sub -> concats (of_string default) [ "frama-c" ; sub ]
+  | _, None -> concat (of_string default) "frama-c"
+
+let cache () =
+  env_or_default "XDG_CACHE_HOME" (Sys.getenv "TEMP") None
+let config () =
+  env_or_default "XDG_CONFIG_HOME" (Sys.getenv "LOCALAPPDATA") (Some "config")
+let state () =
+  env_or_default "XDG_STATE_HOME" (Sys.getenv "LOCALAPPDATA") (Some "state")
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 11f898a7554002cd18584b76880e55f369c59afa..50962dcf30384b01a6d9b535d77e48a85cd42c51 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -973,6 +973,21 @@ module Session_dir =
 let () = Plugin.session_is_set_ref := Session_dir.is_set
 let () = Plugin.session_ref := Session_dir.get
 
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module Cache_dir =
+  P.Filepath
+    (struct
+      let option_name = "-cache"
+      let arg_name = "path"
+      let existence = Filepath.Indifferent
+      let file_kind = "directory"
+      let help = "directory in which cache files are stored"
+    end)
+let () = Plugin.cache_is_set_ref := Cache_dir.is_set
+let () = Plugin.cache_ref := Cache_dir.get
+
 let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
 let () = Parameter_customize.set_group saveload
 let () = Parameter_customize.do_not_projectify ()
@@ -983,11 +998,26 @@ module Config_dir =
       let arg_name = "path"
       let existence = Filepath.Indifferent
       let file_kind = "directory"
-      let help = "directory in which configuration files are searched"
+      let help = "directory in which configuration files are stored"
     end)
 let () = Plugin.config_is_set_ref := Config_dir.is_set
 let () = Plugin.config_ref := Config_dir.get
 
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.do_not_projectify ()
+module State_dir =
+  P.Filepath
+    (struct
+      let option_name = "-state"
+      let arg_name = "path"
+      let existence = Filepath.Indifferent
+      let file_kind = "directory"
+      let help = "directory in which state files are stored"
+    end)
+let () = Plugin.state_is_set_ref := State_dir.is_set
+let () = Plugin.state_ref := State_dir.get
+
 (* ************************************************************************* *)
 (** {2 Parsing} *)
 (* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 13e35743a12a0bde3dc27e575bdf4e1bcd98023d..861c22d2901f73192c4fa74c6d3c578aaeaccc1a 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -418,12 +418,22 @@ module Session_dir: Parameter_sig.Filepath
     @before 23.0-Vanadium parameter type was string instead of Filepath.
 *)
 
+module Cache_dir: Parameter_sig.Filepath
+(** Directory in which cache files are searched.
+    @since Frama-C+dev
+*)
+
 module Config_dir: Parameter_sig.Filepath
 (** Directory in which config files are searched.
     @since Neon-20140301
     @before 23.0-Vanadium parameter type was string instead of Filepath.
 *)
 
+module State_dir: Parameter_sig.Filepath
+(** Directory in which state files are searched.
+    @since Frama-C+dev
+*)
+
 (* this stop special comment does not work as expected (and as explained in the
    OCamldoc manual, Section 15.2.2. It just skips all the rest of the file
    instead of skipping until the next stop comment...
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 7d0e44b8cbdd324ad0058815a032afc5acae2a04..7731ea1766c77f69eac03207a2b103672fd9099a 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -27,8 +27,12 @@ let empty_string = ""
 let positive_debug_ref = ref 0
 let session_is_set_ref = Extlib.mk_fun "session_is_set_ref"
 let session_ref = Extlib.mk_fun "session_ref"
+let cache_is_set_ref = Extlib.mk_fun "cache_is_set_ref"
+let cache_ref = Extlib.mk_fun "cache_ref"
 let config_is_set_ref = Extlib.mk_fun "config_is_set_ref"
 let config_ref = Extlib.mk_fun "config_ref"
+let state_is_set_ref = Extlib.mk_fun "state_is_set_ref"
+let state_ref = Extlib.mk_fun "state_ref"
 
 (* ************************************************************************* *)
 (** {2 Signatures} *)
@@ -40,7 +44,9 @@ module type S_no_log = sig
   module Debug: Parameter_sig.Int
   module Share: Parameter_sig.Specific_dir
   module Session: Parameter_sig.Specific_dir
-  module Config: Parameter_sig.Specific_dir
+  module Cache_dir () : Parameter_sig.Specific_dir
+  module Config_dir () : Parameter_sig.Specific_dir
+  module State_dir () : Parameter_sig.Specific_dir
   val help: Cmdline.Group.t
   val messages: Cmdline.Group.t
   val add_plugin_output_aliases:
@@ -82,8 +88,12 @@ let is_share_visible () = share_visible_ref := true
 let session_visible_ref = ref false
 let is_session_visible () = session_visible_ref := true
 
+let cache_visible_ref = ref false
+let is_cache_visible () = cache_visible_ref := true
 let config_visible_ref = ref false
 let is_config_visible () = config_visible_ref := true
+let state_visible_ref = ref false
+let is_state_visible () = state_visible_ref := true
 
 let plugin_subpath_ref = ref None
 let plugin_subpath s = plugin_subpath_ref := Some s
@@ -94,7 +104,9 @@ let reset_plugin () =
   kernel := false;
   share_visible_ref := false;
   session_visible_ref := false;
+  cache_visible_ref := false;
   config_visible_ref := false;
+  state_visible_ref := false;
   plugin_subpath_ref := None;
   default_msg_keys_ref := [];
 ;;
@@ -466,36 +478,61 @@ struct
         let visible_ref = !session_visible_ref
       end)
 
-  module Config =
-    Make_specific_dir
+  module type User_dir_input = sig
+    val name: string
+    val getter: unit -> Fc_Filepath.Normalized.t
+    val visible_ref: bool ref
+    val kernel_get: unit -> Fc_Filepath.Normalized.t
+    val kernel_is_set: unit -> bool
+  end
+
+  module User_dir (I: User_dir_input) = struct
+    include Make_specific_dir
+        (struct
+          let option_name = I.name
+          let arg_name = "dir"
+          let help = Format.asprintf
+              "set the plug-in %s directory to <dir> \
+               (may be used on systems with no default user directory)"
+              I.name
+        end)
+        (struct
+          let dirs () = [
+            let var = "FRAMAC_" ^ (Stdlib.String.uppercase_ascii I.name) in
+            if I.kernel_is_set () then I.kernel_get ()
+            else match Sys.getenv_opt var with
+              | Some p when p <> "" -> Fc_Filepath.Normalized.of_string p
+              | _ -> I.getter ()
+          ]
+          let visible_ref = !I.visible_ref
+        end)
+  end
+
+  module Cache_dir () = User_dir
       (struct
-        let option_name = "config"
-        let arg_name = "dir"
-        let help = "set the plug-in config directory to <dir> \
-                    (may be used on systems with no default user directory)"
+        let name = "cache"
+        let getter = System_config.User_dirs.cache
+        let visible_ref = cache_visible_ref
+        let kernel_get () = !cache_ref ()
+        let kernel_is_set () = !cache_is_set_ref ()
       end)
+
+  module Config_dir () = User_dir
       (struct
-        let dirs () = [
-          let to_path = Fc_Filepath.Normalized.of_string in
-          let d, vis =
-            if !config_is_set_ref () then !config_ref (), false
-            else
-              try to_path (Sys.getenv "FRAMAC_CONFIG"), false
-              with Not_found ->
-              try to_path (Sys.getenv "USERPROFILE"), false (* Win32 *)
-              with Not_found ->
-              (* Unix like *)
-              try to_path (Sys.getenv "XDG_CONFIG_HOME"), true
-              with Not_found ->
-              try
-                Fc_Filepath.Normalized.concat
-                  (to_path (Sys.getenv "HOME")) ".config", true
-              with Not_found -> to_path ".", false
-          in
-          Fc_Filepath.Normalized.concat
-            d (if vis then "frama-c" else ".frama-c")
-        ]
-        let visible_ref = !config_visible_ref
+        let name = "config"
+        let getter = System_config.User_dirs.config
+        let visible_ref = config_visible_ref
+        let kernel_get () = !config_ref ()
+        let kernel_is_set () = !config_is_set_ref ()
+      end)
+
+  module State_dir () = User_dir
+      (struct
+        let name = "state"
+        let getter = System_config.User_dirs.state
+        let visible_ref = state_visible_ref
+        let kernel_get () = !state_ref ()
+        let kernel_is_set () = !state_is_set_ref ()
       end)
 
   let help = add_group "Getting Information"
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 887bdc5befc77e2ff76837694e78a33d6a24b97f..58f69a3f5541f8a2b7ef7ff52b11db2d0508d4ea 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -51,9 +51,21 @@ module type S_no_log = sig
       @since Neon-20140301 *)
   module Session: Parameter_sig.Specific_dir
 
+  (** Handle the specific `cache' directory of the plug-in.
+      @since Frama-C+dev
+  *)
+  module Cache_dir (): Parameter_sig.Specific_dir
+
   (** Handle the specific `config' directory of the plug-in.
-      @since Neon-20140301 *)
-  module Config: Parameter_sig.Specific_dir
+      @since Neon-20140301
+      @before Frama-C+dev this was not a functor
+  *)
+  module Config_dir (): Parameter_sig.Specific_dir
+
+  (** Handle the specific `state' directory of the plug-in.
+      @since Frama-C+dev
+  *)
+  module State_dir (): Parameter_sig.Specific_dir
 
   val help: Cmdline.Group.t
   (** The group containing option -*-help.
@@ -131,8 +143,18 @@ val is_session_visible: unit -> unit
     To be called just before applying {!Register} to create plug-in services.
     @since Neon-20140301 *)
 
+val is_cache_visible: unit -> unit
+(** Make visible to the end-user the -<plug-in>-cache-dir option.
+    To be called just before applying {!Register} to create plug-in services.
+    @since Neon-20140301 *)
+
 val is_config_visible: unit -> unit
-(** Make visible to the end-user the -<plug-in>-config option.
+(** Make visible to the end-user the -<plug-in>-config-dir option.
+    To be called just before applying {!Register} to create plug-in services.
+    @since Neon-20140301 *)
+
+val is_state_visible: unit -> unit
+(** Make visible to the end-user the -<plug-in>-state-dir option.
     To be called just before applying {!Register} to create plug-in services.
     @since Neon-20140301 *)
 
@@ -178,9 +200,15 @@ val positive_debug_ref: int ref
 val session_is_set_ref: (unit -> bool) ref
 val session_ref: (unit -> Filepath.Normalized.t) ref
 
+val cache_is_set_ref: (unit -> bool) ref
+val cache_ref: (unit -> Filepath.Normalized.t) ref
+
 val config_is_set_ref: (unit -> bool) ref
 val config_ref: (unit -> Filepath.Normalized.t) ref
 
+val state_is_set_ref: (unit -> bool) ref
+val state_ref: (unit -> Filepath.Normalized.t) ref
+
 (**/**)
 
 (*
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 9879790fff9578c6b4aecf115d7ddc7262e7527a..8a62282176800b1a76e1432543bd0e199de55c43 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -48,7 +48,7 @@ let framac_logo, framac_icon =
 module Configuration = struct
   include Cilconfig
   let configuration_file () =
-    Gui_parameters.Config.get_file ~mode:`Create_path "frama-c-gui.config"
+    Gui_parameters.Config_dir.get_file ~mode:`Create_path "frama-c-gui.config"
   let load () = loadConfiguration (configuration_file ())
   let save () = saveConfiguration (configuration_file ())
   let reset () = Extlib.safe_remove (configuration_file () :> string);
diff --git a/src/plugins/gui/gui_parameters.ml b/src/plugins/gui/gui_parameters.ml
index 70882c2143ae26620c0dfb60a8e94b116ef114a1..4284fb0a1a6a12e0f1bc0330ac99c7c459bad446 100644
--- a/src/plugins/gui/gui_parameters.ml
+++ b/src/plugins/gui/gui_parameters.ml
@@ -28,6 +28,8 @@ include Plugin.Register
       let help = "Graphical User Interface"
     end)
 
+module Config_dir = Config_dir ()
+
 let () = Parameter_customize.do_not_projectify ()
 module Project_name =
   Empty_string
diff --git a/src/plugins/gui/gui_parameters.mli b/src/plugins/gui/gui_parameters.mli
index ecc785aeda042a503c414c139ff8c92ec2d89e3a..2c665e2dc1bcb2c7d3e822bf270a48227a767c58 100644
--- a/src/plugins/gui/gui_parameters.mli
+++ b/src/plugins/gui/gui_parameters.mli
@@ -24,6 +24,8 @@
 
 include Plugin.S
 
+module Config_dir : Parameter_sig.Specific_dir
+
 module Project_name: Parameter_sig.String
 (** Option -gui-project. *)