[prev in list] [next in list] [prev in thread] [next in thread] 

List:       klee-dev
Subject:    Re: [klee-dev] How should the function parameter be symbolised if the function parameter is a file t
From:       Cristian Cadar <c.cadar () imperial ! ac ! uk>
Date:       2022-03-09 13:43:54
Message-ID: a343528b-4e58-b328-e077-43560053a5fd () imperial ! ac ! uk
[Download RAW message or body]

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

[prev in list] [next in list] [prev in thread] [next in thread]