2021-01-25 15:18 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002180Frama-CPlug-in > wppublic2019-10-17 18:01
Reporteryakobowski 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionwon't fix 
Product Version 
Target VersionFixed in Version 
Summary0002180: Crash on loop with global assigns and per-behavior assigns
Descriptionframa-c -wp crashes on the following program

/*@ behavior foo:
       */
void main(void)
{
  int i;
  int t[10];
  i = 0;
  /*@ loop assigns t[0 .. i];
      for foo: loop assigns t[0 .. i]; */
  while (i < 10) {
    t[i] = 0;
    i ++;
  }
  return;
}
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006907

correnson (manager)

Last edited: 2019-10-17 17:20

View 2 revisions

loop-assigns by behavior not implementable for loops in current engine

+Notes

-Issue History
Date Modified Username Field Change
2015-10-19 21:31 yakobowski New Issue
2015-10-19 21:31 yakobowski Status new => assigned
2015-10-19 21:31 yakobowski Assigned To => correnson
2019-10-17 17:20 correnson Note Added: 0006907
2019-10-17 17:20 correnson Status assigned => resolved
2019-10-17 17:20 correnson Resolution open => won't fix
2019-10-17 17:20 correnson Note Edited: 0006907 View Revisions
2019-10-17 18:01 signoles Status resolved => closed
+Issue History