blob: f205aca71b4bdb8663af6df412195e7c4418443f (
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
|
// REQUIRES: stp
// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
//
// RUN: rm -rf %t.klee-out-minisat
// RUN: %klee --output-dir=%t.klee-out-minisat -solver-backend=stp --stp-sat-solver=minisat %t1.bc
// RUN: cat %t.klee-out-minisat/messages.txt %t.klee-out-minisat/warnings.txt > %t.klee-out-minisat/all.txt
// RUN: FileCheck --input-file=%t.klee-out-minisat/all.txt --check-prefix=MINISAT %s
//
// RUN: rm -rf %t.klee-out-riss
// RUN: %klee --output-dir=%t.klee-out-riss -solver-backend=stp --stp-sat-solver=riss %t1.bc
// RUN: cat %t.klee-out-riss/messages.txt %t.klee-out-riss/warnings.txt > %t.klee-out-riss/all.txt
// RUN: FileCheck --input-file=%t.klee-out-riss/all.txt --check-prefix=RISS %s
#include "klee/klee.h"
int main(void) {
int foo;
int bar = 42;
klee_make_symbolic(&foo, sizeof(foo), "foo");
if (foo) bar -= 17;
else bar += 5;
return bar;
}
// MINISAT: KLEE: Using STP solver backend
// MINISAT: {{KLEE: SAT solver: MiniSat|KLEE: Fallback SAT solver}}
// RISS: KLEE: Using STP solver backend
// RISS: {{KLEE: SAT solver: RISS|KLEE: Fallback SAT solver}}
|
