blob: fde864d7b65a92f4a9d6d9ac33a7d45ba3c217ea (
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
36
37
38
39
40
41
|
// RUN: %llvmgcc -I../../../include -emit-llvm -g -c %s -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --write-kqueries %t.bc > %t.log
// RUN: cat %t.klee-out/test000001.kquery %t.klee-out/test000002.kquery %t.klee-out/test000003.kquery %t.klee-out/test000004.kquery > %t1
// RUN: grep "a\[1\]" %t1 | wc -l | grep 2
// RUN: grep "a\[100\]" %t1 | wc -l | grep 2
/* Tests that the Array factory correctly distinguishes between arrays created at the same location but with different sizes */
#include <stdio.h>
#include <stdlib.h>
char* mk_sym(int size) {
char *a = malloc(size);
klee_make_symbolic(a, size, "a");
return a;
}
int main() {
int t;
char *a, *b;
klee_make_symbolic(&t, sizeof(t), "t");
if (t) {
printf("Allocate obj of size 1\n");
a = mk_sym(1);
if (a[0] > 'a')
printf("Yes\n");
else printf("No\n");
}
else {
printf("Allocate obj of size 2\n");
b = mk_sym(100);
if (b[99] > 'a')
printf("Yes\n");
else printf("No\n");
}
return 0;
}
|
