[klee-dev] GCov in KLEE

[Nowack, Martin]

Hi Norlina,


On 29. Jun 2018, at 08:10, Norlina Pasaribu <norlinap at xlfutureleaders.com<mailto:norlinap at xlfutureleaders.com>> wrote:

Hello all

I would like to try to test the space c program using gCov in KLEE. I tried the tutorial in KLEE from this site http://klee.github.io/tutorials/testing-coreutils/
and for this step, I find this result

klee at a6bf3640ea87:~$ ls
klee-last   klee-out-1  klee_build  obj-gcov  space.c
klee-out-0  klee-out-2  klee_src    space.bc  strutt.h
klee at a6bf3640ea87:~$ ls klee-output-0

There is a small mistake: the directory is actually called `klee-out-0`,
Therefore `ls klee-out-0` should print the right output.


ls: cannot access klee-output-0: No such file or directory
klee at a6bf3640ea87:~$ ls klee-last
assembly.ll   test000001.ktest  test000006.ktest  test000011.ktest
info          test000002.ktest  test000007.ktest  test000012.ktest
messages.txt  test000003.ktest  test000008.ktest  test000013.ktest
run.istats    test000004.ktest  test000009.ktest  warnings.txt
run.stats     test000005.ktest  test000010.ktest

This was successful.


klee at a6bf3640ea87:~$ klee-replay ./space.c ../../klee-last/*.ktest
klee-replay: error: input file ../../klee-last/*.ktest not valid.

To run the test, you need to provide the native binary as an input and the correct location of the test files.
In your case, it should be:
`klee-replay ./space klee-last/*.ktest`

Best,
Martin
-------------- next part --------------
HTML attachment scrubbed and removed