diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 6f613040deb368220e3c4f7f8b086c9b468064f1..51604605640e95544f498f6a89a7a37dd2944533 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,7 +3,11 @@
 This chapter summarizes the changes in this documentation between each \FramaC
 release. First we list changes of the last release.
 
-%\section*{Frama-C+dev}
+\section*{Frama-C+dev}
+\begin{itemize}
+\item \textbf{Preparing the Sources:} add subsection on standard library about
+  portability considerations.
+\end{itemize}
 
 \section*{27.0 (Cobalt)}
 \begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index c85b8d259a195f135e42e439883182af860ef279..a30490e6448385e21fea8046bf6589a8cb0e8479 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -594,6 +594,36 @@ As stated before, if you want to ensure the code analyzed by \FramaC is
 strictly equivalent to the one from the target system, you must either
 proofread the definitions, or provide your own library files.
 
+\subsection*{Portability considerations}
+
+A few POSIX types are specified in an abstract way: {\em not required to be
+  arithmetic types}. This enables them to be defined as e.g. structures.
+Portable code using these types must not inspect them or apply operators
+that are only compatible with arithmetic types (e.g. comparing them with
+\texttt{NULL}). However, such comparisons do exist in the wild, and their
+parsing leads to two issues:
+\begin{itemize}
+\item \FramaC will fail parsing with a generic typing error message;
+\item the user may be unable or unwilling to modify the non-portable code,
+  since they may assume a specific libc implementation that uses an arithmetic
+  type.
+\end{itemize}
+The table below lists a few of such types that currently have special support
+in \FramaC's libc: by adding {\em \#define} macros to the preprocessing
+command-line (e.g. via \texttt{-cpp-extra-args=-D<macro>}), the user can ask
+\FramaC to handle such types as arithmetic.
+
+\begin{table}[!ht]
+  \centering
+  \begin{tabular}{l|l|l}
+    \textbf{Type name} & \textbf{Header} & \textbf{Macro name} \\
+    \midrule
+    \lstinline|pthread_t| & \lstinline|sys/types.h| & \lstinline|__FC_PTHREAD_T_IS_SCALAR| \\
+    \lstinline|fexcept_t| & \lstinline|fenv.h| & \lstinline|__FC_FEXCEPT_T_IS_SCALAR| \\
+  \end{tabular}
+\end{table}
+
+
 \section{Warnings during normalization}\label{sec:warnings-normalize}
 
 \emph{Note: the options below are deprecated, replaced by the more general and
diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h
index 391d2ae3a1af9bb9049df234d2b27dcab19fd7b9..3e102d19894f21c048e0528be8cefd54c2c77254 100644
--- a/share/libc/__fc_define_pthread_types.h
+++ b/share/libc/__fc_define_pthread_types.h
@@ -44,7 +44,14 @@ typedef struct __fc_pthread_once_t { int _fc; } pthread_once_t;
 typedef struct __fc_pthread_rwlock_t { int _fc; } pthread_rwlock_t;
 typedef struct __fc_pthread_rwlockattr_t { int _fc; } pthread_rwlockattr_t;
 typedef struct __fc_pthread_spinlock_t { int _fc; } pthread_spinlock_t;
-typedef struct __fc_pthread_t { int _fc; } pthread_t;
+
+#ifdef __FC_PTHREAD_T_IS_SCALAR
+// Some non-portable code assumes pthread_t as a scalar; this allows
+// such code to be parsed.
+typedef unsigned long pthread_t;
+#else
+typedef struct __fc_pthread_t { unsigned long _fc; } pthread_t;
+#endif
 __END_DECLS
 __POP_FC_STDLIB
 #endif
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index 7f656ff4aa67659c61002e0037cce0e3ea882059..c63e0856f119234bebfbb573d4b3d6f70b838f9e 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -1103,7 +1103,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
     int __gen_e_acsl_or;
     int __gen_e_acsl_valid_2;
     __e_acsl_store_block((void *)(& retval),8UL);
-    __e_acsl_store_block((void *)(& thread),4UL);
+    __e_acsl_store_block((void *)(& thread),8UL);
     __gen_e_acsl_contract = __e_acsl_contract_init(2UL);
     __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -1851,8 +1851,8 @@ int main(void)
   __e_acsl_store_block((void *)(& tmp_0),4UL);
   __e_acsl_store_block((void *)(& tmp),4UL);
   __e_acsl_store_block((void *)(args),40UL);
-  __e_acsl_store_block((void *)(readers),40UL);
-  __e_acsl_store_block((void *)(writers),40UL);
+  __e_acsl_store_block((void *)(readers),80UL);
+  __e_acsl_store_block((void *)(writers),80UL);
   __e_acsl_store_block((void *)(& __retres),4UL);
   __e_acsl_full_init((void *)(& tmp));
   tmp = __gen_e_acsl_pthread_mutex_init(& write_mutex,
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c
index ba28a676db6b9fb7449708c4eafb135d1741f684..08aa527836da75ff1801f7b3a1dec938dc19ad52 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_sequential_threads.c
@@ -207,7 +207,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
     int __gen_e_acsl_or;
     int __gen_e_acsl_valid_2;
     __e_acsl_store_block((void *)(& retval),8UL);
-    __e_acsl_store_block((void *)(& thread),4UL);
+    __e_acsl_store_block((void *)(& thread),8UL);
     __gen_e_acsl_contract = __e_acsl_contract_init(2UL);
     __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -515,7 +515,7 @@ int main(void)
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __e_acsl_globals_init();
   __e_acsl_store_block((void *)(args),40UL);
-  __e_acsl_store_block((void *)(& t),4UL);
+  __e_acsl_store_block((void *)(& t),8UL);
   __e_acsl_store_block((void *)(& __retres),4UL);
   {
     int i = 0;
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 6a4c17bd9fe799e43e81072c64d4c02488159519..329f8afa81c9d07634f0b0efe4550a700cacb64d 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -785,7 +785,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
     int __gen_e_acsl_or;
     int __gen_e_acsl_valid_2;
     __e_acsl_store_block((void *)(& retval),8UL);
-    __e_acsl_store_block((void *)(& thread),4UL);
+    __e_acsl_store_block((void *)(& thread),8UL);
     __gen_e_acsl_contract = __e_acsl_contract_init(2UL);
     __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -1533,8 +1533,8 @@ int main(void)
   __e_acsl_store_block((void *)(& tmp_0),4UL);
   __e_acsl_store_block((void *)(& tmp),4UL);
   __e_acsl_store_block((void *)(args),40UL);
-  __e_acsl_store_block((void *)(readers),40UL);
-  __e_acsl_store_block((void *)(writers),40UL);
+  __e_acsl_store_block((void *)(readers),80UL);
+  __e_acsl_store_block((void *)(writers),80UL);
   __e_acsl_store_block((void *)(& __retres),4UL);
   __e_acsl_full_init((void *)(& tmp));
   tmp = __gen_e_acsl_pthread_mutex_init(& write_mutex,
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
index 3113cefa8b2f90ffb5b527648584b9295619fe39..2bb83096a37b444aaa320e4fa64a095c8e1e3c56 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
@@ -256,7 +256,7 @@ int __gen_e_acsl_pthread_join(pthread_t thread, void **retval)
     int __gen_e_acsl_or;
     int __gen_e_acsl_valid_2;
     __e_acsl_store_block((void *)(& retval),8UL);
-    __e_acsl_store_block((void *)(& thread),4UL);
+    __e_acsl_store_block((void *)(& thread),8UL);
     __gen_e_acsl_contract = __e_acsl_contract_init(2UL);
     __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
     __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"retval",
@@ -562,7 +562,7 @@ int main(void)
   pthread_t t;
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __e_acsl_globals_init();
-  __e_acsl_store_block((void *)(& t),4UL);
+  __e_acsl_store_block((void *)(& t),8UL);
   __e_acsl_store_block((void *)(& __retres),4UL);
   __gen_e_acsl_pthread_create(& t,(pthread_attr_t const *)0,& thread_start,
                               (void *)0);
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8bc8f679bba9a04c85d13e4e3d60bde10a6fa53b..b5874f1ef25baa4b60527857038a1a5052e3bc20 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -113,7 +113,7 @@ struct __fc_pthread_mutexattr_t {
 };
 typedef struct __fc_pthread_mutexattr_t pthread_mutexattr_t;
 struct __fc_pthread_t {
-   int _fc ;
+   unsigned long _fc ;
 };
 typedef struct __fc_pthread_t pthread_t;
 typedef int pid_t;
diff --git a/tests/libc/oracle/pthread_h.res.oracle b/tests/libc/oracle/pthread_h.0.res.oracle
similarity index 79%
rename from tests/libc/oracle/pthread_h.res.oracle
rename to tests/libc/oracle/pthread_h.0.res.oracle
index 6511a6631d2a9b6d6aff6c645a310d9ce3dac12f..41d84474ca4898b748bbbbfc0b39a62bc8906c28 100644
--- a/tests/libc/oracle/pthread_h.res.oracle
+++ b/tests/libc/oracle/pthread_h.0.res.oracle
@@ -6,73 +6,73 @@
   retval ∈ {0}
   v ∈ [--..--]
 [eva] computing for function pthread_create <- main.
-  Called from pthread_h.c:17.
+  Called from pthread_h.c:23.
 [eva] using specification for function pthread_create
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_thread' got status valid.
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_null_attr' got status valid.
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_routine' got status valid.
-[eva] pthread_h.c:17: 
+[eva] pthread_h.c:23: 
   function pthread_create: precondition 'valid_null_arg' got status valid.
 [eva] Done for function pthread_create
 [eva] computing for function printf_va_2 <- main.
-  Called from pthread_h.c:19.
+  Called from pthread_h.c:25.
 [eva] using specification for function printf_va_2
-[eva] pthread_h.c:19: function printf_va_2: precondition got status valid.
+[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
 [eva] Done for function printf_va_2
 [eva] computing for function printf_va_3 <- main.
-  Called from pthread_h.c:22.
+  Called from pthread_h.c:28.
 [eva] using specification for function printf_va_3
-[eva] pthread_h.c:22: function printf_va_3: precondition got status valid.
+[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
 [eva] Done for function printf_va_3
 [eva] computing for function pthread_setname_np <- main.
-  Called from pthread_h.c:23.
+  Called from pthread_h.c:29.
 [eva] using specification for function pthread_setname_np
-[eva] pthread_h.c:23: 
+[eva] pthread_h.c:29: 
   function pthread_setname_np: precondition 'valid_name' got status valid.
 [eva] Done for function pthread_setname_np
 [eva] computing for function pthread_getname_np <- main.
-  Called from pthread_h.c:26.
+  Called from pthread_h.c:32.
 [eva] using specification for function pthread_getname_np
-[eva] pthread_h.c:26: 
+[eva] pthread_h.c:32: 
   function pthread_getname_np: precondition 'valid_name' got status valid.
 [eva] Done for function pthread_getname_np
 [eva] computing for function printf_va_4 <- main.
-  Called from pthread_h.c:27.
+  Called from pthread_h.c:33.
 [eva] using specification for function printf_va_4
-[eva:alarm] pthread_h.c:27: Warning: 
+[eva:alarm] pthread_h.c:33: Warning: 
   function printf_va_4: precondition valid_read_string(param0) got status unknown.
-[eva] pthread_h.c:27: 
+[eva] pthread_h.c:33: 
   function printf_va_4: precondition valid_read_string(format) got status valid.
 [eva] Done for function printf_va_4
 [eva] computing for function start_routine <- main.
-  Called from pthread_h.c:32.
+  Called from pthread_h.c:38.
 [eva] computing for function printf_va_1 <- start_routine <- main.
-  Called from pthread_h.c:8.
+  Called from pthread_h.c:14.
 [eva] using specification for function printf_va_1
-[eva] pthread_h.c:8: function printf_va_1: precondition got status valid.
+[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
 [eva] Done for function printf_va_1
 [eva] Recording results for start_routine
 [eva] Done for function start_routine
 [eva] computing for function pthread_join <- main.
-  Called from pthread_h.c:34.
+  Called from pthread_h.c:40.
 [eva] using specification for function pthread_join
-[eva] pthread_h.c:34: 
+[eva] pthread_h.c:40: 
   function pthread_join: precondition 'valid_or_null_retval' got status valid.
 [eva] Done for function pthread_join
 [eva] computing for function printf_va_5 <- main.
-  Called from pthread_h.c:36.
+  Called from pthread_h.c:42.
 [eva] using specification for function printf_va_5
-[eva] pthread_h.c:36: function printf_va_5: precondition got status valid.
+[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
 [eva] Done for function printf_va_5
-[eva:alarm] pthread_h.c:39: Warning: 
+[eva:alarm] pthread_h.c:45: Warning: 
   out of bounds read. assert \valid_read(retv);
 [eva] computing for function printf_va_6 <- main.
-  Called from pthread_h.c:39.
+  Called from pthread_h.c:45.
 [eva] using specification for function printf_va_6
-[eva] pthread_h.c:39: function printf_va_6: precondition got status valid.
+[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
 [eva] Done for function printf_va_6
 [eva] Recording results for main
 [eva] Done for function main
diff --git a/tests/libc/oracle/pthread_h.1.res.oracle b/tests/libc/oracle/pthread_h.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e9962e514fbafdf75537930f75b0d121b8272671
--- /dev/null
+++ b/tests/libc/oracle/pthread_h.1.res.oracle
@@ -0,0 +1,94 @@
+[kernel] Parsing pthread_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  retval ∈ {0}
+  v ∈ [--..--]
+[eva] computing for function pthread_create <- main.
+  Called from pthread_h.c:23.
+[eva] using specification for function pthread_create
+[eva] pthread_h.c:23: 
+  function pthread_create: precondition 'valid_thread' got status valid.
+[eva] pthread_h.c:23: 
+  function pthread_create: precondition 'valid_null_attr' got status valid.
+[eva] pthread_h.c:23: 
+  function pthread_create: precondition 'valid_routine' got status valid.
+[eva] pthread_h.c:23: 
+  function pthread_create: precondition 'valid_null_arg' got status valid.
+[eva] Done for function pthread_create
+[eva] computing for function printf_va_2 <- main.
+  Called from pthread_h.c:25.
+[eva] using specification for function printf_va_2
+[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
+[eva] Done for function printf_va_2
+[eva] computing for function printf_va_3 <- main.
+  Called from pthread_h.c:28.
+[eva] using specification for function printf_va_3
+[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
+[eva] Done for function printf_va_3
+[eva:alarm] pthread_h.c:29: Warning: 
+  accessing uninitialized left-value. assert \initialized(&thread);
+[eva] computing for function pthread_setname_np <- main.
+  Called from pthread_h.c:29.
+[eva] using specification for function pthread_setname_np
+[eva] pthread_h.c:29: 
+  function pthread_setname_np: precondition 'valid_name' got status valid.
+[eva] Done for function pthread_setname_np
+[eva] computing for function pthread_getname_np <- main.
+  Called from pthread_h.c:32.
+[eva] using specification for function pthread_getname_np
+[eva] pthread_h.c:32: 
+  function pthread_getname_np: precondition 'valid_name' got status valid.
+[eva] Done for function pthread_getname_np
+[eva] computing for function printf_va_4 <- main.
+  Called from pthread_h.c:33.
+[eva] using specification for function printf_va_4
+[eva:alarm] pthread_h.c:33: Warning: 
+  function printf_va_4: precondition valid_read_string(param0) got status unknown.
+[eva] pthread_h.c:33: 
+  function printf_va_4: precondition valid_read_string(format) got status valid.
+[eva] Done for function printf_va_4
+[eva] computing for function start_routine <- main.
+  Called from pthread_h.c:38.
+[eva] computing for function printf_va_1 <- start_routine <- main.
+  Called from pthread_h.c:14.
+[eva] using specification for function printf_va_1
+[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
+[eva] Done for function printf_va_1
+[eva] Recording results for start_routine
+[eva] Done for function start_routine
+[eva] computing for function pthread_join <- main.
+  Called from pthread_h.c:40.
+[eva] using specification for function pthread_join
+[eva] pthread_h.c:40: 
+  function pthread_join: precondition 'valid_or_null_retval' got status valid.
+[eva] Done for function pthread_join
+[eva] computing for function printf_va_5 <- main.
+  Called from pthread_h.c:42.
+[eva] using specification for function printf_va_5
+[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
+[eva] Done for function printf_va_5
+[eva:alarm] pthread_h.c:45: Warning: 
+  out of bounds read. assert \valid_read(retv);
+[eva] computing for function printf_va_6 <- main.
+  Called from pthread_h.c:45.
+[eva] using specification for function printf_va_6
+[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
+[eva] Done for function printf_va_6
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function start_routine:
+  retval ∈ {43}
+  __retres ∈ {{ (void *)&retval }}
+  S___fc_stdout[0..1] ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  retval ∈ {0; 43}
+  thread ∈ [--..--] or UNINITIALIZED
+  thread_arg ∈ {42}
+  r ∈ [--..--]
+  buf[0..15] ∈ [--..--] or UNINITIALIZED
+  retv ∈ {{ NULL + [--..--] ; &retval }} or UNINITIALIZED
+  __retres ∈ {0; 1; 2}
+  S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/pthread_h.2.res.oracle b/tests/libc/oracle/pthread_h.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e4df7ae1f77abe53df109934c2223f2a686334f3
--- /dev/null
+++ b/tests/libc/oracle/pthread_h.2.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing pthread_h.c (with preprocessing)
+[kernel] pthread_h.c:49: User Error: 
+  cannot perform the following comparison thread == 0
+  47      // Test non-portable usage of pthread_t
+  48    #ifdef NON_PORTABLE
+  49      if (thread == 0) {
+              ^^^^^^^^^^^
+  50        return 2;
+  51      }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/libc/pthread_h.c b/tests/libc/pthread_h.c
index 28ba09c9d4716d471d96325499c2802bcd9b75e3..5b875173489763f5c7042f319717774a15c2fd83 100644
--- a/tests/libc/pthread_h.c
+++ b/tests/libc/pthread_h.c
@@ -1,3 +1,9 @@
+/*run.config
+  STDOPT:
+  STDOPT: -cpp-extra-args="-D__FC_PTHREAD_T_IS_SCALAR -DNON_PORTABLE"
+  EXIT: 1
+  STDOPT: -cpp-extra-args="-DNON_PORTABLE"
+ */
 #define _GNU_SOURCE // if you want to compile with GCC
 #include <pthread.h>
 #include <stdio.h>
@@ -37,5 +43,13 @@ int main() {
     return 1;
   }
   printf("pthread_join succeeded, retval = %d\n", *retv);
+
+  // Test non-portable usage of pthread_t
+#ifdef NON_PORTABLE
+  if (thread == 0) {
+    return 2;
+  }
+#endif
+
   return 0;
 }