diff --git a/examples/get_sign.c b/examples/get_sign.c index 0e5cf99d0193dab34b8ed2a1fb152557f8e5a4f2..1c7353c762afb8694d34d2247a6e7cc20c817d83 100644 --- a/examples/get_sign.c +++ b/examples/get_sign.c @@ -9,8 +9,11 @@ int get_sign(int x) { if (x == 0) return 0; + if (x == 1) + return 0; + - if (x < 0) + if (x < 2) return -1; else return 1; @@ -193,7 +196,8 @@ int main() // `klee_make_symbolic(&a, sizeof(a), "a");` // works when you run `klee` to generate test cases: // -// [your answer here] +// [It takes the address of variable a and treat is as symbolic. +// It will mark the memory locattion of a as symbolic.] // (hint, mark memory region as symbolic) // // Explain in your own words how