diff --git a/share/libc/limits.h b/share/libc/limits.h
index 40e674b2b6d78b2d22cd2f7bac416809e8fba3a3..b5c0bb1ab2788b06ef2b9ffaff1b5b310d4f08ab 100644
--- a/share/libc/limits.h
+++ b/share/libc/limits.h
@@ -76,30 +76,10 @@
 /* Maximum value an `unsigned long long int' can hold.  (Minimum is 0.)  */
 #   define ULLONG_MAX	__FC_ULLONG_MAX
 
-/* Maximum number of bytes in a pathname, including the terminating
-   null character. (Minimum is 256.) */
-#define PATH_MAX  __FC_PATH_MAX
-
-/* Maximum length of a host name (not including the terminating null)
-   as returned from the gethostname() function.
-   Note: Mac OS does not define this constant. */
-#define HOST_NAME_MAX __FC_HOST_NAME_MAX
-
-/* Maximum length of a terminal device name. */
-#define TTY_NAME_MAX __FC_TTY_NAME_MAX
-
-/* Maximum length of argument to the exec functions including environment data.
-   Minimum Acceptable Value: {_POSIX_ARG_MAX} (4096 in POSIX.1-2008)
-   "... the total space used to store the environment and the arguments to the
-    process is limited to {ARG_MAX} bytes."
- */
-#define ARG_MAX 4096
-
-// POSIX; used by <sys/uio.h>.
-// Must be >= _XOPEN_IOV_MAX, which is 16.
-// 1024 is the value used by some Linux implementations.
-#define IOV_MAX 1024
+// POSIX-specific definitions
+#ifdef __FC_POSIX_VERSION
 
+/*** Most restrictive values for the constants below, as mandated by POSIX */
 
 // Maximum Values
 
@@ -166,4 +146,82 @@
 #define NL_TEXTMAX _POSIX2_LINE_MAX
 #define NZERO 20
 
+/*** POSIX constants. Frama-C usually takes Linux' values by default, but
+     it can be overloaded by passing e.g. `-cpp-extra-args="-D__FC_XXXX=nnnn"`
+     on Frama-C's command line. A value of -1 will deactivate the macro (all of
+     them are optional).
+*/
+#define STR(S) # S
+#define expand(macro) STR(macro)
+
+/* Maximum number of bytes in a pathname, including the terminating
+   null character. (Minimum is 256.) */
+#ifdef __FC_PATH_MAX
+#  if __FC_PATH_MAX >= 0
+      _Static_assert(__FC_PATH_MAX >=_POSIX_PATH_MAX, "__FC_PATH_MAX is too small (" expand(__FC_PATH_MAX) "): minimal value is "expand( _POSIX_PATH_MAX));
+#      define PATH_MAX __FC_PATH_MAX
+#  else
+#    undef PATH_MAX
+#  endif
+#else
+#  define PATH_MAX  4096
+#endif
+
+/* Maximum length of a host name (not including the terminating null)
+   as returned from the gethostname() function.
+   Note: Mac OS does not define this constant. 
+*/
+#ifdef __FC_HOST_NAME_MAX
+#  if __FC_HOST_NAME_MAX >= 0
+     _Static_assert(__FC_HOST_NAME_MAX >=_POSIX_HOST_NAME_MAX, "__FC_HOST_NAME_MAX is too small (" expand(__FC_HOST_NAME_MAX) "): minimal value is " expand(_POSIX_HOST_NAME_MAX));
+#    define HOST_NAME_MAX __FC_HOST_NAME_MAX
+#  else
+#    undef HOST_NAME_MAX
+#  endif
+#else
+#  define HOST_NAME_MAX 255
+#endif
+
+/* Maximum length of a terminal device name. */
+#ifdef __FC_TTY_NAME_MAX
+#  if __FC_TTY_NAME_MAX >= 0
+     _Static_assert(__FC_HOST_NAME_MAX >=_POSIX_TTY_NAME_MAX, "__FC_TTY_NAME_MAX is too small (" expand(__FC_TTY_NAME_MAX) "): minimal value is " expand(_POSIX_TTY_NAME_MAX));
+#    define TTY_NAME_MAX __FC_TTY_NAME_MAX
+#  else
+#    undef TTY_NAME_MAX
+#  endif
+#else
+#  define TTY_NAME_MAX 9
+#endif
+
+/* Maximum length of argument to the exec functions including environment data.
+   Minimum Acceptable Value: {_POSIX_ARG_MAX} (4096 in POSIX.1-2008)
+   "... the total space used to store the environment and the arguments to the
+    process is limited to {ARG_MAX} bytes."
+ */
+#ifdef __FC_ARG_NAME_MAX
+#  if __FC_ARG_MAX >= 0
+     _Static_assert(__FC_ARG_MAX >=_POSIX_ARG_MAX, "__FC_ARG_MAX is too small (" expand(__FC_ARG_MAX) "): minimal value is " expand(__POSIX_ARG_MAX));
+#    define ARG_MAX __FC_ARG_MAX
+#  else
+#    undef ARG_MAX
+#  endif
+#else
+#  define ARG_MAX 4096
+#endif
+
+// POSIX; used by <sys/uio.h>.
+// Must be >= _XOPEN_IOV_MAX, which is 16.
+#ifdef __FC_IOV_MAX
+#  if __FC_IOV_MAX >= 0
+     _Static_assert(__FC_IOV_MAX >=_XOPEN_IOV_MAX, "__FC_IOV_MAX is too small (" expand(__FC_IOV_MAX) "): minimal value is " expand(_XOPEN_IOV_MAX));
+#    define IOV_MAX __FC_IOV_MAX
+#  else
+#    undef IOV_MAX
+#  endif
+#else
+#  define IOV_MAX 255
+#endif
+
+#endif // __FC_POSIX_VERSION
 #endif
diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
index 1b7168a5e94261fe8235f9feeeff1b0e3b7a30fb..3a71d5b18f210b0094de91e58a3ec57a9881b2cc 100644
--- a/share/machdeps/Makefile
+++ b/share/machdeps/Makefile
@@ -26,7 +26,7 @@ machdep_avr_16.yaml \
 machdep_gcc_x86_32.yaml \
 machdep_gcc_x86_64.yaml \
 machdep_ppc_32.yaml : \
-%.yaml: machdep-schema.yaml make_machdep/make_machdep.py
+%.yaml: machdep-schema.yaml make_machdep/make_machdep.py make_machdep/*.c
 	@./make_machdep/make_machdep.py -i --from-file $@ --check
 
 machdep_x86_16.yaml machdep_x86_32.yaml machdep_x86_64.yaml: \
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 3b0ea4d4f2b435c4be0c693f914b75b60bfea767..0d4b2f34d58af18ed677c59a1c28d3a5f8ed644c 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -66,6 +66,12 @@ alignof_str:
 
   type: integer
 
+bufsiz:
+
+  description: value of 'BUFSIZ' macro
+
+  type: string
+
 char_is_unsigned:
 
   description:  whether 'char' is unsigned
@@ -90,6 +96,24 @@ cpp_arch_flags:
 
     - type: string
 
+eof:
+
+  description: value of 'EOF' macro
+
+  type: string
+
+filename_max:
+
+  description: value of 'FILENAME_MAX' macro
+
+  type: string
+
+fopen_max:
+
+  description: value of 'FOPEN_MAX' macro
+
+  type: string
+
 has__builtin_va_list:
 
   description:  Whether '__builtin_va_list' is a known type
@@ -101,12 +125,24 @@ intptr_t:
 
   type: string
 
+l_tmpnam:
+
+  description: value of 'L_tmpnam' macro
+
+  type: string
+
 little_endian:
 
   description:  whether the architecture is little-endian
 
   type: boolean
 
+mb_cur_max:
+
+  description: expansion of 'MB_CUR_MAX' macro
+
+  type: string
+
 posix_version:
   description: |
     value of the macro '_POSIX_VERSION'
@@ -118,6 +154,12 @@ ptrdiff_t:
 
   type: string
 
+rand_max:
+
+  description: expansion of 'RAND_MAX' macro
+
+  type: string
+
 size_t:
 
   description:  type of 'sizeof e'
@@ -190,6 +232,12 @@ ssize_t:
 
   type: string
 
+tmp_max:
+
+  description: value of 'TMP_MAX' macro
+
+  type: string
+
 uintptr_t:
 
   description: definition of 'uintptr_t'
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index 6f2e4bec15efadc003195b32be626e952b338816..3a32f6fad473cf57727a6c7c31076473dff807cb 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -9,17 +9,24 @@ alignof_longlong: 1
 alignof_ptr: 1
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: false
 compiler: clang
 cpp_arch_flags:
 - -target
 - avr
 - -m16
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: int
+l_tmpnam: '20'
 little_endian: true
+mb_cur_max: ((size_t)16)
 posix_version: 200809L
 ptrdiff_t: int
+rand_max: '2147483647'
 size_t: unsigned int
 sizeof_double: 4
 sizeof_float: 4
@@ -32,6 +39,7 @@ sizeof_ptr: 2
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+tmp_max: '238328'
 uintptr_t: unsigned int
 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
index 007ce9e7d3f756b07184a196220d0a427e5624e6..f538eb0df63193ae59d0f766306178203e1249b1 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -36,3 +36,11 @@ weof: (0xffffffffUL)
 wint_t: unsigned long
 wordsize: '16'
 posix_version: '200809L'
+bufsiz: '8192'
+eof: '(-1)'
+fopen_max: '16'
+filename_max: '2048'
+l_tmpnam: '2048'
+tmp_max: '0xFFFFFFFF'
+rand_max: '32767'
+mb_cur_max: '((size_t)16)'
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index ed625f542ebebc90635088f0c61efc979de956cf..8ccb3952e2c95094d578b8036768c3d6e397c08c 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -9,15 +9,22 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: false
 compiler: gcc
 cpp_arch_flags:
 - -m32
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: int
+l_tmpnam: '20'
 little_endian: true
+mb_cur_max: ((size_t) 16 )
 posix_version: 200809L
 ptrdiff_t: int
+rand_max: '2147483647'
 size_t: unsigned int
 sizeof_double: 8
 sizeof_float: 4
@@ -30,6 +37,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+tmp_max: '238328'
 uintptr_t: unsigned int
 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
index b3b1c4b03b30fd7688e5f2259cf6e2bc11e95ae6..39f935901bc56f8d9e6ccaa002a4376144ecbaf1 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -9,15 +9,22 @@ alignof_longlong: 8
 alignof_ptr: 8
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: false
 compiler: gcc
 cpp_arch_flags:
 - -m64
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: long
+l_tmpnam: '20'
 little_endian: true
+mb_cur_max: ((size_t) 16 )
 posix_version: 200809L
 ptrdiff_t: long
+rand_max: '2147483647'
 size_t: unsigned long
 sizeof_double: 8
 sizeof_float: 4
@@ -30,6 +37,7 @@ sizeof_ptr: 8
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: long
+tmp_max: '238328'
 uintptr_t: unsigned long
 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
index c0d9ec1d73af5cf6deb15c1bd953aa7f318ae446..ba58f4d8eace71b8fff6f7879e2f3ad271e58d36 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -36,3 +36,14 @@ weof: (0xffffU)
 wint_t: unsigned short
 wordsize: '64'
 posix_version: ''
+# NB: except for l_tmpnam, the corresponding macro are not defined in the old
+# __fc_machdep.h in the MSVC_X86_64 section. The values below have thus been 
+# taken from gnu
+bufsiz: '8192'
+eof: '(-1)'
+fopen_max: '16'
+filename_max: '2048'
+l_tmpnam: '20'
+tmp_max: '0xFFFFFFFF'
+rand_max: 32767
+mb_cur_max: '((size_t)16)'
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 4f309f9155cd95048d7bd796cad81f696314b2cd..244a3c3874dea50d65c592e3b154f7901f153b5b 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -9,17 +9,24 @@ alignof_longlong: 8
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: true
 compiler: clang
 cpp_arch_flags:
 - -target
 - powerpc-apple-linux
 - -mcpu=603
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: int
+l_tmpnam: '20'
 little_endian: false
+mb_cur_max: ((size_t)16)
 posix_version: 200809L
 ptrdiff_t: int
+rand_max: '2147483647'
 size_t: unsigned int
 sizeof_double: 8
 sizeof_float: 4
@@ -32,6 +39,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+tmp_max: '238328'
 uintptr_t: unsigned int
 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
index 8d417a3b9e11e8a1762318b7fc3179ec5fa81b76..33be991a565ebb04c0640683a93e1909a47ad1b2 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -36,3 +36,11 @@ weof: (0xffffffffUL)
 wint_t: unsigned long
 wordsize: '16'
 posix_version: '200809L'
+bufsiz: '8192'
+eof: '(-1)'
+fopen_max: '16'
+filename_max: '2048'
+l_tmpnam: '2048'
+tmp_max: '0xFFFFFFFF'
+rand_max: '32767'
+mb_cur_max: '((size_t)16)'
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index ed6a4c8423e8a8bb6103b3559c5fe574308816e5..154475ce0fabb9bec55040ab20a0ee9b7de26a59 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -9,15 +9,22 @@ alignof_longlong: 4
 alignof_ptr: 4
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: false
 compiler: generic
 cpp_arch_flags:
 - -m32
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: int
+l_tmpnam: '20'
 little_endian: true
+mb_cur_max: ((size_t) 16 )
 posix_version: 200809L
 ptrdiff_t: int
+rand_max: '2147483647'
 size_t: unsigned int
 sizeof_double: 8
 sizeof_float: 4
@@ -30,6 +37,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: -1
 ssize_t: int
+tmp_max: '238328'
 uintptr_t: unsigned int
 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
index 5e322f71b455002d6341a5b6491a82f52b383aad..dcb294278cf8f21ae6868081c48cb5015f74b6e7 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -9,15 +9,22 @@ alignof_longlong: 8
 alignof_ptr: 8
 alignof_short: 2
 alignof_str: 1
+bufsiz: '8192'
 char_is_unsigned: false
 compiler: generic
 cpp_arch_flags:
 - -m64
+eof: (-1)
+filename_max: '4096'
+fopen_max: '16'
 has__builtin_va_list: true
 intptr_t: long
+l_tmpnam: '20'
 little_endian: true
+mb_cur_max: ((size_t) 16 )
 posix_version: 200809L
 ptrdiff_t: long
+rand_max: '2147483647'
 size_t: unsigned long
 sizeof_double: 8
 sizeof_float: 4
@@ -30,6 +37,7 @@ sizeof_ptr: 8
 sizeof_short: 2
 sizeof_void: -1
 ssize_t: long
+tmp_max: '238328'
 uintptr_t: unsigned long
 version: gcc (GCC) 12.2.1 20230201
 wchar_t: int
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index 243e7f9e9fd914d0bec96811f2bbdfae15858000..add95aab7340597a593a83b23fa9e751c4ce0bef 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -178,6 +178,8 @@ source_files = [
     ("weof.c", "macro"),
     ("wordsize.c", "macro"),
     ("posix_version.c", "macro"),
+    ("stdio_macros.c", "macro"),
+    ("stdlib_macros.c", "macro"),
 ]
 
 
@@ -226,23 +228,19 @@ def cleanup_cpp(output):
     return " ".join(macro)
 
 
-def find_macro_value(name, output):
-    msg = re.compile(name + "_is = ([^;]+);")
-    res = re.search(msg, output)
-    if res:
+def find_macros_value(output):
+    msg = re.compile("(\w+)_is = ([^;]+);")
+    for res in re.finditer(msg, output):
+        name = res.group(1)
         if name in machdep:
-            value = res.group(1).strip()
+            value = res.group(2).strip()
             if args.verbose:
                 print(f"[INFO] setting {name} to {value}")
             machdep[name] = value
         else:
             warnings.warn(f"unexpected symbol '{name}', ignoring")
-    else:
-        warnings.warn(f"cannot find value of field '{name}', treating as empty")
-        if name in machdep:
-            machdep[name] = ""
-        if args.verbose:
-            print(f"compiler output is:{output}")
+    if args.verbose:
+        print(f"compiler output is:{output}")
 
 
 for (f, typ) in source_files:
@@ -258,14 +256,14 @@ for (f, typ) in source_files:
     Path(f).with_suffix(".o").unlink(missing_ok=True)
     if typ == "macro":
         if proc.returncode != 0:
-            warnings.warn(f"error in determining value of '{p,stem}', treating as empty")
+            warnings.warn(f"error in preprocessing value '{p}', some values won't be filled")
             if args.verbose:
                 print(f"compiler output is:{proc.stderr.decode()}")
             name = p.stem
             if name in machdep:
                 machdep[name] = ""
             continue
-        find_macro_value(p.stem, cleanup_cpp(proc.stdout.decode()))
+        find_macros_value(cleanup_cpp(proc.stdout.decode()))
         continue
     if typ == "has__builtin_va_list":
         # Special case: compilation success determines presence or absence
diff --git a/share/machdeps/make_machdep/stdio_macros.c b/share/machdeps/make_machdep/stdio_macros.c
new file mode 100644
index 0000000000000000000000000000000000000000..0655981e55c1f5c3540fb2c1f13e7f387997566b
--- /dev/null
+++ b/share/machdeps/make_machdep/stdio_macros.c
@@ -0,0 +1,8 @@
+#include <stdio.h>
+
+int bufsiz_is = BUFSIZ;
+int eof_is = EOF;
+int fopen_max_is = FOPEN_MAX;
+int filename_max_is = FILENAME_MAX;
+int l_tmpnam_is = L_tmpnam;
+int tmp_max_is = TMP_MAX;
diff --git a/share/machdeps/make_machdep/stdlib_macros.c b/share/machdeps/make_machdep/stdlib_macros.c
new file mode 100644
index 0000000000000000000000000000000000000000..db6291aff28efc6fd1f9949d228336ae46e24612
--- /dev/null
+++ b/share/machdeps/make_machdep/stdlib_macros.c
@@ -0,0 +1,9 @@
+#include <limits.h>
+#include <stdlib.h>
+
+int rand_max_is = RAND_MAX;
+/* NB: MB_LEN_MAX is the maximal value of MB_CUR_MAX;
+   however, the current Frama-C libc is not equipped to
+   fully deal with a non-constant MB_CUR_MAX
+*/
+size_t mb_cur_max_is = ((size_t)MB_LEN_MAX);
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 707e122ae15ea7541fb56cdd9e726af54e3d3aba..c1c2f636c7d08fc6bc0fb8cf196a1fa366cf2565 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -234,18 +234,16 @@ let gen_all_defines fmt mach =
     (List.assoc (no_signedness mach.intptr_t) pp_of_kind);
   gen_define_macro fmt "__FC_WORDSIZE" mach.wordsize;
   gen_define_macro fmt "__FC_POSIX_VERSION" mach.posix_version;
