Hi,
To use symbolic files, you should use KLEE's symbolic environment
support. See https://klee.github.io/docs/options/#symbolic-environment
and the tutorials for information on how KLEE supports symbolic files.
Best wishes,
Cristian
On 18/01/2022 03:46, rongze xv wrote:
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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
