[klee-dev] About filename extension of symbolic files

[Weiqi Wang]

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