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

2022-03-09 Thread 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@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

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

2022-01-17 Thread 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
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev