Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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 file icon frama-c_crash_float_param.c [^] (991 bytes) 2011-02-09 10:13 [Show Content]

- Relationships

-  Notes
(0001470)
signoles (manager)
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 (reporter)
2011-02-14 16:14

It doesn't crash for me :-/

@Julien: did you use the current version to reproduce the problem ?
(0001501)
signoles (manager)
2011-02-14 16:24

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

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker