2021-01-24 22:13 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000710Frama-CPlug-in > slicingpublic2011-02-14 16:24
Reportertukarammuske 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon frama-c_crash_float_param.c (991 bytes) 2011-02-09 10:13 -
    // Problem: The frama-c is giving 'crash' while slicing
    // Frama-C command to run: frama-c -slice-print -slice-pragma f2 frama-c_crash_float_param.c
    int  glb_int;
    float  glb_float;
     
    int f2 (int param_int, float param_float ) {
    	//@slice pragma stmt;
       if ( param_float == 32 && param_int == 31 );  // for this stmt, there is crash
    
       /* Below are the some of the observations...
       if ( param_float == 32 && param_int == 31 );  // for this stmt, there is crash
       if ( param_int == 32 && param_float == 31 );  // for this stmt, there is NO crash
       if ( param_float == 32 || param_int == 31 );  // for this stmt, there is NO crash
       if ( param_float > 32 && param_int == 31 );  // for this stmt, there is NO crash
       if ( param_float == 32);		  // for this stmt, there is NO crash
       */
    }
    
    int main( ) { 
    	inputsOf_ff_f2( );
    	f2 ( glb_int,  glb_float);
    }
    
    int nondet_int ( );
    float nondet_float ( );
    void inputsOf_ff_f2 () {
    	glb_int = nondet_int ( );
    	glb_float = nondet_float ( );
    }
    
    
    
    c file icon frama-c_crash_float_param.c (991 bytes) 2011-02-09 10:13 +

-Relationships
+Relationships

-Notes

~0001470

signoles (manager)

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 (reporter)

It doesn't crash for me :-/

@Julien: did you use the current version to reproduce the problem ?

~0001501

signoles (manager)

The bug is actually fixed in the latest Frama-C public version, aka Carbon.
+Notes

-Issue History
Date Modified Username Field Change
2011-02-09 10:13 tukarammuske New Issue
2011-02-09 10:13 tukarammuske File Added: frama-c_crash_float_param.c
2011-02-09 14:30 signoles Assigned To => Anne
2011-02-09 14:30 signoles Status new => assigned
2011-02-09 14:30 signoles Category Kernel => Plug-in > slicing
2011-02-09 14:30 signoles Status assigned => confirmed
2011-02-09 14:33 signoles Note Added: 0001470
2011-02-14 16:14 Anne Note Added: 0001500
2011-02-14 16:24 signoles Note Added: 0001501
2011-02-14 16:24 signoles Status confirmed => closed
2011-02-14 16:24 signoles Resolution open => fixed
2011-02-14 16:24 signoles Fixed in Version => Frama-C Carbon-20110201
+Issue History