Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000184Frama-CPlug-in > slicingpublic2014-02-12 16:57
Reporterlukaszc 
Assigned ToAnne 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090901 
Summary0000184: slicing crashes when there is no entry point to the function
Descriptionframa-c -slice-pragma x file.c

file.c -----

int x(int y, int z)
{
/*@ slice pragma expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
 return y;
}

int main()
{
 return 0;
}

int z1()
{
 return x(2,2);
}
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2009-07-14 14:13 lukaszc New Issue
2009-07-14 14:13 lukaszc Status new => assigned
2009-07-14 14:13 lukaszc Assigned To => Anne
2009-07-15 09:44 svn
2009-07-15 09:51 svn
2009-07-15 09:51 svn Status assigned => resolved
2009-07-15 09:51 svn Resolution open => fixed
2009-09-02 10:54 signoles Status resolved => closed
2009-09-02 10:57 signoles Fixed in Version => Frama-C Beryllium
2013-12-19 01:13 Anne Source_changeset_attached => framac master 94d44a72
2013-12-19 01:13 Anne Source_changeset_attached => framac master 96002425
2013-12-19 01:14 Source_changeset_attached => framac master 49d969de
2014-02-12 16:56 Anne Source_changeset_attached => framac stable/neon 94d44a72
2014-02-12 16:56 Anne Source_changeset_attached => framac stable/neon 96002425
2014-02-12 16:57 Source_changeset_attached => framac stable/neon 49d969de
+Issue History