0000968: Slicing generates empty program (csmith)

(0002285)
Anne (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2011-09-19 18:52

Le bug est présent dans 15060. Je pense que ça ne vient pas de moi,

(0002289)
yakobowski (manager)
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 (manager)
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.

Issue History
Date Modified	Username	Field	Change
2011-09-19 16:11	pascal	New Issue
2011-09-19 16:11	pascal	Status	new => assigned
2011-09-19 16:11	pascal	Assigned To	=> Anne
2011-09-19 16:13	pascal	Description Updated
2011-09-19 16:13	pascal	File Added: 968.tgz
2011-09-19 16:48	Anne	Note Added: 0002285
2011-09-19 18:20	pascal	Note Added: 0002286
2011-09-19 18:20	pascal	Assigned To	Anne => pascal
2011-09-19 18:21	pascal	Note Edited: 0002286
2011-09-19 18:30	pascal	Note Added: 0002287
2011-09-19 18:34	pascal	Category	Plug-in > slicing => Plug-in > value analysis
2011-09-19 18:43	pascal	Note Edited: 0002287
2011-09-19 18:43	pascal	Assigned To	pascal => yakobowski
2011-09-19 18:52	pascal	Note Added: 0002288
2011-09-19 21:35	yakobowski	Note Added: 0002289
2011-09-19 21:53	yakobowski	Note Added: 0002290
2011-09-19 21:55	svn	Checkin
2011-09-19 21:55	yakobowski	Status	assigned => resolved
2011-09-19 21:55	yakobowski	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-12-18 20:08	pascal	Status	closed => feedback
2011-12-18 20:08	pascal	Resolution	fixed => reopened
2011-12-18 20:09	pascal	View Status	private => public
2011-12-19 09:51	pascal	Status	feedback => closed
2011-12-19 09:51	pascal	Resolution	reopened => fixed
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Notes
(0002285) Anne (reporter) 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 (reporter) 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 (reporter) 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 (reporter) 2011-09-19 18:52	Le bug est présent dans 15060. Je pense que ça ne vient pas de moi,

(0002289) yakobowski (manager) 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 (manager) 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.

Relationships