Hi, I’m posting my solution here in case anybody else would find it useful. Commenting out https://github.com/klee/klee/blob/master/runtime/POSIX/fd.c#L60-L61 works in my case. If anyone would like to use the same approach, keep in mind that any filename starting with A, B … would now be symbolic.
Best, Weiqi From: Weiqi Wang<mailto:wq.w...@mail.utoronto.ca> Sent: Friday, August 20, 2021 6:55 PM To: klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> Subject: [klee-dev] About filename extension of symbolic files EXTERNAL EMAIL: Hi, I was trying to run klee with GraphicsMagick(GM) using command: klee --disable-verify --only-replay-seeds --libc=uclibc --posix-runtime --seed-file rectangular.ktest ./gm.bc identify A -sym-files 1 80 rectangular.ktest is generated using `gen-bout –sym-file rectangular.mvg –but-file rectangular.ktest` Content of rectangular.mvg: push graphic-context viewbox 0 0 100 60 rectangle 5,5 15,15 pop graphic-context In the output I saw GM complains: ./gm.bc identify: No decode delegate for this image format (A) ./gm.bc identify: Request did not return an image I suspect this is because GM checks the filename extension. Because when I run it without klee `gm identify A` returns same error `gm identify A.mvg` works fine (In this case I manually created concrete file A and A.mvg containing the same content as rectangular.mvg) Could anyone explain how to specify symbolic file with extensions? Best, Weiqi
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
