Frama-C Bug Tracking System - Frama-C
View Issue Details
0000968Frama-CPlug-in > Evapublic2011-09-19 16:112014-02-12 16:54
pascal 
yakobowski 
normalminorhave not tried
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000968: Slicing generates empty program (csmith)
Le programme slicé s.15102009.9.s.c, obtenu avec la commande slice_src_dest.sh, est vide.
No tags attached.
tgz 968.tgz (93,771) 2011-09-19 16:13
https://bts.frama-c.com/file_download.php?file_id=278&type=bug
Issue History
2011-09-19 16:11pascalNew Issue
2011-09-19 16:11pascalStatusnew => assigned
2011-09-19 16:11pascalAssigned To => Anne
2011-09-19 16:13pascalDescription Updated
2011-09-19 16:13pascalFile Added: 968.tgz
2011-09-19 16:48AnneNote Added: 0002285
2011-09-19 18:20pascalNote Added: 0002286
2011-09-19 18:20pascalAssigned ToAnne => pascal
2011-09-19 18:21pascalNote Edited: 0002286
2011-09-19 18:30pascalNote Added: 0002287
2011-09-19 18:34pascalCategoryPlug-in > slicing => Plug-in > value analysis
2011-09-19 18:43pascalNote Edited: 0002287
2011-09-19 18:43pascalAssigned Topascal => yakobowski
2011-09-19 18:52pascalNote Added: 0002288
2011-09-19 21:35yakobowskiNote Added: 0002289
2011-09-19 21:53yakobowskiNote Added: 0002290
2011-09-19 21:55svnCheckin
2011-09-19 21:55yakobowskiStatusassigned => resolved
2011-09-19 21:55yakobowskiResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2011-12-18 20:08pascalStatusclosed => feedback
2011-12-18 20:08pascalResolutionfixed => reopened
2011-12-18 20:09pascalView Statusprivate => public
2011-12-19 09:51pascalStatusfeedback => closed
2011-12-19 09:51pascalResolutionreopened => fixed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002285)
Anne   
2011-09-19 16:48   
Premier diagnostic : tous les appels à [transparent_crc] et donc [Frama_C_show_each] sont du code mort selon l'analyse de valeur. Le slicing ne fait donc rien :-)
(0002286)
pascal   
2011-09-19 18:20   
(edited on: 2011-09-19 18:21)
Ça me rassurerait que ça soit un bug dans les nouveaux Ival. Ça semble le plus probable. Du coup, pour l'autre, je ne peux pas garantir que ce n'est pas encore l'analyse de valeurs qui fait des siennes. Il faudrait que je la reteste toute seule.
(0002287)
pascal   
2011-09-19 18:30   
(edited on: 2011-09-19 18:43)
Ça date d'avant les nouveaux Ival. ~/dist15107full/bin/frama-c -val -slevel 50 s.15102009.9.i -machdep x86_64 -val-signed-overflow-alarms -no-val-show-progress -slevel-function crc32_gentab:0 [value] Values for function main: NON TERMINATING FUNCTION (pas bien) ~/dist15037full/bin/frama-c -val -slevel 50 s.15102009.9.i -machdep x86_64 -val-signed-overflow-alarms -no-val-show-progress -slevel-function crc32_gentab:0 [value] Values for function main: i ? {3} j ? {3} ... (bien) C'est donc entre 15037 et 15107.
(0002288)
pascal   
2011-09-19 18:52   
Le bug est présent dans 15060. Je pense que ça ne vient pas de moi,
(0002289)
yakobowski   
2011-09-19 21:35   
Bouh. Bonne nouvelle, grâce à tes réponses à ma question "mais comment ça peut marcher vis-à-vis de signé vs non signé sans faire des cast partout", le bug est facile à corriger. Et oui, Cvalue.Model.find_cast serait utile :-)
(0002290)
yakobowski   
2011-09-19 21:53   
Dans les tests, ça ne change que case_analysis.i dans le cas flottant. Il fallait statuer dessus de toute façon, et il était "unknown" avant mes changements dans la logique. Je fais donc le commit.