test/Feature/SetForking.c


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

// RUN: %clang -emit-llvm -g -c %s -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log
// RUN: sort %t.log | uniq -c > %t.uniq.log
// RUN: grep "1 A" %t.uniq.log
// RUN: grep "1 B" %t.uniq.log
// RUN: grep "1 C" %t.uniq.log
#include "klee/klee.h"
#include <stdio.h>

int main() {
  klee_set_forking(0);
  
  if (klee_range(0, 2, "range")) {
    printf("A\n");
  } else {
    printf("A\n");
  }

  klee_set_forking(1);

  if (klee_range(0, 2, "range")) {
    printf("B\n");
  } else {
    printf("C\n");
  }

  return 0;
}