1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
// RUN: %clang -D_FILE_OFFSET_BITS=64 %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out %t.klee-out-tmp
// RUN: %gentmp %t.klee-out-tmp
// RUN: %klee --output-dir=%t.klee-out --run-in-dir=%t.klee-out-tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
// RUN: sort %t1.log %t2.log | uniq -c > %t3.log
// RUN: grep -q "4 COUNT" %t3.log
// For this test really to work as intended it needs to be run in a
// directory large enough to cause uclibc to do multiple getdents
// calls (otherwise uclibc will handle the seeks itself). We should
// create a bunch of files or something.
//
// It is even more important for this test because it requires the
// directory not to change while running, which might be a lot to
// demand of /tmp.
#define _LARGEFILE64_SOURCE
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <dirent.h>
#include <sys/stat.h>
#include <errno.h>
int main(int argc, char **argv) {
struct stat s;
int res = stat("A", &s);
int hasA = !(res!=0 && errno==ENOENT);
//printf("sizeof(dirent) = %d\n", sizeof(struct dirent));
//printf("sizeof(dirent64) = %d\n", sizeof(struct dirent64));
//printf("\"A\" exists: %d\n", hasA);
DIR *d = opendir(".");
assert(d);
int snum = 1;
if (klee_range(0,2,"range")) {
snum = 2;
printf("state%d\n", snum);
}
int foundA = 0, count = 0;
struct dirent *de;
while ((de = readdir(d))) {
// printf("state%d: dirent: %s\n", snum, de->d_name);
if (strcmp(de->d_name, "A") == 0)
foundA = 1;
count++;
}
closedir(d);
//printf("found A: %d\n", foundA);
// Ensure atomic write
char buf[64];
sprintf(buf, "COUNT: %d\n", count);
fputs(buf, stdout);
assert(hasA == foundA);
return 0;
}
|
