2021-01-27 11:46 CET
  

View Issue Details [ Jump to Notes ] [ 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 
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 Files
  • tgz file icon 968.tgz (93,771 bytes) 2011-09-19 16:13

-Relationships
+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

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.

~0002287

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.

~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.
+Notes

-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
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
+Issue History