Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000370Frama-CPlug-in > jessiepublic2010-01-13 18:112010-04-19 16:14
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000370: pragma JessieIntegerModel
DescriptionOn the following annotated code, omitting the pragma (first line in comments), generates an error (see below) :

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

Error:
gwhy-bin [...] why/d4.why
Computation of VCs...
File "why/d4.why", line 781, characters 68-178:
Term (JC_22 : jessie_35) is expected to have type int
make: *** [d4.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f d4.makefile gui

This problem might be related to BTS#178 (first feedback from Frama-C team).
TagsNo tags attached.
Attached Files

- Relationships
related to 0000178confirmedcmarche type error in generated why file 
related to 0000072assignedcmarche The specifications of statements are not translated 

-  Notes
(0000678)
cmarche (developer)
2010-02-11 17:38


fixed in Why CVS
(0000781)
signoles (manager)
2010-04-19 16:14

Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2010-01-13 18:11 dpariente New Issue
2010-01-13 18:11 dpariente Status new => assigned
2010-01-13 18:11 dpariente Assigned To => cmarche
2010-01-14 08:41 signoles Relationship added related to 0000178
2010-02-11 17:38 cmarche Note Added: 0000678
2010-02-11 17:38 cmarche Status assigned => resolved
2010-02-11 17:38 cmarche Resolution open => fixed
2010-02-12 09:00 signoles Relationship added related to 0000072
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000781


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker