1+ // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
2+ // RUN: rm -rf %t.klee-out
3+ // RUN: %klee --output-dir=%t.klee-out --entry-point=klee_entry --skip-not-lazy-initialized --min-number-elements-li=1 %t1.bc 2>&1
4+ // RUN: %ktest-tool %t.klee-out/test000003.ktest | FileCheck %s
5+
6+ #include "klee/klee.h"
7+
8+ struct StructWithPointer {
9+ int x ;
10+ int * y ;
11+ };
12+
13+ struct StructWithDoublePointer {
14+ int x ;
15+ int * * y ;
16+ };
17+
18+ struct StructWithArrayOfPointer {
19+ int x ;
20+ int * y [2 ];
21+ };
22+
23+ struct StructWithStructWithPointer {
24+ struct StructWithPointer swp ;
25+ struct StructWithDoublePointer * swdp ;
26+ };
27+
28+ struct StructManyPointers {
29+ int a ;
30+ int * b ;
31+ int * * c ;
32+ int * * * d ;
33+ };
34+
35+ struct StructComplex {
36+ int x ;
37+ int * y ;
38+ int * * z ;
39+ struct StructWithPointer * swp ;
40+ struct StructWithDoublePointer * * swdp ;
41+ struct StructManyPointers smp ;
42+ };
43+
44+ int sumStructWithPointer (struct StructWithPointer par ) {
45+ return par .x + * par .y ;
46+ }
47+
48+ int sumStructWithPointerAsPointer (struct StructWithPointer * par ) {
49+ return par -> x + * par -> y ;
50+ }
51+
52+ int sumStructWithDoublePointer (struct StructWithDoublePointer par ) {
53+ return par .x + * * par .y ;
54+ }
55+
56+ int sumStructWithArrayOfPointer (struct StructWithArrayOfPointer par ) {
57+ return par .x + * (par .y [0 ]) + * (par .y [1 ]);
58+ }
59+
60+ int sumStructWithStructWithPointer (struct StructWithStructWithPointer par ) {
61+ int sswp = sumStructWithPointer (par .swp );
62+ int sswdp = sumStructWithDoublePointer (* par .swdp );
63+ return sswp + sswdp ;
64+ }
65+
66+ int sumStructManyPointers (struct StructManyPointers par ) {
67+ return par .a + * par .b + * * par .c + * * * par .d ;
68+ }
69+
70+ int sumStructComplex (struct StructComplex par ) {
71+ int sswp = sumStructWithPointer (* par .swp );
72+ int sswdp = sumStructWithDoublePointer (* * par .swdp );
73+ int ssmp = sumStructManyPointers (par .smp );
74+ return par .x + * par .y + * * par .z + sswp + sswdp + ssmp ;
75+ }
76+
77+ // CHECK: object 2: pointers: [(8, 3, 0)]
78+ int klee_entry (int utbot_argc , char * * utbot_argv , char * * utbot_envp ) {
79+ struct StructComplex par ;
80+ klee_make_symbolic (& par , sizeof (par ), "par" );
81+ klee_prefer_cex (& par , par .x >= -10 & par .x <= 10 );
82+ klee_prefer_cex (& par , par .smp .a >= -10 & par .smp .a <= 10 );
83+ ////////////////////////////////////////////
84+ int utbot_result ;
85+ klee_make_symbolic (& utbot_result , sizeof (utbot_result ), "utbot_result" );
86+ int utbot_tmp = sumStructComplex (par );
87+ klee_assume (utbot_tmp == utbot_result );
88+ return 0 ;
89+ }
0 commit comments