diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 424d9a2a67667859cf5b297c541bbb81075e88ac..1b31299d8c2ad05fe41c32e4e1ec5b49bb003981 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -296,6 +296,7 @@ share/libc/sys/param.h: CEA_LGPL
share/libc/sys/random.h: CEA_LGPL
share/libc/sys/resource.h: CEA_LGPL
share/libc/sys/select.h: CEA_LGPL
+share/libc/sys/sendfile.h: CEA_LGPL
share/libc/sys/shm.h: CEA_LGPL
share/libc/sys/signal.h: CEA_LGPL
share/libc/sys/socket.h: CEA_LGPL
diff --git a/share/compliance/nonstandard_identifiers.json b/share/compliance/nonstandard_identifiers.json
index 597eb9212001ea484dce3c52deff1c1b902a9bd9..3e921766cd4c962142d20d13ad2e5645fa9afdb0 100644
--- a/share/compliance/nonstandard_identifiers.json
+++ b/share/compliance/nonstandard_identifiers.json
@@ -8,6 +8,7 @@
"makedev": {"header":"sys/types.h"},
"option": {"header":"getopt.h"},
"prioritynames": {"header":"syslog.h"},
+ "sendfile": {"header":"sys/sendfile.h"},
"setresgid": {"header":"unistd.h"},
"setresuid": {"header":"unistd.h"},
"strcspn": {"header":"string.h"},
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index f48c2a451635a25714abca51a28b18f3442e7d2b..6e43667ac7d10ff995a1a2977499d078c211dbd6 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -88,6 +88,7 @@
#include "sys/random.h"
#include "sys/resource.h"
#include "sys/select.h"
+#include "sys/sendfile.h"
#include "sys/shm.h"
#include "sys/signal.h"
#include "sys/socket.h"
diff --git a/share/libc/sys/sendfile.h b/share/libc/sys/sendfile.h
new file mode 100644
index 0000000000000000000000000000000000000000..9636ecebbf0103c85d7ddd35e4a0b47252991153
--- /dev/null
+++ b/share/libc/sys/sendfile.h
@@ -0,0 +1,56 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+// Non-POSIX; Linux-specific
+
+#ifndef __FC_SYS_SENDFILE_H__
+#define __FC_SYS_SENDFILE_H__
+
+#include "../features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+
+#include "../__fc_define_max_open_files.h"
+#include "../__fc_define_off_t.h"
+#include "../__fc_define_size_t.h"
+#include "../__fc_define_ssize_t.h"
+#include "../errno.h"
+
+/*@
+ //missing: requires in_fd opened for reading
+ //missing: requires out_fd opened for writing
+ requires valid_in_fd: 0 <= in_fd < __FC_MAX_OPEN_FILES;
+ requires valid_out_fd: 0 <= out_fd < __FC_MAX_OPEN_FILES;
+ requires valid_offset_or_null: offset == \null || \valid(offset);
+ requires initialization:offset: offset == \null || \initialized(offset);
+ assigns errno, \result, *offset \from indirect:out_fd, indirect:in_fd,
+ indirect:offset, indirect:count;
+ //missing: assigns "out_fd's state (offset/buffer if file; or socket's state)"
+ //missing: assigns "in_fd's offset, if offset == null"
+ ensures error_or_chars_sent: \result == -1 || 0 <= \result <= count;
+ ensures initialization:offset: \initialized(offset);
+ */
+ssize_t sendfile(int out_fd, int in_fd, off_t *offset, size_t count);
+
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index c222f77c8033529b9f07801298f9ab474d5dc783..2010e74f9536538808b93fe910035b7b948f485d 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -130,6 +130,7 @@
#include "sys/random.h"
#include "sys/resource.h"
#include "sys/select.h"
+#include "sys/sendfile.h"
#include "sys/shm.h"
#include "sys/signal.h"
#include "sys/socket.h"
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 483efb112ac3b086e079422c67dff159473513fe..42266a3a00f369cd9dfa692f7122427645010878 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] tests/libc/fc_libc.c:159: assertion got status valid.
[eva] tests/libc/fc_libc.c:160: assertion got status valid.
[eva] tests/libc/fc_libc.c:161: assertion got status valid.
[eva] tests/libc/fc_libc.c:162: assertion got status valid.
+[eva] tests/libc/fc_libc.c:163: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -41,7 +41,7 @@
wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call);
- Specified-only functions (421)
+ Specified-only functions (422)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -137,36 +137,37 @@
recv (0 call); recvfrom (0 call); recvmsg (0 call); remove (0 call);
rename (0 call); rewind (0 call); round (0 call); roundf (0 call);
roundl (0 call); seed48 (0 call); select (0 call); send (0 call);
- sendto (0 call); setbuf (0 call); setegid (0 call); seteuid (0 call);
- setgid (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
- setlogmask (0 call); setpgid (0 call); setpriority (0 call);
- setregid (0 call); setresgid (0 call); setresuid (0 call);
- setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
- settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
- sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
- sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
- siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
- sinf (0 call); sinl (0 call); sleep (0 call); socket (0 call);
- socketpair (0 call); sqrt (0 call); sqrtf (0 call); sqrtl (0 call);
- srand (0 call); srand48 (0 call); srandom (0 call); stat (0 call);
- stpcpy (0 call); strcasestr (0 call); strchrnul (0 call); strcoll (0 call);
- strcspn (0 call); strftime (0 call); strlcat (0 call); strlcpy (0 call);
- strncasecmp (0 call); strpbrk (0 call); strsep (0 call); strspn (0 call);
- strtod (0 call); strtof (0 call); strtoimax (0 call); strtok (0 call);
- strtok_r (0 call); strtol (0 call); strtold (0 call); strtoll (0 call);
- strtoul (0 call); strtoull (0 call); strxfrm (0 call); sync (0 call);
- sysconf (0 call); syslog (0 call); system (0 call); tcflush (0 call);
- tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
- tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
- truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
- uname (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
- utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
- vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
- wait (0 call); waitpid (0 call); wcscasecmp (0 call); wcschr (0 call);
- wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
- wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
- wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
- wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ sendfile (0 call); sendto (0 call); setbuf (0 call); setegid (0 call);
+ seteuid (0 call); setgid (0 call); sethostname (0 call); setitimer (0 call);
+ setjmp (0 call); setlogmask (0 call); setpgid (0 call);
+ setpriority (0 call); setregid (0 call); setresgid (0 call);
+ setresuid (0 call); setreuid (0 call); setrlimit (0 call); setsid (0 call);
+ setsockopt (0 call); settimeofday (0 call); setuid (0 call);
+ setvbuf (0 call); shutdown (0 call); sigaction (0 call); sigaddset (0 call);
+ sigdelset (0 call); sigemptyset (0 call); sigfillset (0 call);
+ sigismember (0 call); siglongjmp (0 call); signal (0 call);
+ sigprocmask (0 call); sin (0 call); sinf (0 call); sinl (0 call);
+ sleep (0 call); socket (0 call); socketpair (0 call); sqrt (0 call);
+ sqrtf (0 call); sqrtl (0 call); srand (0 call); srand48 (0 call);
+ srandom (0 call); stat (0 call); stpcpy (0 call); strcasestr (0 call);
+ strchrnul (0 call); strcoll (0 call); strcspn (0 call); strftime (0 call);
+ strlcat (0 call); strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call);
+ strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
+ strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
+ strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
+ strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
+ system (0 call); tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call);
+ time (0 call); times (0 call); tmpfile (0 call); tmpnam (0 call);
+ trunc (0 call); truncf (0 call); truncl (0 call); ttyname (0 call);
+ tzset (0 call); umask (0 call); uname (0 call); ungetc (0 call);
+ unlink (0 call); usleep (0 call); utimes (0 call); vfprintf (0 call);
+ vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
+ vsprintf (0 call); vsyslog (0 call); wait (0 call); waitpid (0 call);
+ wcscasecmp (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
+ wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
+ wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
+ wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
+ write (0 call);
Undefined and unspecified functions (1)
=======================================
@@ -195,7 +196,7 @@
Goto = 99
Assignment = 466
Exit point = 84
- Function = 506
+ Function = 507
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
@@ -252,6 +253,7 @@
#include "stropts.h"
#include "sys/file.h"
#include "sys/resource.h"
+#include "sys/sendfile.h"
#include "sys/socket.h"
#include "sys/stat.h"
#include "sys/time.h"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index d1496ec153c6da59da7b3edd9387612b067730ce..c99ba102c79368d6a0891069a36e52ff359cfd10 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8274,6 +8274,27 @@ extern int getrusage(int who, struct rusage *r_usage);
*/
extern int setrlimit(int resource, struct rlimit const *rlp);
+/*@ requires valid_in_fd: 0 ≤ in_fd < 1024;
+ requires valid_out_fd: 0 ≤ out_fd < 1024;
+ requires valid_offset_or_null: offset ≡ \null ∨ \valid(offset);
+ requires
+ initialization: offset: offset ≡ \null ∨ \initialized(offset);
+ ensures
+ error_or_chars_sent: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(count));
+ ensures initialization: offset: \initialized(\old(offset));
+ assigns __fc_errno, \result, *offset;
+ assigns __fc_errno
+ \from (indirect: out_fd), (indirect: in_fd), (indirect: offset),
+ (indirect: count);
+ assigns \result
+ \from (indirect: out_fd), (indirect: in_fd), (indirect: offset),
+ (indirect: count);
+ assigns *offset
+ \from (indirect: out_fd), (indirect: in_fd), (indirect: offset),
+ (indirect: count);
+ */
+ssize_t sendfile(int out_fd, int in_fd, off_t *offset, size_t count);
+
/*@ requires valid_buffer: \valid(buffer);
assigns \result, *buffer;
assigns \result \from __fc_time;
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index ff8de64ff7b2a0c175e479d63f98a86db1289469..548b5555639845571c43ccce9622f06b69de87dd 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -105,6 +105,7 @@ skipping share/libc/complex.h
[kernel] Parsing share/libc/sys/random.h (with preprocessing)
[kernel] Parsing share/libc/sys/resource.h (with preprocessing)
[kernel] Parsing share/libc/sys/select.h (with preprocessing)
+[kernel] Parsing share/libc/sys/sendfile.h (with preprocessing)
[kernel] Parsing share/libc/sys/shm.h (with preprocessing)
[kernel] Parsing share/libc/sys/signal.h (with preprocessing)
[kernel] Parsing share/libc/sys/socket.h (with preprocessing)
diff --git a/tests/libc/oracle/sys_sendfile_h.res.oracle b/tests/libc/oracle/sys_sendfile_h.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7cd2c9b5e2e868d3c4d187c0ba490cc914ca80a2
--- /dev/null
+++ b/tests/libc/oracle/sys_sendfile_h.res.oracle
@@ -0,0 +1,80 @@
+[kernel] Parsing tests/libc/sys_sendfile_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
+
+[eva] computing for function __va_open_void <- main.
+ Called from tests/libc/sys_sendfile_h.c:7.
+[eva] using specification for function __va_open_void
+[eva] tests/libc/sys_sendfile_h.c:7:
+ function __va_open_void: precondition 'valid_filename' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:7:
+ function __va_open_void: precondition 'flag_not_CREAT' got status valid.
+[eva] Done for function __va_open_void
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_sendfile_h.c:9.
+[eva] using specification for function __va_open_mode_t
+[eva] tests/libc/sys_sendfile_h.c:9:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] computing for function sendfile <- main.
+ Called from tests/libc/sys_sendfile_h.c:13.
+[eva] using specification for function sendfile
+[eva] tests/libc/sys_sendfile_h.c:13:
+ function sendfile: precondition 'valid_in_fd' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:13:
+ function sendfile: precondition 'valid_out_fd' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:13:
+ function sendfile: precondition 'valid_offset_or_null' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:13:
+ function sendfile: precondition 'initialization,offset' got status valid.
+[eva] Done for function sendfile
+[eva] tests/libc/sys_sendfile_h.c:14: assertion got status valid.
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_sendfile_h.c:15.
+[eva] using specification for function close
+[eva] tests/libc/sys_sendfile_h.c:15:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function __va_open_mode_t <- main.
+ Called from tests/libc/sys_sendfile_h.c:17.
+[eva] tests/libc/sys_sendfile_h.c:17:
+ function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] computing for function sendfile <- main.
+ Called from tests/libc/sys_sendfile_h.c:19.
+[eva] tests/libc/sys_sendfile_h.c:19:
+ function sendfile: precondition 'valid_in_fd' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:19:
+ function sendfile: precondition 'valid_out_fd' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:19:
+ function sendfile: precondition 'valid_offset_or_null' got status valid.
+[eva] tests/libc/sys_sendfile_h.c:19:
+ function sendfile: precondition 'initialization,offset' got status valid.
+[eva:invalid-assigns] tests/libc/sys_sendfile_h.c:19:
+ Completely invalid destination for assigns clause *offset. Ignoring.
+[eva] Done for function sendfile
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_sendfile_h.c:20.
+[eva] tests/libc/sys_sendfile_h.c:20:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] computing for function close <- main.
+ Called from tests/libc/sys_sendfile_h.c:21.
+[eva] tests/libc/sys_sendfile_h.c:21:
+ function close: precondition 'valid_fd' got status valid.
+[eva] Done for function close
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
+ __fc_fds[0..1023] ∈ [--..--]
+ out_fd ∈ [-1..1023] or UNINITIALIZED
+ in_fd ∈ [-1..1023]
+ offset ∈ [--..--]
+ r1 ∈ [-1..42] or UNINITIALIZED
+ r3 ∈ [-1..42] or UNINITIALIZED
+ r ∈ {-1; 0}
+ __retres ∈ {0; 1}
diff --git a/tests/libc/sys_sendfile_h.c b/tests/libc/sys_sendfile_h.c
new file mode 100644
index 0000000000000000000000000000000000000000..fbb613b304999f3676735757c4be4d327fae576e
--- /dev/null
+++ b/tests/libc/sys_sendfile_h.c
@@ -0,0 +1,23 @@
+#include <sys/sendfile.h>
+#include <fcntl.h>
+#include <unistd.h>
+
+int main() {
+ int out_fd, in_fd;
+ in_fd = open("/tmp/in.txt", O_RDONLY);
+ if (in_fd == -1) return 1;
+ out_fd = open("/tmp/out.txt", O_CREAT, O_WRONLY);
+ if (out_fd == -1) return 1;
+ off_t offset = 0;
+ ssize_t r1, r2, r3;
+ r1 = sendfile(out_fd, in_fd, &offset, 42);
+ //@ assert -1 <= r1 <= 42;
+ int r = close(out_fd);
+ if (r) return 1;
+ out_fd = open("/tmp/out.txt", O_CREAT, O_WRONLY);
+ if (out_fd == -1) return 1;
+ r3 = sendfile(out_fd, in_fd, 0, 42);
+ close(out_fd);
+ close(in_fd);
+ return 0;
+}