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 <[email protected]> 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 <[email protected]> > 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
