diff -Ndurp frama-c-Neon-20140301.orig/share/libc/__fc_define_ssize_max.h frama-c-Neon-20140301/share/libc/__fc_define_ssize_max.h
--- frama-c-Neon-20140301.orig/share/libc/__fc_define_ssize_max.h	1969-12-31 19:00:00.000000000 -0500
+++ frama-c-Neon-20140301/share/libc/__fc_define_ssize_max.h	2014-10-08 22:44:30.679246685 -0400
@@ -0,0 +1,27 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2014                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_SSIZE_MAX
+#define __FC_DEFINE_SSIZE_MAX
+#include "__fc_machdep.h"
+#define __SSIZE_MAX __FC_SSIZE_MAX
+#endif
diff -Ndurp frama-c-Neon-20140301.orig/share/libc/__fc_machdep.h frama-c-Neon-20140301/share/libc/__fc_machdep.h
--- frama-c-Neon-20140301.orig/share/libc/__fc_machdep.h	2014-03-12 11:07:51.000000000 -0400
+++ frama-c-Neon-20140301/share/libc/__fc_machdep.h	2014-10-08 22:44:30.683246685 -0400
@@ -66,6 +66,8 @@
 /* stdint.h */
 #define __FC_PTRDIFF_MIN __FC_INT_MIN
 #define __FC_PTRDIFF_MAX __FC_INT_MAX
+/* limits.h */
+#define __FC_SSIZE_MAX __FC_INT_MAX
 
 #else
 #ifdef __FC_MACHDEP_X86_64
@@ -144,6 +146,8 @@
 #define __FC_PTRDIFF_MIN __FC_LONG_MIN
 #define __FC_PTRDIFF_MAX __FC_LONG_MAX
 #else
+/* limits.h */
+#define __FC_SSIZE_MAX __FC_LONG_MAX
 
 #error Must define __FC_MACHDEP_X86_32 or __FC_MACHDEP_X86_64 or \
        __FC_MACHDEP_X86_16.
diff -Ndurp frama-c-Neon-20140301.orig/share/libc/limits.h frama-c-Neon-20140301/share/libc/limits.h
--- frama-c-Neon-20140301.orig/share/libc/limits.h	2014-03-12 11:07:51.000000000 -0400
+++ frama-c-Neon-20140301/share/libc/limits.h	2014-10-08 22:44:30.707246686 -0400
@@ -76,5 +76,8 @@
 /* Maximum value an `unsigned long long int' can hold.  (Minimum is 0.)  */
 #   define ULLONG_MAX	__FC_ULLONG_MAX
 
+/* Maximum value an `ssize_t` can hold.  */
+#   define SSIZE_MAX     __FC_SSIZE_MAX
+
 #endif
 
diff -Ndurp frama-c-Neon-20140301.orig/share/libc/unistd.h frama-c-Neon-20140301/share/libc/unistd.h
--- frama-c-Neon-20140301.orig/share/libc/unistd.h	2014-03-12 11:07:51.000000000 -0400
+++ frama-c-Neon-20140301/share/libc/unistd.h	2014-10-08 22:44:30.791246691 -0400
@@ -32,6 +32,7 @@
 #include "__fc_define_useconds_t.h"
 #include "__fc_define_intptr_t.h"
 #include "__fc_select.h"
+#include "__fc_define_ssize_max.h"
 
 #include <getopt.h>
 
@@ -767,7 +768,19 @@ ssize_t      pread(int, void *, size_t,
 int          pthread_atfork(void (*)(void), void (*)(void),
                  void(*)(void));
 ssize_t      pwrite(int, const void *, size_t, off_t);
-ssize_t      read(int, void *, size_t);
+/*@ 
+    requires \valid((char *) buf);
+    requires nbyte <= __SSIZE_MAX;
+    behavior success:
+        assigns *((char *)buf + (0 .. nbyte - 1)) \from fd, nbyte;
+        ensures 0 <= \result <= nbyte;
+    behavior failure:
+        ensures \result < 0;
+        assigns \nothing;
+    complete behaviors success, failure;
+    disjoint behaviors success, failure;
+ */
+ssize_t      read(int fd, void *buf, size_t nbyte);
 int          readlink(const char *, char *, size_t);
 int          rmdir(const char *);
 void        *sbrk(intptr_t);