Hi Norlina,
On 29. Jun 2018, at 08:10, Norlina Pasaribu <[email protected]<mailto:[email protected]>> 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@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@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@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@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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
