Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000273Frama-CPlug-in > jessiepublic2009-10-08 07:482010-12-09 19:20
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000273: Uncaught exception: assert false on bitvector
DescriptionCommand line: frama-c -jessie foo.c

with foo.c containing:

/* ==================================== */
typedef float real;
struct T26_27 { real _F0 ; real _F1 ; };
typedef struct T26_27 _T26;
struct T28_29 { _T26 _F0 ; _T26 _F1 ; };
typedef struct T28_29 _T28;
typedef _T28 RR;
void f(RR const *tab , real *y )
{ *y = (float )(double )(*((real *)tab + 1)); }
/* ==================================== */

yields:

Uncaught exception: File "jc/jc_interp.ml", line 1819, characters 1-7: Assertion failed

Any means allowing to overcome temporarily this exception (by modifying the C source code) will be welcome!

Regards,
Dillon
Additional Informationfixed in Why 2.21
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-10-08 07:48 dpariente New Issue
2009-10-09 15:18 signoles Status new => assigned
2009-10-09 15:18 signoles Assigned To => cmarche
2009-10-15 10:20 cmarche Status assigned => resolved
2009-10-15 10:20 cmarche Additional Information Updated
2009-10-15 12:25 signoles Status resolved => closed
2009-10-15 12:25 signoles Fixed in Version => Frama-C Beryllium 2
2010-12-09 19:20 signoles Resolution open => fixed
2010-12-09 19:20 signoles Additional Information Updated


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker