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 <[email protected] > 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 < > [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
