2021-01-27 11:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000370Frama-CPlug-in > jessiepublic2010-04-19 16:14
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 
+Relationships

-Notes

~0000678

cmarche (developer)


fixed in Why CVS

~0000781

signoles (manager)

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

-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
+Issue History