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@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
