Question regarding -write-cov parameter

[Breno Miranda]

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

[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 }

Post by Breno Miranda
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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.

Post by 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 -----
19 %1 = alloca i32, align 4
20 %z = alloca i32, align 4
21 store i32 0, i32* %1
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 }

Post by Breno Miranda
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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

Post by 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 <

Post by 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 -----
19 %1 = alloca i32, align 4
20 %z = alloca i32, align 4
21 store i32 0, i32* %1
@.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 }

Post by Breno Miranda
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev