about summary refs log tree commit diff homepage
path: root/test/Feature/LowerSwitch.c
blob: c4d9644abe9389961a0afa75e9b85c46ed798ae9 (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
// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
// RUN: not test -f klee-last/test000010.bout
// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
// RUN: test -f klee-last/test000010.bout

#include <stdio.h>

int main(int argc, char **argv) {
  int c = klee_range(0, 256, "range");
  
  switch(c) {
  case 0: printf("0\n"); break;
  case 10: printf("10\n"); break;
  case 16: printf("16\n"); break;
  case 17: printf("17\n"); break;
  case 18: printf("18\n"); break;
  case 19: printf("19\n"); break;
#define C(x) case x: case x+1: case x+2: case x+3
#define C2(x) C(x): C(x+4): C(x+8): C(x+12)
#define C3(x) C2(x): C2(x+16): C2(x+32): C2(x+48)
  C3(128):
    printf("bignums: %d\n", c); break;
  default: 
    printf("default\n");
    break;
  }

  return 0;
}