Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001518Frama-CKernelpublic2013-10-25 14:092017-03-14 17:46
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001518: Cast on funspec not considering typedef
Description[STANCE]

The following code:

/* Generated by Frama-C */
struct rr;
typedef struct rr rr;
struct apf;
struct rr {
   struct apf *of ;
};
typedef struct apf apf;
struct apf {
   apf *next ;
   rr *r ;
};
/*@ requires r->of == ((void *)0); */
static apf *f(rr *r)
{
  apf *__retres;
  __retres = r->of;
  return __retres;
}

analyzed by:
frama-c -no-unicode cast.c -ocode cast2.c -print ; frama-c -no-unicode cast2.c

generates an error:
cast2.c:13:[kernel] user error: unexpected token 'apf'
[kernel] user error: skipping file "cast2.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004153)
virgile (developer)
2013-10-25 19:12

ACSL parser should not prevent a typedef name to be also a struct name
(0004554)

2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-10-25 14:09 dpariente New Issue
2013-10-25 19:12 virgile Note Added: 0004153
2013-10-25 19:12 virgile Assigned To => virgile
2013-10-25 19:12 virgile Status new => confirmed
2013-10-25 19:22 svn Checkin
2013-10-28 16:09 dpariente Note Added: 0004170
2013-10-28 16:13 dpariente Note Deleted: 0004170
2013-10-29 11:40 svn Checkin
2013-10-29 11:40 svn Status confirmed => resolved
2013-10-29 11:40 svn Resolution open => fixed
2014-02-12 16:57 Note Added: 0004554
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker