about summary refs log tree commit diff homepage
path: root/examples/get_sign/get_sign.c
blob: a379193df2c5fae6005c5eb5ab9e7e2ab1da88a6 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
/*
 * First KLEE tutorial: testing a small function
 */

#include "klee/klee.h"

int get_sign(int x) {
  if (x == 0)
     return 0;
  
  if (x < 0)
     return -1;
  else 
     return 1;
} 

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}