diff options
Diffstat (limited to 'examples/get_sign/get_sign.c')
-rw-r--r-- | examples/get_sign/get_sign.c | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/examples/get_sign/get_sign.c b/examples/get_sign/get_sign.c new file mode 100644 index 00000000..a97ac375 --- /dev/null +++ b/examples/get_sign/get_sign.c @@ -0,0 +1,20 @@ +/* + * First KLEE tutorial: testing a small function + */ + + +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); +} |