[klee-dev] About filename extension of symbolic files

[Weiqi Wang]

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.wang at mail.utoronto.ca>
Sent: Friday, August 20, 2021 6:55 PM
To: klee-dev at imperial.ac.uk<mailto:klee-dev at 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


-------------- next part --------------
HTML attachment scrubbed and removed