View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000969 | Frama-C | Kernel | public | 2011-09-19 16:16 | 2011-12-19 09:50 | ||||
Reporter | pascal | ||||||||
Assigned To | pascal | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000969: Sliced program computes differently from original (csmith) | ||||||||
Description | 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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Anne (reporter) 2011-09-19 16:37 Last edited: 2011-09-19 16:39 |
Waouh... ça a été vite ! :-( Merci quand même... je regarde ça. |
pascal (reporter) 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. |
yakobowski (manager) 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. |
pascal (reporter) 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. |
Anne (reporter) 2011-09-20 08:01 Last edited: 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. |
Anne (reporter) 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}) |
pascal (reporter) 2011-09-20 08:44 |
Ça ressemble à un bug connu mais pas encore corrigé, le 933. |
Anne (reporter) 2011-09-20 08:49 |
Oui, en effet, ça semble être le même problème... |
Anne (reporter) 2011-09-20 08:50 |
Plus d'autres bugs ? :-D |
pascal (reporter) 2011-09-20 09:33 |
Fixed by commit 15185. |
pascal (reporter) 2011-10-13 14:37 |
Peuh! Déjà corrigé. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-09-19 16:16 | pascal | New Issue | |
2011-09-19 16:16 | pascal | Status | new => assigned |
2011-09-19 16:16 | pascal | Assigned To | => Anne |
2011-09-19 16:16 | pascal | File Added: 969.tgz | |
2011-09-19 16:37 | Anne | Note Added: 0002283 | |
2011-09-19 16:39 | Anne | Note Edited: 0002283 | |
2011-09-19 16:45 | pascal | Note Added: 0002284 | |
2011-09-19 22:03 | yakobowski | Note Added: 0002292 | |
2011-09-19 22:07 | pascal | Note Added: 0002293 | |
2011-09-20 08:01 | Anne | Note Added: 0002294 | |
2011-09-20 08:02 | Anne | Note Edited: 0002294 | |
2011-09-20 08:04 | Anne | Note Edited: 0002294 | |
2011-09-20 08:23 | Anne | Note Added: 0002295 | |
2011-09-20 08:44 | pascal | Note Added: 0002296 | |
2011-09-20 08:45 | pascal | Relationship added | related to 0000933 |
2011-09-20 08:49 | Anne | Note Added: 0002297 | |
2011-09-20 08:50 | Anne | Note Added: 0002298 | |
2011-09-20 08:55 | pascal | Assigned To | Anne => pascal |
2011-09-20 09:33 | pascal | Note Added: 0002300 | |
2011-09-20 09:33 | pascal | Status | assigned => resolved |
2011-09-20 09:33 | pascal | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |
2011-10-13 14:36 | pascal | Status | closed => feedback |
2011-10-13 14:36 | pascal | Resolution | fixed => reopened |
2011-10-13 14:36 | pascal | Category | Plug-in > slicing => Kernel |
2011-10-13 14:37 | pascal | Note Added: 0002394 | |
2011-10-13 14:37 | pascal | Status | feedback => closed |
2011-10-13 14:37 | pascal | Resolution | reopened => fixed |
2011-12-18 20:08 | pascal | Status | closed => feedback |
2011-12-18 20:08 | pascal | Resolution | fixed => reopened |
2011-12-18 20:08 | pascal | View Status | private => public |
2011-12-19 09:50 | pascal | Status | feedback => closed |
2011-12-19 09:50 | pascal | Resolution | reopened => fixed |