[klee-dev] Simple code for KLEE

[Daniel Liew]

Your code uses atoi() which isn't part of your 2plus2 program. Notice
that KLEE warns about this

KLEE: WARNING: undefined reference to function: atoi

and later calls this function

KLEE: WARNING ONCE: calling external: atoi(53548944)

An external function, is a function that isn't in the bitcode being
executed (which is your 2plus2.o code linked with which ever libraries
you asked KLEE to use. In your case you asked only for the POSIX
runtime).

When KLEE encounters an external function it makes the arguments to
that function concrete and then calls the native function ``atoi()``.
In your case making arguments to atoi() concrete will cause test cases
to be lost.

Try linking with klee-uclibc (use -libc=uclibc) which probably
provides an implementation of atoi(). If it doesn't you can always add
your own.

Note atoi() probably has quite a lot of branching behaviour so you may
generate many more paths that you might expect. In which case you
might just want to do something much simpler like this...

```
int plus(int first){

                  if(first+2 == 4)return 1;

                  return 0;
}


int main(int argc, char *argv[]){

                   int x;
                   klee_make_symbolic(&x, sizeof(x));
                   return plus(x);
}
```

Hope that helps.