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
Reportervirgile 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker