Frama-C Bug Tracking System - Frama-C
View Issue Details
0002180Frama-CPlug-in > wppublic2015-10-19 21:312019-10-17 18:01
yakobowski 
correnson 
normalcrashalways
closedwon't fix 
 
 
0002180: Crash on loop with global assigns and per-behavior assigns
frama-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; }
No tags attached.
Issue History
2015-10-19 21:31yakobowskiNew Issue
2015-10-19 21:31yakobowskiStatusnew => assigned
2015-10-19 21:31yakobowskiAssigned To => correnson
2019-10-17 17:20corrensonNote Added: 0006907
2019-10-17 17:20corrensonStatusassigned => resolved
2019-10-17 17:20corrensonResolutionopen => won't fix
2019-10-17 17:20corrensonNote Edited: 0006907View Revisions
2019-10-17 18:01signolesStatusresolved => closed

Notes
(0006907)
correnson   
2019-10-17 17:20   
loop-assigns by behavior not implementable for loops in current engine