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

[Chaoqiang Zhang]

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