[klee-dev] Question regarding -write-cov parameter

[Breno Miranda]

Dear Chaoqiang Zhang,

First of all, thank you very much for your prompt answer!
I performed the change you suggested and it seems to be working fine: now
the .cov files contain all the lines covered by the test case.

However, as I'm new to KLEE, I cannot tell you whether or not this is the
correct way. Maybe someone else from this list could answer this.

Thank you again for your support!

--
Yours sincerely,
Breno Miranda


On Wed, Aug 20, 2014 at 10:57 PM, Chaoqiang Zhang <chaoqiang.zhang at gmail.com
> wrote:

> by the way, I tried llvm-gcc 2.9, the meta data is correct for this
> example. So, it's just clang 3.4 problem.
>
>
> On Wed, Aug 20, 2014 at 1:50 PM, Chaoqiang Zhang <
> chaoqiang.zhang at gmail.com> wrote:
>
>> is disabling falseState->coveredLines.clear(); in ExecutionState::branch
>> the right way?
>>
>> I tried this way with a simple example (I pasted the assembly.ll and .c
>> file here also) and found that the line #10 is covered by both of tests, I
>> checked the generated assembly.ll file and found that the meta data for the
>> assembly line 26 is !dbg !131, which corresponds to the line 10 in the
>> source, I understand that's due to compiler optimization. So, I think clang
>> 3.4(which I am using) messed up the meta data, which caused this way output
>> the incorrect result?
>>
>> -----original c file ----
>> #include <klee/klee.h>
>> #include <stdio.h>
>>
>>   1
>>   2 #include <klee/klee.h>
>>   3 #include <stdio.h>
>>   4
>>   5 int main()
>>   6 {
>>   7         int z=klee_int("z");
>>   8         if(z)
>>   9         {
>>  10                 z--;
>>  11         }
>>  12         else
>>  13         {
>>  14                 z++;
>>  15         }
>>  16 }
>>
>>  ----- assembly.ll -----
>>  18 define i32 @main() #0 {
>>  19   %1 = alloca i32, align 4
>>  20   %z = alloca i32, align 4
>>  21   store i32 0, i32* %1
>>  22   %2 = call i32 @klee_int(i8* getelementptr inbounds ([2 x i8]*
>> @.str, i32 0, i32 0)), !dbg !128
>>  23   store i32 %2, i32* %z, align 4, !dbg !128
>>  24   %3 = load i32* %z, align 4, !dbg !129
>>  25   %4 = icmp ne i32 %3, 0, !dbg !129
>>  26   %5 = load i32* %z, align 4, !dbg !131
>>  27   br i1 %4, label %6, label %8, !dbg !129
>>  28
>>  29 ; <label>:6                                       ; preds = %0
>>  30   %7 = add nsw i32 %5, -1, !dbg !131
>>  31   store i32 %7, i32* %z, align 4, !dbg !131
>>  32   br label %10, !dbg !133
>>  33
>>  34 ; <label>:8                                       ; preds = %0
>>  35   %9 = add nsw i32 %5, 1, !dbg !134
>>  36   store i32 %9, i32* %z, align 4, !dbg !134
>>  37   br label %10
>>  38
>>  39 ; <label>:10                                      ; preds = %8, %6
>>  40   %11 = load i32* %1, !dbg !136
>>  41   ret i32 %11, !dbg !136
>>  42 }
>>
>>
>>
>>
>> On Wed, Aug 20, 2014 at 1:00 PM, Breno Miranda <brenoafmiranda at gmail.com>
>> wrote:
>>
>>> Dear All,
>>>
>>> The -write-cov parameter provides, for each test case, the *new* lines
>>> that have been covered by that test case. Is there a way I could get
>>> *ALL* the lines visited by each test case in the .cov files?
>>>
>>> I look forward to hearing from you.
>>>
>>> --
>>> Yours sincerely,
>>> Breno Miranda
>>>
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>>
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed