C library: add creat, open, openat

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

@@ -0,0 +1,15 @@
+#include <fcntl.h>
+
+#ifdef _WIN32
+#  define MODE_T int
+#else
+#  define MODE_T mode_t
+#endif
+
+int main()
+{
+  char *unint_path;
+  MODE_T mode;
+  int fd = creat(unint_path, mode);
+  return 0;
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+dereference failure: pointer invalid in \*pathname: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -3,7 +3,10 @@
 
 int main()
 {
-  fcntl();
-  assert(0);
+  int flags;
+  int fd = open("foo", flags);
+  int cmd;
+  int result = fcntl(fd, cmd);
+  assert(fd >= 0 || result == -1);
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

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

@@ -0,0 +1,9 @@
+#include <fcntl.h>
+
+int main()
+{
+  char *unint_path;
+  int flags;
+  int fd = open(unint_path, flags);
+  return 0;
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+dereference failure: pointer invalid in \*pathname: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

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

@@ -0,0 +1,10 @@
+#include <fcntl.h>
+
+int main()
+{
+  int dirfd;
+  char *unint_path;
+  int flags;
+  int fd = openat(dirfd, unint_path, flags);
+  return 0;
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+dereference failure: pointer invalid in \*pathname: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/library/fcntl.c

@@ -1,17 +1,252 @@
-/* FUNCTION: fcntl */
+/* FUNCTION: __CPROVER_fcntl */
 
 #ifndef __CPROVER_FCNTL_H_INCLUDED
 #include <fcntl.h>
 #define __CPROVER_FCNTL_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 int __VERIFIER_nondet_int(void);
 
-int fcntl(int fd, int cmd, ...)
+int __CPROVER_fcntl(int fd, int cmd)
 {
 __CPROVER_HIDE:;
+  if(fd < 0)
+  {
+    errno = EBADF;
+    return -1;
+  }
+
   int return_value=__VERIFIER_nondet_int();
   (void)fd;
   (void)cmd;
   return return_value;
 }
+
+/* FUNCTION: fcntl */
+
+int __CPROVER_fcntl(int, int);
+
+int fcntl(int fd, int cmd, ...)
+{
+  return __CPROVER_fcntl(fd, cmd);
+}
+
+/* FUNCTION: _fcntl */
+
+int __CPROVER_fcntl(int, int);
+
+int _fcntl(int fd, int cmd, ...)
+{
+  return __CPROVER_fcntl(fd, cmd);
+}
+
+/* FUNCTION: fcntl64 */
+
+int __CPROVER_fcntl(int, int);
+
+int fcntl64(int fd, int cmd, ...)
+{
+  return __CPROVER_fcntl(fd, cmd);
+}
+
+/* FUNCTION: __CPROVER_open */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int(void);
+
+int __CPROVER_open(const char *pathname, int flags)
+{
+__CPROVER_HIDE:;
+  int return_value = __VERIFIER_nondet_int();
+  __CPROVER_assume(return_value >= -1);
+  (void)*pathname;
+  (void)flags;
+  return return_value;
+}
+
+/* FUNCTION: open */
+
+int __CPROVER_open(const char *, int);
+
+int open(const char *pathname, int flags, ...)
+{
+  return __CPROVER_open(pathname, flags);
+}
+
+/* FUNCTION: _open */
+
+int __CPROVER_open(const char *, int);
+
+int _open(const char *pathname, int flags, ...)
+{
+  return __CPROVER_open(pathname, flags);
+}
+
+/* FUNCTION: open64 */
+
+int __CPROVER_open(const char *, int);
+
+int open64(const char *pathname, int flags, ...)
+{
+  return __CPROVER_open(pathname, flags);
+}
+
+/* FUNCTION: __CPROVER_creat */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+#ifndef MODE_T
+#  ifdef _WIN32
+#    define MODE_T int
+#  else
+#    define MODE_T mode_t
+#  endif
+#endif
+
+int __VERIFIER_nondet_int(void);
+
+int __CPROVER_creat(const char *pathname, MODE_T mode)
+{
+__CPROVER_HIDE:;
+  int return_value = __VERIFIER_nondet_int();
+  __CPROVER_assume(return_value >= -1);
+  (void)*pathname;
+  (void)mode;
+  return return_value;
+}
+
+/* FUNCTION: creat */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+#ifndef MODE_T
+#  ifdef _WIN32
+#    define MODE_T int
+#  else
+#    define MODE_T mode_t
+#  endif
+#endif
+
+int __CPROVER_creat(const char *, MODE_T);
+
+int creat(const char *pathname, MODE_T mode)
+{
+  return __CPROVER_creat(pathname, mode);
+}
+
+/* FUNCTION: _creat */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+#ifndef MODE_T
+#  ifdef _WIN32
+#    define MODE_T int
+#  else
+#    define MODE_T mode_t
+#  endif
+#endif
+
+int __CPROVER_creat(const char *, MODE_T);
+
+int _creat(const char *pathname, MODE_T mode)
+{
+  return __CPROVER_creat(pathname, mode);
+}
+
+/* FUNCTION: creat64 */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+#ifndef MODE_T
+#  ifdef _WIN32
+#    define MODE_T int
+#  else
+#    define MODE_T mode_t
+#  endif
+#endif
+
+int __CPROVER_creat(const char *, MODE_T);
+
+int creat64(const char *pathname, MODE_T mode)
+{
+  return __CPROVER_creat(pathname, mode);
+}
+
+/* FUNCTION: __CPROVER_openat */
+
+#ifndef __CPROVER_FCNTL_H_INCLUDED
+#  include <fcntl.h>
+#  define __CPROVER_FCNTL_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int(void);
+
+int __CPROVER_openat(int dirfd, const char *pathname, int flags)
+{
+__CPROVER_HIDE:;
+  if(dirfd < 0)
+  {
+    errno = EBADF;
+    return -1;
+  }
+
+  int return_value = __VERIFIER_nondet_int();
+  __CPROVER_assume(return_value >= -1);
+  (void)dirfd;
+  (void)*pathname;
+  (void)flags;
+  return return_value;
+}
+
+/* FUNCTION: openat */
+
+int __CPROVER_openat(int dirfd, const char *pathname, int flags);
+
+int openat(int dirfd, const char *pathname, int flags, ...)
+{
+  return __CPROVER_openat(dirfd, pathname, flags);
+}
+
+/* FUNCTION: _openat */
+
+int __CPROVER_openat(int dirfd, const char *pathname, int flags);
+
+int _openat(int dirfd, const char *pathname, int flags, ...)
+{
+  return __CPROVER_openat(dirfd, pathname, flags);
+}
+
+/* FUNCTION: openat64 */
+
+int __CPROVER_openat(int dirfd, const char *pathname, int flags);
+
+int openat64(int dirfd, const char *pathname, int flags, ...)
+{
+  return __CPROVER_openat(dirfd, pathname, flags);
+}

src/ansi-c/library_check.sh

@@ -31,10 +31,14 @@ perl -p -i -e 's/^__CPROVER_contracts_library\n//' __functions
 
 # Some functions are implicitly covered by running on different operating
 # systems:
+perl -p -i -e 's/^_creat\n//' __functions # creat, macOS
+perl -p -i -e 's/^_fcntl\n//' __functions # fcntl, macOS
 perl -p -i -e 's/^_fopen\n//' __functions # fopen, macOS
 perl -p -i -e 's/^_getopt\n//' __functions # getopt, macOS
 perl -p -i -e 's/^_mmap\n//' __functions # mmap, macOS
 perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
+perl -p -i -e 's/^_open\n//' __functions # open, macOS
+perl -p -i -e 's/^_openat\n//' __functions # openat, macOS
 perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS
 perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
 perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows
@@ -52,6 +56,8 @@ perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
 perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
 
 # Some functions are covered by existing tests:
+perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
+perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
 perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen