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
