View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000968 | Frama-C | Plug-in > Eva | public | 2011-09-19 16:11 | 2014-02-12 16:54 | ||||
Reporter | pascal | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000968: Slicing generates empty program (csmith) | ||||||||
Description | Le programme slicé s.15102009.9.s.c, obtenu avec la commande slice_src_dest.sh, est vide. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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 :-) |
pascal (reporter) 2011-09-19 18:20 Last edited: 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. |
pascal (reporter) 2011-09-19 18:30 Last edited: 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. |
pascal (reporter) 2011-09-19 18:52 |
Le bug est présent dans 15060. Je pense que ça ne vient pas de moi, |
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 :-) |
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. |
![]() |
|||
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 | ||
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 |
2013-12-19 01:12 | yakobowski | Source_changeset_attached | => framac master d9c18b46 |
2014-02-12 16:54 | yakobowski | Source_changeset_attached | => framac stable/neon d9c18b46 |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |