2021-02-27 10:47 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000969Frama-CKernelpublic2011-09-19 16:162011-12-19 09:50
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000969: Sliced program computes differently from original (csmith)
DescriptionMê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.
TagsNo tags attached.
Attached Files
  • tgz file icon 969.tgz (60,392 bytes) 2011-09-19 16:16

-Relationships
related to 0000933closedpascal Wrong AST (csmith) 
+Relationships

-Notes

~0002283

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.

~0002284

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.

~0002292

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.

~0002293

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.

~0002294

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.

~0002295

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})

~0002296

pascal (reporter)

2011-09-20 08:44

 Ça ressemble à un bug connu mais pas encore corrigé, le 933.

~0002297

Anne (reporter)

2011-09-20 08:49

 Oui, en effet, ça semble être le même problème...

~0002298

Anne (reporter)

2011-09-20 08:50

 Plus d'autres bugs ? :-D

~0002300

pascal (reporter)

2011-09-20 09:33

 Fixed by commit 15185.

~0002394

pascal (reporter)

2011-10-13 14:37

 Peuh! Déjà corrigé.
+Notes

-Issue History
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
+Issue History