Hello,
In the meantime, I found out under what circumstances the FilePerm.c
test fails. The problem is compiler-dependent and occurs with LLVM 2.9,
but not with LLVM 3.4.
The part of the code that is relevant for this test case is in the
has_permission() method in runtime/POSIX/fd.c (this method is called by
__fd_open()). At the end of has_permission() there are the following two
checks:
if (read_access && ((mode & S_IRUSR) | (mode & S_IRGRP) | (mode & S_IROTH)))
return 0;
if (write_access && !((mode & S_IWUSR) | (mode & S_IWGRP) | (mode &
S_IWOTH)))
return 0;
Since the method is called with a symbolic file's symbolic stat (and
thus the mode in stat is symbolic, too), and the file is opened with
O_RDWR (so both read_access and write_access are true), the following 3
paths are explored:
1) open() succeeds: first if's condition is false, second if's condition
is false -> has_permission() returns 1 -> __fd_open()/open() returns
non-negative fd
2) open() fails: first if's condition is true -> has_permission()
returns 0 -> __fd_open()/open() returns -1
3) open() fails: first if's condition is false, second if's condition is
true -> has_permission() returns 0 -> __fd_open()/open() returns -1
But if a debug build of KLEE is built according to the instructions in
the developer's guide, namely using CXXFLAGS="-g -O0" CFLAGS="-g -O0",
then path 3 is not explored, thus only 2 test cases are generated and
FilePerm.c fails.
I've tested this on Ubuntu 14.04 with LLVM 2.9 (LLVM-GCC 4.2), STP r-940
and upstream, klee-uclibc klee_0_9_29, and KLEE revisions e87af57 and
547dd6f (the current newest one).
As mentioned above, with LLVM 3.4 (Clang 3.4) the error does not occur.
Best regards,
Emil
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
