Summary
Our benchmarks
On this page we will introduce the erroneous programs that we have built. For each program, we have built a version in JAVA annotated by a JML specification (for LocFaults), and a version in ANSI-C equivalent annotated by the same spefication but in ACSL (for BugAssist). The programs are divided into three broad categories : programs without loops, with loops, and realistics. The purpose of the use of these programs is to validate our approach of error localization (LocFaults) by comparing its performances with that of BugAssist.
Programs used
- Programs without loops and without non-linear calculations
- AbsMinus
- AbsMinusKO.java, AbsMinusKO.c
- AbsMinusKO2.java, AbsMinusKO2.c
- AbsMinusKO3.java, AbsMinusKO3.c
- AbsMinusV2KO.java,AbsMinusV2KO.c
- AbsMinusV2KO2.java,AbsMinusV2KO2.c
- yZero
- Minmax
- MinmaxKO.java, MinmaxKO.c
- ExempleMCSCardinalite2
- ExempleMCSCardinalite2.java, ExempleMCSCardinalite2.c
- Mid
- Maxmin6var
- the greatest value to the variable max ;
- and the smallest value to the variable min.
- Maxmin6varKO.java, Maxmin6varKO.c
- Maxmin6varKO2.java, Maxmin6varKO2.c
- Maxmin6varKO3.java, Maxmin6varKO3.c
- Maxmin6varKO4.java, Maxmin6varKO4.c
- Maxmin6varKO5.java,Maxmin6varKO5.java
- Maxmin6varKO6.java,Maxmin6varKO6.java
- Tritype
- TritypeKO.java, TritypeKO.c
- TritypeKO2.java, TritypeKO2.c
- TritypeKO2V2.java, TritypeKO2V2.c
- TritypeKO3.java, TritypeKO3.c
- TritypeKO4.java, TritypeKO4.c
- TritypeKO5.java, TritypeKO5.c
- TritypeKO6.java, TritypeKO6.c
- TriPerimetre
- TriPerimetreKO.java, TriPerimetreKO.c
- TriPerimetreKOV2.java, TriPerimetreKOV2.c
- TriPerimetreKO2.java, TriPerimetreKO2.c
- TriPerimetreKO2V2.java,TriPerimetreKO2V2.c
- TriPerimetreKO3.java, TriPerimetreKO3.c
- TriPerimetreKO4.java,TriPerimetreKO4.c
- TriPerimetreKO5.java,TriPerimetreKO5.c
- TriPerimetreKO6.java,TriPerimetreKO6.c
- Programs without loops and with non-linear calculations
- TriMultPerimetre
- TriMultPerimetreKO.java, TriMultPerimetreKO.c
- TriMultPerimetreKO2.java,TriMultPerimetreKO2.c
- TriMultPerimetreKO2V2.java,TriMultPerimetreKO2V2.c
- TriMultPerimetreKO3.java,TriMultPerimetreKO3.c
- TriMultPerimetreKO4.java,TriMultPerimetreKO4.c
- TriMultPerimetreKO5.java,TriMultPerimetreKO5.c
- TriMultPerimetreKO6.java,TriMultPerimetreKO6.c
- Heron
- HeronKO.java, HeronKO.c
- HeronKO2.java, HeronKO2.c
- HeronV1.java, HeronV2.java, HeronV1.c, HeronV2.c
- HeronKO2V2.java,HeronKO2V2.c
- HeronKO3.java,HeronKO3.c
- HeronKO4.java,HeronKO4.c
- HeronKO5.java,HeronKO5.c
- HeronKO6.java,HeronKO6.c
- Programs with loops
- Without arrays
- SquareRoot
- SquareRootKO.java, SquareRootKO.c
- SquareRootV0.java, SquareRootV1.java,..., SquareRootV90.java, SquareRootV0.c, SquareRootV1.c,..., SquareRootV90.c (91 versions)
- Sum
- SumKO.java, SumKO.c
- SumKO_OK.java, SumKO_OK.c
- SumV0.java, SumV1.java,...,SumV95.java, SumV0.c, SumV1.c,...,SumV95.c (96 versions)
- SumFromPtoN
- SquareSum
- SquareSumFromPtoN
- With arrays
- Minimum
- ArrayInit
- BSearch
- BSearchKO.java, BSearchKO.c
- BSearchKO2.java, BSearchKO2.c
- BubbleSort
- BubbleSortKO.java, BubbleSortKO.c
- BubbleSortKO2.java, BubbleSortKO2.c
- BubbleSortV0.java,...,BubbleSortV96.java, BubbleSortV0.c,...,BubbleSortV96.c (97 versions)
- Bf[5-20], Bf[5-20]V2
- Bf5KO.java, Bf5KO.c
- Bf6KO.java, Bf6KO.c
- Bf7KO.java, Bf7KO.c
- Bf8KO.java, Bf8KO.c
- Bf9KO.java, Bf9KO.c
- Bf10KO.java, Bf10KO.c
- Bf11KO.java, Bf11KO.c
- Bf12KO.java, Bf12KO.c
- Bf13KO.java, Bf13KO.c
- Bf14KO.java, Bf14KO.c
- Bf15KO.java, Bf15KO.c
- Bf16KO.java, Bf16KO.c
- Bf17KO.java, Bf17KO.c
- Bf18KO.java, Bf18KO.c
- Bf19KO.java, Bf19KO.c
- Bf20KO.java, Bf20KO.c
- Bf5V2KO.java, Bf5V2KO.c
- Bf6V2KO.java, Bf6V2KO.c
- Bf7V2KO.java, Bf7V2KO.c
- Bf8V2KO.java, Bf8V2KO.c
- Bf9V2KO.java, Bf9V2KO.c
- Bf10V2KO.java, Bf10V2KO.c
- Bf11V2KO.java, Bf11V2KO.c
- Bf12V2KO.java, Bf12V2KO.c
- Bf13V2KO.java, Bf13V2KO.c
- Bf14V2KO.java, Bf14V2KO.c
- Bf15V2KO.java, Bf15V2KO.c
- Bf16V2KO.java, Bf16V2KO.c
- Bf17V2KO.java, Bf17V2KO.c
- Bf18V2KO.java, Bf18V2KO.c
- Bf19V2KO.java, Bf19V2KO.c
- Bf20V2KO.java, Bf20V2KO.c
- Prim
- Prim_4.java, Prim_4.c
- Prim_5.java, Prim_5.c
- Prim_6.java, Prim_6.c
- Prim_7.java, Prim_7.c
- Prim_8.java, Prim_8.c
- Realistic benchmarks
- Tcas
- TcasKO
- 1 error (line 77): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 131 counter-examples considered
- TcasKO2
- 2 errors (line 68 et line 86): 2 assignments, 0 condition.
- Versions JAVA, versions C
- The 67 counter-examples considered
- TcasKO3
- 1 error (line 63): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 23 counter-examples considered
- TcasKO4
- 1 error (line 81): 1 assignment , 0 condition.
- Versions JAVA, versions C
- The 20 counter-examples considered
- TcasKO5
- 1 error (line 61): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 10 counter-examples considered
- TcasKO6
- 3 errors (line 77, line 84 et line 94): 3 assignments, 0 condition.
- Versions JAVA, versions C
- The 12 counter-examples considered
- TcasKO7
- 1 error (line 58): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 36 counter-examples considered
- TcasKO8
- 1 error (line 60): 1 assignment, 0 condition.
- Versions JAVA, versions C
- Le contre-exemple considéré
- TcasKO9
- 1 error (line 92): 0 assignment, 1 condition.
- Versions JAVA, versions C
- The 7 counter-examples considered
- TcasKO10
- 6 errors (line 77, line 81, line 84, line 94, line 98 et line 101): 6 assignments, 0 condition.
- Versions JAVA, versions C
- The 14 counter-examples considered
- TcasKO11
- 6 errors (line 77, line 81, line 84, line 94, line 98 et line 101): 6 assignments, 0 condition. On note que les errors dans TcasKO11 sont les mêmes dans TcasKO10, la différence est que dans TcasKO11 l'instruction conditionelle "((need_upward_RA)&&(need_downward_RA))" et l'assignment "alt_sep = UNRESOLVED" sont supprimées (voir respectivement les lines 102 et 106 dans le programme TcasKO10).
- Versions JAVA, versions C
- The 14 counter-examples considered
- TcasKO12
- 1 error (line 61): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 70 counter-examples considered
- TcasKO13
- 1 error (line 48): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 4 counter-examples considered
- TcasKO14
- 1 error (line 49): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 50 counter-examples considered
- TcasKO16
- 1 error (line 57): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 70 counter-examples considered
- TcasKO17
- 1 error (line 58): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 35 counter-examples considered
- TcasKO18
- 1 error (line 59): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 29 counter-examples considered
- TcasKO19
- 1 error (line 60): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 19 counter-examples considered
- TcasKO20
- 1 error (line 75): 0 assignment, 1 condition.
- Versions JAVA, versions C
- The 18 counter-examples considered
- TcasKO21
- 1 error (line 75): 0 assignment, 1 condition.
- Versions JAVA, versions C
- The 16 counter-examples considered
- TcasKO22
- 1 error (line 75): 0 assignment, 1 condition. On note que l'error est sur la même line de condition dans les trois programmes :TcasKO20, TcasKO21 et TcasKO22; la différence est qu'elle est provoquée différemment dans les trois programmes: "(Inhibit_Biased_Climb>=Down_Separation)" dans TcasKO20, "((Up_Separation+NOZCROSS)>Down_Separation)" dans TcasKO21 et "(Up_Separation>Down_Separation)" dans TcasKO22. Or l'instruction correcte devra être "(Inhibit_Biased_Climb>Down_Separation)"
- Versions JAVA, versions C
- The 11 counter-examples considered
- TcasKO23
- 1 error (line 92): 0 assignment, 1 condition.
- Versions JAVA, versions C
- The 41 counter-examples considered
- TcasKO24
- 1 error (line 92): 0 assignment, 1 condiiton. On note que l'error est sur la même line de condition dans TcasKO23 et dans TcasKO24, mais elle est provoquée différemment dans les deux programmes: "((Up_Separation+NOZCROSS)>Down_Separation)" dans TcasKO23 et "(Up_Separation>Down_Separation)" dans TcasKO24.
- Versions JAVA, versions C
- The 7 counter-examples considered
- TcasKO25
- 1 error (line 98): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 3 counter-examples considered
- TcasKO26
- 1 error (line 61): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 11 counter-examples considered
- TcasKO27
- 1 error (line 61): 1 assignment, 0 condition. On note que l'error porte sur la même line d'assignment dans TcasKO26 et dans TcasKO25, mais elle n'est pas provoquée de la même façcon: "enabled = High_Confidence && (Cur_Vertical_Sep>MAXALTDIFF)" dans TcasKO26 et "enabled=High_Confidence&&(Own_Tracked_Alt_Rate<=OLEV)" dans TcasKO27
- Versions JAVA, versions C
- The 10 counter-examples considered
- TcasKO28
- 2 errors (line 67 et line 85): 0 assignment, 2 conditions.
- Versions JAVA, versions C
- The 75 counter-examples considered
- TcasKO29
- 2 errors (line 68 et line 86): 2 assignments, 0 condition.
- Versions JAVA, versions C
- The 18 counter-examples considered
- TcasKO30
- 2 errors (line 71 et line 89): 2 assignments, 0 condition.
- Versions JAVA, versions C
- The 57 counter-examples considered
- TcasKO34
- 1 error (line 65): 0 assignment, 1 condition.
- Versions JAVA, versions C
- The 77 counter-examples considered
- TcasKO35
- 4 errors (line 68, line 71, line 86 et line 89): 4 assignments, 0 condition.
- Versions JAVA, versions C
- The 75 counter-examples considered
- TcasKO36
- 1 error (line 56): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 122 counter-examples considered
- TcasKO37
- 4 errors (line 77, line 81, line 94 et line 98): 4 assignments, 0 condition.
- Versions JAVA, versions C
- The 92 counter-examples considered
- TcasKO39
- 1 error (line 98): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 3 counter-examples considered
- TcasKO40
- 2 errors (line 77 et line 84): 2 assignments, 0 condition.
- Versions JAVA, versions C
- The 122 counter-examples considered
- TcasKO41
- 1 error (line 81): 1 assignment, 0 condition.
- Versions JAVA, versions C
- The 20 counter-examples considered
- TcasKOV2T1.java, TcasKOV2T1.c
- Schedule2
- Schedule
- Replace
- Tot_info
- Print_tokens2
- Print_tokens
- Space
- Gzip
- Sed
- Flex
- Grep
- Make
- Bash
- Emp-server
- Pine
- Vim
- Nanoxml
- Siena
- Galileo
- Ant
- Xml-security
- Jmeter
- Jtopas
The program AbsMinus takes as input two integers, i and j, and returns the absolute value of i-j. Below the erroneous versions considered in JAVA for LocFaults and in C for BugAssist:
The error in this program is on the assignment statement "result = i-j" (line 17), the correct instruction should be "result = i-j". By taking the values as input of the program {i=0,j=1}, it returns the value -1 as an absolute value of i-j, while it should return the value 1.
The error in this program is on the assignment statement "result=i+1" (line 11), the correct instruction should be "result=i". By taking the counterexample {i=0,j=1}, the program fails and returns 0, while it should return the value 1 as an absolute value of i-j. All conditions in this program are correct.
The error in this program is on the assignment statement "k = k+2" (line 14), the correct instruction should be "k = k+1". By taking the counterexample as input {i=0,j=1}, this error contradicts the condition "(k == 1 && i != j)" and therefore the execution of the instruction "result = i-j" (line 20), causing an output other than the one expected, -1 instead of 1.
AbsMinusV2 represents a rewriting of the program AbsMinus, which calculates the absolute value of (i-j) (i and j are the inputs), so that it becomes easier. The resulting program contains four instructions : lines 11, 12, 13 and 16. In other words, AbsMinusV2 is semantically equivalent to AbsMinus. The programs AbsMinusV2KO and AbsMinusV2KO2 (erroneous verions of AbsMinusV2 program) are equivalent respectively to AbsMinusKO and AbsMinusKO2.
The yZero program is a simple illustrative example. Below the erroneous version considered in JAVA for LocFaults and in C for BugAssist:
The program Minmax takes as input three integers and affects the smallest value to the variable least and the greatest value to the variable most. This program has been used in the following paper Error Explanation with Distance Metrics. Below considered erroneous version in JAVA for LocFaults and in C for BugAssist:
The error in this program is on the assignment statement "most = in2" (line 19), the instruction should be "least = in2". For an input equal to {in1=2, in2=1, in3=3}, we should have as output least=1 and most=3. With this input the program outputs least=2 and most=1, which is ce qui est not comply with the postcondition used "(least <= most)".
This program takes as input a variable i, and calculates the following assignment :"z=i*(|v|+|w|)". The output should be comply with the the following post condition: "((z==0||i!=0)&&(v>=0)&&(w>=0))". Below the erroneous version considered in JAVA for LocFaults and in C for BugAssist:
The error in this program is on the assignment statement "z=i+(|v|+|w|)", the correct instruction should be "z=i*(|v|+|w|)". By taking as input {i=0}, the program fails and violates its postcondition.
This program was used in the paper "Visualization of Test Information to Assist Fault Localization" to introduce and explain the Tarantula approach. We used the wrong version used in the mentioned paper:
This program takes six variables as input of integer values and allows to assign:
We used 4 erroneous versions:
The error in this program is on the condition instruction If (e>f) (line 27). The following counterexample {a=1, b=-4, c=-3, d=-1, e=0, f=-4} produces a bad branching and calculate the following output {max=1,min=0} instead of {max=1,min=-4}.
The error in this program is on the condition instruction if ((a>b) && (a>c) && (b>d) && (a>e) && (a>f)) (line 12), the correct instruction should be if ((a>b) && (a>c) && (a>d) && (a>e) && (a>f)). This error creates a bad branching, by taking as input the following counterexample {a=1, b=-3, c=0, d=-2, e=-1, f=-2} ; the program returns the following output {max=0,min=-3} instead of {max=1,min=-3}.
The errors in this program are introduced at the two conditions: lignes 12 et 15. By taking the input {a=1, b=-3, c=0, d=-2, e=-1, f=-2}, these errors produce two bad branchings ; the program returns {max=0,min=-3} instead of {max=1,min=-3}.
This program contains three conditional errors: lines 12, 15 et 20. By taking the following input {a=1, b=-3, c=-4, d=-2, e=-1, f=-2}, the program returns {max=-1,min=-4} instead of {max=1,min=-4}.
The program Tritype takes as input three variables (the sides of a triangle) and returns 3 if the inputs correspond to an equilateral, 2 if they match an isosceles, 1 if they correspond to another type of triangle, 4 if they do not correspond to a valid triangle. Below considered erroneous versions in JAVA for LocFaults and in C for BugAssist:
The error in this program is on the assignment statement "trityp = 1" (line 54), the correct instruction should be "trityp = 2". By taking as input the values {i=2,j=3,k=2}, the program returns 1, while it should return 2 (the input triangle is an isosceles).
The error in this program is on the assignment statement "(trityp == 1 && (i + k) > j)" (line 53), the instruction should be "(trityp == 2 && (i + k) > j)". By taking as input {i=2,j=2,k=2}, the program returns 2 to indicate that the triangle is an isosceles, while it should return the value 4 to indicate that the entry does not match a valid triangle..
The error in this program is on the assignment statement of the line 31: "trityp = trityp+1", the correct instruction should be "trityp = trityp + 2". By taking as input values {i=1,j=2,k=1}, the program returns the value 2 (input corresponds to an isosceles), while it should return 4 (input does not correspond to a valid triangle).
The error in this program is on the conditional statement "(trityp == 2 && (i+j) > k)" (line 53), the correct instruction is "(trityp == 2 && (i+k) > j). With the input {i=1, j=2, k=1}, the program should return the input triangle is an isosceles (output equal to 2). This program with the same input returns that the corresponding triangle is not valid.
The error in this program is on the statement "(trityp >= 3)", the instruction should be "(trityp > 3)". By taking the input {i=2,j=3,k=3}, the program satisfies the condition and executes the instruction "trityp = 3" (line 46) to return that the input triangle is an equilateral, while it should return that it is isosceles (the returned value should be equal to 2).
The errors in this program are on the condition "(j != k)" (line 32) and on the condition "(trityp >= 3)" (line 45), the correct instructions will be respectively "(j == k)" and "(trityp >= 3)". By taking the input {i=2,j=3,k=3}, the program returns the value 1, while it should return the value 2 (the triangle is an isosceles).
The errors in this program are on the condition "(j != k)" (line 32) and on the assignment "trityp = trityp + 4" (line 33), the correct instructions will be respectively "(j == k)" and "trityp = trityp + 3". By taking as input the program {i=2,j=3,k=3}, it returns that the triangle is equilateral (the value 1), while it should return it isosceles (the value 2).
The program TriPerimetre has exactly the same structure of the control of Tritype. The difference is that TriPerimetre returns the sum of the sides of the triangle if the inputs correspond to a valid triangle ; and returns -1 in the opposite case. Below erroneous versions considered in JAVA for LocFaults and in C for BugAssist:
The error in this program is on the assignment statement "res = 2*i + k" (line 58), the instruction should be "res = 2*i+j". By taking the input {i=2,j=1,k=2}, the program returns the value 6, while it should return the value 5.
The error in this program is on the assignment statement "res = 2*j" (line 34), the instruction should be "res = 2*i". By taking as input {i=2,j=3,k=2}, the returns 9, while it should return the sum 7. This program is semantically equivalent to TriPerimetreKO, the difference is that the error is not on the same instruction for both programs.
The error in this program is on the condition "(trityp == 1 && (i+k) > j)", the correct instruction should be "(trityp == 2 && (i+k) > j)". By taking as input {i=1,j=1,k=2}, the program returns as sum the value 4, while it should return -1 (the entries do not correspond to a valid triangle).
The error in this program is on the affectation "trityp = trityp + 1", the correct instruction should be "trityp = trityp + 2". With the following entry {i=1,j=2,k=1}, the program calculates the sum of the triangle : 4, while it should return the value -1 ( the entries do not correspond to a valid triangle).
The error in this program is the second part of the condition "(trityp == 1 && (i+j) > k)" (line 57), the correct instruction should be "(trityp == 2 && (i+k) > j)". By taking as input {i=1, j=2, k=1}, the program outputs the sum 4, while it should return -1 to indicate that the entries do not correspond to a valid triangle.
The error in this program is on the conditional statement "(trityp >= 3)", this instruction should be "(trityp> 3)". With the following entry {i=2,j=3,k=3}, the program executes the instruction "res = 3 * i" and returns the value 6, while it should return the value 8 (the sum of the sides of the triangle).
In this program, we have introduced two errors : on the condition "(j! = k)" (line 34) and on the condition "(trityp> = 3)" (line 49), the correct instructions are to be respectively "(j == k)" and "(trityp> = 3)". With the following entry {i = 2, j = 2, k = 3}, this program should return the value 7.
The errors in this program are on the conditional statement "(j! = K)" (line 34) and the affectation "trityp trityp = + 4" (line 35), the correct instructions are to be respectively "(j == k)" and "trityp = trityp + 3". With the following counterexample {i=2,j=2,k=3}, TriPerimetreKO6 should return the sum 7.
This program also has the same structure as the control tritype. In addition, it can calculate the multiplication of sides of a triangle. Below the erroneous version considered in JAVA for LocFaults and in C for BugAssist:
The error injected into the program is on the line 58, the instruction should be "res = i * i * j" instead of "res = i * i * k".
The injected error in this program is on the condition of line 57 : "(trityp == 1 && (i + k) > j)", the instruction should be "(trityp == 2 && (i + k) > j)".
The error in this program is inserted on the instruction "trityp = trityp + 1", on the line 33, the correct instruction should be rather "trityp trityp = + 2".
The error in TriMultPerimetreKO3 is on line 56 (conditional error) : "(i+j) > k" instead of "(i+k) > j".
The problem in this program comes from the line 48 : the condition "(trityp> = 3)" is incorrect, the correct statement is "(trityp> 3)".
This program has two erroneous instructions, the first is on the line 33: the condition "(j = k!)", And the second is at line 48: the condition "(trityp> = 3)"; to make this program correct, we should replace the errors respectively by "(j == k)" and "(trityp> 3)".
This program contains an error at line 33 (the condition "(j != k)"), and another on the next line (the assignment "trityp = trityp + 4"); these instructions had to be respectively "(j == k)" and "trityp = trityp + 4".
This program also has the same structure of control as tritype. With the difference that it returns the square of the area of the triangle (i, j, k) entry using Heron's formula. Here are two versions erroneous in JAVA for LocFaults and in C for BugAssist:
This program has the same type of error in the program TritypeKO and TriPerimetreKO (it is on a final calculation in the path of counterexample), the mutated instruction is on the line 61 : "res = s*(s-i)*(s-j)*(s-i)" instead of "res = s*(s-i)*(s-j)*(s-j)".
The error in this program is injected is on the line condition 59 (same type of error in TritypeKO2 and TriPerimetreKO2) : "trityp == 1" instead of "trityp == 2". The case of error associated with this program is as follows: {i=2, j=2, k=4}. By taking as input this counterexample , the program HeronKO2 calculates the value 32 by executing the instruction "res = s*(s-i)*(s-j)*(s-i)" in line 62; while it should return -1 as what the program entries correspond to an invalid triangle.
The programs HeronV1 and HeronV2 are respectively equivalent to HeronKO and HeronKO2. The difference is that in HeronV1 and HeronV2, the instruction "s=(i+j+k)/2" (line 19) is deleted ; the expression "(i+j+k)/2" is substituted for "s" in the instructions that compute "res".
The error in HeronKO2V2 is on the line 31: the assignment "trityp = trityp + 1"; the correct statement should be "trityp = trityp + 2".
The error in HeronKO3 is on the line condition 59 : "(i + j)> k" instead of "(i + k)> j".
The error in HeronKO4 is on the condition of the line 47 : "trityp >= 3" instead of "trityp > 3". With the following entry {i=2,j=3,k=3}, the program should calculate the value 8.
There are two conditionals errors in HeronKO5 on lines 32 and 47: "(j != k)" and "(trityp >= 3)" instead of respectively "(j == k)" and "(trityp > 3 ) ".
This program contains two errors, a conditional (line 32: "(j != k)") and the other in an assignment (line 33: "trityp = trityp + 4"); these instructions had to be respectively "(j == k)" and "trityp = trityp + 3".
This program form the paper describing the approach BugAssist: Cause Clue Clauses: Error Localization using Maximum Satisfiability (see page 9, section 6.4), to find the nearest integer square root of a value. Below the wrong version used in this paper in C, and in JAVA for our tool.
This program takes a positive integer "n" form the user, and it calculates the value of "1+2+3+...+n". Here are all the erroneous versions we have built and used in our experiments for this program:
The program Minimum takes as input an array of integers, and return the minimum value. Below the considered erroneous version in JAVA for LocFaults and in C for BugAssist:
-
MinimumKO.java, MinimumKO.c
This program is wrong because of its while loop, The instruction is falsified on the condition of the loop (line 9). From the following counterexample {a[0]=3,a[1]=2,a[3]=1,a[4]=0}, it returns a[2]==1 because the stopping criterion of the loop that does not allow testing to the fourth cell of the table "a" ; it should return a[2]==0.
The program ArrayInit takes as input an array of integers whose elements are initialized to zero 0. It allows to assign each of its cells the value of the index plus one. Below the considered erroneous version in JAVA for LocFaults and in C for BugAssist:
The program BSearch takes as input an array of integers and an integer x. By a dichotomous process, it can return the index of the box in the table whose value is x. If x not on the table, the program returns the value -1. Below the considered erroneous version in JAVA for LocFaults and in C for BugAssist:
This program contains an error that is on the line 16: "result = milieu" instead of "result = gauche". By using the verification tool CPBPV, we looked for a counterexample for an array of languor 128. From this counterexample, we specified a precondition in JML and in ACSL respectively to annotate the JAVA (for our tool LocFaults) and C (for BugAssist) version. The postcondition of the two programs indicates the correct output expected: ((result==3) and (result==63)).
The error in this program is on the assignment statement "droite = milieu - 1" (line 20), the correct instruction should be "gauche = milieu + 1". By taking as input {tab[0]=-2147477728, tab[1]=-2147470009, tab[2]=-2147468773, tab[3]=-2147466336, tab[4]=-2147457481, tab[5]=-2147457481, tab[6]=-2147457481, tab[7]=-2147457481, tab[8]=2147457481, tab[9]=-2147457480, x=-2147457480}, the program returns -1 to indicate that x=-2147457480 not on the table entry tab, while it should return 9 because the value of the ninth cell of tab is equal to x.
This program implements the bubble sort algorithm. Here erroneous version we used in our experiments (in JAVA for LocFaults and in C for BugAssist) :
The erroneous instruction in this program causes the program to sort the input array by considering only its n-1 first elements, n is the length of the array. The malfunction of BubblesortKO2 is due to the insufficient number of iterations performed by the loop. This is due to the incorrect initialization of the variable i : i = tab.length - 1 ; this instruction should be i = tab.length.
The programs Bf[5-20]V2 inspired from programs found in the database of benchs of LLBMC (Bf[5-20]). The programs Bf[5-20] represent an implementation of the algorithm of Dijkstra by fixing the number of nodes in the graph and by varying the number of arcs, weights and the nodes of origin and destination. They allow you to calculate the shortest path between the source vertex (node 0) and any node in the input graph. Below the considered erroneous versions in JAVA for LocFaults and in C for BugAssist:
-
Bf[5-20]
The error in these programs is on the assignment statement "distance[i] = -1" (line 24), the correct instruction should be "distance[i] = 0": the error indicates that the distance between the root node and itself is -1, while it should be 0.
Tcas program of the Siemens test suite is a traffic alert system and collision avoidance. It is a real application, and a critical embedded system to avoid collisions between aircraft in flight. There are 41 erroneous versions ans 1608 test cases. They considered all but versions TcasKO15, TcasKO31, TcasKO32, TcasKO33 and TcasKO38 and test cases whose index AltLayerValue overflows the table PositiveRAAltThresh.
Below the considered erroneous versions in JAVA for LocFaults and in C for BugAssist:
The errors in these programs are injected in different places in the correct version of Tcas, créant des versions erronées. For each version, we built a set of programs In fact, for a given version TcasV{i}, we first find all counterexamples. And then for each counterexample T{j} found, we build a program TcasV{i}T{j} that will take as input the counterexample, and as postcondition the correct output expected.
The error is on the instruction assignment "altsep = DOWNWARDRA" (line 114), the correct instruction should be "altsep = UNRESOLVED". By taking as input T1={CurVerticalSep=958, HighConfidence=true, TwoofThreeReportsValid=true, OwnTrackedAlt=2597, OwnTrackedAltRate=574, OtherTrackedAlt=4253, PositiveRAAltThresh=400, UpSeparation=399, DownSeparation =400, OtherRAC=0, OtherCapability=0, ClimbInhibit=true}, the program fails and returns 2, while it should return the value 0.
The results
In this section, we will show, describe and analyze tables containing the experimental results mentioned above.
- Programs without loops
- Programs with loops
- The sources of the results
- BubbleSort benchmark
- The counterexamples generated by CPBPV tool
- LocFaults with 0 deviated condition
- LocFaults with at most 1 deviated condition
- LocFaults with at most 2 deviated conditions
- LocFaults with at most 3 deviated conditions
- BugAssist
- Sum benchmark
- The counterexamples generated by CPBPV tool
- LocFaults with 0 deviated condition
- LocFaults with at most 1 deviated condition
- LocFaults with at most 2 deviated conditions
- LocFaults with at most 3 deviated conditions
- BugAssist
- SquareRoot benchmark
- Realistic benchmarks