about summary refs log tree commit diff homepage
path: root/test/Merging/state_termination.c
blob: 2bf60f9174331f1cd4ef2cc4a8df92e9cb7668ea (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;
}