[klee-dev] Error using klee-replay

[Cristian Cadar]

Hi Sean, this is a KLEE bug.  Please open an issue on GitHub, and I'll 
try to fix it soon.

Thanks,
Cristian

On 12/12/16 17:48, Sean Heelan wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>