[klee-dev] How should the function parameter be symbolised if the function parameter is a file type?

[rongze xv]

Hi,

I am confused about How should the function parameter be symbolised if
the function parameter is a file type.

For example, I use KLEE to test a function ok_png ok_png_read(FILE *file,
ok_png_decode_flags decode_flags), the test code written is as follows:
int main(int argc, char **argv){
     FILE *file = malloc(sizeof(FILE));
     klee_make_symbolic(file,sizeof(FILE),"file");
     ok_png_read(file,OK_PNG_COLOR_FORMAT_RGBA);
}
But always get something like this, “memcpy.c:29: memory error: out of
bound pointer”, I think the function is not tested successfully, I don't
know how to handle such a situation, please help.

If you can reply to me in your spare time, thank you very much!!

Sincerely，
Xu Rongze
-------------- next part --------------
HTML attachment scrubbed and removed