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; } }