2021-01-15 16:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000190Frama-CPlug-in > slicingpublic2009-09-02 10:57
Reporterlukaszc 
Assigned Topatrick 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0000257

Anne (reporter)

test file : tests/slicing/bts0190.c

~0000258

Anne (reporter)

Patrick, I leave this one to you, beacause I don't know where is the best place to catch the exception.

~0000259

patrick (developer)

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)

correction of a crash coming from an user error
+Notes

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