From c79a8b9451e8ef3dde3274cf1fb754917655ce06 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Thu, 18 Nov 2021 10:35:46 +0100 Subject: [PATCH] [Libc] add C stubs for getpwnam_r and getpwuid_r --- headers/header_spec.txt | 1 + share/libc/__fc_runtime.c | 1 + share/libc/pwd.c | 105 +++++++++++++++++++ src/plugins/value/utils/library_functions.ml | 2 + 4 files changed, 109 insertions(+) create mode 100644 share/libc/pwd.c diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 75a8014972c..fc3f7cd5925 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -286,6 +286,7 @@ share/libc/netinet/tcp.h: CEA_LGPL share/libc/nl_types.h: CEA_LGPL share/libc/poll.h: CEA_LGPL share/libc/pthread.h: CEA_LGPL +share/libc/pwd.c: CEA_LGPL share/libc/pwd.h: CEA_LGPL share/libc/regex.h: CEA_LGPL share/libc/resolv.h: CEA_LGPL diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c index 2c456c4d037..533b13ee312 100644 --- a/share/libc/__fc_runtime.c +++ b/share/libc/__fc_runtime.c @@ -33,6 +33,7 @@ #include "math.c" #include "netdb.c" #include "netinet/in.c" +#include "pwd.c" #include "signal.c" #include "stdatomic.c" #include "stdio.c" diff --git a/share/libc/pwd.c b/share/libc/pwd.c new file mode 100644 index 00000000000..624bc1f8409 --- /dev/null +++ b/share/libc/pwd.c @@ -0,0 +1,105 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2022 */ +/* 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). */ +/* */ +/**************************************************************************/ + +#include "__fc_builtin.h" +#include "errno.h" +#include "pwd.h" +#include "string.h" + +__PUSH_FC_STDLIB + +char __fc_getpw_pw_name[64]; +char __fc_getpw_pw_passwd[64]; +char __fc_getpw_pw_gecos[64]; +char __fc_getpw_pw_dir[64]; +char __fc_getpw_pw_shell[64]; + +static int __fc_getpw_init; // used to initialize the __fc_getpw* strings + +#define COPY_FIELD(fieldname) \ + len = strlen(__fc_pwd.fieldname); \ + if (remaining <= len) { \ + *result = NULL; \ + return ERANGE; \ + } \ + strcpy(buf, __fc_pwd.fieldname); \ + buf[len] = 0; \ + pwd->fieldname = buf; \ + buf += len + 1; \ + remaining -= len + +// Common code between getpwman_r and getpwuid_r +static int __fc_getpw_r(struct passwd *pwd, char *buf, + size_t buflen, struct passwd **result) { + // initialize global strings (only during first execution) + if (!__fc_getpw_init) { + __fc_getpw_init = 1; + Frama_C_make_unknown(__fc_getpw_pw_name, 63); + __fc_getpw_pw_name[63] = 0; + Frama_C_make_unknown(__fc_getpw_pw_passwd, 63); + __fc_getpw_pw_passwd[63] = 0; + Frama_C_make_unknown(__fc_getpw_pw_gecos, 63); + __fc_getpw_pw_gecos[63] = 0; + Frama_C_make_unknown(__fc_getpw_pw_dir, 63); + __fc_getpw_pw_dir[63] = 0; + Frama_C_make_unknown(__fc_getpw_pw_shell, 63); + __fc_getpw_pw_shell[63] = 0; + } + + // simulate one of several possible errors, or "not found" + if (Frama_C_interval(0, 1)) { + // 'error or not found' case + *result = NULL; + if (Frama_C_interval(0, 1)) return EIO; + if (Frama_C_interval(0, 1)) return EMFILE; + if (Frama_C_interval(0, 1)) return ENFILE; + // Note: POSIX only specifies these values, but several implementations + // return others, including ENOENT, EBADF, ESRCH, EWOULDBLOCK, EPERM. + return 0; + } else { + // 'found without errors' case + size_t len, remaining = buflen; + // copy string fields to buf + COPY_FIELD(pw_name); + COPY_FIELD(pw_passwd); + COPY_FIELD(pw_gecos); + COPY_FIELD(pw_dir); + COPY_FIELD(pw_shell); + pwd->pw_uid = Frama_C_unsigned_int_interval(0, UINT_MAX); + pwd->pw_gid = Frama_C_unsigned_int_interval(0, UINT_MAX); + *result = pwd; + return 0; + } +} + +int getpwnam_r(const char *name, struct passwd *pwd, + char *buf, size_t buflen, struct passwd **result) { + //@ assert valid_read_string(name); + return __fc_getpw_r(pwd, buf, buflen, result); +} + +int getpwuid_r(uid_t uid, struct passwd *pwd, + char *buf, size_t buflen, struct passwd **result) { + return __fc_getpw_r(pwd, buf, buflen, result); +} + +__POP_FC_STDLIB diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml index 51eee549394..31cc22262c6 100644 --- a/src/plugins/value/utils/library_functions.ml +++ b/src/plugins/value/utils/library_functions.ml @@ -78,6 +78,8 @@ let unsupported_specifications = "getaddrinfo", "netdb.c"; "getenv", "stdlib.c"; "getline", "stdio.c"; + "getpwnam_r", "pwd.c"; + "getpwuid_r", "pwd.c"; "glob", "glob.c"; "globfree", "glob.c"; "posix_memalign", "stdlib.c"; -- GitLab