about summary refs log tree commit diff homepage
path: root/examples
diff options
context:
space:
mode:
Diffstat (limited to 'examples')
-rw-r--r--examples/get_sign/get_sign.c20
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);
+}