Decreases clause
ID0000369: This issue was created automatically from Mantis Issue 369. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000369 | Frama-C | Plug-in > jessie | public | 2010-01-13 | 2010-12-09 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | duplicate |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
When 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; } }