[klee-dev] Question about uclibc with scanf

[Randall]

Hi,

                I meet a odd problem when using klee to symbolize files. The
source code follows as:

                int main(int argc, char** argv)

                {

                                FILE* fp;

                                fp = fopen("A", "r+");

 

                                if(fp == NULL)

                                                printf("A file open
failed.\n");

                                else

                                {

                                                int n, re;

                                                if((re = fscanf(fp, "%d",
&n)) == -1)

                                                                printf("read
integer failed.\n");

                                                else

                                                                printf("read
integer successed.\n");

                                }

                

                                return 0;

                }

 

                Then, the klee command is:

                klee -libc=uclibc -posix-runtime ./test.bc -sym-files 1 4

 

                However, klee is halting when calling fscanf.

                KLEE: WARING ONCE: ioctl: (TCGETS) symbolic file, incomplete
model

                KLEE: WARING ONCE: calling external:
__isoc99_fscanf(181308416, 172167656, 172170256)

                halting here.

                

                Here I find it refers incomlete model,  and it mean that the
uclibc can not use fscanf ? I don't understand what happened. What should I
do so that I can use fscanf to read fomatting data from symbolize files?

                

                Thanks in advance.

                Randall  from Xidian University

 

-------------- next part --------------
HTML attachment scrubbed and removed