Okay, I think the problem is that KLEE doesn't treat the first
argument as symbolic because it's usually the name of the program, so
the argv[0][0] expression refers to a concrete value.
Suhabe
On Fri, Sep 25, 2009 at 3:17 PM, Suhabe Bugrara <suhabe at stanford.edu> wrote:
> Hello,
>
> I'm running KLEE on the following program:
>
> int main(int argc, char* argv[]) {
> ? ? ? ?if (argc >= 1) {
> ? ? ? ? ? ? ? ?printf("zero ");
>
> ? ? ? ? ? ? ? ?if (argv[0][0] == 'c') {
> ? ? ? ? ? ? ? ? ? ? ? ?printf("one ");
> ? ? ? ? ? ? ? ?}
> ? ? ? ? ? ? ? ?else {
> ? ? ? ? ? ? ? ? ? ? ? ?printf("two ");
> ? ? ? ? ? ? ? ?}
> ? ? ? ?}
> ? ? ? ?else {
> ? ? ? ? ? ? ? ?printf("three ");
> ? ? ? ?}
>
> ? ? ? ?return 0;
> }
>
> using the following command:
>
> klee --libc=klee --posix-runtime --init-env test.bc --sym-args 0 1 15
>
> I expected the output to be "zero one two three", but actual output is
> "zero two". It looks like it's not forking at each of the branches.
> Any ideas on where I'm going wrong?
>
> Thanks.
>
> Suhabe
>
