Sommaire
Notre base de benchs
Sur cette page nous allons présenter les programmes erronés que nous avons construits. Pour chaque programme, nous avons construit une version en JAVA annotée par une spécification JML (pour LocFaults), et une version en ANSI-C équivalente annotée par la même spéfication mais en ACSL (pour BugAssist). Nous avons réparti notre base de benchmarks en trois grandes catégories : programmes sans boucles, avec boucles et réalistes. Le but de l'utilisation de ces programmes consiste à valider notre approche de localisation d'erreurs (LocFaults) en comparant ses performances avec celles de BugAssist.
Les programmes expérimentés
- Programmes sans boucles et sans calculs non linéaires
- 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
- la plus grande valeur à la variable max ;
- et la plus petite valeur à la 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
- Programmes sans boucles et avec calculs non linéaires
- 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
- Programmes avec boucles
- Sans tableau
- 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
- Avec tableau
- 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
- Benchmarks réalistes
- Tcas
- TcasKO
- 1 erreur (ligne 77): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 131 contre-exemples considérés
- TcasKO2
- 2 erreurs (ligne 68 et ligne 86): 2 affectations, 0 condition.
- Versions JAVA, versions C
- Les 67 contre-exemples considérés
- TcasKO3
- 1 erreur (ligne 63): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 23 contre-exemples considérés
- TcasKO4
- 1 erreur (ligne 81): 1 affectation , 0 condition.
- Versions JAVA, versions C
- Les 20 contre-exemples considérés
- TcasKO5
- 1 erreur (ligne 61): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 10 contre-exemples considérés
- TcasKO6
- 3 erreurs (ligne 77, ligne 84 et ligne 94): 3 affectations, 0 condition.
- Versions JAVA, versions C
- Les 12 contre-exemples considérés
- TcasKO7
- 1 erreur (ligne 58): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 36 contre-exemples considérés
- TcasKO8
- 1 erreur (ligne 60): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Le contre-exemple considéré
- TcasKO9
- 1 erreur (ligne 92): 0 affectation, 1 condition.
- Versions JAVA, versions C
- Les 7 contre-exemples considérés
- TcasKO10
- 6 erreurs (ligne 77, ligne 81, ligne 84, ligne 94, ligne 98 et ligne 101): 6 affectations, 0 condition.
- Versions JAVA, versions C
- Les 14 contre-exemples considérés
- TcasKO11
- 6 erreurs (ligne 77, ligne 81, ligne 84, ligne 94, ligne 98 et ligne 101): 6 affectations, 0 condition. On note que les erreurs 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'affectation "alt_sep = UNRESOLVED" sont supprimées (voir respectivement les lignes 102 et 106 dans le programme TcasKO10).
- Versions JAVA, versions C
- Les 14 contre-exemples considérés
- TcasKO12
- 1 erreur (ligne 61): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 70 contre-exemples considérés
- TcasKO13
- 1 erreur (ligne 48): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 4 contre-exemples considérés
- TcasKO14
- 1 erreur (ligne 49): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 50 contre-exemples considérés
- TcasKO16
- 1 erreur (ligne 57): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 70 contre-exemples considérés
- TcasKO17
- 1 erreur (ligne 58): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 35 contre-exemples considérés
- TcasKO18
- 1 erreur (ligne 59): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 29 contre-exemples considérés
- TcasKO19
- 1 erreur (ligne 60): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 19 contre-exemples considérés
- TcasKO20
- 1 erreur (ligne 75): 0 affectation, 1 condition.
- Versions JAVA, versions C
- Les 18 contre-exemples considérés
- TcasKO21
- 1 erreur (ligne 75): 0 affectation, 1 condition.
- Versions JAVA, versions C
- Les 16 contre-exemples considérés
- TcasKO22
- 1 erreur (ligne 75): 0 affectation, 1 condition. On note que l'erreur est sur la même ligne 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
- Les 11 contre-exemples considérés
- TcasKO23
- 1 erreur (ligne 92): 0 affectation, 1 condition.
- Versions JAVA, versions C
- Les 41 contre-exemples considérés
- TcasKO24
- 1 erreur (ligne 92): 0 affectation, 1 condiiton. On note que l'erreur est sur la même ligne 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
- Les 7 contre-exemples considérés
- TcasKO25
- 1 erreur (ligne 98): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 3 contre-exemples considérés
- TcasKO26
- 1 erreur (ligne 61): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 11 contre-exemples considérés
- TcasKO27
- 1 erreur (ligne 61): 1 affectation, 0 condition. On note que l'erreur porte sur la même ligne d'affectation 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
- Les 10 contre-exemples considérés
- TcasKO28
- 2 erreurs (ligne 67 et ligne 85): 0 affectation, 2 conditions.
- Versions JAVA, versions C
- Les 75 contre-exemples considérés
- TcasKO29
- 2 erreurs (ligne 68 et ligne 86): 2 affectations, 0 condition.
- Versions JAVA, versions C
- Les 18 contre-exemples considérés
- TcasKO30
- 2 erreurs (ligne 71 et ligne 89): 2 affectations, 0 condition.
- Versions JAVA, versions C
- Les 57 contre-exemples considérés
- TcasKO34
- 1 erreur (ligne 65): 0 affectation, 1 condition.
- Versions JAVA, versions C
- Les 77 contre-exemples considérés
- TcasKO35
- 4 erreurs (ligne 68, ligne 71, ligne 86 et ligne 89): 4 affectations, 0 condition.
- Versions JAVA, versions C
- Les 75 contre-exemples considérés
- TcasKO36
- 1 erreur (ligne 56): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 122 contre-exemples considérés
- TcasKO37
- 4 erreurs (ligne 77, ligne 81, ligne 94 et ligne 98): 4 affectations, 0 condition.
- Versions JAVA, versions C
- Les 92 contre-exemples considérés
- TcasKO39
- 1 erreur (ligne 98): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 3 contre-exemples considérés
- TcasKO40
- 2 erreurs (ligne 77 et ligne 84): 2 affectations, 0 condition.
- Versions JAVA, versions C
- Les 122 contre-exemples considérés
- TcasKO41
- 1 erreur (ligne 81): 1 affectation, 0 condition.
- Versions JAVA, versions C
- Les 20 contre-exemples considérés
- 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
Le programme AbsMinus prend en entrée deux entiers i et j et renvoie la valeur absolue de i-j. Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
L'erreur dans ce programme est sur l'instruction d'affectation "result = i-j" (ligne 17), l'instruction correcte devra être "result = i-j". En prenant comme entrée de ce programme {i=0,j=1}, il retourne la valeur -1 comme valeur absolue de i-j, alors qu'il devait retourner 1. Ce programme présente le cas où toutes les condition sont correctes.
L'erreur dans ce programme est sur l'instruction d'affectation "result=i+1" (ligne 11), l'instruction correcte devra être "result=i". En prenant le contre-exemple {i=0,j=1}, le programme échoue et renvoie la valeur 0, alors qu'il devait renvoyer la valeur 1 comme valeur absolue de i-j. Toutes les conditions dans ce programme sont correctes.
L'erreur dans ce programme est sur l'instruction d'affectation "k = k+2" (ligne 14), l'instruction correcte devra être "k = k+1". En prenant l'entrée {i=0,j=1}, cette erreur permet de contredire la condition "(k == 1 && i != j)" et donc l'exécution de l'instruction "result = i-j" (ligne 20), ce qui cause une sortie autre que celle attendue, -1 au lieu de 1.
AbsMinusV2 représente une réécriture du programme qui calcule la valeur absolue de (i - j) (i et j sont les entrées) de telle sorte qu'il devient plus simple : le programme obtenu contient 4 instructions : les lignes 11, 12, 13 et 16. Autrement dit, AbsMinusV2 est sémantiquement équivalent à AbsMinus. Les programmes AbsMinusV2KO et AbsMinusV2KO2 (versions erronées du programme AbsMinusV2) sont équivalents respectivement aux programmes AbsMinusKO et AbsMinusKO2.
Le yZero est un exemple illustratif simple. Ci-dessous la version erronée considérée en JAVA pour LocFaults et en C pour BugAssist:
Le programme Minmax prend en entrée trois entiers et permet de d'affecter la plus petite valeur à la variable least et la plus grande valeur à la variable most. Ce programme a été utilisé dans le papier suivant Error Explanation with Distance Metrics. Ci-dessous la version erronée considérée en JAVA pour LocFaults et C pour BugAssist:
L'erreur dans ce programme est sur l'instruction d'affectation "most = in2" (ligne 19), l'instruction devra être "least = in2". Pour une entrée égale à {in1=2, in2=1, in3=3}, on devra avoir comme sortie least=1 et most=3. Avec cette entrée le programme sort least=2 et most=1, ce qui est non-conforme avec la postcondition posée "(least <= most)".
Ce programme prend en entrée une variable i, et il permet de calculer l'affectation suivante :"z=i*(|v|+|w|)". En sortie il faudrait respecter la postcondition suivante: "((z==0||i!=0)&&(v>=0)&&(w>=0))". Ci-dessous la version erronée considérée en JAVA pour LocFaults et en C pour BugAssist:
L'erreur dans ce programme porte sur l'instruction "z=i+(|v|+|w|)", l'instruction correcte devra être "z=i*(|v|+|w|)". En prenant comme entrée {i=0} le programme échoue et viole sa postcondition.
Ce programme a été utilisé dans le papier "Visualization of Test Information to Assist Fault Localization" pour introduire et expliquer l'approche Tarantula. Nous avons utilisé la version erronée utilisée dans le papier mentionné:
Ce programme prend en entrée six variables à valeurs entières et permet d'affecter:
Nous avons utilisé 4 versions erronées:
L'erreur dans ce programme porte sur l'instruction If (e>f) (ligne 27). Le contre-exemple suivant {a=1, b=-4, c=-3, d=-1, e=0, f=-4} permet de produire un mauvais branchement et de calculer la sortie suivante {max=1,min=0} au lieu de {max=1,min=-4}.
L'erreur dans ce programme est provoquée dans la condition if ((a>b) && (a>c) && (b>d) && (a>e) && (a>f)) (ligne 12), l'instruction correcte devait être if ((a>b) && (a>c) && (a>d) && (a>e) && (a>f)). Cette erreur crée un mauvais branchement, en prenant comme entrée le contre-exemple suivant {a=1, b=-3, c=0, d=-2, e=-1, f=-2} ; elle entraîne la sortie suivante {max=0,min=-3} au lieu de {max=1,min=-3}.
Les erreurs dans ce programme sont introduites au niveau des deux conditions (lignes 12 et 15). En prenant comme entrée {a=1, b=-3, c=0, d=-2, e=-1, f=-2}, ces erreurs produisent deux mauvais branchements ; le programme renvoie {max=0,min=-3} au lieu de {max=1,min=-3}.
Ce programme contient 3 erreurs conditionnelles: lignes 12, 15 et 20. En prenant l'entrée suivante {a=1, b=-3, c=-4, d=-2, e=-1, f=-2}, le programme entraîne la sortie suivante {max=-1,min=-4} au lieu de {max=1,min=-4}.
Le programme Tritype prend en entrée trois entiers (les côtés d'un triangle) et retourne 3 si les entrées correspondent à un équilatéral, 2 si elles correspondent à un isocèle, 1 si elles correspondent à un autre type de triangle, 4 si elles ne correspondent pas à un triangle valide. Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
L'erreur dans ce programme est sur l'instruction d'affectation "trityp = 1" (ligne 54), l'instruction correcte devra être "trityp = 2". En prenant comme entrée les valeurs {i=2,j=3,k=2}, le programme exécute l'instruction erronée et renvoie 1, alors qu'il devait renvoyer 2 (le triangle en entrée est un isocèle). Le programme ne présente aucune condition incorrecte.
L'erreur dans ce programme est sur la condition "(trityp == 1 && (i + k) > j)" (ligne 53), l'instruction devra être "(trityp == 2 && (i + k) > j)". En prenant comme entrée {i=2,j=2,k=2}, le programme renvoie 2 pour indiquer que le triangle est un isocèle, alors que qu'il devait renvoyer la valeur 4 pour signaler que l'entrée ne correspond pas à un triangle valide.
L'erreur dans ce programme est sur l'instruction d'affectation de la ligne 31: "trityp = trityp+1", l'instruction correcte devra être "trityp = trityp + 2". En prenant comme contre-exemple l'entrée {i=1,j=2,k=1}, le programme renvoie la valeur 2 (l'entrée correspond à un isocèle), alors qu'il devait renvoyer la valeur 4 (l'entrée ne correspond pas à un triangle valide).
L'erreur dans ce programme est sur l'instruction conditionnelle "(trityp == 2 && (i+j) > k)" (ligne 53), l'instruction correcte est "(trityp == 2 && (i+k) > j). Avec l'entrée {i=1, j=2, k=1}, le programme devra renvoyer que le triangle en entrée est un isocèle (sortie égale à 2). Ce programme avec cette même entrée renvoie que le triangle correspondant n'est pas valide.
L'erreur dans ce programme est sur l'instruction "(trityp >= 3)", l'instruction devra être "(trityp > 3)". En prenant l'entrée suivante {i=2,j=3,k=3}, le programme satisfait la condition et exécute l'instruction "trityp = 3" (ligne 46) pour renvoyer que le triangle en entrée est un équilatéral, alors qu'il devrait la contredire et renvoyer que qu'il est isocèle (la valeur renvoyée devait être égale à 2).
Les erreurs dans ce programme sont sur la condition "(j != k)" (ligne 32) et sur la condition "(trityp >= 3)" (ligne 45), les instructions correctes devront être respectivement "(j == k)" et "(trityp >= 3)". En prenant l'entrée {i=2,j=3,k=3}, le programme renvoie la valeur 1, alors qu'il devait renvoyer la valeur 2 (le triangle est un isocèle).
Les erreurs dans ce programme sont sur l'instruction conditionnelle "(j != k)" (ligne 32) et sur l'affectation "trityp = trityp + 4" (ligne 33), les instructions correctes devront être respectivement "(j == k)" et "trityp = trityp + 3". En prenant comme entrée du programme {i=2,j=3,k=3}, il retourne que le triangle est équilatéral (la valeur 1), or il devait renvoyer qu'il est isocèle (la valeur 2).
Le programme TriPerimetre a exactement la même structure de contrôle que tritype. La différence est que TriPerimetre renvoie un calcul sur les entrée et pas une constante. Le programme renvoie la somme des côtès du triangle si les entrées correspondent à un triangle valide ; et retourne -1 dans le cas inverse. Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
L'erreur dans ce programme est sur l'instruction d'affectation "res = 2*i + k" (ligne 58), l'instruction devra être "res = 2*i+j". En prenant l'entrée {i=2,j=1,k=2}, le programme renvoie comme somme des cotés du triangle correspondant la valeur 6, alors qu'il devait renvoyer plutôt la valeur 5. Toutes les conditions dans les programme sont correctes.
L'erreur dans ce programme est sur l'instruction d'affectation "res = 2*j" (ligne 34), l'instruction correcte devra être "res = 2*i". En prenant comme entrée {i=2,j=3,k=2}, le programme renvoie que la somme du triangle est 9, alors qu'il devait renvoyer la somme 7. Toutes les conditions présentes dans ce programme sont correctes. Ce programme est sémantiquement équivalent à TriPerimetreKO, la différence est que l'erreur provoquée est n'est pas sur la même instruction pour les deux programmes.
L'erreur dans ce programme est sur la condition "(trityp == 1 && (i+k) > j)", l'instruction correcte devrait être "(trityp == 2 && (i+k) > j)". En prenant comme entrée {i=1,j=1,k=2}, le programme renvoie que la somme du triangle correspondant est 4, or il devait renvoyer -1 (les entrées ne correspondent pas à un triangle valide).
L'erreur dans ce programme se situe sur l'affectation "trityp = trityp + 1", l'instruction correcte devrait être "trityp = trityp + 2". Avec l'entrée suivante {i=1,j=2,k=1}, le programme calcule la somme du triangle : 4, or il devait renvoyer la valeur -1 comme quoi les entrées ne correspondent pas à un triangle valide.
L'erreur dans ce programme est sur la deuxième partie de la condition (trityp == 1 && (i+j) > k) (ligne 57), l'instruction correcte devra être (trityp == 2 && (i+k) > j). En prenant l'entrée {i=1, j=2, k=1}, le programme fournit en sortie la somme 4, or il devrait retourner la valeur -1 pour signaler que les entrées ne correspondent pas à un triangle valide.
L'erreur dans ce programme se trouve sur l'instruction conditionnelle "(trityp >= 3)", l'instruction devra être "(trityp > 3)". Avec l'entrée suivante {i=2,j=3,k=3}, le programme exécute l'instruction "res = 3*i" et renvoie la valeur 6, or il devait renvoyer la valeur 8 (la somme des cotés du triangle en entrée du programme).
Dans ce programme, nous avons introduit deux erreurs : sur la condition "(j != k)" (ligne 34) et sur la condition "(trityp >= 3)" (ligne 49), les instructions correctes devront être respectivement "(j == k)" et "(trityp >= 3)". Avec l'entrée suivante {i=2,j=2,k=3}, ce programme doit renvoyer la valeur 7.
Les erreurs présentes dans ce programme se situent sur l'instruction conditionnelle "(j != k)" (ligne 34) et sur l'affectation "trityp = trityp + 4" (ligne 35), les instructions correctes devront être respectivement "(j == k)" et "trityp = trityp + 3". Avec le contre-exemple suivant {i=2,j=2,k=3}, TriPerimetreKO6 devait retourner la somme 7.
Ce programme a aussi la même structure de contrôle que le tritype. En plus, il permet de calculer la multiplication des cotés d'un triangle. Voici une version erronée en JAVA pour LocFaults et en C pour BugAssist:
L'erreur provoquée dans le programme est sur la ligne 58, l'instruction devrait être "res = i * i * j" au lieu de "res = i * i * k".
L'erreur injectée dans ce programme est sur la condition de ligne 57 : "(trityp == 1 && (i + k) > j)", l'instruction devra être "(trityp == 2 && (i + k) > j)".
L'erreur insérée dans ce programme est sur l'affectation "trityp = trityp + 1", sur la ligne 33 ; l'instruction correcte devait être plutôt "trityp = trityp + 2".
L'erreur affectant ce programme se trouve à la ligne 56 (erreur conditionelle) : "(i+j) > k" au lieu de "(i+k) > j".
Le problème dans ce programme vient de la ligne 48 : la condition "(trityp >= 3)" est erronée, l'instruction correcte est "(trityp > 3)".
Ce programme a deux instructions erronées, la première est sur la ligne 33 : la condition "(j != k)", et la deuxième est au niveau de la ligne 48 : la condition "(trityp >= 3)" ; pour restaurer la conformité vis-à-vis de la postcondition, il faut les remplacer respectivement par "(j == k)" et "(trityp > 3)".
Ce programme contient une erreur à la ligne 33 (la condition "(j != k)") et une autre à la ligne suivante (l'affectation "trityp = trityp + 4"); ces instructions devait être respectivement "(j==k)" et "trityp = trityp + 4".
Ce programme a aussi la même structure de contrôle que le tritype. Avec la différence qu'il renvoie le carré de l'aire du triangle (i,j,k) en entrée en utilisant la formule de Héron. Voici deux versions erronées en JAVA pour LocFaults et en C pour BugAssist:
Ce programme présente le même type d'erreur que dans le TritypeKO et TriPerimetreKO (elle est sur un calcul final dans le chemin du contre-exemple), l'instruction mutée est sur la ligne 61 : "res = s*(s-i)*(s-j)*(s-i)" au lieu de "res = s*(s-i)*(s-j)*(s-j)".
L'erreur dans ce programme est injectée est sur la condition de la ligne 59 (même type d'erreur que dans le TritypeKO2 et TriPerimetreKO2) : trityp == 1 au lieu de trityp == 2. Le contre-exemple associé à ce programme est le suivant: {i=2, j=2, k=4}. En prenant en entrée ce cas d'erreur, le programme HeronKO2 calcule la valeur 32 en exécutant l'instruction "res = s*(s-i)*(s-j)*(s-i)" de la ligne 62; or il devait retourner la valeur -1 comme quoi les entrées du programme correspondent à un triangle invalide.
Les programmes HeronV1 et HeronV2 sont équivalents respectivement aux programmes HeronKO et HeronKO2. La différence est que dans HeronV1 et HeronV2, l'instruction "s=(i+j+k)/2" (ligne 19) est supprimée ; l'expression "(i+j+k)/2" est substituée à "s" dans les instructions qui calculent "res".
L'erreur dans HeronKO2V2 est sur la ligne 31 : l'affectation "trityp = trityp + 1"; pour la corriger, il faut mettre à sa place "trityp = trityp + 2".
L'erreur dans HeronKO3 est située sur la condition de ligne 59 : "(i+j) > k" au lieu de "(i+k) > j".
L'erreur dans HeronKO4 est sur la condition de la ligne 47 : "trityp >= 3" au lieu de "trityp > 3". Avec l'entrée suivante {i=2,j=3,k=3}, le programme devrait calculer la valeur 8.
Il y a deux erreurs conditionelles dans HeronKO5 sur les lignes 32 et 47 : "(j != k)" et "(trityp >= 3)" au lieu de respectivement "(j == k)" et "(trityp > 3)".
Ce programme contient deux erreurs, une conditionelle (ligne 32 : "(j != k)") et l'autre dans une affectation (ligne 33 : "trityp = trityp + 4"); ces instructions devait être respectivement "(j == k)" et "trityp = trityp + 3".
Ce programme, pris du papier decrivant l'approche de BugAssist: Cause Clue Clauses: Error Localization using Maximum Satisfiability (voir la page 9, section 6.4), pour trouver la plus proche racine carrée de nombre entier d'une valeur. Ci-dessous la version erronée utilisée dans ce papier, traduite en JAVA aussi pour notre outil.
Ce programme prend un entier positif de l'utilisateur "n", et il permet de calculer la valeur de "1+2+3+...+n". Voici l'ensemble des versions erronées que nous avons construit et utilisé dans nos expérimentations pour ce programme :
Le programme Minimum prend en entrée un tableau des entiers, et retourne sa valeur minimum. Ci-dessous la version erronée considérée en JAVA pour LocFaults et en C pour BugAssist:
-
MinimumKO.java, MinimumKO.c
Ce programme est erroné à cause de sa boucle While, l'instruction falsifiée se situe sur la condition de la boucle (ligne 9). A partir du contre-exemple suivant {a[0]=3, a[1]=2, a[3]=1, a[4]=0}, il renvoie a[2]==1 à cause du critère d'arrêt de la boucle qui ne permet pas de tester jusqu'à la quatrième case du tableau "a" ; or il devait renvoyer a[2]==0.
Le programme ArrayInit prend en entrée un tableau des entiers dont les élements sont initialisés à 0. Il permet d'affecter à chacune des ses cases la valeur de son indice plus 1. Ci-dessous la version erronée considérée en JAVA pour LocFaults et en C pour BugAssist:
Le programme BSearch prend en entrée un tableau des entiers et un entier x. Par un processus dichotomique, il permet de renvoyer l'indice de la case dans le tableau dont la valeur est x. Dans le cas où x ne figure pas sur le tableau, le programme retourne la valeur -1. Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
Ce programme contient une erreur qui se situe sur la ligne 16: "result = milieu" au lieu de "result = gauche". En utilisant l'outil CPBPV, nous avons cherché un contre-exemple pour un tableau de langueur 128. A partir de ce contre-exemple, nous avons spécifié une précondition JML et ACSL pour annoter respectivement la version JAVA (pour notre outil LocFaults) et C (pour BugAssist). La postcondition des deux programmes indique la sortie correcte attendue ((result==3) and (result==63)).
L'erreur dans ce programme est sur l'instruction d'affectation "droite = milieu - 1" (ligne 20), l'instruction correcte devra être "gauche = milieu + 1". En prenant l'entrée {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}, le programme renvoie -1 indiquant que x=-2147457480 ne figure pas sur le tableau en entrée tab, alors qu'il devait renvoyer l'indice 9 car la valeur de la neuvième case du tab est égale à x.
Ce programme implémente l'algorithme de tri à bulles (appelé aussi tri par propagation). Voici les versions erronées que nous avons utilisées dans nos expérimentations (en JAVA pour notre outil et en C pour BugAssist) :
L'instruction erronée dans ce programme entraîne le programme à trier le tableau en entrée en considérant seulement ses n-1 premiers éléments, n représente la longueur du tableau. Le mauvais fonctionnement du BubblesortKO2 est dû au nombre d'itérations insuffisant effectué par la boucle. Cela est dû à l’initialisation fautive de la variable i : i = tab.length - 1 ; l'instruction devait être i = tab.length.
Les programmes Bf[5-20]V2 sont inspirés des programmes qu'on a trouvés dans la base de benchs de LLBMC (Bf[5-20]). Les programmes Bf[5-20] représentent une implémentation de l'algorithme de Dijkstra en fixant le nombre de nœuds dans le graphe et en faisant varier le nombre d'arcs, leurs poids et leurs sommets de départ et de destinations. Ils permettent de calculer le plus court chemin entre le sommet source (noeud 0) et n'importe quel noeud dans le graphe pris en entrée. Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
-
Bf[5-20]
L'erreur dans ces programmes est sur l'instruction d'affectation "distance[i] = -1" (ligne 24), l'instruction correcte devra être "distance[i] = 0": l'erreur provoquée indique que la distance entre le sommet source et lui-même est -1, or elle devra être égale à 0.
Ce programme implémente un algorithme de glouton permettant de trouver un arbre couvrant minimal dans un graphe connexe. Plus précisément, il permet de trouver un ensemble d'arcs dans le graphe formant un arbre couvrant de poids minimal.
Le Tcas de la suite de test de Siemens est un système d'alerte de trafic et d'évitement de collision. Il s'agit d'une application réelle, et d'un système critique embarqué destiné à éviter les collisions en vol entre aéronefs. Il y a 41 versions erronées et 1608 cas de tests. On les a considéré toutes, hormis les versions TcasKO15, TcasKO31, TcasKO32, TcasKO33 et TcasKO38 et les cas de tests dont l'indice AltLayerValue déborde le tableau PositiveRAAltThresh.
Ci-dessous les versions erronées considérées en JAVA pour LocFaults et en C pour BugAssist:
Les erreurs dans ces programmes sont provoquées dans des endroits différents dans la version correcte du Tcas, créant des versions erronées. Pour chaque version, on a construit un ensemble de programmes, selon les contre-exemples pour chacune parmi les 1608 cas de tests. En effet, pour une version donnée TcasV{i}, on commence par trouver tous les contre-exemple. Et puis pour chaque contre-exemple T{j} trouvé, on construit un programme TcasV{i}T{j} qui va prendre comme entrée le contre-exemple, et comme postcondition la sortie correcte attendue.
L'erreur est sur l'instruction d'affectation "altsep = DOWNWARDRA" (ligne 114), l'instruction correcte devra être "altsep = UNRESOLVED". En prenant l'entrée 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}, le programme échoue et renvoie la valeur 2, alors qu'il devait renvoyer la valeur 0.
Les résultats
Dans cette section, nous allons montrer, décrire et analyser les tableaux contenant les résultats expérimentaux pour les programmes cités ci-dessus.
- Programmes sans boucles
- Programmes avec boucles
- Les sources des résultats
- Le benchmark BubbleSort
- Les contre-exemples générés par l'outil CPBPV
- LocFaults avec 0 condition déviée
- LocFaults avec au plus 1 condition déviée
- LocFaults avec au plus 2 conditions déviées
- LocFaults avec au plus 3 conditions déviées
- BugAssist
- Le benchmark Sum
- Les contre-exemples générés par l'outil CPBPV
- LocFaults avec 0 condition déviée
- LocFaults avec au plus 1 condition déviée
- LocFaults avec au plus 2 conditions déviées
- LocFaults avec au plus 3 conditions déviées
- BugAssist
- Le benchmark SquareRoot
- Benchmarks réalistes