[klee-dev] Errors when files unconform to the format!

[Cristian Cadar]

Hi Yukai,

You can use klee_assume 
(https://klee.github.io/docs/intrinsics/#klee_assumecondition) on the 
desired symbolic file created by the POSIX runtime, see 
https://github.com/klee/klee/blob/master/runtime/POSIX/fd_init.c#L61

Best,
Cristian

On 06/06/2022 15:06, 房合钧 wrote:
> Hello!
> 
> I recently tried to use Klee to detect a project that handles PNG 
> images. I use sym files to generate input files, but the generated files 
> do not necessarily meet the format requirements of PNG pictures. 
> Therefore, I hope to fix some characters to make the generated files 
> conform to the format.
> 
> I found in the past mailing list that you mentioned that it can be 
> specified through the file in POSIX, but I can't figure out which file 
> can be set. So can you tell me the specific file path.
> 
> Similarly, I want to confirm whether Klee is also used in POSIX_ Assume 
> (), or there are other functions.
> 
> If you are willing to give a simple example, it would be great.
> 
> 
> Thanks and regards,
> yukai
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev