Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000369Frama-CPlug-in > jessiepublic2010-01-13 18:102010-12-09 19:22
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000369: Decreases clause
DescriptionWhen analyzing the following annotated code by "frama-c -jessie", one PO related to 'decreases' clause can not be discharged by ATP.
This problem might be related to BTS#102 (Frama-C team said in previous discussions).

///////////////////////////////////////////////////

# pragma JessieIntegerModel(exact)
typedef struct qr { int q; int r; } qr;

// md is a recursive function
/*@ requires d>0 && n>=0;
decreases n;
*/
qr md(int n,int d)
{ int q,r; qr v;
if (n==0)
{ v.q = 0;
        v.r = 0;
        return v;
} else { v = md(n-1,d);
        return v;
}
}
TagsNo tags attached.
Attached Files

- Relationships
related to 0000102confirmedcmarche Jessie: struct field's validity 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-01-13 18:10 dpariente New Issue
2010-01-13 18:10 dpariente Status new => assigned
2010-01-13 18:10 dpariente Assigned To => cmarche
2010-01-14 08:40 signoles Relationship added related to 0000102
2010-02-11 17:41 cmarche Resolution open => duplicate
2010-12-09 19:22 signoles Status assigned => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker