[Libc] add non-POSIX header sys/sendfile.h

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

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"},

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"

share/libc/sys/sendfile.h

+/**************************************************************************/
+/*                                                                        */
+/*  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

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"

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"

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;

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)

tests/libc/oracle/sys_sendfile_h.res.oracle

+[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}

tests/libc/sys_sendfile_h.c

+#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;
+}