2021-02-24 19:16 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001293Frama-CPlug-in > wppublic2012-11-01 12:102013-04-19 11:05
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001293: proc name in assigns clause causes crash
DescriptionRunning "frama-c -wp ftest.c >ftest.log 2>&1" on the attached program, and yielding the attached log file, the Kernel reports an unexpected stack overflow. Although referring to a procedure name ("ftest") in an assigns-clause (line 4) is one of the most stupid user-errors that can be made, it should not cause a crash.
TagsNo tags attached.
Attached Files
  • c file icon ftest1.c (61 bytes) 2012-11-01 12:13 - 
    void ftest(void) {}

//@ assigns ftest;
void main(void) {}
    c file icon ftest1.c (61 bytes) 2012-11-01 12:13 +
  • log file icon ftest.log (1,767 bytes) 2012-11-01 12:14

-Relationships
+Relationships

-Notes

~0003603

correnson (manager)

2012-12-06 13:13

 Fixed in revision 20919.
+Notes

-Issue History
Date Modified Username Field Change
2012-11-01 12:10 Jochen New Issue
2012-11-01 12:10 Jochen File Added: ftest.c
2012-11-01 12:13 Jochen File Added: ftest1.c
2012-11-01 12:14 Jochen File Added: ftest.log
2012-11-01 23:05 yakobowski File Deleted: ftest.c
2012-11-02 18:33 signoles Assigned To => correnson
2012-11-02 18:33 signoles Status new => assigned
2012-11-02 18:33 signoles Category Kernel => Plug-in > wp
2012-12-06 13:13 correnson Note Added: 0003603
2012-12-06 13:13 correnson Status assigned => resolved
2012-12-06 13:13 correnson Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
+Issue History