pragma JessieIntegerModel
ID0000370: This issue was created automatically from Mantis Issue 370. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000370 | Frama-C | Plug-in > jessie | public | 2010-01-13 | 2010-04-19 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
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).