From fb96b6370b88d9b7b07fa52ebf54706a8e8a110b Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Thu, 19 Mar 2020 14:46:29 +0000 Subject: [posix-runtime] Simple GET/SET_LK model --- runtime/POSIX/fd.c | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'runtime/POSIX') 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; -- cgit 1.4.1