Frama-C Bug Tracking System - Frama-C
View Issue Details
0000369Frama-CPlug-in > jessiepublic2010-01-13 18:102010-12-09 19:22
dpariente 
cmarche 
normalminoralways
closedduplicate 
Frama-C GIT, precise the release id 
 
0000369: Decreases clause
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; } }
No tags attached.
related to 0000102confirmed cmarche Jessie: struct field's validity 
Issue History
2010-01-13 18:10dparienteNew Issue
2010-01-13 18:10dparienteStatusnew => assigned
2010-01-13 18:10dparienteAssigned To => cmarche
2010-01-14 08:40signolesRelationship addedrelated to 0000102
2010-02-11 17:41cmarcheResolutionopen => duplicate
2010-12-09 19:22signolesStatusassigned => closed

There are no notes attached to this issue.