blob: c49bbd1b145fcd5c6c51dda41602d99b8e0dc1fe (
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
|
// REQUIRES: z3
// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -solver-backend=z3 -write-cvcs -write-smt2s -debug-z3-dump-queries=%t.smt2 %t1.bc
// RUN: cat %t.klee-out/test000001.smt2 | FileCheck --check-prefix=TEST-CASE %s
// RUN: cat %t.klee-out/test000002.smt2 | FileCheck --check-prefix=TEST-CASE %s
// RUN: cat %t.smt2 | FileCheck %s
#include "klee/klee.h"
int main(int argc, char **argv) {
// CHECK-DAG: (assert (= (select const_arr1_1 #x00000000) #x67))
// CHECK-DAG: (assert (= (select const_arr1_1 #x00000001) #x79))
// CHECK-DAG: (assert (= (select const_arr1_1 #x00000002) #x7a))
// CHECK-DAG: (assert (= (select const_arr1_1 #x00000003) #x00))
// TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv0 32) ) (_ bv103 8) ) )
// TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv1 32) ) (_ bv121 8) ) )
// TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv2 32) ) (_ bv122 8) ) )
// TEST-CASE-DAG: (assert (= (select const_arr1 (_ bv3 32) ) (_ bv0 8) ) )
char c[4] = {'g', 'y', 'z', '\0'};
unsigned i;
klee_make_symbolic(&i, sizeof i, "i");
klee_assume(i < 4);
if (c[i] < 'y')
return 0;
else
return 1;
}
|
