From 82ede5fa03cb5e76fc447575b9645f6d6f748eb4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 3 Apr 2019 11:12:40 +0200
Subject: [PATCH] [Libc] add a few specs for sys/stat.h and sys/types.h
---
share/compliance/nonstandard_identifiers.json | 1 +
share/libc/sys/stat.h | 45 ++++++++++++++++---
share/libc/sys/types.h | 4 ++
.../tests/known/oracle/printf.res.oracle | 1 +
.../oracle/printf_wrong_arity.res.oracle | 1 +
tests/libc/oracle/fc_libc.0.res.oracle | 9 ++--
tests/libc/oracle/fc_libc.1.res.oracle | 42 +++++++++++++++--
tests/libc/oracle/sys_stat_h.res.oracle | 33 +++++++++++++-
tests/libc/oracle/sys_types.res.oracle | 16 +++++++
tests/libc/sys_stat_h.c | 3 ++
tests/libc/sys_types.c | 6 +++
11 files changed, 145 insertions(+), 16 deletions(-)
create mode 100644 tests/libc/oracle/sys_types.res.oracle
create mode 100644 tests/libc/sys_types.c
diff --git a/share/compliance/nonstandard_identifiers.json b/share/compliance/nonstandard_identifiers.json
index e25a2fe06e2..34dc8300e44 100644
--- a/share/compliance/nonstandard_identifiers.json
+++ b/share/compliance/nonstandard_identifiers.json
@@ -5,6 +5,7 @@
{"ident":"facilitynames", "header":"syslog.h"},
{"ident":"getresgid", "header":"unistd.h"},
{"ident":"getresuid", "header":"unistd.h"},
+ {"ident":"makedev", "header":"sys/types.h"},
{"ident":"option", "header":"getopt.h"},
{"ident":"prioritynames", "header":"syslog.h"},
{"ident":"setresgid", "header":"unistd.h"},
diff --git a/share/libc/sys/stat.h b/share/libc/sys/stat.h
index f54dcb99bb3..8dc437102d8 100644
--- a/share/libc/sys/stat.h
+++ b/share/libc/sys/stat.h
@@ -32,25 +32,58 @@ __BEGIN_DECLS
extern int chmod(const char *, mode_t);
extern int fchmod(int, mode_t);
extern int fstat(int, struct stat *);
-extern int lstat(const char *, struct stat *);
+
+/*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG,
+ // ENOENT, ENOMEM, ENOTDIR, EOVERFLOW,
+ // EINVAL
+ // missing: assigns \result, *buf \from 'filesystem'
+ requires valid_path: valid_read_string(path);
+ requires valid_buf: \valid(buf);
+ assigns \result, *buf \from indirect:path, indirect:path[0..strlen(path)];
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int lstat(const char *path, struct stat *buf);
/*@ // missing: may assign to errno: EACCES, EEXIST, ELOOP, EMLINK,
// ENAMETOOLONG, ENOENT, ENOSPC,
// ENOTDIR, EROFS
// missing: assigns \result \from 'filesystem'
- requires valid_string_path: valid_read_string(path);
- assigns \result \from indirect:path, indirect:path[0..], indirect:mode;
+ requires valid_path: valid_read_string(path);
+ assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+ indirect:mode;
ensures result_ok_or_error: \result == 0 || \result == -1;
*/
extern int mkdir(const char *path, mode_t mode);
-extern int mkfifo(const char *, mode_t);
-extern int mknod(const char *, mode_t, dev_t);
+/*@ // missing: may assign to errno: EACCES, EEXIST, ELOOP, ENAMETOOLONG,
+ // ENOENT, ENOTDIR, ENOSPC, EROFS
+ // missing: assigns \result \from 'filesystem'
+ // missing: assigns 'filesystem' \from indirect:path,
+ // indirect:path[0..strlen(path)], mode;
+ requires valid_path: valid_read_string(path);
+ assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+ indirect:mode;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int mkfifo(const char *path, mode_t mode);
+
+/*@ // missing: may assign to errno: EACCES, EEXIST, EINVAL, EIO, ELOOP,
+ // ENAMETOOLONG, ENOENT, ENOTDIR, ENOSPC,
+ // EPERM, EROFS
+ // missing: assigns \result \from 'filesystem'
+ // missing: assigns 'filesystem' \from indirect:path,
+ // indirect:path[0..strlen(path)], mode, dev;
+ requires valid_path: valid_read_string(path);
+ assigns \result \from indirect:path, indirect:path[0..strlen(path)],
+ indirect:mode, indirect:dev;
+ ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int mknod(const char *path, mode_t mode, dev_t dev);
/*@ //missing: assigns \from 'filesystem'
requires valid_pathname: valid_read_string(pathname);
requires valid_buf: \valid(buf);
- assigns \result, *buf \from pathname[0..];
+ assigns \result, *buf \from pathname[0..strlen(pathname)];
ensures result_ok_or_error: \result == 0 || \result == -1;
ensures init_on_success:initialization:buf:
\result == 0 ==> \initialized(buf);
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index 16cf512ac59..41ba9673a06 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -49,6 +49,10 @@ typedef unsigned long u_long;
typedef unsigned int u_int;
typedef unsigned short u_short;
typedef unsigned char u_char;
+
+// Note: makedev (non-POSIX) is usually a macro; in case of problems,
+// consider redefining this.
+/*@ assigns \result \from maj, min; */
extern dev_t makedev(int maj, int min);
#define __u_char_defined
#endif
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 83d6f21822e..f04b44a2b44 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -164,6 +164,7 @@
#include "stdlib.h"
#include "string.h"
#include "strings.h"
+#include "sys/types.h"
#include "time.h"
#include "wchar.h"
/*@ requires valid_read_string(format);
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index f04220bcfaa..d7f8115fec3 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -44,6 +44,7 @@
#include "stdio.c"
#include "stdio.h"
#include "stdlib.h"
+#include "sys/types.h"
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 4576d6a15ca..02529fbe95f 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (390)
+ Undefined functions (394)
=========================
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);
@@ -111,8 +111,9 @@
localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
- lseek (0 call); malloc (7 calls); mblen (0 call); mbstowcs (0 call);
- mbtowc (0 call); mkdir (0 call); mkstemp (0 call); mktime (0 call);
+ lseek (0 call); lstat (0 call); makedev (0 call); malloc (7 calls);
+ mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+ mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call);
mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
@@ -180,7 +181,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 472
+ Function = 476
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 705dcf5c78c..3ac0899086f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4954,6 +4954,10 @@ extern int pclose(FILE *stream);
ssize_t getline(char **lineptr, size_t *n, FILE *stream);
+/*@ assigns \result;
+ assigns \result \from maj, min; */
+extern dev_t makedev(int maj, int min);
+
FILE __fc_initial_stdout =
{.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U};
FILE *__fc_stdout = & __fc_initial_stdout;
@@ -7531,14 +7535,44 @@ extern int setitimer(int which,
extern int select(int nfds, fd_set *readfds, fd_set *writefds,
fd_set *errorfds, struct timeval *timeout);
-/*@ requires valid_string_path: valid_read_string(path);
+/*@ requires valid_path: valid_read_string(path);
+ requires valid_buf: \valid(buf);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result, *buf;
+ assigns \result
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path))));
+ assigns *buf
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path))));
+ */
+extern int lstat(char const *path, struct stat *buf);
+
+/*@ requires valid_path: valid_read_string(path);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result
- \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: mode);
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: mode);
*/
extern int mkdir(char const *path, mode_t mode);
+/*@ requires valid_path: valid_read_string(path);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: mode);
+ */
+extern int mkfifo(char const *path, mode_t mode);
+
+/*@ requires valid_path: valid_read_string(path);
+ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result
+ \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+ (indirect: mode), (indirect: dev);
+ */
+extern int mknod(char const *path, mode_t mode, dev_t dev);
+
/*@ requires valid_pathname: valid_read_string(pathname);
requires valid_buf: \valid(buf);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
@@ -7546,8 +7580,8 @@ extern int mkdir(char const *path, mode_t mode);
init_on_success: initialization: buf:
\result ≡ 0 ⇒ \initialized(\old(buf));
assigns \result, *buf;
- assigns \result \from *(pathname + (0 ..));
- assigns *buf \from *(pathname + (0 ..));
+ assigns \result \from *(pathname + (0 .. strlen{Old}(pathname)));
+ assigns *buf \from *(pathname + (0 .. strlen{Old}(pathname)));
*/
extern int stat(char const *pathname, struct stat *buf);
diff --git a/tests/libc/oracle/sys_stat_h.res.oracle b/tests/libc/oracle/sys_stat_h.res.oracle
index 713de92c6ef..1fded86b56e 100644
--- a/tests/libc/oracle/sys_stat_h.res.oracle
+++ b/tests/libc/oracle/sys_stat_h.res.oracle
@@ -28,12 +28,12 @@
Called from tests/libc/sys_stat_h.c:17.
[eva] using specification for function mkdir
[eva] tests/libc/sys_stat_h.c:17:
- function mkdir: precondition 'valid_string_path' got status valid.
+ function mkdir: precondition 'valid_path' got status valid.
[eva] Done for function mkdir
[eva] computing for function mkdir <- main.
Called from tests/libc/sys_stat_h.c:20.
[eva:alarm] tests/libc/sys_stat_h.c:20: Warning:
- function mkdir: precondition 'valid_string_path' got status invalid.
+ function mkdir: precondition 'valid_path' got status invalid.
[eva] Done for function mkdir
[eva] computing for function mkdir <- main.
Called from tests/libc/sys_stat_h.c:20.
@@ -45,6 +45,32 @@
[eva] computing for function umask <- main.
Called from tests/libc/sys_stat_h.c:22.
[eva] Done for function umask
+[eva] computing for function lstat <- main.
+ Called from tests/libc/sys_stat_h.c:23.
+[eva] using specification for function lstat
+[eva] tests/libc/sys_stat_h.c:23:
+ function lstat: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_stat_h.c:23:
+ function lstat: precondition 'valid_buf' got status valid.
+[eva] Done for function lstat
+[eva] computing for function lstat <- main.
+ Called from tests/libc/sys_stat_h.c:23.
+[eva] Done for function lstat
+[eva] computing for function mkfifo <- main.
+ Called from tests/libc/sys_stat_h.c:24.
+[eva] using specification for function mkfifo
+[eva] tests/libc/sys_stat_h.c:24:
+ function mkfifo: precondition 'valid_path' got status valid.
+[eva] Done for function mkfifo
+[eva] computing for function mknod <- main.
+ Called from tests/libc/sys_stat_h.c:25.
+[eva] using specification for function mknod
+[eva] tests/libc/sys_stat_h.c:25:
+ function mknod: precondition 'valid_path' got status valid.
+[eva] Done for function mknod
+[eva] computing for function mknod <- main.
+ Called from tests/libc/sys_stat_h.c:25.
+[eva] Done for function mknod
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -55,4 +81,7 @@
r ∈ {-1; 0}
r_mkdir ∈ {-1; 0}
old_mask ∈ [--..--]
+ r2 ∈ {-1; 0}
+ r3 ∈ {-1; 0}
+ r4 ∈ {-1; 0}
__retres ∈ {-1; 0; 1; 2; 3}
diff --git a/tests/libc/oracle/sys_types.res.oracle b/tests/libc/oracle/sys_types.res.oracle
new file mode 100644
index 00000000000..68e4552bf4e
--- /dev/null
+++ b/tests/libc/oracle/sys_types.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/libc/sys_types.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 makedev <- main.
+ Called from tests/libc/sys_types.c:4.
+[eva] using specification for function makedev
+[eva] Done for function makedev
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ dev ∈ [--..--]
+ __retres ∈ {0}
diff --git a/tests/libc/sys_stat_h.c b/tests/libc/sys_stat_h.c
index 464a9e8e00e..65ddbfc8890 100644
--- a/tests/libc/sys_stat_h.c
+++ b/tests/libc/sys_stat_h.c
@@ -20,5 +20,8 @@ int main() {
mkdir(non_terminated, 0422);
}
mode_t old_mask = umask(0644);
+ int r2 = lstat("/tmp/bla", &st);
+ int r3 = mkfifo("/tmp/fifo", 0644);
+ int r4 = mknod("/tmp/fifo2", 0644, 42);
return 0;
}
diff --git a/tests/libc/sys_types.c b/tests/libc/sys_types.c
new file mode 100644
index 00000000000..50a3e33fef8
--- /dev/null
+++ b/tests/libc/sys_types.c
@@ -0,0 +1,6 @@
+#include <sys/types.h>
+
+int main() {
+ dev_t dev = makedev(1, 42);
+ return 0;
+}
--
GitLab