[klee-dev] FilePerm.c test fails

[Cristian Cadar]

Unfortunately, we haven't documented that issue very well, but this is 
why I remember we had that option.  We could consider enabling that 
option by default and see if we encounter any problems.

Regarding .cov files, they only record any previously uncovered lines 
executed by that path.

Cristian

On 22/08/14 14:04, Daniel Liew wrote:
> 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.
>