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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
