Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001290Frama-CPlug-in > aoraïpublic2012-10-25 19:002014-02-12 16:58
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001290: aorai doesn't enrich user's "loop assigns" by generated internal variables
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (71 bytes) 2012-10-25 19:00 [Show Content]
? file icon ftest.ya [^] (33 bytes) 2012-10-25 19:00
c file icon ftest_annot.c [^] (1,773 bytes) 2012-10-25 19:01 [Show Content]

- Relationships

-  Notes
(0004610)

2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-10-25 19:00 Jochen New Issue
2012-10-25 19:00 Jochen Status new => assigned
2012-10-25 19:00 Jochen Assigned To => virgile
2012-10-25 19:00 Jochen File Added: ftest.c
2012-10-25 19:00 Jochen File Added: ftest.ya
2012-10-25 19:01 Jochen File Added: ftest_annot.c
2012-10-26 15:53 virgile Status assigned => acknowledged
2012-10-31 16:55 svn Checkin
2012-10-31 16:55 svn Status acknowledged => resolved
2012-10-31 16:55 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2014-02-12 16:58 Note Added: 0004610
2014-02-12 16:58 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker