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<n; i++) {
    a[i] = 0;
  }

the loop invariant

  //@ loop invariant 0 <= i;

should be inferred by default.


A similar loop invariant should be inferred for decreasing loops.
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<n; i++) {
    a[i] = 0;
  }
}
=================
with the command line:
$ frama-c -jessie-gui -jessie-analysis -jessie-infer-annot inv inv.c

- 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