Breno Miranda

2014-08-21 16:40:32 UTC

Dear all,

I was playing around with klee using a toy example of the algorithm that

tells the triangle type according to its angles' values (code attached) to

get acquainted with the klee_assume method.

If I want to restrict KLEE to generate test cases that will explore only

isosceles triangles, I could use a klee_assume like this one:

klee_assume((a + b > c & a + c > b & b + c > a) & (a > 0 & b > 0 & c > 0) &

(a + b + c == 180) & (a == b | b == c | a == c) & !(a == b & b == c));

When KLEE explores the attached code, it outputs three test cases:

TC #1: a=80, b=80, *c=20*

TC #2: *a=20*, b=80, c=80

TC #3: a=80, *b=20*, c=80

Each time a different variable (a, b, c) is assigned to the "different"

angle (20). This is perfectly fine as KLEE is providing the three different

ways in which an isosceles triangle can be achieved to guarantee *full path

coverage*.

When considering branch coverage, however, the 3 test cases explore the

"same" branch (I understand that due to some C characteristics, the actual

number of branches is not exactly the number of branches associated with

the conditional statements, but here I am referring to the source-level

branches).

*Is there any way I could identify that these 3 test cases generated by

KLEE explore the same (source-level) branch?*

My initial thought was to get the information from .cov files generated for

each test cases but, differently from what I was expecting, it is not the

case that the three test cases explore the same lines:

TC #1: 7,8,*12,13,22*,30,31,32,35

TC #2: 7,8,11,30,31,32,35

TC #3: 7,8,11,30,31,32,35

Any ideas would be highly appreciated.

I look forward to hearing from you.

--

Yours sincerely,

Breno Miranda

I was playing around with klee using a toy example of the algorithm that

tells the triangle type according to its angles' values (code attached) to

get acquainted with the klee_assume method.

If I want to restrict KLEE to generate test cases that will explore only

isosceles triangles, I could use a klee_assume like this one:

klee_assume((a + b > c & a + c > b & b + c > a) & (a > 0 & b > 0 & c > 0) &

(a + b + c == 180) & (a == b | b == c | a == c) & !(a == b & b == c));

When KLEE explores the attached code, it outputs three test cases:

TC #1: a=80, b=80, *c=20*

TC #2: *a=20*, b=80, c=80

TC #3: a=80, *b=20*, c=80

Each time a different variable (a, b, c) is assigned to the "different"

angle (20). This is perfectly fine as KLEE is providing the three different

ways in which an isosceles triangle can be achieved to guarantee *full path

coverage*.

When considering branch coverage, however, the 3 test cases explore the

"same" branch (I understand that due to some C characteristics, the actual

number of branches is not exactly the number of branches associated with

the conditional statements, but here I am referring to the source-level

branches).

*Is there any way I could identify that these 3 test cases generated by

KLEE explore the same (source-level) branch?*

My initial thought was to get the information from .cov files generated for

each test cases but, differently from what I was expecting, it is not the

case that the three test cases explore the same lines:

TC #1: 7,8,*12,13,22*,30,31,32,35

TC #2: 7,8,11,30,31,32,35

TC #3: 7,8,11,30,31,32,35

Any ideas would be highly appreciated.

I look forward to hearing from you.

--

Yours sincerely,

Breno Miranda