diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 75a8014972c92d933188bcb17480f0c050a7ab7f..fc3f7cd5925d9bdd595efa5286da61869aff2c7b 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_builtin.c b/share/libc/__fc_builtin.c
index 2654932223c2c5f397627cb5e75f75376aaa6a16..b7b973543cc9603fb2bc3946bfa69b80daccbe86 100644
--- a/share/libc/__fc_builtin.c
+++ b/share/libc/__fc_builtin.c
@@ -22,6 +22,7 @@
#include "__fc_builtin.h"
__PUSH_FC_STDLIB
+#include "limits.h"
/* Those builtins implementations could probably be removed entirely for
Value, as the spec is informative enough. There remains a slight difference
@@ -30,6 +31,11 @@ __PUSH_FC_STDLIB
int volatile Frama_C_entropy_source;
+// Additional entropy sources for some interval functions
+unsigned int volatile __fc_unsigned_int_entropy;
+long volatile __fc_long_entropy;
+unsigned long volatile __fc_unsigned_long_entropy;
+
//@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
void Frama_C_update_entropy(void) {
Frama_C_entropy_source = Frama_C_entropy_source;
@@ -56,10 +62,10 @@ void *Frama_C_nondet_ptr(void *a, void *b)
int Frama_C_interval(int min, int max)
{
- int r,aux;
+ int r, aux;
Frama_C_update_entropy();
aux = Frama_C_entropy_source;
- if ((aux>=min) && (aux <=max))
+ if (aux >= min && aux <= max)
r = aux;
else
r = min;
@@ -68,27 +74,60 @@ int Frama_C_interval(int min, int max)
char Frama_C_char_interval(char min, char max)
{
- int r;
- char aux;
+ return (char)Frama_C_interval(min, max);
+}
+
+float Frama_C_float_interval(float min, float max)
+{
Frama_C_update_entropy();
- aux = Frama_C_entropy_source;
- if ((aux>=min) && (aux <=max))
+ return Frama_C_entropy_source ? min : max;
+}
+
+double Frama_C_double_interval(double min, double max)
+{
+ Frama_C_update_entropy();
+ return Frama_C_entropy_source ? min : max;
+}
+
+unsigned char Frama_C_unsigned_char_interval(unsigned char min, unsigned char max)
+{
+ return (unsigned char)Frama_C_interval(min, max);
+}
+
+unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
+{
+ unsigned int r, aux;
+ Frama_C_update_entropy();
+ aux = __fc_unsigned_int_entropy;
+ if (aux >= min && aux <= max)
r = aux;
else
r = min;
return r;
}
-float Frama_C_float_interval(float min, float max)
+long Frama_C_long_interval(long min, long max)
{
+ long r, aux;
Frama_C_update_entropy();
- return Frama_C_entropy_source ? min : max;
+ aux = __fc_long_entropy;
+ if (aux >= min && aux <= max)
+ r = aux;
+ else
+ r = min;
+ return r;
}
-double Frama_C_double_interval(double min, double max)
+unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long max)
{
+ unsigned long r, aux;
Frama_C_update_entropy();
- return Frama_C_entropy_source ? min : max;
+ aux = __fc_unsigned_long_entropy;
+ if (aux >= min && aux <= max)
+ r = aux;
+ else
+ r = min;
+ return r;
}
extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c
index 2c456c4d0378b7a74a7c19c357d7ded48aa02697..533b13ee312bb0397b6d75fbf7c2de9a49ec504a 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 0000000000000000000000000000000000000000..624bc1f8409fe460412997bee3f1027b97aa34cd
--- /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/share/libc/pwd.h b/share/libc/pwd.h
index fb9ddca482764743f31efef8d52ae07c97b5adda..5dfc799d95d6122af31d2486b840f5f1b6e6bc84 100644
--- a/share/libc/pwd.h
+++ b/share/libc/pwd.h
@@ -29,9 +29,9 @@ __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 {
@@ -44,16 +44,18 @@ struct passwd {
char *pw_shell;
};
-__FC_EXTERN char __fc_getpwuid_pw_name[64];
-__FC_EXTERN char __fc_getpwuid_pw_passwd[64];
-__FC_EXTERN char __fc_getpwuid_pw_dir[64];
-__FC_EXTERN char __fc_getpwuid_pw_shell[64];
+__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];
struct passwd __fc_pwd =
- {.pw_name = __fc_getpwuid_pw_name,
- .pw_passwd = __fc_getpwuid_pw_passwd,
- .pw_dir = __fc_getpwuid_pw_dir,
- .pw_shell = __fc_getpwuid_pw_shell};
+ {.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;
@@ -76,11 +78,41 @@ extern struct passwd *getpwnam(const char *name);
*/
extern struct passwd *getpwuid(uid_t uid);
+/*@
+ // 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);
-extern int getpwnam_r(const char *, struct passwd *, char *,
- size_t, struct passwd **);
-extern int getpwuid_r(uid_t, struct passwd *, char *,
- size_t, struct passwd **);
extern void endpwent(void);
extern struct passwd *getpwent(void);
extern void setpwent(void);
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 51eee5493942a52e12279d33f5578f8ea2c689ab..31cc22262c686da14b52601fcb751379a012d83c 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";
diff --git a/tests/libc/fc_builtin_c.c b/tests/libc/fc_builtin_c.c
new file mode 100644
index 0000000000000000000000000000000000000000..ea336b1e04e74964ed8d1f4be98dbe91cc52e110
--- /dev/null
+++ b/tests/libc/fc_builtin_c.c
@@ -0,0 +1,37 @@
+#include "__fc_builtin.c"
+#include <limits.h>
+
+// The "sampling:unknown" assertions check whether a given value _may_ be
+// in the interval; they are supposed to return 'unknown', but never 'invalid'.
+
+int main() {
+ int i = Frama_C_interval(10, INT_MAX - 20);
+ //@ assert bounds: 10 <= i <= INT_MAX - 20;
+ //@ assert sampling:unknown: i == INT_MAX/2;
+
+ char c = Frama_C_char_interval(CHAR_MIN + 1, CHAR_MAX - 4);
+ //@ assert bounds: CHAR_MIN + 1 <= c <= CHAR_MAX - 4;
+ //@ assert sampling:unknown: c == 42;
+
+ unsigned int ui = Frama_C_unsigned_int_interval(INT_MAX, UINT_MAX);
+ //@ assert bounds: INT_MAX <= ui <= UINT_MAX;
+ //@ assert sampling:unknown: ui == UINT_MAX - 10000;
+
+ float f = Frama_C_float_interval(1.0, 2.0);
+ //@ assert bounds: 1.0 <= f <= 2.0;
+ //@ assert sampling:unknown: f == 1.5;
+
+ double one_e_100 = 0x1.249ad2594c37dp332;
+ double d = Frama_C_double_interval(1e10, one_e_100);
+ //@ assert bounds: 1e10 <= d <= one_e_100;
+ //@ assert sampling:unknown: d == 12345678901.2;
+
+ long l = Frama_C_long_interval(LONG_MIN, -2L);
+ //@ assert bounds: LONG_MIN <= l <= -2;
+ //@ assert sampling:unknown: l == -3;
+
+ unsigned long ul =
+ Frama_C_unsigned_long_interval(LONG_MAX - 1UL, LONG_MAX + 1UL);
+ //@ assert bounds: LONG_MAX - 1 <= ul <= LONG_MAX + 1;
+ //@ assert sampling:unknown: ul == LONG_MAX;
+}
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index f69e8856f26f206fb02669e031372919d735029e..8df9bf49c3366011cd6c9e3a700d0b59c9060c04 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
new file mode 100644
index 0000000000000000000000000000000000000000..d922ab4e1efacfb6929daebe1b0ce6160246ba19
--- /dev/null
+++ b/tests/libc/oracle/fc_builtin_c.res.oracle
@@ -0,0 +1,114 @@
+[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 fc_builtin_c.c:8.
+[eva] computing for function Frama_C_update_entropy <- Frama_C_interval <- main.
+ 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] 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 fc_builtin_c.c:12.
+[eva] computing for function Frama_C_interval <- Frama_C_char_interval <- main.
+ 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] 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 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] 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 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] 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 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] 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 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] 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 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] 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
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function Frama_C_update_entropy:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_double_interval:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_float_interval:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [-127..2147483627]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_char_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ __retres ∈ [-127..123]
+[eva:final-states] Values at end of function Frama_C_long_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [-2147483648..-2]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_int_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [2147483647..4294967295]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_long_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ {2147483646; 2147483647; 2147483648}
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ i ∈ {1073741823}
+ c ∈ {42}
+ ui ∈ {4294957295}
+ f ∈ {1.5}
+ one_e_100 ∈ {1e+100}
+ d ∈ [12345678901.2 .. 12345678901.2]
+ l ∈ {-3}
+ ul ∈ {2147483647}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 1309a406e2983d2ba843ca0103d55413f512e366..4cc020e5cf67e2cd14bf36a7352becb045d90275 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 703535ed601a795d89b306eadc7e5bd34a338857..a2690ea17cec097b5479a970ea4c1346d1363a57 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 0000000000000000000000000000000000000000..d2523bf304f3c2609e99a6d4a229739525eacf22
--- /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 9d329cca5b9c2c7685cd8b3e2cacecfdec83c97e..1ef5e0ebc0b91745bbe4736f93732c39357f5158 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 0000000000000000000000000000000000000000..d60731f7f1083760b046905442bf96b156a62413
--- /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);
+ }
+}