[klee-dev] Question about uclibc with scanf

[Cristian Cadar]

Hi Randall, this is a known bug:
https://github.com/klee/klee/issues/30

If you'd like to help fix it, please follow up on GitHub.

Best,
Cristian

On 20/10/16 11:13, Randall wrote:
> 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
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>