Merge pull request #7919 from tautschnig/features/library-pwd

C library: model getpwnam, getpwuid

Author: kroening

regression/cbmc-library/getpwnam-01/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+#ifndef _WIN32
+#  include <pwd.h>
+
+int main()
+{
+  const char *user = "user";
+  struct passwd *result = getpwnam(user);
+  (void)*result;
+  return 0;
+}
+#else
+int main()
+{
+}
+#endif

regression/cbmc-library/getpwnam-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/getpwuid-01/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#ifndef _WIN32
+#  include <pwd.h>
+
+int main()
+{
+  struct passwd *result = getpwuid(0);
+  (void)*result;
+  return 0;
+}
+#else
+int main()
+{
+}
+#endif

regression/cbmc-library/getpwuid-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/pwd.c

@@ -0,0 +1,48 @@
+/* FUNCTION: getpwnam */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_PWD_H_INCLUDED
+#    include <pwd.h>
+#    define __CPROVER_PWD_H_INCLUDED
+#  endif
+
+unsigned __VERIFIER_nondet_unsigned(void);
+
+struct passwd __CPROVER_passwd;
+
+struct passwd *getpwnam(const char *name)
+{
+  // make some fields non-null
+  __CPROVER_passwd.pw_name = (char *)name;
+  __CPROVER_passwd.pw_uid = __VERIFIER_nondet_unsigned();
+  __CPROVER_passwd.pw_gid = __VERIFIER_nondet_unsigned();
+  return &__CPROVER_passwd;
+}
+
+#endif
+
+/* FUNCTION: getpwuid */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_PWD_H_INCLUDED
+#    include <pwd.h>
+#    define __CPROVER_PWD_H_INCLUDED
+#  endif
+
+unsigned __VERIFIER_nondet_unsigned(void);
+
+#  ifndef LIBRARY_CHECK
+struct passwd __CPROVER_passwd;
+#  endif
+
+struct passwd *getpwuid(uid_t uid)
+{
+  // make some fields non-null
+  __CPROVER_passwd.pw_uid = uid;
+  __CPROVER_passwd.pw_gid = __VERIFIER_nondet_unsigned();
+  return &__CPROVER_passwd;
+}
+
+#endif