about summary refs log tree commit diff homepage
path: root/test/Merging/state_termination.c
blob: 3fe187606547a22cab5bfc82700609a48742a04f (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// RUN: %clang -emit-llvm -g -c -o %t.bc %s
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs  %t.bc 

#include <klee/klee.h>

int main(int argc, char** args){

  int x;

  char str[5];
  klee_make_symbolic(str, sizeof(str), "str");
  char *s = str;

  klee_open_merge();
  while(*s != 's')
      s++;
  klee_close_merge();

  return 0;
}