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

[Chaoqiang Zhang]

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