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