Frama-C Bug Tracking System - Frama-C
View Issue Details
0000370Frama-CPlug-in > jessiepublic2010-01-13 18:112010-04-19 16:14
dpariente 
cmarche 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Boron-20100401 
0000370: pragma JessieIntegerModel
On 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).
No tags attached.
related to 0000178confirmed cmarche type error in generated why file 
related to 0000072assigned cmarche The specifications of statements are not translated 
Issue History
2010-01-13 18:11dparienteNew Issue
2010-01-13 18:11dparienteStatusnew => assigned
2010-01-13 18:11dparienteAssigned To => cmarche
2010-01-14 08:41signolesRelationship addedrelated to 0000178
2010-02-11 17:38cmarcheNote Added: 0000678
2010-02-11 17:38cmarcheStatusassigned => resolved
2010-02-11 17:38cmarcheResolutionopen => fixed
2010-02-12 09:00signolesRelationship addedrelated to 0000072
2010-04-19 16:13signolesStatusresolved => closed
2010-04-19 16:13signolesFixed in Version => Frama-C Boron
2010-04-19 16:14signolesNote Added: 0000781

Notes
(0000678)
cmarche   
2010-02-11 17:38   
fixed in Why CVS
(0000781)
signoles   
2010-04-19 16:14   
Fix in Why 2.24 (require Frama-C Boron-20100401).