[posix-runtime] Simple GET/SET_LK model

1 files changed, 19 insertions, 0 deletions

diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index ae08183f..240e589e 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -995,6 +995,7 @@ int fcntl(int fd, int cmd, ...) {
   exe_file_t *f = __get_file(fd);
   va_list ap;
   unsigned arg; /* 32 bit assumption (int/ptr) */
+  struct flock *lock;
 
   if (!f) {
     errno = EBADF;
@@ -1007,6 +1008,10 @@ int fcntl(int fd, int cmd, ...) {
    if (cmd==F_GETFD || cmd==F_GETFL || cmd==F_GETOWN) {
 #endif
     arg = 0;
+  } else if (cmd == F_GETLK || cmd == F_SETLK || cmd == F_SETLKW) {
+    va_start(ap, cmd);
+    lock = va_arg(ap, struct flock *);
+    va_end(ap);
   } else {
     va_start(ap, cmd);
     arg = va_arg(ap, int);
@@ -1036,6 +1041,20 @@ int fcntl(int fd, int cmd, ...) {
       */
       return 0;
     }
+    // Initially no other process keeps a lock, so we say the file is unlocked.
+    // Of course this doesn't account for a program locking and then checking if
+    // a lock is there. However this is quite paranoid programming and we assume
+    // doesn't happen.
+    case F_GETLK: {
+      lock->l_type = F_UNLCK;
+      return 0;
+    }
+    // We assume the application does locking correctly and will lock/unlock
+    // files correctly.
+    // Therefore this call always succeeds.
+    case F_SETLK: {
+      return 0;
+    }
     default:
       klee_warning("symbolic file, ignoring (EINVAL)");
       errno = EINVAL;