diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index af58bb507356e496b140a90f202e7f66b70b49ea..00963b7c188013277f088feacc2a3cbdbd2b416e 100644
--- a/share/libc/__fc_builtin.c
+++ b/share/libc/__fc_builtin.c
@@ -20,8 +20,9 @@
 /*                                                                        */
 /**************************************************************************/
 
-#include "__fc_builtin.h"
+#include "features.h"
 __PUSH_FC_STDLIB
+#include "__fc_builtin.h"
 #include "limits.h"
 
 /* Those builtins implementations could probably be removed entirely for
@@ -32,9 +33,17 @@ __PUSH_FC_STDLIB
 int volatile Frama_C_entropy_source;
 
 // Additional entropy sources for some interval functions
+unsigned short volatile __fc_unsigned_short_entropy;
 unsigned int volatile __fc_unsigned_int_entropy;
 long volatile __fc_long_entropy;
 unsigned long volatile __fc_unsigned_long_entropy;
+long long volatile __fc_long_long_entropy;
+unsigned long long volatile __fc_unsigned_long_long_entropy;
+size_t volatile __fc_size_t_entropy;
+intmax_t volatile __fc_intmax_t_entropy;
+uintmax_t volatile __fc_uintmax_t_entropy;
+ptrdiff_t volatile __fc_ptrdiff_t_entropy;
+wint_t volatile __fc_wint_t_entropy;
 
 //@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 void Frama_C_update_entropy(void) {
@@ -48,6 +57,13 @@ void Frama_C_make_unknown(char *p, size_t l) {
   }
 }
 
+void Frama_C_make_unknown_wchar(wchar_t *p, size_t l) {
+  Frama_C_update_entropy();
+  for (size_t i = 0; i < l; i++) {
+    p[i] = Frama_C_entropy_source;
+  }
+}
+
 int Frama_C_nondet(int a, int b)
 {
   Frama_C_update_entropy();
@@ -77,6 +93,11 @@ char Frama_C_char_interval(char min, char max)
   return (char)Frama_C_interval(min, max);
 }
 
+short Frama_C_short_interval(short min, short max)
+{
+  return (short)Frama_C_interval(min, max);
+}
+
 float Frama_C_float_interval(float min, float max)
 {
   Frama_C_update_entropy();
@@ -94,6 +115,18 @@ unsigned char Frama_C_unsigned_char_interval(unsigned char min, unsigned char ma
   return (unsigned char)Frama_C_interval(min, max);
 }
 
+unsigned short Frama_C_unsigned_short_interval(unsigned short min, unsigned short max)
+{
+  unsigned short r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_unsigned_short_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
 unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
 {
   unsigned int r, aux;
@@ -130,6 +163,90 @@ unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long ma
   return r;
 }
 
+long long Frama_C_long_long_interval(long long min, long long max)
+{
+  long long r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_long_long_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min, unsigned long long max)
+{
+  unsigned long long r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_unsigned_long_long_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+size_t Frama_C_size_t_interval(size_t min, size_t max)
+{
+  size_t r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_size_t_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+intmax_t Frama_C_intmax_t_interval(intmax_t min, intmax_t max)
+{
+  intmax_t r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_intmax_t_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+uintmax_t Frama_C_uintmax_t_interval(uintmax_t min, uintmax_t max)
+{
+  uintmax_t r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_uintmax_t_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+ptrdiff_t Frama_C_ptrdiff_t_interval(ptrdiff_t min, ptrdiff_t max)
+{
+  ptrdiff_t r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_ptrdiff_t_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
+wint_t Frama_C_wint_t_interval(wint_t min, wint_t max)
+{
+  wint_t r, aux;
+  Frama_C_update_entropy();
+  aux = __fc_wint_t_entropy;
+  if (aux >= min && aux <= max)
+    r = aux;
+  else
+    r = min;
+  return r;
+}
+
 /*@ assigns \nothing; */
 extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
 
diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index 3e174f67b340c06c2036fbf927351f2e04e58484..d2ed15cc0b0b307d93098b8724eda79d7c90d28b 100644
--- a/share/libc/__fc_builtin.h
+++ b/share/libc/__fc_builtin.h
@@ -25,7 +25,9 @@
 #include "features.h"
 __PUSH_FC_STDLIB
 #include "__fc_alloc_axiomatic.h"
-#include "__fc_define_size_t.h"
+#include "__fc_define_wint_t.h"
+#include "stddef.h"
+#include "stdint.h"
 
 __BEGIN_DECLS
 
