Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000968Frama-CPlug-in > Evapublic2011-09-19 16:112014-02-12 16:54
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000968: Slicing generates empty program (csmith)
DescriptionLe programme slicé s.15102009.9.s.c, obtenu avec la commande slice_src_dest.sh, est vide.
TagsNo tags attached.
Attached Filestgz file icon 968.tgz [^] (93,771 bytes) 2011-09-19 16:13

- Relationships

-  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.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker