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

[Cristian Cadar]

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