[klee-dev] Error using klee-replay

[Sean Heelan]

Hi all,

When trying to use klee-replay to replay a test case I'm getting the
following errors:

$ ./Documents/git/klee/Release+Asserts/bin/klee-replay ./target
klee-out-0/test000044.ktest
./Documents/git/klee/Release+Asserts/bin/klee-replay: TEST CASE:
klee-out-0/test000044.ktest
./Documents/git/klee/Release+Asserts/bin/klee-replay: ARGS: "./target" "-f"
"B"
warning: check_file A: dev mismatch: 64770 vs 0
warning: check_file A: mode mismatch: 0100000 vs 0
warning: check_file A: nlink mismatch: 1 vs 0
warning: check_file A: blksize mismatch: 4096 vs 0
warning: check_file B: dev mismatch: 64770 vs 0
warning: check_file B: mode mismatch: 0100000 vs 0
warning: check_file B: nlink mismatch: 1 vs 0
warning: check_file B: blksize mismatch: 4096 vs 0
cannot open input image file B
./Documents/git/klee/Release+Asserts/bin/klee-replay: EXIT STATUS: ABNORMAL
1 (0 seconds)

Two files called A and B have been created in the current directory with
the following properties:

$ ls -l A B
----------.  1 sean sean   64 Jan  1  1970 B
----------.  1 sean sean   64 Jan  1  1970 A

The contents of the files are correct, and if I chmod them so they are
readable then they do produce the expected results when run, so it looks
like its just an issue with how the permissions of the file, and its
attributes, are set.

Any thoughts on what might be causing the above?

FYI: I'm using Fedora 24, kernel 4.8.4 and the latest version of klee from
github.

Cheers,
Sean
-------------- next part --------------
HTML attachment scrubbed and removed