Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000190Frama-CPlug-in > slicingpublic2009-07-15 12:012009-09-02 10:57
Reporterlukaszc 
Assigned Topatrick 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Beryllium-20090901 
Summary0000190: crash when unbound variable
Description"frama-c -slice-rd y -pp-annot test.c" results in a crash
------------
test.c
------------
int x(int y, int z)
{
/*@ slice pragma expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
 return 2*y*z1();
}

int main()
{
 x(1,2);
 return 0;
}

int z1()
{
 return 1;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000257)
Anne (reporter)
2009-07-15 13:07

test file : tests/slicing/bts0190.c
(0000258)
Anne (reporter)
2009-07-15 13:09

Patrick, I leave this one to you, beacause I don't know where is the best place to catch the exception.
(0000259)
patrick (developer)
2009-07-15 14:16

The raised exception comes from an error in the command line. The variable "y" isn't in the scope related to the -slicd-rd option: the end of the function selected as the entry point (the main function here).
The correction is the following: catching the initial error exception to raise the Log.AbortError exception.
(0000260)
patrick (developer)
2009-07-15 14:20

correction of a crash coming from an user error

- Issue History
Date Modified Username Field Change
2009-07-15 12:01 lukaszc New Issue
2009-07-15 12:01 lukaszc Status new => assigned
2009-07-15 12:01 lukaszc Assigned To => Anne
2009-07-15 13:07 Anne Note Added: 0000257
2009-07-15 13:09 Anne Assigned To Anne => patrick
2009-07-15 13:09 Anne Note Added: 0000258
2009-07-15 14:16 patrick Note Added: 0000259
2009-07-15 14:20 patrick Note Added: 0000260
2009-07-15 14:20 patrick Status assigned => resolved
2009-07-15 14:20 patrick Resolution open => fixed
2009-09-02 10:54 signoles Status resolved => closed
2009-09-02 10:57 signoles Fixed in Version => Frama-C Beryllium


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker