Frama-C Bug Tracking System - Frama-C
View Issue Details
0001290Frama-CPlug-in > aoraïpublic2012-10-25 19:002014-02-12 16:58
Jochen 
virgile 
normalminoralways
closedfixed 
Frama-C Oxygen-20120901 
Frama-C Fluorine-20130401 
0001290: aorai doesn't enrich user's "loop assigns" by generated internal variables
Running "frama-c ftest.c -aorai-automata ftest.ya" on the attached files yields an annotated file "ftest_annot.c" (also attached) with a wrong "loop assigns" clause. In line 74, the user-given clause (from line 3 of "ftest.c") is just copied, while the assignment to the generated variable "aorai_Loop_Init_11" in line 78 should lead to the inclusion of that variable into the loop assigns clause.
No tags attached.
c ftest.c (71) 2012-10-25 19:00
https://bts.frama-c.com/file_download.php?file_id=437&type=bug
? ftest.ya (33) 2012-10-25 19:00
https://bts.frama-c.com/file_download.php?file_id=438&type=bug
c ftest_annot.c (1,773) 2012-10-25 19:01
https://bts.frama-c.com/file_download.php?file_id=439&type=bug
Issue History
2012-10-25 19:00JochenNew Issue
2012-10-25 19:00JochenStatusnew => assigned
2012-10-25 19:00JochenAssigned To => virgile
2012-10-25 19:00JochenFile Added: ftest.c
2012-10-25 19:00JochenFile Added: ftest.ya
2012-10-25 19:01JochenFile Added: ftest_annot.c
2012-10-26 15:53virgileStatusassigned => acknowledged
2012-10-31 16:55svnCheckin
2012-10-31 16:55svnStatusacknowledged => resolved
2012-10-31 16:55svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2014-02-12 16:58Note Added: 0004610
2014-02-12 16:58Statusclosed => resolved

Notes
(0004610)
   
2014-02-12 16:58   
Fix committed to stable/neon branch.