[klee-dev] FilePerm.c test fails

Daniel Liew daniel.liew at imperial.ac.uk
Fri Aug 22 14:04:19 BST 2014


On 22 August 2014 12:43, Cadar, Cristian <c.cadar at imperial.ac.uk> wrote:
> Hi Emil,
>
> Lines are truncated to go over a kcachegrind bug; to avoid this problem,
> just pass -no-truncate-source-lines to KLEE.


Does KCacheGrind work with .ll files? If not I don't see a reason to
truncate the .ll file. Also is this bug in kcachegrind still relevant
with a modern version (e.g. I have 0.7.4).

I also tried looking  FilePerm.c . Whilst the test does pass for me I
tried adding the -write-cov option. The coverage files seem completely
wrong (I'm assuming each .cov file is supposed to show the set of
lines that were visited), lots lines that ought to be there are
missing.




More information about the klee-dev mailing list