Frama-C/Jessie: typing error
ID0000040: This issue was created automatically from Mantis Issue 40. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000040 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-10-15 |
| Reporter | virgile | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Lithium-20081201 | Target Version | - | Fixed in Version | - |
Description :
[bug 7554 from old bts, reported by Dillon Pariente] Hello,
The two following files can be compiled separately:
//===== FILE FOO.c typedef struct {float k;} las; void g (float * y); void f (las *c) { g(&(c->k)); }
//===== FILE SPECS.h typedef struct {float k;} las; //@ requires \valid(c); assigns c->k; void f (las * c);
but the command line below:
//===== COMMAND LINE frama-c.byte.exe -jessie-analysis -jessie-gui FOO.c SPECS.h
generates the following error:
//===== STDOUT Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing error: type float_P[..] expected instead of real Jessie subprocess failed: jessie -why-opt -split-user-conj -v -why-opt -fast-wp -separation -locs wholeprogram.cloc w holeprogram.jc