diff --git a/share/dune b/share/dune
index a28032dc9b9e3a45dc4eaae9b561fb7e899591ac..103579ad676118526fe1fe5a9f1e23cc34d66fd8 100644
--- a/share/dune
+++ b/share/dune
@@ -332,15 +332,15 @@
  (package frama-c)
  (section share)
  (files
-  (machdeps/machdep_avr_16.json as share/machdeps/machdep_avr_16.json)
-  (machdeps/machdep_x86_16.json as share/machdeps/machdep_x86_16.json)
-  (machdeps/machdep_x86_32.json as share/machdeps/machdep_x86_32.json)
-  (machdeps/machdep_x86_64.json as share/machdeps/machdep_x86_64.json)
-  (machdeps/machdep_gcc_x86_16.json as share/machdeps/machdep_gcc_x86_16.json)
-  (machdeps/machdep_gcc_x86_32.json as share/machdeps/machdep_gcc_x86_32.json)
-  (machdeps/machdep_gcc_x86_64.json as share/machdeps/machdep_gcc_x86_64.json)
-  (machdeps/machdep_msvc_x86_64.json as share/machdeps/machdep_msvc_x86_64.json)
-  (machdeps/machdep_ppc_32.json as share/machdeps/machdep_ppc_32.json))
+  (machdeps/machdep_avr_16.yaml as share/machdeps/machdep_avr_16.yaml)
+  (machdeps/machdep_x86_16.yaml as share/machdeps/machdep_x86_16.yaml)
+  (machdeps/machdep_x86_32.yaml as share/machdeps/machdep_x86_32.yaml)
+  (machdeps/machdep_x86_64.yaml as share/machdeps/machdep_x86_64.yaml)
+  (machdeps/machdep_gcc_x86_16.yaml as share/machdeps/machdep_gcc_x86_16.yaml)
+  (machdeps/machdep_gcc_x86_32.yaml as share/machdeps/machdep_gcc_x86_32.yaml)
+  (machdeps/machdep_gcc_x86_64.yaml as share/machdeps/machdep_gcc_x86_64.yaml)
+  (machdeps/machdep_msvc_x86_64.yaml as share/machdeps/machdep_msvc_x86_64.yaml)
+  (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml))
 )
 
 ; machdep generation script
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..c3bf0e5f4e01c82aa2ad33f242c501ac1ea301e6
--- /dev/null
+++ b/share/machdeps/machdep-schema.yaml
@@ -0,0 +1,193 @@
+# Schema for use with kwalify tool https://pykwalify.readthedocs.io/
+
+alignof_aligned:
+
+  # alignment of a type with 'aligned' attribute
+
+  type: integer
+
+alignof_double:
+
+  # alignment of 'double' type
+
+  type: integer
+
+alignof_float:
+
+  # alignment of 'float' type
+
+  type: integer
+
+alignof_fun:
+
+  # (non-standard) alignment of a function type. Negative if unsupported
+
+  type: integer
+
+alignof_int:
+
+  #  alignment of 'int' type
+
+  type: integer
+
+alignof_long:
+
+  #  alignment of 'long' type
+
+  type: integer
+
+alignof_longdouble:
+
+  #  alignment of 'long double' type
+
+  type: integer
+
+alignof_longlong:
+
+  #  alignment of 'long long' type
+
+  type: integer
+
+alignof_ptr:
+
+  #  alignment of 'void*' type
+
+  type: integer
+
+alignof_short:
+
+  #  alignment of 'short' type
+
+  type: integer
+
+alignof_string:
+
+  #  alignment of string
+
+  type: integer
+
+alignof_void:
+
+  #  (non-standard) alignment of 'void' type. Negative if unsupported
+
+  type: integer
+
+char_is_unsigned:
+
+  #  whether 'char' is unsigned
+
+  type: boolean
+
+compiler:
+
+  #  compiler being used
+
+  type: string
+
+cpp_arch_flags:
+
+  # arguments to be given to the compiler when this machdep is selected
+
+  # (e.g. '-m32')
+
+  type: list
+
+  items:
+
+    - type: string
+
+has__builtin_va_list:
+
+  #  Whether '__builtin_va_list' is a known type
+
+  type: boolean
+
+little_endian:
+
+  #  whether the architecture is little-endian
+
+  type: boolean
+
+ptr_diff_t:
+
+  #  definition of 'ptrdiff_t'
+
+  type: string
+
+size_t:
+
+  #  type of 'sizeof e'
+
+  type: string
+
+sizeof_double:
+
+  #  size of 'double' type
+
+  type: integer
+
+sizeof_float:
+
+  #  size of 'float' type
+
+  type: integer
+
+sizeof_fun:
+
+  #  (non-standard) size of a function type. Negative if unsupported
+
+  type: integer
+
+sizeof_int:
+
+  #  size of 'int' type
+
+  type: integer
+
+sizeof_long:
+
+  #  size of 'long' type
+
+  type: integer
+
+sizeof_longdouble:
+
+  #  size of 'long double' type
+
+  type: integer
+
+sizeof_longlong:
+
+  #  size of 'long long' type
+
+  type: integer
+
+sizeof_ptr:
+
+  #  size of 'void*' type
+
+  type: integer
+
+sizeof_short:
+
+  #  size of 'short' type
+
+  type: integer
+
+sizeof_void:
+
+  #  (non-standard) size of 'void' type. Negative if unsupported
+
+  type: integer
+
+version:
+
+  #  information on this machdep
+
+  type: string
+
+wchar_t:
+
+  #  definition of 'wchar_t'
+
+  type: string
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..fdfbf0d6c9f014fab7e7fabe93931cc6de5d026c
--- /dev/null
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -0,0 +1,33 @@
+alignof_aligned: 1
+alignof_double: 1
+alignof_float: 1
+alignof_fun: 4
+alignof_int: 1
+alignof_long: 1
+alignof_longdouble: 1
+alignof_longlong: 1
+alignof_ptr: 1
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: clang
+cpp_arch_flags:
+- -target
+- avr
+- -m16
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 4
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 2
+sizeof_long: 4
+sizeof_longdouble: 4
+sizeof_longlong: 8
+sizeof_ptr: 2
+sizeof_short: 2
+sizeof_void: 1
+version: clang version 15.0.7
+wchar_t: int
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..7dc8c9fe44601e43fd43ef584880fd614fcff7d5
--- /dev/null
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 8
+alignof_double: 8
+alignof_float: 2
+alignof_fun: 1
+alignof_int: 2
+alignof_long: 4
+alignof_longdouble: 16
+alignof_longlong: 4
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: gcc
+cpp_arch_flags:
+- -m16
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 2
+sizeof_long: 4
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: 1
+version: none
+wchar_t: int
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..e98f9707ad177626f2e6ae0edaaf882cfe7a4ec5
--- /dev/null
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 16
+alignof_double: 4
+alignof_float: 4
+alignof_fun: 1
+alignof_int: 4
+alignof_long: 4
+alignof_longdouble: 4
+alignof_longlong: 4
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: gcc
+cpp_arch_flags:
+- -m32
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 4
+sizeof_long: 4
+sizeof_longdouble: 12
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: 1
+version: gcc (GCC) 12.2.1 20230201
+wchar_t: long
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..cfc63451a76827b077dcbdf30555ace7360c2adb
--- /dev/null
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 16
+alignof_double: 8
+alignof_float: 4
+alignof_fun: 1
+alignof_int: 4
+alignof_long: 8
+alignof_longdouble: 16
+alignof_longlong: 8
+alignof_ptr: 8
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: gcc
+cpp_arch_flags:
+- -m64
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: long
+size_t: unsigned long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 4
+sizeof_long: 8
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 8
+sizeof_short: 2
+sizeof_void: 1
+version: gcc (GCC) 12.2.1 20230201
+wchar_t: int
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..73c60421095eb21a9eff6043c95d6845dca818e8
--- /dev/null
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 1
+alignof_double: 8
+alignof_float: 4
+alignof_fun: -1
+alignof_int: 4
+alignof_long: 4
+alignof_longdouble: 8
+alignof_longlong: 8
+alignof_ptr: 8
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: msvc
+cpp_arch_flags:
+- -m64
+has__builtin_va_list: false
+little_endian: true
+ptrdiff_t: long long
+size_t: unsigned long long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: -1
+sizeof_int: 4
+sizeof_long: 4
+sizeof_longdouble: 8
+sizeof_longlong: 8
+sizeof_ptr: 8
+sizeof_short: 2
+sizeof_void: 0
+version: MSVC - X86-64bits mode
+wchar_t: unsigned short
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..43a2779dbd18ac600b588b595cb83bc5cb366c2f
--- /dev/null
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -0,0 +1,33 @@
+alignof_aligned: 16
+alignof_double: 8
+alignof_float: 4
+alignof_fun: 4
+alignof_int: 4
+alignof_long: 4
+alignof_longdouble: 16
+alignof_longlong: 8
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: true
+compiler: clang
+cpp_arch_flags:
+- -target
+- powerpc-apple-linux
+- -mcpu=603
+has__builtin_va_list: true
+little_endian: false
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 4
+sizeof_long: 4
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: 1
+version: clang version 15.0.7
+wchar_t: int
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..a139bf041da3d84a6c60c7cdf93aa63efdb29c0b
--- /dev/null
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 8
+alignof_double: 8
+alignof_float: 2
+alignof_fun: -1
+alignof_int: 2
+alignof_long: 4
+alignof_longdouble: 16
+alignof_longlong: 4
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: generic
+cpp_arch_flags:
+- -m16
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: -1
+sizeof_int: 2
+sizeof_long: 4
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: -1
+version: none
+wchar_t: int
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..df6493927a4e87573387d8d2ee23bf8bc3770847
--- /dev/null
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 16
+alignof_double: 4
+alignof_float: 4
+alignof_fun: -1
+alignof_int: 4
+alignof_long: 4
+alignof_longdouble: 4
+alignof_longlong: 4
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: generic
+cpp_arch_flags:
+- -m32
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+size_t: unsigned int
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: -1
+sizeof_int: 4
+sizeof_long: 4
+sizeof_longdouble: 12
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: -1
+version: gcc (GCC) 12.2.1 20230201
+wchar_t: long
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..6ab3b343b0fcbf88fd80f5936b33621aadb2631f
--- /dev/null
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -0,0 +1,31 @@
+alignof_aligned: 16
+alignof_double: 8
+alignof_float: 4
+alignof_fun: -1
+alignof_int: 4
+alignof_long: 8
+alignof_longdouble: 16
+alignof_longlong: 8
+alignof_ptr: 8
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: generic
+cpp_arch_flags:
+- -m64
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: long
+size_t: unsigned long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: -1
+sizeof_int: 4
+sizeof_long: 8
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 8
+sizeof_short: 2
+sizeof_void: -1
+version: clang version 15.0.7
+wchar_t: int
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index a4295c73770aa3338c201382bfa591a4217eea15..fe84a770ce45ec0d75b63cd2c7cc666178ab811d 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -22,35 +22,24 @@
 ##########################################################################
 
 """
-Produces a machdep.ml file for a given architecture.
+Produces a machdep.yaml file for a given architecture.
 
 Prerequisites:
 
 - A C11-compatible (cross-)compiler (with support for _Generic),
-  or a (cross-)compiler having __builtin_types_compatible_p
-
 - A (cross-)compiler supporting _Static_assert
 - A (cross-)compiler supporting _Alignof or alignof
 
-- objdump
-
-This script tries to compile several source files into object files,
-then uses objdump to extract information from the compilation.
-
-We want to obtain values produced by the compiler.
-In an ideal scenario, we are able to execute the binary, so we can just use
-printf(). However, when cross-compiling, we may be unable to run the program.
-Even worse, we may lack a proper runtime, and thus simply obtaining an
-executable may be impossible.
-However, we don't really need it: having an object file (with symbols) is
-usually enough.
+This script tries to compile several source files to extract the
+information we need in terms of sizeof, alignof and representation
+of the various types defined by the standard (e.g. size_t, wchar_t, ...)
 
-Compilation is split in several files because, for non-standard constructions,
-some compilers (e.g. CompCert) may fail to parse them. We must detect these
-cases and output warnings, but without preventing compilation of the rest.
+In case some values are not identified, the YAML format can be edited
+by hand afterwards.
 """
 
 import argparse
+import yaml
 import json
 from pathlib import Path
 import re
@@ -72,13 +61,13 @@ parser.add_argument(
 
 parser.add_argument(
     "--from-file",
-    help="reads compiler and arch flags from existing json file. Use -i to update it in place",
+    help="reads compiler and arch flags from existing yaml file. Use -i to update it in place",
 )
 parser.add_argument(
     "-i",
     "--in-place",
     action="store_true",
-    help="when reading compiler config from json, update the file in place. unused otherwise",
+    help="when reading compiler config from yaml, update the file in place. unused otherwise",
 )
 
 parser.add_argument(
@@ -104,10 +93,10 @@ if not args.compiler_flags:
 
 if args.from_file:
     orig_file = open(args.from_file, "r")
-    orig_machdep = json.load(orig_file)
+    orig_machdep = yaml.safe_load(orig_file)
     orig_file.close()
     if not "compiler" in orig_machdep or not "cpp_arch_flags" in orig_machdep:
-        raise Exception("Missing fields in json file")
+        raise Exception("Missing fields in yaml file")
     args.compiler = orig_machdep["compiler"]
     if isinstance(orig_machdep["cpp_arch_flags"], list):
         args.cpp_arch_flags = orig_machdep["cpp_arch_flags"]
@@ -118,7 +107,7 @@ if args.from_file:
 def print_machdep(machdep):
     if args.in_place:
         args.dest_file = open(args.from_file, "w")
-    json.dump(machdep, args.dest_file, indent=4, sort_keys=True)
+    yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
     # Python does not end the dump with a newline by itself
     args.dest_file.write("\n")
 
diff --git a/src/dune b/src/dune
index 30b7a156d889e7732ca1fbd3ae1788f6318b9315..599d3f7423ac6a0e1daba6de1ea8c204345e76e3 100644
--- a/src/dune
+++ b/src/dune
@@ -32,12 +32,14 @@
           (echo "  - dynlink:" %{lib-available:dynlink} "\n")
           (echo "  - bytes:" %{lib-available:bytes} "\n")
           (echo "  - yojson:" %{lib-available:yojson} "\n")
+          (echo "  - yaml.unix:" %{lib-available:yaml.unix} "\n")
+          (echo "  - fpath:" %{lib-available:fpath} "\n")
           (echo "  - menhirLib:" %{lib-available:menhirLib} "\n")
           (echo "  - dune-site:" %{lib-available:dune-site} "\n")
           (echo "  - dune-site.plugins:" %{lib-available:dune-site.plugins} "\n")
           (echo "  - ppx_import:" %{lib-available:ppx_import} "\n")
           (echo "  - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
-          (echo "  - ppx_deriving_yojson:" %{lib-available:ppx_deriving_yojson} "\n")
+          (echo "  - ppx_deriving_yaml:" %{lib-available:ppx_deriving_yaml} "\n")
   )
   )
 )
@@ -47,9 +49,9 @@
   (public_name frama-c.kernel)
   (foreign_stubs (language c) (names c_bindings))
   (flags :standard -w -9)
-  (libraries frama-c.init str unix zarith ocamlgraph dynlink bytes yojson menhirLib dune-site dune-site.plugins)
+  (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins)
   (instrumentation (backend landmarks))
-  (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving_yojson))
+  (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving_yaml))
 )
 
 (generate_sites_module (module config_data) (sites frama-c) (plugins (frama-c plugins) (frama-c plugins_gui)))
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 54a324407c6554d55cc8539849edb1d2cfd1b42a..6ee4c8d90eb2d6adee171537fad6869f849da191 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -316,10 +316,10 @@ module CustomMachdeps =
 
 let machdep_dir () = Kernel.Share.get_dir ~mode:`Must_exist "machdeps"
 
-let regexp_machdep = Str.regexp "^machdep_\\([^.]*\\).json$"
+let regexp_machdep = Str.regexp "^machdep_\\([^.]*\\).yaml$"
 
 let default_machdep_file machdep =
-  let filename = "machdep_" ^ machdep ^ ".json" in
+  let filename = "machdep_" ^ machdep ^ ".yaml" in
   Filepath.Normalized.concat (machdep_dir()) filename
 
 let is_default_machdep machdep =
@@ -368,7 +368,7 @@ let set_machdep () =
 
 let () = Cmdline.run_after_configuring_stage set_machdep
 
-type mach = [%import: Cil_types.mach] [@@deriving of_yojson]
+type mach = [%import: Cil_types.mach] [@@deriving yaml]
 
 (* Local to this module. Use Cil.theMachine.theMachine outside *)
 let get_machdep () =
@@ -380,11 +380,14 @@ let get_machdep () =
       if is_default_machdep m then default_machdep_file m
       else Filepath.Normalized.of_string ~existence:Must_exist m
     in
-    match
-      mach_of_yojson (Yojson.Safe.from_file (file:>string))
-    with
+    let res =
+      Result.bind
+        (Yaml_unix.of_file (Fpath.v (file:>string)))
+        mach_of_yaml
+    in
+    match res with
     | Ok machdep -> machdep
-    | Error s ->
+    | Error (`Msg s) ->
       Kernel.fatal "Error during machdep parsing: %s" s
 
 let list_available_machdeps () =