Frama-C Bug Tracking System - Frama-C
View Issue Details
0000710Frama-CPlug-in > slicingpublic2011-02-09 10:132011-02-14 16:24
Reportertukarammuske 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000710: Crash during slicing
DescriptionFrama-c is used for slicing of the c code in attached test case and its getting crashed while slicing.

Also we observe, the slicing does work (wrt C statement - if ( param_float == 32 && param_int == 31 ); ) --
1. when && is replaced with ||
2. when the conditions are interchanged, that is, if ( param_float == 32 || param_int == 31 );
3. when the == operator in condition param_float == 32 is replaced by other comparison operator.

The command to run and the some observations are put in the test case as comments.
Additional InformationFrama-C command to run:
frama-c -slice-print -slice-pragma f2 frama-c_crash_float_param.c
TagsNo tags attached.
Attached Filesc frama-c_crash_float_param.c (991) 2011-02-09 10:13
https://bts.frama-c.com/file_download.php?file_id=165&type=bug

Notes
(0001470)
signoles   
2011-02-09 14:33   
Reproduced.

@Anne: Run the command with -debug 1. An exception PdgIndex.NotFound seems to be raised when module Filter handles the slicing pragma.
(0001500)
Anne   
2011-02-14 16:14   
It doesn't crash for me :-/

@Julien: did you use the current version to reproduce the problem ?
(0001501)
signoles   
2011-02-14 16:24   
The bug is actually fixed in the latest Frama-C public version, aka Carbon.

Issue History
2011-02-09 10:13tukarammuskeNew Issue
2011-02-09 10:13tukarammuskeFile Added: frama-c_crash_float_param.c
2011-02-09 14:30signolesAssigned To => Anne
2011-02-09 14:30signolesStatusnew => assigned
2011-02-09 14:30signolesCategoryKernel => Plug-in > slicing
2011-02-09 14:30signolesStatusassigned => confirmed
2011-02-09 14:33signolesNote Added: 0001470
2011-02-14 16:14AnneNote Added: 0001500
2011-02-14 16:24signolesNote Added: 0001501
2011-02-14 16:24signolesStatusconfirmed => closed
2011-02-14 16:24signolesResolutionopen => fixed
2011-02-14 16:24signolesFixed in Version => Frama-C Carbon-20110201