-  (* TODO: __FC_HOST_NAME_MAX *)
-  (* TODO: __FC_TTY_NAME_MAX *)
   (* TODO: __FC_SIG_ATOMIC_MIN *)
   (* TODO: __FC_SIG_ATOMIC_MAX *)
-  (* TODO: __FC_BUFSIZ *)
-  (* TODO: __FC_EOF *)
-  (* TODO: __FC_FOPEN_MAX *)
-  (* TODO: __FC_FILENAME_MAX *)
-  (* TODO: __FC_L_tmpnam *)
-  (* TODO: __FC_TMP_MAX *)
-  (* TODO: __FC_RAND_MAX *)
-  (* TODO: __FC_MB_CUR_MAX *)
+  gen_define_macro fmt "__FC_BUFSIZ" mach.bufsiz;
+  gen_define_macro fmt "__FC_EOF" mach.eof;
+  gen_define_macro fmt "__FC_FOPEN_MAX" mach.fopen_max;
+  gen_define_macro fmt "__FC_FILENAME_MAX" mach.filename_max;
+  gen_define_macro fmt "__FC_L_tmpnam" mach.l_tmpnam;
+  gen_define_macro fmt "__FC_TMP_MAX" mach.tmp_max;
+  gen_define_macro fmt "__FC_RAND_MAX" mach.rand_max;
+  gen_define_macro fmt "__FC_MB_CUR_MAX" mach.mb_cur_max;
   (* TODO: __FC_E*, errno enumeration *)
   (* TODO: __FC_TIME_T *)
   (* TODO: __FC_NSIG *)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index b9361bc473e758109906106461dcd91bd17d24e8..722c99194bcec6aa6de3f764e0b24319b4908f40 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1904,6 +1904,15 @@ type mach = {
   weof: string; (* expansion of WEOF macro, empty if undefined *)
   wordsize: string; (* expansion of __WORDSIZE macro, empty if undefined *)
   posix_version: string; (* expansion of _POSIX_VERSION macro, empty if undefined *)
+  bufsiz: string; (* expansion of BUFSIZ macro *)
+  eof: string; (* expansion of EOF macro *)
+  fopen_max: string; (* expansion of FOPEN_MAX macro *)
+  filename_max: string; (* expansion of FILENAME_MAX macro *)
+  l_tmpnam: string; (* expansion of L_tmpnam macro *)
+  tmp_max: string; (* expansion of TMP_MAX macro *)
+  rand_max: string; (* expansion of RAND_MAX macro *)
+  mb_cur_max: string; (* expansion of MB_CUR_MAX macro *)
+
 }
 
 (*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index b6efe80bca28f1978596213da545ab9f9831d332..9c9f4c62f9525603755a69050617acf9f9ec4fc2 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2666,6 +2666,14 @@ let dummy_machdep =
     weof = "(-1)";
     wordsize = "64";
     posix_version = "";
+    bufsiz = "255";
+    eof = "(-1)";
+    fopen_max = "255";
+    filename_max = "4095";
+    l_tmpnam = "63";
+    tmp_max = "1024";
+    rand_max = "0xFFFFFFFE";
+    mb_cur_max = "16";
   }
 
 module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index e00cd79dc58aed4ef1ca40801daf23fc85b694c4..99d86dd1467e4257a574ce130b122a8f24423d07 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -39,6 +39,14 @@ let mach =
     weof = "(-1)";
     wordsize = "24";
     posix_version = "200809L";
+    bufsiz = "255";
+    eof = "(-1)";
+    fopen_max = "128";
+    filename_max = "1023";
+    l_tmpnam = "255";
+    tmp_max = "4095";
+    rand_max = "0xFFFFFFFE";
+    mb_cur_max = "16";
   }
 
 let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 7b1dbeb487f94f7613c921948c0634ddb1fc5da0..d779f218d20ea925e1a58d99a37c9ea3f8e8b99d 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -35,3 +35,11 @@ wchar_t: int
 weof: (-1)
 wordsize: '24'
 posix_version: '200809L'
+bufsiz: '255'
+eof: (-1)
+fopen_max: '128'
+filename_max: '1023'
+l_tmpnam: '255'
+tmp_max: '255'
+rand_max: '0xFFFFFE'
+mb_cur_max: 16
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index c35154121ae9fb3f351b9cb37e3adca0c98a4382..48f3d97acbce62b9f220e8736f6f497774d21743 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -38,6 +38,14 @@ let md = {
   weof = "(-1L)";
   wordsize = "16";
   posix_version = "";
+  bufsiz = "8192";
+  eof = "(-1)";
+  fopen_max = "16";
+  filename_max = "2048";
+  l_tmpnam = "2048";
+  tmp_max = "0xFFFFFFFF";
+  rand_max = "0xFFFFFFFE";
+  mb_cur_max = "16";
 }
 
 let () =