Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000042Frama-CPlug-in > jessiepublic2009-04-07 15:372009-06-17 14:38
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000042: Default invariant should be inferred for loops
Description[bug 7561 from old bts, reported by Boris Hollas] For loops that loop on a variable i that is not decreased inside the loop a default loop invariant should be inferred. For example, in for(i=0; i
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000196)
signoles (manager)
2009-06-17 14:38

Using the option -jessie-infer-annot inv (which requires Apron), some useful invariants are inferred and even proved correct by alt-ergo or simplify. However they do not appear as hypotheses for proving the loop body. So they are quite useless. Try on: ===== inv.c ===== void main(void) { int i; int a[10]; int n = 10; for(i=0; i

- Issue History
Date Modified Username Field Change
2009-04-07 15:37 virgile New Issue
2009-04-07 15:38 virgile Assigned To => monate
2009-04-07 15:38 virgile Status new => assigned
2009-04-07 16:04 monate Assigned To monate => signoles
2009-04-07 16:04 signoles Assigned To signoles => monate
2009-04-07 16:07 monate Assigned To monate => virgile
2009-04-07 16:20 signoles Assigned To virgile =>
2009-04-07 16:20 signoles Status assigned => acknowledged
2009-04-09 13:46 virgile Status acknowledged => assigned
2009-04-09 13:46 virgile Assigned To => monate
2009-05-28 21:19 signoles Relationship added child of 0000008
2009-06-17 14:35 signoles Assigned To monate => cmarche
2009-06-17 14:38 signoles Note Added: 0000196


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker