about summary refs log tree commit diff homepage
path: root/test/Feature/ReadStringAtAddress.c
blob: 64766282197bf683733879eb7e7b83f53e341d27 (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
extern void klee_warning(const char *);

// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s

int main(void) {
	char strings[] = {'s', 't', 'r', '1', '\0',
			  's', 't', 'r', '2', '\0',
			  's', 't', 'r', '3', '\0'};

	klee_warning(strings);
	// CHECK: WARNING: main: str1
	klee_warning(strings+5);
	// CHECK: WARNING: main: str2
	klee_warning(strings+2);
	// CHECK: WARNING: main: r1
	klee_warning(strings+10);
	// CHECK: WARNING: main: str3
	klee_warning(strings+6);
	// CHECK: WARNING: main: tr2

	char bytes[] = {'a', 'b', 'c', 'd'};
	// We should not crash, since it reads
	// only up to the size of the object
	klee_warning(bytes);
	// CHECK: WARNING ONCE: String not terminated by \0 passed to one of the klee_ functions
	// CHECK: WARNING: main: abcd

	return 0;
}