Newer
Older
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* 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_PWD_H__
#define __FC_PWD_H__
#include "features.h"
__PUSH_FC_STDLIB
#include "__fc_define_uid_and_gid.h"
#include "__fc_string_axiomatic.h"
#include "errno.h"
// for size_t
#include "stddef.h"
__BEGIN_DECLS
struct passwd {
char *pw_name;
char *pw_passwd; // not POSIX, but allowed by it, and present in glibc
uid_t pw_uid;
gid_t pw_gid;
char *pw_gecos; // not POSIX, but present in most implementations
char *pw_dir;
char *pw_shell;
};
__FC_EXTERN char __fc_getpw_pw_name[64];
__FC_EXTERN char __fc_getpw_pw_passwd[64];
__FC_EXTERN char __fc_getpw_pw_gecos[64];
__FC_EXTERN char __fc_getpw_pw_dir[64];
__FC_EXTERN char __fc_getpw_pw_shell[64];
{.pw_name = __fc_getpw_pw_name,
.pw_passwd = __fc_getpw_pw_passwd,
.pw_gecos = __fc_getpw_pw_gecos,
.pw_dir = __fc_getpw_pw_dir,
.pw_shell = __fc_getpw_pw_shell};
struct passwd *__fc_p_pwd = & __fc_pwd;
/*@
// missing: may assign to errno: EIO, EINTR, EMFILE, ENFILE
// missing: assigns \result, __fc_pwd[0..] \from 'password database'
requires valid_name: valid_read_string(name);
assigns \result \from __fc_p_pwd, indirect:name[0..];
assigns __fc_pwd \from indirect:name[0..];
ensures result_null_or_internal_struct:
\result == \null || \result == __fc_p_pwd;
*/
extern struct passwd *getpwnam(const char *name);
/*@ // missing: assigns \result, __fc_pwd[0..] \from 'password database'
assigns \result \from __fc_p_pwd, indirect:uid;
assigns __fc_pwd \from indirect:uid;
ensures result_null_or_internal_struct:
\result == \null || \result == __fc_p_pwd;
*/
extern struct passwd *getpwuid(uid_t uid);
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
/*@
// missing: assigns \result, *result, *pwd, __fc_pwd[0..] \from 'password database'
requires valid_name: valid_read_string(name);
requires valid_buf: \valid(buf+(0 .. buflen-1));
requires valid_pwd: \valid(pwd);
requires valid_result: \valid(result);
assigns \result \from indirect:__fc_p_pwd, indirect:name[0..];
assigns __fc_pwd \from indirect:name[0..];
assigns *pwd, *result \from __fc_p_pwd;
assigns buf[0 .. buflen-1] \from indirect:*__fc_p_pwd;
ensures result_null_or_assigned:
*result == \null || *result == pwd;
ensures result_ok_or_error:
\result == 0 || \result \in {EIO, EMFILE, ENFILE, ERANGE};
*/
extern int getpwnam_r(const char *name, struct passwd *pwd,
char *buf, size_t buflen, struct passwd **result);
/*@
// missing: assigns \result, *result, *pwd, __fc_pwd[0..] \from 'password database'
requires valid_buf: \valid(buf+(0 .. buflen-1));
requires valid_pwd: \valid(pwd);
requires valid_result: \valid(result);
assigns \result \from indirect:__fc_p_pwd;
assigns __fc_pwd \from indirect:uid;
assigns *pwd, *result \from __fc_p_pwd;
assigns buf[0 .. buflen-1] \from indirect:*__fc_p_pwd;
ensures result_null_or_assigned:
*result == \null || *result == pwd;
ensures result_ok_or_error:
\result == 0 || \result \in {EIO, EMFILE, ENFILE, ERANGE};
*/
extern int getpwuid_r(uid_t uid, struct passwd *pwd,
char *buf, size_t buflen, struct passwd **result);