test/regression/2015-08-30-sdiv-1.c


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=false %t.bc

/* Division by constant can be optimized.using mul/shift
 * For signed division, div by 1 or -1 cannot be optimized like that.
 */
#include <stdint.h>
int main() {
  int32_t dividend;
  klee_make_symbolic(&dividend, sizeof dividend, "Dividend");
  if ((3 ^ (dividend & 2)) / 1)
    return 1;
  if ((3 ^ (dividend & 2)) / -1)
    return 1;
  return 0;
}