blob: 00deab5f08e280f3c1113fd8cf5aad444f13d9da (
plain) (
blame)
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
|
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-files 1 8 >%t.log
#include <unistd.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <errno.h>
#include <assert.h>
int main(int argc, char** argv) {
char buf[32];
// If count is zero, read() returns zero and has no other results. (man page)
int x = read(0, 0, 0);
assert(x == 0);
int fd = open("A", O_RDONLY);
assert(fd != -1);
// EFAULT buf is outside your accessible address space. (man page)
x = read(fd, 0, 1);
assert(x == -1 && errno == EFAULT);
// EBADF fd is not a valid file descriptor (man page)
x = read(-1, buf, 1);
assert(x == -1 && errno == EBADF);
fd = open("A", O_RDONLY);
assert(fd != -1);
x = read(fd, buf, 1);
assert(x == 1);
}
|
