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