@@ -38,6 +40,13 @@ extern volatile int Frama_C_entropy_source __attribute__((unused));
 */
 extern void Frama_C_make_unknown(char *p, size_t l) __attribute__((FC_BUILTIN));
 
+/*@ requires valid_p: \valid(p + (0 .. l-1));
+    assigns p[0 .. l-1] \from Frama_C_entropy_source;
+    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+    ensures initialization: \initialized(p + (0 .. l-1));
+*/
+extern void Frama_C_make_unknown_wchar(wchar_t *p, size_t l) __attribute__((FC_BUILTIN));
+
 /*@ assigns \result \from a, b, Frama_C_entropy_source;
     assigns Frama_C_entropy_source \from Frama_C_entropy_source;
     ensures result_a_or_b: \result == a || \result == b ;
@@ -155,21 +164,69 @@ extern long long Frama_C_long_long_interval(long long min, long long max)
 extern size_t Frama_C_size_t_interval(size_t min, size_t max)
     __attribute__((FC_BUILTIN));
 
-/*@ requires finite: \is_finite(min) && \is_finite(max);
-    requires order: min <= max;
+/*@ requires order: min <= max;
     assigns \result \from min, max, Frama_C_entropy_source;
     assigns Frama_C_entropy_source \from Frama_C_entropy_source;
-    ensures result_bounded: \is_finite(\result) && min <= \result <= max;
+    ensures result_bounded: min <= \result <= max ;
  */
-extern float Frama_C_float_interval(float min, float max)
+extern intmax_t Frama_C_intmax_t_interval(intmax_t min, intmax_t max)
     __attribute__((FC_BUILTIN));
 
-/*@ requires finite: \is_finite(min) && \is_finite(max);
-    requires order: min <= max;
+/*@ requires order: min <= max;
     assigns \result \from min, max, Frama_C_entropy_source;
     assigns Frama_C_entropy_source \from Frama_C_entropy_source;
-    ensures result_bounded: \is_finite(\result) && min <= \result <= max;
+    ensures result_bounded: min <= \result <= max ;
+ */
+extern uintmax_t Frama_C_uintmax_t_interval(uintmax_t min, uintmax_t max)
+    __attribute__((FC_BUILTIN));
+
+/*@ requires order: min <= max;
+    assigns \result \from min, max, Frama_C_entropy_source;
+    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+    ensures result_bounded: min <= \result <= max ;
+ */
+extern ptrdiff_t Frama_C_ptrdiff_t_interval(ptrdiff_t min, ptrdiff_t max)
+    __attribute__((FC_BUILTIN));
+
+/*@ requires order: min <= max;
+    assigns \result \from min, max, Frama_C_entropy_source;
+    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+    ensures result_bounded: min <= \result <= max ;
  */
+extern wint_t Frama_C_wint_t_interval(wint_t min, wint_t max)
+    __attribute__((FC_BUILTIN));
+
+/*@
+  assigns \result \from min, max, Frama_C_entropy_source;
+  assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+  behavior finite:
+    assumes finite: \is_finite(min) && \is_finite(max);
+    requires order: min <= max;
+    ensures result_bounded: \is_finite(\result) && min <= \result <= max;
+  behavior infinite_not_nan:
+    assumes infinite: \is_infinite(min) || \is_infinite(max);
+    assumes not_nan: !\is_NaN(min) && !\is_NaN(max);
+    requires order: min <= max;
+    ensures result_bounded: !\is_NaN(\result) && min <= \result <= max;
+  disjoint behaviors;
+*/
+extern float Frama_C_float_interval(float min, float max)
+    __attribute__((FC_BUILTIN));
+
+/*@
+  assigns \result \from min, max, Frama_C_entropy_source;
+  assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+  behavior finite:
+    assumes finite: \is_finite(min) && \is_finite(max);
+    requires order: min <= max;
+    ensures result_bounded: \is_finite(\result) && min <= \result <= max;
+  behavior infinite_not_nan:
+    assumes infinite: \is_infinite(min) || \is_infinite(max);
+    assumes not_nan: !\is_NaN(min) && !\is_NaN(max);
+    requires order: min <= max;
+    ensures result_bounded: !\is_NaN(\result) && min <= \result <= max;
+  disjoint behaviors;
+*/
 extern double Frama_C_double_interval(double min, double max)
     __attribute__((FC_BUILTIN));