Frama-C Bug Tracking System - Frama-C
View Issue Details
0000897Frama-CPlug-in > slicingpublic2011-07-28 17:332014-02-12 16:59
pascal 
Anne 
normalminorhave not tried
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000897: error: label ‘__invalid_label’ used but not defined (csmith)
Je rapporte au plus vite pendant que c'est encore frais. Ça semble bien être un petit bug lié aux changements récents.

La commande de slicing était :

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress s.28172412.1.i -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.28172412.1.s.c

Il y en a un deuxième qui est sorti pendant que je faisais l'archive et qui s'est glissé dedans. Le deuxième semble être un autre problème mais est trop gros pour être regardé, j'en trouverai un plus petit.

No tags attached.
tgz invalid_label.tgz (130,891) 2011-07-28 17:33
https://bts.frama-c.com/file_download.php?file_id=246&type=bug
Issue History
2011-07-28 17:33pascalNew Issue
2011-07-28 17:33pascalStatusnew => assigned
2011-07-28 17:33pascalAssigned To => Anne
2011-07-28 17:33pascalFile Added: invalid_label.tgz
2011-07-28 17:37pascalNote Added: 0002071
2011-07-29 08:10svnCheckin
2011-07-29 08:10svnStatusassigned => resolved
2011-07-29 08:10svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2011-12-19 09:57pascalStatusclosed => feedback
2011-12-19 09:57pascalResolutionfixed => reopened
2011-12-19 09:59pascalView Statusprivate => public
2011-12-19 10:00pascalStatusfeedback => closed
2011-12-19 10:00pascalResolutionreopened => fixed
2014-02-12 16:59AnneNote Added: 0004758
2014-02-12 16:59AnneStatusclosed => resolved

Notes
(0002071)
pascal   
2011-07-28 17:37   
Le deuxième programme compile mais fait division par zéro là où l'original ne le faisait pas. Ça ne semble pas être le même problème.
(0004758)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.