From 322bb488bb73c68e00a9377a1bf43af503f1bea1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 18 Nov 2021 10:36:26 +0100
Subject: [PATCH] [Libc] add test and update test oracles
---
tests/libc/fc_libc.c | 2 +-
tests/libc/oracle/fc_builtin_c.res.oracle | 60 ++--
tests/libc/oracle/fc_libc.0.res.oracle | 1 +
tests/libc/oracle/fc_libc.1.res.oracle | 374 +++++++++++++++++-----
tests/libc/oracle/pwd_c.res.oracle | 314 ++++++++++++++++++
tests/libc/oracle/pwd_h.res.oracle | 11 +-
tests/libc/pwd_c.c | 38 +++
7 files changed, 680 insertions(+), 120 deletions(-)
create mode 100644 tests/libc/oracle/pwd_c.res.oracle
create mode 100644 tests/libc/pwd_c.c
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index f69e8856f26..8df9bf49c33 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -12,7 +12,7 @@
MODULE: check_compliance
OPT: -kernel-msg-key printer:attrs
MODULE:
- OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | %{dep:./check_some_metrics.sh} "> 100" "> 400" "< 2" "> 20" "= 1" "= 1" "= 0" "= 0" "= 0" "= 1"
+ OPT: -load %{dep:@PTEST_NAME@.sav} -metrics -metrics-libc -then -lib-entry -metrics-no-libc | %{dep:./check_some_metrics.sh} "> 100" "> 400" "< 2" "> 0" "= 1" "= 1" "= 0" "= 0" "= 0" "= 1"
CMD: %{dep:./check_full_libc.sh} @FRAMAC_SHARE@/libc
OPT:
**/
diff --git a/tests/libc/oracle/fc_builtin_c.res.oracle b/tests/libc/oracle/fc_builtin_c.res.oracle
index ff75607cc47..d922ab4e1ef 100644
--- a/tests/libc/oracle/fc_builtin_c.res.oracle
+++ b/tests/libc/oracle/fc_builtin_c.res.oracle
@@ -1,77 +1,77 @@
-[kernel] Parsing tests/libc/fc_builtin_c.c (with preprocessing)
+[kernel] Parsing fc_builtin_c.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 Frama_C_interval <- main.
- Called from tests/libc/fc_builtin_c.c:8.
+ Called from fc_builtin_c.c:8.
[eva] computing for function Frama_C_update_entropy <- Frama_C_interval <- main.
- Called from share/libc/__fc_builtin.c:66.
+ Called from FRAMAC_SHARE/libc/__fc_builtin.c:66.
[eva] Recording results for Frama_C_update_entropy
[eva] Done for function Frama_C_update_entropy
[eva] Recording results for Frama_C_interval
[eva] Done for function Frama_C_interval
-[eva] tests/libc/fc_builtin_c.c:9: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:10: Warning:
+[eva] fc_builtin_c.c:9: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:10: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_char_interval <- main.
- Called from tests/libc/fc_builtin_c.c:12.
+ Called from fc_builtin_c.c:12.
[eva] computing for function Frama_C_interval <- Frama_C_char_interval <- main.
- Called from share/libc/__fc_builtin.c:77.
-[eva] share/libc/__fc_builtin.c:66:
+ Called from FRAMAC_SHARE/libc/__fc_builtin.c:77.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:66:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_interval
[eva] Done for function Frama_C_interval
[eva] Recording results for Frama_C_char_interval
[eva] Done for function Frama_C_char_interval
-[eva] tests/libc/fc_builtin_c.c:13: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:14: Warning:
+[eva] fc_builtin_c.c:13: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:14: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_unsigned_int_interval <- main.
- Called from tests/libc/fc_builtin_c.c:16.
-[eva] share/libc/__fc_builtin.c:100:
+ Called from fc_builtin_c.c:16.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:100:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_unsigned_int_interval
[eva] Done for function Frama_C_unsigned_int_interval
-[eva] tests/libc/fc_builtin_c.c:17: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:18: Warning:
+[eva] fc_builtin_c.c:17: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:18: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_float_interval <- main.
- Called from tests/libc/fc_builtin_c.c:20.
-[eva] share/libc/__fc_builtin.c:82:
+ Called from fc_builtin_c.c:20.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:82:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_float_interval
[eva] Done for function Frama_C_float_interval
-[eva] tests/libc/fc_builtin_c.c:21: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:22: Warning:
+[eva] fc_builtin_c.c:21: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:22: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_double_interval <- main.
- Called from tests/libc/fc_builtin_c.c:25.
-[eva] share/libc/__fc_builtin.c:88:
+ Called from fc_builtin_c.c:25.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:88:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_double_interval
[eva] Done for function Frama_C_double_interval
-[eva] tests/libc/fc_builtin_c.c:26: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:27: Warning:
+[eva] fc_builtin_c.c:26: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:27: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_long_interval <- main.
- Called from tests/libc/fc_builtin_c.c:29.
-[eva] share/libc/__fc_builtin.c:112:
+ Called from fc_builtin_c.c:29.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:112:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_long_interval
[eva] Done for function Frama_C_long_interval
-[eva] tests/libc/fc_builtin_c.c:30: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:31: Warning:
+[eva] fc_builtin_c.c:30: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:31: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] computing for function Frama_C_unsigned_long_interval <- main.
- Called from tests/libc/fc_builtin_c.c:34.
-[eva] share/libc/__fc_builtin.c:124:
+ Called from fc_builtin_c.c:34.
+[eva] FRAMAC_SHARE/libc/__fc_builtin.c:124:
Reusing old results for call to Frama_C_update_entropy
[eva] Recording results for Frama_C_unsigned_long_interval
[eva] Done for function Frama_C_unsigned_long_interval
-[eva] tests/libc/fc_builtin_c.c:35: assertion 'bounds' got status valid.
-[eva:alarm] tests/libc/fc_builtin_c.c:36: Warning:
+[eva] fc_builtin_c.c:35: assertion 'bounds' got status valid.
+[eva:alarm] fc_builtin_c.c:36: Warning:
assertion 'sampling,unknown' got status unknown.
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 1309a406e29..4cc020e5cf6 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -55,6 +55,7 @@
#include "netinet/in.h"
#include "poll.h"
#include "pthread.h"
+#include "pwd.c"
#include "pwd.h"
#include "setjmp.h"
#include "signal.c"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 703535ed601..a2690ea17ce 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -235,6 +235,15 @@ struct __fc_gethostbyname {
char *host_aliases[2] ;
char hostbuf[128] ;
};
+struct passwd {
+ char *pw_name ;
+ char *pw_passwd ;
+ uid_t pw_uid ;
+ gid_t pw_gid ;
+ char *pw_gecos ;
+ char *pw_dir ;
+ char *pw_shell ;
+};
typedef unsigned int ino_t;
typedef long time_t;
typedef unsigned int blkcnt_t;
@@ -340,15 +349,6 @@ struct pollfd {
short revents ;
};
typedef unsigned long nfds_t;
-struct passwd {
- char *pw_name ;
- char *pw_passwd ;
- uid_t pw_uid ;
- gid_t pw_gid ;
- char *pw_gecos ;
- char *pw_dir ;
- char *pw_shell ;
-};
typedef int jmp_buf[5];
struct __fc_sigjmp_buf {
jmp_buf buf ;
@@ -417,14 +417,8 @@ int Frama_C_interval(int min, int max);
*/
extern int Frama_C_interval_split(int min, int max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
- unsigned char max);
+unsigned char Frama_C_unsigned_char_interval(unsigned char min,
+ unsigned char max);
char Frama_C_char_interval(char min, char max);
@@ -445,14 +439,7 @@ extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
*/
extern short Frama_C_short_interval(short min, short max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
- unsigned int max);
+unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max);
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
@@ -462,22 +449,10 @@ extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
*/
extern int Frama_C_int_interval(int min, int max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned long Frama_C_unsigned_long_interval(unsigned long min,
- unsigned long max);
+unsigned long Frama_C_unsigned_long_interval(unsigned long min,
+ unsigned long max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern long Frama_C_long_interval(long min, long max);
+long Frama_C_long_interval(long min, long max);
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
@@ -537,6 +512,9 @@ extern long long Frama_C_abstract_max(long long i);
assigns \result \from i; */
extern long long Frama_C_abstract_min(long long i);
+unsigned int volatile __fc_unsigned_int_entropy;
+long volatile __fc_long_entropy;
+unsigned long volatile __fc_unsigned_long_entropy;
/*@ assigns Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
@@ -618,14 +596,9 @@ int Frama_C_interval(int min, int max)
char Frama_C_char_interval(char min, char max)
{
char __retres;
- int r;
- char aux;
- Frama_C_update_entropy();
- aux = (char)Frama_C_entropy_source;
- if ((int)aux >= (int)min)
- if ((int)aux <= (int)max) r = (int)aux; else r = (int)min;
- else r = (int)min;
- __retres = (char)r;
+ int tmp;
+ tmp = Frama_C_interval((int)min,(int)max);
+ __retres = (char)tmp;
return __retres;
}
@@ -663,6 +636,77 @@ double Frama_C_double_interval(double min, double max)
return tmp;
}
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+unsigned char Frama_C_unsigned_char_interval(unsigned char min,
+ unsigned char max)
+{
+ unsigned char __retres;
+ int tmp;
+ tmp = Frama_C_interval((int)min,(int)max);
+ __retres = (unsigned char)tmp;
+ return __retres;
+}
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
+{
+ unsigned int r;
+ unsigned int aux;
+ Frama_C_update_entropy();
+ aux = __fc_unsigned_int_entropy;
+ if (aux >= min)
+ if (aux <= max) r = aux; else r = min;
+ else r = min;
+ return r;
+}
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+long Frama_C_long_interval(long min, long max)
+{
+ long r;
+ long aux;
+ Frama_C_update_entropy();
+ aux = __fc_long_entropy;
+ if (aux >= min)
+ if (aux <= max) r = aux; else r = min;
+ else r = min;
+ return r;
+}
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+unsigned long Frama_C_unsigned_long_interval(unsigned long min,
+ unsigned long max)
+{
+ unsigned long r;
+ unsigned long aux;
+ Frama_C_update_entropy();
+ aux = __fc_unsigned_long_entropy;
+ if (aux >= min)
+ if (aux <= max) r = aux; else r = min;
+ else r = min;
+ return r;
+}
+
extern __attribute__((__noreturn__)) void __builtin_abort(void);
/*@ terminates \false;
@@ -5218,6 +5262,204 @@ struct in6_addr const in6addr_loopback =
(unsigned char)0,
(unsigned char)0,
(unsigned char)1}};
+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];
+struct passwd __fc_pwd =
+ {.pw_name = __fc_getpw_pw_name,
+ .pw_passwd = __fc_getpw_pw_passwd,
+ .pw_uid = 0U,
+ .pw_gid = 0U,
+ .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;
+/*@ requires valid_name: valid_read_string(name);
+ ensures
+ result_null_or_internal_struct:
+ \result ≡ \null ∨ \result ≡ __fc_p_pwd;
+ assigns \result, __fc_pwd;
+ assigns \result \from __fc_p_pwd, (indirect: *(name + (0 ..)));
+ assigns __fc_pwd \from (indirect: *(name + (0 ..)));
+ */
+extern struct passwd *getpwnam(char const *name);
+
+/*@ ensures
+ result_null_or_internal_struct:
+ \result ≡ \null ∨ \result ≡ __fc_p_pwd;
+ assigns \result, __fc_pwd;
+ assigns \result \from __fc_p_pwd, (indirect: uid);
+ assigns __fc_pwd \from (indirect: uid);
+ */
+extern struct passwd *getpwuid(uid_t uid);
+
+int getpwnam_r(char const *name, struct passwd *pwd, char *buf,
+ size_t buflen, struct passwd **result);
+
+int getpwuid_r(uid_t uid, struct passwd *pwd, char *buf, size_t buflen,
+ struct passwd **result);
+
+static int __fc_getpw_init;
+static int __fc_getpw_r(struct passwd *pwd, char *buf, size_t buflen,
+ struct passwd **result)
+{
+ int __retres;
+ int tmp_2;
+ if (! __fc_getpw_init) {
+ __fc_getpw_init = 1;
+ Frama_C_make_unknown(__fc_getpw_pw_name,(unsigned int)63);
+ __fc_getpw_pw_name[63] = (char)0;
+ Frama_C_make_unknown(__fc_getpw_pw_passwd,(unsigned int)63);
+ __fc_getpw_pw_passwd[63] = (char)0;
+ Frama_C_make_unknown(__fc_getpw_pw_gecos,(unsigned int)63);
+ __fc_getpw_pw_gecos[63] = (char)0;
+ Frama_C_make_unknown(__fc_getpw_pw_dir,(unsigned int)63);
+ __fc_getpw_pw_dir[63] = (char)0;
+ Frama_C_make_unknown(__fc_getpw_pw_shell,(unsigned int)63);
+ __fc_getpw_pw_shell[63] = (char)0;
+ }
+ tmp_2 = Frama_C_interval(0,1);
+ if (tmp_2) {
+ int tmp;
+ int tmp_0;
+ int tmp_1;
+ *result = (struct passwd *)0;
+ tmp = Frama_C_interval(0,1);
+ if (tmp) {
+ __retres = 5;
+ goto return_label;
+ }
+ tmp_0 = Frama_C_interval(0,1);
+ if (tmp_0) {
+ __retres = 24;
+ goto return_label;
+ }
+ tmp_1 = Frama_C_interval(0,1);
+ if (tmp_1) {
+ __retres = 23;
+ goto return_label;
+ }
+ __retres = 0;
+ goto return_label;
+ }
+ else {
+ size_t len;
+ size_t remaining = buflen;
+ len = strlen((char const *)__fc_pwd.pw_name);
+ if (remaining <= len) {
+ *result = (struct passwd *)0;
+ __retres = 34;
+ goto return_label;
+ }
+ strcpy(buf,(char const *)__fc_pwd.pw_name);
+ *(buf + len) = (char)0;
+ pwd->pw_name = buf;
+ buf += len + (size_t)1;
+ remaining -= len;
+ len = strlen((char const *)__fc_pwd.pw_passwd);
+ if (remaining <= len) {
+ *result = (struct passwd *)0;
+ __retres = 34;
+ goto return_label;
+ }
+ strcpy(buf,(char const *)__fc_pwd.pw_passwd);
+ *(buf + len) = (char)0;
+ pwd->pw_passwd = buf;
+ buf += len + (size_t)1;
+ remaining -= len;
+ len = strlen((char const *)__fc_pwd.pw_gecos);
+ if (remaining <= len) {
+ *result = (struct passwd *)0;
+ __retres = 34;
+ goto return_label;
+ }
+ strcpy(buf,(char const *)__fc_pwd.pw_gecos);
+ *(buf + len) = (char)0;
+ pwd->pw_gecos = buf;
+ buf += len + (size_t)1;
+ remaining -= len;
+ len = strlen((char const *)__fc_pwd.pw_dir);
+ if (remaining <= len) {
+ *result = (struct passwd *)0;
+ __retres = 34;
+ goto return_label;
+ }
+ strcpy(buf,(char const *)__fc_pwd.pw_dir);
+ *(buf + len) = (char)0;
+ pwd->pw_dir = buf;
+ buf += len + (size_t)1;
+ remaining -= len;
+ len = strlen((char const *)__fc_pwd.pw_shell);
+ if (remaining <= len) {
+ *result = (struct passwd *)0;
+ __retres = 34;
+ goto return_label;
+ }
+ strcpy(buf,(char const *)__fc_pwd.pw_shell);
+ *(buf + len) = (char)0;
+ pwd->pw_shell = buf;
+ buf += len + (size_t)1;
+ remaining -= len;
+ pwd->pw_uid = Frama_C_unsigned_int_interval((unsigned int)0,4294967295U);
+ pwd->pw_gid = Frama_C_unsigned_int_interval((unsigned int)0,4294967295U);
+ *result = pwd;
+ __retres = 0;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+/*@ 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);
+ ensures
+ result_null_or_assigned:
+ *\old(result) ≡ \null ∨ *\old(result) ≡ \old(pwd);
+ ensures
+ result_ok_or_error: \result ≡ 0 ∨ \result ∈ {5, 24, 23, 34};
+ assigns \result, __fc_pwd, *pwd, *result, *(buf + (0 .. buflen - 1));
+ assigns \result
+ \from (indirect: __fc_p_pwd), (indirect: *(name + (0 ..)));
+ assigns __fc_pwd \from (indirect: *(name + (0 ..)));
+ assigns *pwd \from __fc_p_pwd;
+ assigns *result \from __fc_p_pwd;
+ assigns *(buf + (0 .. buflen - 1)) \from (indirect: *__fc_p_pwd);
+ */
+int getpwnam_r(char const *name, struct passwd *pwd, char *buf,
+ size_t buflen, struct passwd **result)
+{
+ int tmp;
+ /*@ assert valid_read_string(name); */ ;
+ tmp = __fc_getpw_r(pwd,buf,buflen,result);
+ return tmp;
+}
+
+/*@ requires valid_buf: \valid(buf + (0 .. buflen - 1));
+ requires valid_pwd: \valid(pwd);
+ requires valid_result: \valid(result);
+ ensures
+ result_null_or_assigned:
+ *\old(result) ≡ \null ∨ *\old(result) ≡ \old(pwd);
+ ensures
+ result_ok_or_error: \result ≡ 0 ∨ \result ∈ {5, 24, 23, 34};
+ assigns \result, __fc_pwd, *pwd, *result, *(buf + (0 .. buflen - 1));
+ assigns \result \from (indirect: __fc_p_pwd);
+ assigns __fc_pwd \from (indirect: uid);
+ assigns *pwd \from __fc_p_pwd;
+ assigns *result \from __fc_p_pwd;
+ assigns *(buf + (0 .. buflen - 1)) \from (indirect: *__fc_p_pwd);
+ */
+int getpwuid_r(uid_t uid, struct passwd *pwd, char *buf, size_t buflen,
+ struct passwd **result)
+{
+ int tmp;
+ tmp = __fc_getpw_r(pwd,buf,buflen,result);
+ return tmp;
+}
+
/*@ ghost unsigned int volatile __fc_time; */
/*@ assigns \result;
assigns \result \from __fc_time; */
@@ -9310,42 +9552,6 @@ int pthread_setname_np(pthread_t thread, char const *name);
*/
int pthread_getname_np(pthread_t thread, char *name, size_t len);
-extern char __fc_getpwuid_pw_name[64];
-
-extern char __fc_getpwuid_pw_passwd[64];
-
-extern char __fc_getpwuid_pw_dir[64];
-
-extern char __fc_getpwuid_pw_shell[64];
-
-struct passwd __fc_pwd =
- {.pw_name = __fc_getpwuid_pw_name,
- .pw_passwd = __fc_getpwuid_pw_passwd,
- .pw_uid = 0U,
- .pw_gid = 0U,
- .pw_gecos = (char *)0,
- .pw_dir = __fc_getpwuid_pw_dir,
- .pw_shell = __fc_getpwuid_pw_shell};
-struct passwd *__fc_p_pwd = & __fc_pwd;
-/*@ requires valid_name: valid_read_string(name);
- ensures
- result_null_or_internal_struct:
- \result ≡ \null ∨ \result ≡ __fc_p_pwd;
- assigns \result, __fc_pwd;
- assigns \result \from __fc_p_pwd, (indirect: *(name + (0 ..)));
- assigns __fc_pwd \from (indirect: *(name + (0 ..)));
- */
-extern struct passwd *getpwnam(char const *name);
-
-/*@ ensures
- result_null_or_internal_struct:
- \result ≡ \null ∨ \result ≡ __fc_p_pwd;
- assigns \result, __fc_pwd;
- assigns \result \from __fc_p_pwd, (indirect: uid);
- assigns __fc_pwd \from (indirect: uid);
- */
-extern struct passwd *getpwuid(uid_t uid);
-
/*@ assigns *(env + (0 .. 4)); */
extern int setjmp(int env[5]);
diff --git a/tests/libc/oracle/pwd_c.res.oracle b/tests/libc/oracle/pwd_c.res.oracle
new file mode 100644
index 00000000000..d2523bf304f
--- /dev/null
+++ b/tests/libc/oracle/pwd_c.res.oracle
@@ -0,0 +1,314 @@
+[kernel] Parsing pwd_c.c (with preprocessing)
+[eva] Option -eva-precision 1 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 16.
+ option -eva-widening-delay set to 1.
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel set to 10.
+ option -eva-ilevel set to 12.
+ option -eva-plevel set to 20.
+ option -eva-subdivide-non-linear set to 20.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,symbolic-locations'.
+ option -eva-split-return already set to 'full' (not modified).
+ option -eva-equality-through-calls set to 'none'.
+ option -eva-octagon-through-calls set to false (default value).
+[eva] Splitting return states on:
+ \full_split(@all)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ uid ∈ [--..--]
+[eva] computing for function getpwuid_r <- main.
+ Called from pwd_c.c:14.
+[eva] computing for function __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:102.
+[eva] computing for function Frama_C_make_unknown <- __fc_getpw_r <- getpwuid_r <-
+ main.
+ Called from FRAMAC_SHARE/libc/pwd.c:56.
+[eva] using specification for function Frama_C_make_unknown
+[eva] FRAMAC_SHARE/libc/pwd.c:56:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] computing for function Frama_C_make_unknown <- __fc_getpw_r <- getpwuid_r <-
+ main.
+ Called from FRAMAC_SHARE/libc/pwd.c:58.
+[eva] FRAMAC_SHARE/libc/pwd.c:58:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] computing for function Frama_C_make_unknown <- __fc_getpw_r <- getpwuid_r <-
+ main.
+ Called from FRAMAC_SHARE/libc/pwd.c:60.
+[eva] FRAMAC_SHARE/libc/pwd.c:60:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] computing for function Frama_C_make_unknown <- __fc_getpw_r <- getpwuid_r <-
+ main.
+ Called from FRAMAC_SHARE/libc/pwd.c:62.
+[eva] FRAMAC_SHARE/libc/pwd.c:62:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] computing for function Frama_C_make_unknown <- __fc_getpw_r <- getpwuid_r <-
+ main.
+ Called from FRAMAC_SHARE/libc/pwd.c:64.
+[eva] FRAMAC_SHARE/libc/pwd.c:64:
+ function Frama_C_make_unknown: precondition 'valid_p' got status valid.
+[eva] Done for function Frama_C_make_unknown
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:69.
+[eva] using specification for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/pwd.c:69:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:72.
+[eva] FRAMAC_SHARE/libc/pwd.c:72:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:73.
+[eva] FRAMAC_SHARE/libc/pwd.c:73:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:74.
+[eva] FRAMAC_SHARE/libc/pwd.c:74:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/pwd.c:82: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/pwd.c:82:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:82.
+[eva] using specification for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:82:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:82:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:82:
+ function strcpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:373:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:83: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/pwd.c:83:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:83.
+[eva] FRAMAC_SHARE/libc/pwd.c:83:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:83:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:83:
+ function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:84: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/pwd.c:84:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:84.
+[eva] FRAMAC_SHARE/libc/pwd.c:84:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:84:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:84:
+ function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:85: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/pwd.c:85:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:85.
+[eva] FRAMAC_SHARE/libc/pwd.c:85:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:85:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:85:
+ function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:86: Call to builtin strlen
+[eva] FRAMAC_SHARE/libc/pwd.c:86:
+ function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:86.
+[eva] FRAMAC_SHARE/libc/pwd.c:86:
+ function strcpy: precondition 'valid_string_src' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:86:
+ function strcpy: precondition 'room_string' got status valid.
+[eva] FRAMAC_SHARE/libc/pwd.c:86:
+ function strcpy: precondition 'separation' got status valid.
+[eva] Done for function strcpy
+[eva] computing for function Frama_C_unsigned_int_interval <- __fc_getpw_r <-
+ getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:87.
+[eva] using specification for function Frama_C_unsigned_int_interval
+[eva] FRAMAC_SHARE/libc/pwd.c:87:
+ function Frama_C_unsigned_int_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] computing for function Frama_C_unsigned_int_interval <- __fc_getpw_r <-
+ getpwuid_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:88.
+[eva] FRAMAC_SHARE/libc/pwd.c:88:
+ function Frama_C_unsigned_int_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] Recording results for __fc_getpw_r
+[eva] Done for function __fc_getpw_r
+[eva] Recording results for getpwuid_r
+[eva] Done for function getpwuid_r
+[eva] pwd_c.c:16: assertion got status valid.
+[eva] pwd_c.c:17: assertion got status valid.
+[eva] pwd_c.c:18: assertion got status valid.
+[eva:alarm] pwd_c.c:20: Warning: assertion got status unknown.
+[eva:alarm] pwd_c.c:21: Warning: assertion got status unknown.
+[eva:alarm] pwd_c.c:22: Warning: assertion got status unknown.
+[eva:alarm] pwd_c.c:23: Warning: assertion got status unknown.
+[eva] computing for function getpwnam_r <- main.
+ Called from pwd_c.c:27.
+[eva] FRAMAC_SHARE/libc/pwd.c:96: assertion got status valid.
+[eva] computing for function __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:97.
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:69.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:72.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:73.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:74.
+[eva] Done for function Frama_C_interval
+[eva] FRAMAC_SHARE/libc/pwd.c:82: Call to builtin strlen
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:82.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:83: Call to builtin strlen
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:83.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:84: Call to builtin strlen
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:84.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:85: Call to builtin strlen
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:85.
+[eva] Done for function strcpy
+[eva] FRAMAC_SHARE/libc/pwd.c:86: Call to builtin strlen
+[eva] computing for function strcpy <- __fc_getpw_r <- getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:86.
+[eva] Done for function strcpy
+[eva] computing for function Frama_C_unsigned_int_interval <- __fc_getpw_r <-
+ getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:87.
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] computing for function Frama_C_unsigned_int_interval <- __fc_getpw_r <-
+ getpwnam_r <- main.
+ Called from FRAMAC_SHARE/libc/pwd.c:88.
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] Recording results for __fc_getpw_r
+[eva] Done for function __fc_getpw_r
+[eva] Recording results for getpwnam_r
+[eva] Done for function getpwnam_r
+[eva] pwd_c.c:29: assertion got status valid.
+[eva] pwd_c.c:30: assertion got status valid.
+[eva] pwd_c.c:31: assertion got status valid.
+[eva:alarm] pwd_c.c:33: Warning: assertion 'unknown_for_now' got status unknown.
+[eva:alarm] pwd_c.c:34: Warning: assertion 'unknown_for_now' got status unknown.
+[eva:alarm] pwd_c.c:35: Warning: assertion 'unknown_for_now' got status unknown.
+[eva:alarm] pwd_c.c:36: Warning: assertion 'unknown_for_now' got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function __fc_getpw_r:
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_getpw_pw_name[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_passwd[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_gecos[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_dir[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_shell[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ buf ∈ {{ &buf + [0..320] }}
+ pwd_out.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+ result ∈ {{ NULL ; &pwd_out ; &pwd_out2 }}
+ buf[0..319] ∈ [--..--] or UNINITIALIZED
+ pwd_out2.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+ __fc_getpw_init ∈ {1}
+ __retres ∈ {0; 5; 23; 24}
+[eva:final-states] Values at end of function getpwnam_r:
+ Frama_C_entropy_source ∈ [--..--]
+ result ∈ {{ NULL ; &pwd_out2 }}
+ buf[0..319] ∈ [--..--] or UNINITIALIZED
+ pwd_out2.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+[eva:final-states] Values at end of function getpwuid_r:
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_getpw_pw_name[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_passwd[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_gecos[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_dir[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_shell[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ pwd_out.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+ result ∈ {{ NULL ; &pwd_out }}
+ buf[0..319] ∈ [--..--] or UNINITIALIZED
+ __fc_getpw_init ∈ {1}
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ __fc_getpw_pw_name[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_passwd[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_gecos[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_dir[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ __fc_getpw_pw_shell[0..62] ∈ [--..--]
+ [63] ∈ {0}
+ pwd_out.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+ result ∈ {{ NULL ; &pwd_out2 }}
+ buf[0..319] ∈ [--..--] or UNINITIALIZED
+ buflen ∈ {320}
+ res ∈ {0; 5; 23; 24}
+ pwd_out2.pw_name ∈ {{ &buf[0] }} or UNINITIALIZED
+ .pw_passwd ∈ {{ &buf + [1..64] }} or UNINITIALIZED
+ {.pw_uid; .pw_gid} ∈ [--..--] or UNINITIALIZED
+ .pw_gecos ∈ {{ &buf + [2..128] }} or UNINITIALIZED
+ .pw_dir ∈ {{ &buf + [3..192] }} or UNINITIALIZED
+ .pw_shell ∈ {{ &buf + [4..256] }} or UNINITIALIZED
+ __fc_getpw_init ∈ {1}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/pwd_h.res.oracle b/tests/libc/oracle/pwd_h.res.oracle
index 9d329cca5b9..1ef5e0ebc0b 100644
--- a/tests/libc/oracle/pwd_h.res.oracle
+++ b/tests/libc/oracle/pwd_h.res.oracle
@@ -25,10 +25,11 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- __fc_pwd.pw_name ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_name[0] }}
- .pw_passwd ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_passwd[0] }}
- {.pw_uid; .pw_gid; .pw_gecos} ∈ [--..--]
- .pw_dir ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_dir[0] }}
- .pw_shell ∈ {{ NULL + [--..--] ; &__fc_getpwuid_pw_shell[0] }}
+ __fc_pwd.pw_name ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_name[0] }}
+ .pw_passwd ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_passwd[0] }}
+ {.pw_uid; .pw_gid} ∈ [--..--]
+ .pw_gecos ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_gecos[0] }}
+ .pw_dir ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_dir[0] }}
+ .pw_shell ∈ {{ NULL + [--..--] ; &__fc_getpw_pw_shell[0] }}
pw ∈ {{ NULL ; &__fc_pwd }}
__retres ∈ {0}
diff --git a/tests/libc/pwd_c.c b/tests/libc/pwd_c.c
new file mode 100644
index 00000000000..d60731f7f10
--- /dev/null
+++ b/tests/libc/pwd_c.c
@@ -0,0 +1,38 @@
+/*run.config
+ STDOPT: #"-eva-precision 1 -eva-split-return full"
+*/
+#include "pwd.c"
+#include "__fc_string_axiomatic.h"
+
+extern uid_t uid;
+
+int main() {
+ struct passwd pwd_out;
+ struct passwd *result;
+ char buf[320];
+ size_t buflen = sizeof(buf);
+ int res = getpwuid_r(uid, &pwd_out, buf, buflen, &result);
+ if (result) {
+ //@ assert res == 0;
+ //@ assert \initialized(&pwd_out.pw_uid);
+ //@ assert \initialized(&pwd_out.pw_gid);
+ //Note: ideally, the following assertions will be 'true' someday
+ //@ assert valid_read_string(pwd_out.pw_name);
+ //@ assert valid_read_string(pwd_out.pw_passwd);
+ //@ assert valid_read_string(pwd_out.pw_dir);
+ //@ assert valid_read_string(pwd_out.pw_shell);
+ }
+ //@ slevel merge;
+ struct passwd pwd_out2;
+ res = getpwnam_r("root", &pwd_out2, buf, buflen, &result);
+ if (result) {
+ //@ assert res == 0;
+ //@ assert \initialized(&pwd_out2.pw_uid);
+ //@ assert \initialized(&pwd_out2.pw_gid);
+ //Note: ideally, the following assertions will be 'true' someday
+ //@ assert unknown_for_now: valid_read_string(pwd_out2.pw_name);
+ //@ assert unknown_for_now: valid_read_string(pwd_out2.pw_passwd);
+ //@ assert unknown_for_now: valid_read_string(pwd_out2.pw_dir);
+ //@ assert unknown_for_now: valid_read_string(pwd_out2.pw_shell);
+ }
+}
--
GitLab