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 - 2019 MantisBT Team
Powered by Mantis Bugtracker