Hi Wujie,
I don't recall, to be honest, but I think KLEE doesn't currently
support pread because we use it to implement our file model, and don't
instrument it.
- Daniel
On Sun, Jun 6, 2010 at 1:15 AM, Wujie Zheng <wjzheng at cse.cuhk.edu.hk> wrote:
> Hi,
>
> I am running klee on some programs with the pread function, and klee
> cannot return the correct results.
>
> I write a test program test.c as follows.
>
> #include <stdio.h>
> int main(int argc, char* argv[])
> {
> int ch;
> int input = open( "tmp.txt", "r" );
> char buf[10];
> pread(input, buf, 10, 0);
> printf("get %c\n", buf[0]);
> return 0;
> }
>
> The file tmp.txt contains only 1 line "abcd".
>
> I first compiled test.c with gcc. Running the program returned "get a"
> correctly.
>
> I then compiled test.c with llvm-gcc. However, running the program
> returned "get ?", which is incorrect.
>
> Does klee not support pread, or do I misunderstand sth.?
>
> Best wishes,
> Wujie
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
