Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000040Frama-CPlug-in > jessiepublic2009-04-07 15:352009-10-15 11:04
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000040: Frama-C/Jessie: typing error
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
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0000105closed Jessie: float_P[..] expected instead of real 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-07 15:35 virgile New Issue
2009-04-07 15:40 signoles Status new => acknowledged
2009-04-10 10:17 signoles Status acknowledged => assigned
2009-04-10 10:17 signoles Assigned To => cmarche
2009-05-28 21:43 signoles Relationship added has duplicate 0000105
2009-10-15 11:04 cmarche Status assigned => confirmed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker