Frama-C Bug Tracking System - Frama-C
View Issue Details
0000969Frama-CKernelpublic2011-09-19 16:162011-12-19 09:50
pascal 
pascal 
normalminorhave not tried
closedfixed 
 
Frama-C Nitrogen-20111001 
0000969: Sliced program computes differently from original (csmith)
Même fichiers de contexte que le bug 968. le ficher .exec contient le résultat de l'exécution initiale, .execs le résultat de l'exécution de la slice.
No tags attached.
related to 0000933closed pascal Wrong AST (csmith) 
tgz 969.tgz (60,392) 2011-09-19 16:16
https://bts.frama-c.com/file_download.php?file_id=279&type=bug
Issue History
2011-09-19 16:16pascalNew Issue
2011-09-19 16:16pascalStatusnew => assigned
2011-09-19 16:16pascalAssigned To => Anne
2011-09-19 16:16pascalFile Added: 969.tgz
2011-09-19 16:37AnneNote Added: 0002283
2011-09-19 16:39AnneNote Edited: 0002283
2011-09-19 16:45pascalNote Added: 0002284
2011-09-19 22:03yakobowskiNote Added: 0002292
2011-09-19 22:07pascalNote Added: 0002293
2011-09-20 08:01AnneNote Added: 0002294
2011-09-20 08:02AnneNote Edited: 0002294
2011-09-20 08:04AnneNote Edited: 0002294
2011-09-20 08:23AnneNote Added: 0002295
2011-09-20 08:44pascalNote Added: 0002296
2011-09-20 08:45pascalRelationship addedrelated to 0000933
2011-09-20 08:49AnneNote Added: 0002297
2011-09-20 08:50AnneNote Added: 0002298
2011-09-20 08:55pascalAssigned ToAnne => pascal
2011-09-20 09:33pascalNote Added: 0002300
2011-09-20 09:33pascalStatusassigned => resolved
2011-09-20 09:33pascalResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2011-10-13 14:36pascalStatusclosed => feedback
2011-10-13 14:36pascalResolutionfixed => reopened
2011-10-13 14:36pascalCategoryPlug-in > slicing => Kernel
2011-10-13 14:37pascalNote Added: 0002394
2011-10-13 14:37pascalStatusfeedback => closed
2011-10-13 14:37pascalResolutionreopened => fixed
2011-12-18 20:08pascalStatusclosed => feedback
2011-12-18 20:08pascalResolutionfixed => reopened
2011-12-18 20:08pascalView Statusprivate => public
2011-12-19 09:50pascalStatusfeedback => closed
2011-12-19 09:50pascalResolutionreopened => fixed

Notes
(0002283)
Anne   
2011-09-19 16:37   
(edited on: 2011-09-19 16:39)
Waouh... ça a été vite ! :-( Merci quand même... je regarde ça.
(0002284)
pascal   
2011-09-19 16:45   
> Waouh... ça a été vite ! Non, j'avais laissé 8 instances trouver tous les bugs qu'elles pouvaient pendant plusieurs jours, et j'ai seulement rejoué le test des exemples qui ne passaient déjà pas avant tes derniers correctifs. Il y en avait une page dans ls, et il n'en restait plus que deux après nettoyage, les deux que tu vois.
(0002292)
yakobowski   
2011-09-19 22:03   
Je vous laisse vérifier si ce n'était pas le même problème que le 968, je n'ai pas trouvé l'incantation magique pour générer la trace.
(0002293)
pascal   
2011-09-19 22:07   
Le bug est toujours présent dans 15182 après correction du 968. Boris: La commande slice_src_dest.sh fournie dans 968.tgz génère un programme slicé, qu'il faut compiler en 64-bit pour le comparer à l'original. J'ai un script plus automatique pour passer sur des accumulations de programmes douteux obtenues pendant que d'autres bugs sont en train d'être regardés, donc ça n'est jamais la peine de faire ces vérifications manuellement.
(0002294)
Anne   
2011-09-20 08:01   
(edited on: 2011-09-20 08:04)
Bon, enfin un problème différent des dépendances de contrôle,mais peut-être pas directement lié au slicing... Voilà un petit exemple du problème : --------------------------------------------------------- struct S0 { signed f1 : 29; }; int main (void) { int g_341; struct S0 l_175[1]; int l_275 = 0; g_341 = (l_175[l_275].f1 = (int)0x8C8AB594L); Frama_C_show_each (g_341); } --------------------------------------------------------- et voilà les commandes : echo "===== Generate slice" frama-c -slice-calls Frama_C_show_each toto.c \ -then-on 'Slicing export' -print -ocode toto.s.i echo "===== Compile original" gcc toto.c show_each.c -o toto echo "===== Compile slice" gcc toto.s.i show_each.c -o toto.s echo "===== Run original" ./toto echo "===== Run slice" ./toto.s --------------------------------------------------------- Le résultat est étrange : [value] Analyzing a complete application starting at main [value] Called Frama_C_show_each({-1937066604}) ===== Run original [value] Called Frama_C_show_each({210417044}) ===== Run slice [value] Called Frama_C_show_each({2357900692}) --------------------------------------------------------- La décomposition par CIL fait intervenir : int __attribute__((__FRAMA_C_BITFIELD_SIZE__(29))) tmp; c'est peut-être ça la problème ? Je continue à regarder.
(0002295)
Anne   
2011-09-20 08:23   
Le slicing me parait correct... Je vous laisse regarder, car je ne vois pas quoi faire de plus. On a le problème sans passer par le slicing en faisant : frama-c toto.c -print -ocode toto.s.i Je pense que le problème est que la compilation ne tient pas compte de l'attribut de taille, et donc la valeur de la constante n'est pas tronquée. Ça se voit mieux avec : (int)0x8F000000 ===== Run original [value] Called Frama_C_show_each({0xf000000}) ===== Run slice [value] Called Frama_C_show_each({0x8f000000})
(0002296)
pascal   
2011-09-20 08:44   
Ça ressemble à un bug connu mais pas encore corrigé, le 933.
(0002297)
Anne   
2011-09-20 08:49   
Oui, en effet, ça semble être le même problème...
(0002298)
Anne   
2011-09-20 08:50   
Plus d'autres bugs ? :-D
(0002300)
pascal   
2011-09-20 09:33   
Fixed by commit 15185.
(0002394)
pascal   
2011-10-13 14:37   
Peuh! Déjà corrigé.